![]() |
Metamath
Proof Explorer Theorem List (p. 178 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2oppccomf 17701 | The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd 17714. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π = (oppCatβπΆ) β β’ (compfβπΆ) = (compfβ(oppCatβπ)) | ||
Theorem | oppchomfpropd 17702 | If two categories have the same hom-sets, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ (π β (Homf βπΆ) = (Homf βπ·)) β β’ (π β (Homf β(oppCatβπΆ)) = (Homf β(oppCatβπ·))) | ||
Theorem | oppccomfpropd 17703 | If two categories have the same hom-sets and composition, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) β β’ (π β (compfβ(oppCatβπΆ)) = (compfβ(oppCatβπ·))) | ||
Theorem | oppccatf 17704 | oppCat restricted to Cat is a function from Cat to Cat. (Contributed by Zhi Wang, 29-Aug-2024.) |
β’ (oppCat βΎ Cat):CatβΆCat | ||
Syntax | cmon 17705 | Extend class notation with the class of all monomorphisms. |
class Mono | ||
Syntax | cepi 17706 | Extend class notation with the class of all epimorphisms. |
class Epi | ||
Definition | df-mon 17707* | 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 17708 | 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 17709* | Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ π = (MonoβπΆ) & β’ (π β πΆ β Cat) β β’ (π β π = (π₯ β π΅, π¦ β π΅ β¦ {π β (π₯π»π¦) β£ βπ§ β π΅ Fun β‘(π β (π§π»π₯) β¦ (π(β¨π§, π₯β© Β· π¦)π))})) | ||
Theorem | ismon 17710* | Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ π = (MonoβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (πππ) β (πΉ β (ππ»π) β§ βπ§ β π΅ Fun β‘(π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π))))) | ||
Theorem | ismon2 17711* | Write out the monomorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ π = (MonoβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (πππ) β (πΉ β (ππ»π) β§ βπ§ β π΅ βπ β (π§π»π)ββ β (π§π»π)((πΉ(β¨π§, πβ© Β· π)π) = (πΉ(β¨π§, πβ© Β· π)β) β π = β)))) | ||
Theorem | monhom 17712 | A monomorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ π = (MonoβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πππ) β (ππ»π)) | ||
Theorem | moni 17713 | Property of a monomorphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ π = (MonoβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (πππ)) & β’ (π β πΊ β (ππ»π)) & β’ (π β πΎ β (ππ»π)) β β’ (π β ((πΉ(β¨π, πβ© Β· π)πΊ) = (πΉ(β¨π, πβ© Β· π)πΎ) β πΊ = πΎ)) | ||
Theorem | monpropd 17714 | 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 17715 | A monomorphism in the opposite category is an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ (π β πΆ β Cat) & β’ π = (Monoβπ) & β’ πΈ = (EpiβπΆ) β β’ (π β (πππ) = (ππΈπ)) | ||
Theorem | oppcepi 17716 | An epimorphism in the opposite category is a monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π = (oppCatβπΆ) & β’ (π β πΆ β Cat) & β’ πΈ = (Epiβπ) & β’ π = (MonoβπΆ) β β’ (π β (ππΈπ) = (πππ)) | ||
Theorem | isepi 17717* | Definition of an epimorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ πΈ = (EpiβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππΈπ) β (πΉ β (ππ»π) β§ βπ§ β π΅ Fun β‘(π β (ππ»π§) β¦ (π(β¨π, πβ© Β· π§)πΉ))))) | ||
Theorem | isepi2 17718* | Write out the epimorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ πΈ = (EpiβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ β (ππΈπ) β (πΉ β (ππ»π) β§ βπ§ β π΅ βπ β (ππ»π§)ββ β (ππ»π§)((π(β¨π, πβ© Β· π§)πΉ) = (β(β¨π, πβ© Β· π§)πΉ) β π = β)))) | ||
Theorem | epihom 17719 | An epimorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ πΈ = (EpiβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΈπ) β (ππ»π)) | ||
Theorem | epii 17720 | Property of an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ πΈ = (EpiβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΈπ)) & β’ (π β πΊ β (ππ»π)) & β’ (π β πΎ β (ππ»π)) β β’ (π β ((πΊ(β¨π, πβ© Β· π)πΉ) = (πΎ(β¨π, πβ© Β· π)πΉ) β πΊ = πΎ)) | ||
Syntax | csect 17721 | Extend class notation with the sections of a morphism. |
class Sect | ||
Syntax | cinv 17722 | Extend class notation with the inverses of a morphism. |
class Inv | ||
Syntax | ciso 17723 | Extend class notation with the class of all isomorphisms. |
class Iso | ||
Definition | df-sect 17724* | 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 17725* | 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 17726* | 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 17727* | Value of the section operation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β π = (π₯ β π΅, π¦ β π΅ β¦ {β¨π, πβ© β£ ((π β (π₯π»π¦) β§ π β (π¦π»π₯)) β§ (π(β¨π₯, π¦β© Β· π₯)π) = ( 1 βπ₯))})) | ||
Theorem | sectfval 17728* | Value of the section relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πππ) = {β¨π, πβ© β£ ((π β (ππ»π) β§ π β (ππ»π)) β§ (π(β¨π, πβ© Β· π)π) = ( 1 βπ))}) | ||
Theorem | sectss 17729 | 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 17730 | The property "πΉ is a section of πΊ". (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (ππ»π) β§ πΊ β (ππ»π) β§ (πΊ(β¨π, πβ© Β· π)πΉ) = ( 1 βπ)))) | ||
Theorem | issect2 17731 | Property of being a section. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπΆ) & β’ 1 = (IdβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππ»π)) & β’ (π β πΊ β (ππ»π)) β β’ (π β (πΉ(πππ)πΊ β (πΊ(β¨π, πβ© Β· π)πΉ) = ( 1 βπ))) | ||
Theorem | sectcan 17732 | 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 17733 | Composition of two sections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ Β· = (compβπΆ) & β’ π = (SectβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ(πππ)πΊ) & β’ (π β π»(πππ)πΎ) β β’ (π β (π»(β¨π, πβ© Β· π)πΉ)(πππ)(πΊ(β¨π, πβ© Β· π)πΎ)) | ||
Theorem | isofval 17734* | Function value of the function returning the isomorphisms of a category. (Contributed by AV, 5-Apr-2017.) |
β’ (πΆ β Cat β (IsoβπΆ) = ((π₯ β V β¦ dom π₯) β (InvβπΆ))) | ||
Theorem | invffval 17735* | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (SectβπΆ) β β’ (π β π = (π₯ β π΅, π¦ β π΅ β¦ ((π₯ππ¦) β© β‘(π¦ππ₯)))) | ||
Theorem | invfval 17736 | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (SectβπΆ) β β’ (π β (πππ) = ((πππ) β© β‘(πππ))) | ||
Theorem | isinv 17737 | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (SectβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ(πππ)πΊ β§ πΊ(πππ)πΉ))) | ||
Theorem | invss 17738 | The inverse relation is a relation between morphisms πΉ:πβΆπ and their inverses πΊ:πβΆπ. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π» = (Hom βπΆ) β β’ (π β (πππ) β ((ππ»π) Γ (ππ»π))) | ||
Theorem | invsym 17739 | The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΉ(πππ)πΊ β πΊ(πππ)πΉ)) | ||
Theorem | invsym2 17740 | The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β β‘(πππ) = (πππ)) | ||
Theorem | invfun 17741 | 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 17742 | 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 17743 | If πΊ is an inverse to πΉ, then πΉ is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) & β’ (π β πΉ(πππ)πΊ) β β’ (π β πΉ β (ππΌπ)) | ||
Theorem | inviso2 17744 | If πΊ is an inverse to πΉ, then πΊ is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) & β’ (π β πΉ(πππ)πΊ) β β’ (π β πΊ β (ππΌπ)) | ||
Theorem | invf 17745 | The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (πππ):(ππΌπ)βΆ(ππΌπ)) | ||
Theorem | invf1o 17746 | 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 17747 | 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 17748 | 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 17749* | 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 17750* | 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 17751 | 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 17752 | 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 17753 | An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ πΌ = (IsoβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππΌπ) β (ππ»π)) | ||
Theorem | isoco 17754 | 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 17755 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (oppCatβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (SectβπΆ) & β’ π = (Sectβπ) β β’ (π β (πΉ(πππ)πΊ β πΊ(πππ)πΉ)) | ||
Theorem | oppcsect2 17756 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (oppCatβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (SectβπΆ) & β’ π = (Sectβπ) β β’ (π β (πππ) = β‘(πππ)) | ||
Theorem | oppcinv 17757 | An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ π΅ = (BaseβπΆ) & β’ π = (oppCatβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (InvβπΆ) & β’ π½ = (Invβπ) β β’ (π β (ππ½π) = (ππΌπ)) | ||
Theorem | oppciso 17758 | 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 17759 | 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 17760 | 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 17761 | 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 17762 | 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 17763 | The identity is a section of itself. (Contributed by AV, 8-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IdβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) β β’ (π β (πΌβπ)(π(SectβπΆ)π)(πΌβπ)) | ||
Theorem | invid 17764 | The inverse of the identity is the identity. (Contributed by AV, 8-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IdβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) β β’ (π β (πΌβπ)(π(InvβπΆ)π)(πΌβπ)) | ||
Theorem | idiso 17765 | The identity is an isomorphism. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 8-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IdβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) β β’ (π β (πΌβπ) β (π(IsoβπΆ)π)) | ||
Theorem | idinv 17766 | 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 17767 | The inverse of an isomorphism πΉ (which is unique because of invf 17745 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 17768 | The inverse of an isomorphism is invers to the isomorphism. (Contributed by AV, 9-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ πΌ = (IsoβπΆ) & β’ π = (InvβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΌπ)) β β’ (π β πΉ(πππ)((πππ)βπΉ)) | ||
Theorem | invcoisoid 17769 | 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 17770 | 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 17771 | 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 17773). It is shown that this relation is an equivalence relation, see cicer 17783. | ||
Syntax | ccic 17772 | Extend class notation to include the category isomorphism relation. |
class βπ | ||
Definition | df-cic 17773 | 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 19213. (Contributed by AV, 4-Apr-2020.) |
β’ βπ = (π β Cat β¦ ((Isoβπ) supp β )) | ||
Theorem | cicfval 17774 | The set of isomorphic objects of the category π. (Contributed by AV, 4-Apr-2020.) |
β’ (πΆ β Cat β ( βπ βπΆ) = ((IsoβπΆ) supp β )) | ||
Theorem | brcic 17775 | The relation "is isomorphic to" for categories. (Contributed by AV, 5-Apr-2020.) |
β’ πΌ = (IsoβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π( βπ βπΆ)π β (ππΌπ) β β )) | ||
Theorem | cic 17776* | 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 17777 | Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020.) |
β’ πΌ = (IsoβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππΌπ)) β β’ (π β π( βπ βπΆ)π) | ||
Theorem | cicref 17778 | Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020.) |
β’ ((πΆ β Cat β§ π β (BaseβπΆ)) β π( βπ βπΆ)π) | ||
Theorem | ciclcl 17779 | Isomorphism implies the left side is an object. (Contributed by AV, 5-Apr-2020.) |
β’ ((πΆ β Cat β§ π ( βπ βπΆ)π) β π β (BaseβπΆ)) | ||
Theorem | cicrcl 17780 | Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020.) |
β’ ((πΆ β Cat β§ π ( βπ βπΆ)π) β π β (BaseβπΆ)) | ||
Theorem | cicsym 17781 | Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020.) |
β’ ((πΆ β Cat β§ π ( βπ βπΆ)π) β π( βπ βπΆ)π ) | ||
Theorem | cictr 17782 | Isomorphism is transitive. (Contributed by AV, 5-Apr-2020.) |
β’ ((πΆ β Cat β§ π ( βπ βπΆ)π β§ π( βπ βπΆ)π) β π ( βπ βπΆ)π) | ||
Theorem | cicer 17783 | 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 17784 | Extend class notation to include the subset relation for subcategories. |
class βcat | ||
Syntax | cresc 17785 | Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms). |
class βΎcat | ||
Syntax | csubc 17786 | Extend class notation to include the collection of subcategories of a category. |
class Subcat | ||
Definition | df-ssc 17787* | 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 17789, 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 17788* | 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 17789* | (SubcatβπΆ) is the set of all the subcategory specifications of the category πΆ. Like df-subg 19077, 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 17788) 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 17790 | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ Rel βcat | ||
Theorem | brssc 17791* | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π» βcat π½ β βπ‘(π½ Fn (π‘ Γ π‘) β§ βπ β π« π‘π» β Xπ₯ β (π Γ π )π« (π½βπ₯))) | ||
Theorem | sscpwex 17792* | An analogue of pwex 5375 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 17793 | Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π» β (SubcatβπΆ) β πΆ β Cat) | ||
Theorem | sscfn1 17794 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» βcat π½) & β’ (π β π = dom dom π») β β’ (π β π» Fn (π Γ π)) | ||
Theorem | sscfn2 17795 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» βcat π½) & β’ (π β π = dom dom π½) β β’ (π β π½ Fn (π Γ π)) | ||
Theorem | ssclem 17796 | Lemma for ssc1 17798 and similar theorems. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» Fn (π Γ π)) β β’ (π β (π» β V β π β V)) | ||
Theorem | isssc 17797* | Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» Fn (π Γ π)) & β’ (π β π½ Fn (π Γ π)) & β’ (π β π β π) β β’ (π β (π» βcat π½ β (π β π β§ βπ₯ β π βπ¦ β π (π₯π»π¦) β (π₯π½π¦)))) | ||
Theorem | ssc1 17798 | Infer subset relation on objects from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» Fn (π Γ π)) & β’ (π β π½ Fn (π Γ π)) & β’ (π β π» βcat π½) β β’ (π β π β π) | ||
Theorem | ssc2 17799 | Infer subset relation on morphisms from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ (π β π» Fn (π Γ π)) & β’ (π β π» βcat π½) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππ»π) β (ππ½π)) | ||
Theorem | sscres 17800 | Any function restricted to a square domain is a subcategory subset of the original. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ ((π» Fn (π Γ π) β§ π β π) β (π» βΎ (π Γ π)) βcat π») |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |