![]() |
Metamath
Proof Explorer Theorem List (p. 178 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | oppccatf 17701 | oppCat restricted to Cat is a function from Cat to Cat. (Contributed by Zhi Wang, 29-Aug-2024.) |
β’ (oppCat βΎ Cat):CatβΆCat | ||
Syntax | cmon 17702 | Extend class notation with the class of all monomorphisms. |
class Mono | ||
Syntax | cepi 17703 | Extend class notation with the class of all epimorphisms. |
class Epi | ||
Definition | df-mon 17704* | Function returning the monomorphisms of the category π. JFM CAT1 def. 10. (Contributed by FL, 5-Dec-2007.) (Revised by Mario Carneiro, 2-Jan-2017.) |
β’ Mono = (π β Cat β¦ β¦(Baseβπ) / πβ¦β¦(Hom βπ) / ββ¦(π₯ β π, π¦ β π β¦ {π β (π₯βπ¦) β£ βπ§ β π Fun β‘(π β (π§βπ₯) β¦ (π(β¨π§, π₯β©(compβπ)π¦)π))})) | ||
Definition | df-epi 17705 | Function returning the epimorphisms of the category π. JFM CAT1 def. 11. (Contributed by FL, 8-Aug-2008.) (Revised by Mario Carneiro, 2-Jan-2017.) |
β’ Epi = (π β Cat β¦ tpos (Monoβ(oppCatβπ))) | ||
Theorem | monfval 17706* | Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ π = (MonoβπΆ) & β’ (π β πΆ β Cat) β β’ (π β π = (π₯ β π΅, π¦ β π΅ β¦ {π β (π₯π»π¦) β£ βπ§ β π΅ Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))})) | ||
Theorem | ismon 17707* | Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ π = (MonoβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (πππ) β (πΉ β (ππ»π) β§ βπ§ β π΅ Fun β‘(π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π))))) | ||
Theorem | ismon2 17708* | Write out the monomorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ π = (MonoβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (πππ) β (πΉ β (ππ»π) β§ βπ§ β π΅ βπ β (π§π»π)ββ β (π§π»π)((πΉ(β¨π§, πβ© Β· π)π) = (πΉ(β¨π§, πβ© Β· π)β) β π = β)))) | ||
Theorem | monhom 17709 | A monomorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ π = (MonoβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πππ) β (ππ»π)) | ||
Theorem | moni 17710 | Property of a monomorphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ π = (MonoβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (πππ)) & β’ (π β πΊ β (ππ»π)) & β’ (π β πΎ β (ππ»π)) β β’ (π β ((πΉ(β¨π, πβ© Β· π)πΊ) = (πΉ(β¨π, πβ© Β· π)πΎ) β πΊ = πΎ)) | ||
Theorem | monpropd 17711 | If two categories have the same set of objects, morphisms, and compositions, then they have the same monomorphisms. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β (MonoβπΆ) = (Monoβπ·)) | ||
Theorem | oppcmon 17712 | A monomorphism in the opposite category is an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ (π β πΆ β Cat) & β’ π = (Monoβπ) & β’ πΈ = (EpiβπΆ) β β’ (π β (πππ) = (ππΈπ)) | ||
Theorem | oppcepi 17713 | An epimorphism in the opposite category is a monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ (π β πΆ β Cat) & β’ πΈ = (Epiβπ) & β’ π = (MonoβπΆ) β β’ (π β (ππΈπ) = (πππ)) | ||
Theorem | isepi 17714* | Definition of an epimorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ πΈ = (EpiβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππΈπ) β (πΉ β (ππ»π) β§ βπ§ β π΅ Fun β‘(π β (ππ»π§) β¦ (π(β¨π, πβ© Β· π§)πΉ))))) | ||
Theorem | isepi2 17715* | Write out the epimorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ πΈ = (EpiβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππΈπ) β (πΉ β (ππ»π) β§ βπ§ β π΅ βπ β (ππ»π§)ββ β (ππ»π§)((π(β¨π, πβ© Β· π§)πΉ) = (β(β¨π, πβ© Β· π§)πΉ) β π = β)))) | ||
Theorem | epihom 17716 | An epimorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ πΈ = (EpiβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΈπ) β (ππ»π)) | ||
Theorem | epii 17717 | Property of an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ πΈ = (EpiβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΈπ)) & β’ (π β πΊ β (ππ»π)) & β’ (π β πΎ β (ππ»π)) β β’ (π β ((πΊ(β¨π, πβ© Β· π)πΉ) = (πΎ(β¨π, πβ© Β· π)πΉ) β πΊ = πΎ)) | ||
Syntax | csect 17718 | Extend class notation with the sections of a morphism. |
class Sect | ||
Syntax | cinv 17719 | Extend class notation with the inverses of a morphism. |
class Inv | ||
Syntax | ciso 17720 | Extend class notation with the class of all isomorphisms. |
class Iso | ||
Definition | df-sect 17721* | Function returning the section relation in a category. Given arrows π:πβΆπ and π:πβΆπ, we say πSectπ, that is, π is a section of π, if π β π = 1βπ. If there there is an arrow π with πSectπ, the arrow π is called a section, see definition 7.19 of [Adamek] p. 106. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ Sect = (π β Cat β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ {β¨π, πβ© β£ [(Hom βπ) / β]((π β (π₯βπ¦) β§ π β (π¦βπ₯)) β§ (π(β¨π₯, π¦β©(compβπ)π₯)π) = ((Idβπ)βπ₯))})) | ||
Definition | df-inv 17722* | The inverse relation in a category. Given arrows π:πβΆπ and π:πβΆπ, we say πInvπ, that is, π is an inverse of π, if π is a section of π and π is a section of π. Definition 3.8 of [Adamek] p. 28. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 2-Jan-2017.) |
β’ Inv = (π β Cat β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ ((π₯(Sectβπ)π¦) β© β‘(π¦(Sectβπ)π₯)))) | ||
Definition | df-iso 17723* | Function returning the isomorphisms of the category π. Definition 3.8 of [Adamek] p. 28, and definition in [Lang] p. 54. (Contributed by FL, 9-Jun-2014.) (Revised by Mario Carneiro, 2-Jan-2017.) |
β’ Iso = (π β Cat β¦ ((π₯ β V β¦ dom π₯) β (Invβπ))) | ||
Theorem | sectffval 17724* | Value of the section operation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β π = (π₯ β π΅, π¦ β π΅ β¦ {β¨π, πβ© β£ ((π β (π₯π»π¦) β§ π β (π¦π»π₯)) β§ (π(β¨π₯, π¦β© Β· π₯)π) = ( 1 βπ₯))})) | ||
Theorem | sectfval 17725* | Value of the section relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πππ) = {β¨π, πβ© β£ ((π β (ππ»π) β§ π β (ππ»π)) β§ (π(β¨π, πβ© Β· π)π) = ( 1 βπ))}) | ||
Theorem | sectss 17726 | The section relation is a relation between morphisms from π to π and morphisms from π to π. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πππ) β ((ππ»π) Γ (ππ»π))) | ||
Theorem | issect 17727 | The property "πΉ is a section of πΊ". (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (ππ»π) β§ πΊ β (ππ»π) β§ (πΊ(β¨π, πβ© Β· π)πΉ) = ( 1 βπ)))) | ||
Theorem | issect2 17728 | Property of being a section. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππ»π)) & β’ (π β πΊ β (ππ»π)) β β’ (π β (πΉ(πππ)πΊ β (πΊ(β¨π, πβ© Β· π)πΉ) = ( 1 βπ))) | ||
Theorem | sectcan 17729 | If πΊ is a section of πΉ and πΉ is a section of π», then πΊ = π». Proposition 3.10 of [Adamek] p. 28. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΊ(πππ)πΉ) & β’ (π β πΉ(πππ)π») β β’ (π β πΊ = π») | ||
Theorem | sectco 17730 | Composition of two sections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ Β· = (compβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ(πππ)πΊ) & β’ (π β π»(πππ)πΎ) β β’ (π β (π»(β¨π, πβ© Β· π)πΉ)(πππ)(πΊ(β¨π, πβ© Β· π)πΎ)) | ||
Theorem | isofval 17731* | Function value of the function returning the isomorphisms of a category. (Contributed by AV, 5-Apr-2017.) |
β’ (πΆ β Cat β (IsoβπΆ) = ((π₯ β V β¦ dom π₯) β (InvβπΆ))) | ||
Theorem | invffval 17732* | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (SectβπΆ) β β’ (π β π = (π₯ β π΅, π¦ β π΅ β¦ ((π₯ππ¦) β© β‘(π¦ππ₯)))) | ||
Theorem | invfval 17733 | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (SectβπΆ) β β’ (π β (πππ) = ((πππ) β© β‘(πππ))) | ||
Theorem | isinv 17734 | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (SectβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ(πππ)πΊ β§ πΊ(πππ)πΉ))) | ||
Theorem | invss 17735 | The inverse relation is a relation between morphisms πΉ:πβΆπ and their inverses πΊ:πβΆπ. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π» = (Hom βπΆ) β β’ (π β (πππ) β ((ππ»π) Γ (ππ»π))) | ||
Theorem | invsym 17736 | The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ(πππ)πΊ β πΊ(πππ)πΉ)) | ||
Theorem | invsym2 17737 | The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β β‘(πππ) = (πππ)) | ||
Theorem | invfun 17738 | The inverse relation is a function, which is to say that every morphism has at most one inverse. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β Fun (πππ)) | ||
Theorem | isoval 17739 | The isomorphisms are the domain of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof shortened by AV, 21-May-2020.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (ππΌπ) = dom (πππ)) | ||
Theorem | inviso1 17740 | If πΊ is an inverse to πΉ, then πΉ is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) & β’ (π β πΉ(πππ)πΊ) β β’ (π β πΉ β (ππΌπ)) | ||
Theorem | inviso2 17741 | If πΊ is an inverse to πΉ, then πΊ is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) & β’ (π β πΉ(πππ)πΊ) β β’ (π β πΊ β (ππΌπ)) | ||
Theorem | invf 17742 | The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (πππ):(ππΌπ)βΆ(ππΌπ)) | ||
Theorem | invf1o 17743 | The inverse relation is a bijection from isomorphisms to isomorphisms. This means that every isomorphism πΉ β (ππΌπ) has a unique inverse, denoted by ((InvβπΆ)βπΉ). Remark 3.12 of [Adamek] p. 28. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (πππ):(ππΌπ)β1-1-ontoβ(ππΌπ)) | ||
Theorem | invinv 17744 | The inverse of the inverse of an isomorphism is itself. Proposition 3.14(1) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) & β’ (π β πΉ β (ππΌπ)) β β’ (π β ((πππ)β((πππ)βπΉ)) = πΉ) | ||
Theorem | invco 17745 | The composition of two isomorphisms is an isomorphism, and the inverse is the composition of the individual inverses. Proposition 3.14(2) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) & β’ (π β πΉ β (ππΌπ)) & β’ Β· = (compβπΆ) & β’ (π β π β π΅) & β’ (π β πΊ β (ππΌπ)) β β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ)(πππ)(((πππ)βπΉ)(β¨π, πβ© Β· π)((πππ)βπΊ))) | ||
Theorem | dfiso2 17746* | Alternate definition of an isomorphism of a category, according to definition 3.8 in [Adamek] p. 28. (Contributed by AV, 10-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) & β’ πΌ = (IsoβπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππ»π)) & β’ 1 = (IdβπΆ) & β’ β¬ = (β¨π, πβ©(compβπΆ)π) & β’ β = (β¨π, πβ©(compβπΆ)π) β β’ (π β (πΉ β (ππΌπ) β βπ β (ππ»π)((π β¬ πΉ) = ( 1 βπ) β§ (πΉ β π) = ( 1 βπ)))) | ||
Theorem | dfiso3 17747* | Alternate definition of an isomorphism of a category as a section in both directions. (Contributed by AV, 11-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ πΌ = (IsoβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππ»π)) β β’ (π β (πΉ β (ππΌπ) β βπ β (ππ»π)(π(πππ)πΉ β§ πΉ(πππ)π))) | ||
Theorem | inveq 17748 | If there are two inverses of a morphism, these inverses are equal. Corollary 3.11 of [Adamek] p. 28. (Contributed by AV, 10-Apr-2020.) (Revised by AV, 3-Jul-2022.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πΉ(πππ)πΊ β§ πΉ(πππ)πΎ) β πΊ = πΎ)) | ||
Theorem | isofn 17749 | The function value of the function returning the isomorphisms of a category is a function over the square product of the base set of the category. (Contributed by AV, 5-Apr-2020.) |
β’ (πΆ β Cat β (IsoβπΆ) Fn ((BaseβπΆ) Γ (BaseβπΆ))) | ||
Theorem | isohom 17750 | An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ πΌ = (IsoβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΌπ) β (ππ»π)) | ||
Theorem | isoco 17751 | The composition of two isomorphisms is an isomorphism. Proposition 3.14(2) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ Β· = (compβπΆ) & β’ πΌ = (IsoβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΌπ)) & β’ (π β πΊ β (ππΌπ)) β β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) β (ππΌπ)) | ||
Theorem | oppcsect 17752 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (oppCatβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (SectβπΆ) & β’ π = (Sectβπ) β β’ (π β (πΉ(πππ)πΊ β πΊ(πππ)πΉ)) | ||
Theorem | oppcsect2 17753 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (oppCatβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (SectβπΆ) & β’ π = (Sectβπ) β β’ (π β (πππ) = β‘(πππ)) | ||
Theorem | oppcinv 17754 | An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (oppCatβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (InvβπΆ) & β’ π½ = (Invβπ) β β’ (π β (ππ½π) = (ππΌπ)) | ||
Theorem | oppciso 17755 | An isomorphism in the opposite category. See also remark 3.9 in [Adamek] p. 28. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (oppCatβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) & β’ π½ = (Isoβπ) β β’ (π β (ππ½π) = (ππΌπ)) | ||
Theorem | sectmon 17756 | If πΉ is a section of πΊ, then πΉ is a monomorphism. A monomorphism that arises from a section is also known as a split monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (MonoβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ(πππ)πΊ) β β’ (π β πΉ β (πππ)) | ||
Theorem | monsect 17757 | If πΉ is a monomorphism and πΊ is a section of πΉ, then πΊ is an inverse of πΉ and they are both isomorphisms. This is also stated as "a monomorphism which is also a split epimorphism is an isomorphism". (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (MonoβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (InvβπΆ) & β’ (π β πΉ β (πππ)) & β’ (π β πΊ(πππ)πΉ) β β’ (π β πΉ(πππ)πΊ) | ||
Theorem | sectepi 17758 | If πΉ is a section of πΊ, then πΊ is an epimorphism. An epimorphism that arises from a section is also known as a split epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ πΈ = (EpiβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ(πππ)πΊ) β β’ (π β πΊ β (ππΈπ)) | ||
Theorem | episect 17759 | If πΉ is an epimorphism and πΉ is a section of πΊ, then πΊ is an inverse of πΉ and they are both isomorphisms. This is also stated as "an epimorphism which is also a split monomorphism is an isomorphism". (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ πΈ = (EpiβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (InvβπΆ) & β’ (π β πΉ β (ππΈπ)) & β’ (π β πΉ(πππ)πΊ) β β’ (π β πΉ(πππ)πΊ) | ||
Theorem | sectid 17760 | The identity is a section of itself. (Contributed by AV, 8-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IdβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) β β’ (π β (πΌβπ)(π(SectβπΆ)π)(πΌβπ)) | ||
Theorem | invid 17761 | The inverse of the identity is the identity. (Contributed by AV, 8-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IdβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) β β’ (π β (πΌβπ)(π(InvβπΆ)π)(πΌβπ)) | ||
Theorem | idiso 17762 | The identity is an isomorphism. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 8-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IdβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) β β’ (π β (πΌβπ) β (π(IsoβπΆ)π)) | ||
Theorem | idinv 17763 | The inverse of the identity is the identity. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 9-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IdβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) β β’ (π β ((π(InvβπΆ)π)β(πΌβπ)) = (πΌβπ)) | ||
Theorem | invisoinvl 17764 | The inverse of an isomorphism πΉ (which is unique because of invf 17742 and is therefore denoted by ((πππ)βπΉ), see also remark 3.12 in [Adamek] p. 28) is invers to the isomorphism. (Contributed by AV, 9-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IsoβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΌπ)) β β’ (π β ((πππ)βπΉ)(πππ)πΉ) | ||
Theorem | invisoinvr 17765 | The inverse of an isomorphism is invers to the isomorphism. (Contributed by AV, 9-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IsoβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΌπ)) β β’ (π β πΉ(πππ)((πππ)βπΉ)) | ||
Theorem | invcoisoid 17766 | The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 5-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IsoβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΌπ)) & β’ 1 = (IdβπΆ) & β’ β¬ = (β¨π, πβ©(compβπΆ)π) β β’ (π β (((πππ)βπΉ) β¬ πΉ) = ( 1 βπ)) | ||
Theorem | isocoinvid 17767 | The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 10-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IsoβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΌπ)) & β’ 1 = (IdβπΆ) & β’ β¬ = (β¨π, πβ©(compβπΆ)π) β β’ (π β (πΉ β¬ ((πππ)βπΉ)) = ( 1 βπ)) | ||
Theorem | rcaninv 17768 | Right cancellation of an inverse of an isomorphism. (Contributed by AV, 5-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (π(IsoβπΆ)π)) & β’ (π β πΊ β (π(Hom βπΆ)π)) & β’ (π β π» β (π(Hom βπΆ)π)) & β’ π = ((πππ)βπΉ) & β’ β¬ = (β¨π, πβ©(compβπΆ)π) β β’ (π β ((πΊ β¬ π ) = (π» β¬ π ) β πΊ = π»)) | ||
In this subsection, the "is isomorphic to" relation between objects of a category βπ is defined (see df-cic 17770). It is shown that this relation is an equivalence relation, see cicer 17780. | ||
Syntax | ccic 17769 | Extend class notation to include the category isomorphism relation. |
class βπ | ||
Definition | df-cic 17770 | Function returning the set of isomorphic objects for each category π. Definition 3.15 of [Adamek] p. 29. Analogous to the definition of the group isomorphism relation βπ, see df-gic 19205. (Contributed by AV, 4-Apr-2020.) |
β’ βπ = (π β Cat β¦ ((Isoβπ) supp β )) | ||
Theorem | cicfval 17771 | The set of isomorphic objects of the category π. (Contributed by AV, 4-Apr-2020.) |
β’ (πΆ β Cat β ( βπ βπΆ) = ((IsoβπΆ) supp β )) | ||
Theorem | brcic 17772 | The relation "is isomorphic to" for categories. (Contributed by AV, 5-Apr-2020.) |
β’ πΌ = (IsoβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π( βπ βπΆ)π β (ππΌπ) β β )) | ||
Theorem | cic 17773* | Objects π and π in a category are isomorphic provided that there is an isomorphism π:πβΆπ, see definition 3.15 of [Adamek] p. 29. (Contributed by AV, 4-Apr-2020.) |
β’ πΌ = (IsoβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π( βπ βπΆ)π β βπ π β (ππΌπ))) | ||
Theorem | brcici 17774 | Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020.) |
β’ πΌ = (IsoβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΌπ)) β β’ (π β π( βπ βπΆ)π) | ||
Theorem | cicref 17775 | Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020.) |
β’ ((πΆ β Cat β§ π β (BaseβπΆ)) β π( βπ βπΆ)π) | ||
Theorem | ciclcl 17776 | Isomorphism implies the left side is an object. (Contributed by AV, 5-Apr-2020.) |
β’ ((πΆ β Cat β§ π ( βπ βπΆ)π) β π β (BaseβπΆ)) | ||
Theorem | cicrcl 17777 | Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020.) |
β’ ((πΆ β Cat β§ π ( βπ βπΆ)π) β π β (BaseβπΆ)) | ||
Theorem | cicsym 17778 | Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020.) |
β’ ((πΆ β Cat β§ π ( βπ βπΆ)π) β π( βπ βπΆ)π ) | ||
Theorem | cictr 17779 | Isomorphism is transitive. (Contributed by AV, 5-Apr-2020.) |
β’ ((πΆ β Cat β§ π ( βπ βπΆ)π β§ π( βπ βπΆ)π) β π ( βπ βπΆ)π) | ||
Theorem | cicer 17780 | Isomorphism is an equivalence relation on objects of a category. Remark 3.16 in [Adamek] p. 29. (Contributed by AV, 5-Apr-2020.) |
β’ (πΆ β Cat β ( βπ βπΆ) Er (BaseβπΆ)) | ||
Syntax | cssc 17781 | Extend class notation to include the subset relation for subcategories. |
class βcat | ||
Syntax | cresc 17782 | Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms). |
class βΎcat | ||
Syntax | csubc 17783 | Extend class notation to include the collection of subcategories of a category. |
class Subcat | ||
Definition | df-ssc 17784* | Define the subset relation for subcategories. Despite the name, this is not really a "category-aware" definition, which is to say it makes no explicit references to homsets or composition; instead this is a subset-like relation on the functions that are used as subcategory specifications in df-subc 17786, which makes it play an analogous role to the subset relation applied to the subgroups of a group. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ βcat = {β¨β, πβ© β£ βπ‘(π Fn (π‘ Γ π‘) β§ βπ β π« π‘β β Xπ₯ β (π Γ π )π« (πβπ₯))} | ||
Definition | df-resc 17785* | Define the restriction of a category to a given set of arrows. (Contributed by Mario Carneiro, 4-Jan-2017.) |
β’ βΎcat = (π β V, β β V β¦ ((π βΎs dom dom β) sSet β¨(Hom βndx), ββ©)) | ||
Definition | df-subc 17786* | (SubcatβπΆ) is the set of all the subcategory specifications of the category πΆ. Like df-subg 19069, this is not actually a collection of categories (as in definition 4.1(a) of [Adamek] p. 48), but only sets which when given operations from the base category (using df-resc 17785) form a category. All the objects and all the morphisms of the subcategory belong to the supercategory. The identity of an object, the domain and the codomain of a morphism are the same in the subcategory and the supercategory. The composition of the subcategory is a restriction of the composition of the supercategory. (Contributed by FL, 17-Sep-2009.) (Revised by Mario Carneiro, 4-Jan-2017.) |
β’ Subcat = (π β Cat β¦ {β β£ (β βcat (Homf βπ) β§ [dom dom β / π ]βπ₯ β π (((Idβπ)βπ₯) β (π₯βπ₯) β§ βπ¦ β π βπ§ β π βπ β (π₯βπ¦)βπ β (π¦βπ§)(π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯βπ§)))}) | ||
Theorem | sscrel 17787 | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ Rel βcat | ||
Theorem | brssc 17788* | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π» βcat π½ β βπ‘(π½ Fn (π‘ Γ π‘) β§ βπ β π« π‘π» β Xπ₯ β (π Γ π )π« (π½βπ₯))) | ||
Theorem | sscpwex 17789* | An analogue of pwex 5374 for the subcategory subset relation: The collection of subcategory subsets of a given set π½ is a set. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ {β β£ β βcat π½} β V | ||
Theorem | subcrcl 17790 | Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π» β (SubcatβπΆ) β πΆ β Cat) | ||
Theorem | sscfn1 17791 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» βcat π½) & β’ (π β π = dom dom π») β β’ (π β π» Fn (π Γ π)) | ||
Theorem | sscfn2 17792 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» βcat π½) & β’ (π β π = dom dom π½) β β’ (π β π½ Fn (π Γ π)) | ||
Theorem | ssclem 17793 | Lemma for ssc1 17795 and similar theorems. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» Fn (π Γ π)) β β’ (π β (π» β V β π β V)) | ||
Theorem | isssc 17794* | Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» Fn (π Γ π)) & β’ (π β π½ Fn (π Γ π)) & β’ (π β π β π) β β’ (π β (π» βcat π½ β (π β π β§ βπ₯ β π βπ¦ β π (π₯π»π¦) β (π₯π½π¦)))) | ||
Theorem | ssc1 17795 | Infer subset relation on objects from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» Fn (π Γ π)) & β’ (π β π½ Fn (π Γ π)) & β’ (π β π» βcat π½) β β’ (π β π β π) | ||
Theorem | ssc2 17796 | Infer subset relation on morphisms from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» Fn (π Γ π)) & β’ (π β π» βcat π½) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππ»π) β (ππ½π)) | ||
Theorem | sscres 17797 | Any function restricted to a square domain is a subcategory subset of the original. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ ((π» Fn (π Γ π) β§ π β π) β (π» βΎ (π Γ π)) βcat π») | ||
Theorem | sscid 17798 | The subcategory subset relation is reflexive. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ ((π» Fn (π Γ π) β§ π β π) β π» βcat π») | ||
Theorem | ssctr 17799 | The subcategory subset relation is transitive. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ ((π΄ βcat π΅ β§ π΅ βcat πΆ) β π΄ βcat πΆ) | ||
Theorem | ssceq 17800 | The subcategory subset relation is antisymmetric. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ ((π΄ βcat π΅ β§ π΅ βcat π΄) β π΄ = π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |