![]() |
Metamath
Proof Explorer Theorem List (p. 180 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isnat2 17901* | Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ π½ = (Hom βπ·) & β’ Β· = (compβπ·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) β β’ (π β (π΄ β (πΉππΊ) β (π΄ β Xπ₯ β π΅ (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯)) β§ βπ₯ β π΅ βπ¦ β π΅ ββ β (π₯π»π¦)((π΄βπ¦)(β¨((1st βπΉ)βπ₯), ((1st βπΉ)βπ¦)β© Β· ((1st βπΊ)βπ¦))((π₯(2nd βπΉ)π¦)ββ)) = (((π₯(2nd βπΊ)π¦)ββ)(β¨((1st βπΉ)βπ₯), ((1st βπΊ)βπ₯)β© Β· ((1st βπΊ)βπ¦))(π΄βπ₯))))) | ||
Theorem | natffn 17902 | The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΆ Nat π·) β β’ π Fn ((πΆ Func π·) Γ (πΆ Func π·)) | ||
Theorem | natrcl 17903 | Reverse closure for a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) β β’ (π΄ β (πΉππΊ) β (πΉ β (πΆ Func π·) β§ πΊ β (πΆ Func π·))) | ||
Theorem | nat1st2nd 17904 | Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ (π β π΄ β (πΉππΊ)) β β’ (π β π΄ β (β¨(1st βπΉ), (2nd βπΉ)β©πβ¨(1st βπΊ), (2nd βπΊ)β©)) | ||
Theorem | natixp 17905* | A natural transformation is a function from the objects of πΆ to homomorphisms from πΉ(π₯) to πΊ(π₯). (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ (π β π΄ β (β¨πΉ, πΊβ©πβ¨πΎ, πΏβ©)) & β’ π΅ = (BaseβπΆ) & β’ π½ = (Hom βπ·) β β’ (π β π΄ β Xπ₯ β π΅ ((πΉβπ₯)π½(πΎβπ₯))) | ||
Theorem | natcl 17906 | A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ (π β π΄ β (β¨πΉ, πΊβ©πβ¨πΎ, πΏβ©)) & β’ π΅ = (BaseβπΆ) & β’ π½ = (Hom βπ·) & β’ (π β π β π΅) β β’ (π β (π΄βπ) β ((πΉβπ)π½(πΎβπ))) | ||
Theorem | natfn 17907 | A natural transformation is a function on the objects of πΆ. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ (π β π΄ β (β¨πΉ, πΊβ©πβ¨πΎ, πΏβ©)) & β’ π΅ = (BaseβπΆ) β β’ (π β π΄ Fn π΅) | ||
Theorem | nati 17908 | Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ Nat π·) & β’ (π β π΄ β (β¨πΉ, πΊβ©πβ¨πΎ, πΏβ©)) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ Β· = (compβπ·) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β (ππ»π)) β β’ (π β ((π΄βπ)(β¨(πΉβπ), (πΉβπ)β© Β· (πΎβπ))((ππΊπ)βπ )) = (((ππΏπ)βπ )(β¨(πΉβπ), (πΎβπ)β© Β· (πΎβπ))(π΄βπ))) | ||
Theorem | wunnat 17909 | A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.) |
β’ (π β π β WUni) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (πΆ Nat π·) β π) | ||
Theorem | wunnatOLD 17910 | Obsolete proof of wunnat 17909 as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π β WUni) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (πΆ Nat π·) β π) | ||
Theorem | catstr 17911 | A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ {β¨(Baseβndx), πβ©, β¨(Hom βndx), π»β©, β¨(compβndx), Β· β©} Struct β¨1, ;15β© | ||
Theorem | fucval 17912* | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (πΆ Func π·) & β’ π = (πΆ Nat π·) & β’ π΄ = (BaseβπΆ) & β’ Β· = (compβπ·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ (π β β = (π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st βπ£) / πβ¦β¦(2nd βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st ββ)βπ₯))(πβπ₯)))))) β β’ (π β π = {β¨(Baseβndx), π΅β©, β¨(Hom βndx), πβ©, β¨(compβndx), β β©}) | ||
Theorem | fuccofval 17913* | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (πΆ Func π·) & β’ π = (πΆ Nat π·) & β’ π΄ = (BaseβπΆ) & β’ Β· = (compβπ·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ β = (compβπ) β β’ (π β β = (π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st βπ£) / πβ¦β¦(2nd βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st ββ)βπ₯))(πβπ₯)))))) | ||
Theorem | fucbas 17914 | The objects of the functor category are functors from πΆ to π·. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 12-Jan-2017.) |
β’ π = (πΆ FuncCat π·) β β’ (πΆ Func π·) = (Baseβπ) | ||
Theorem | fuchom 17915 | The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) β β’ π = (Hom βπ) | ||
Theorem | fuchomOLD 17916 | Obsolete proof of fuchom 17915 as of 14-Oct-2024. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) β β’ π = (Hom βπ) | ||
Theorem | fucco 17917* | Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ π΄ = (BaseβπΆ) & β’ Β· = (compβπ·) & β’ β = (compβπ) & β’ (π β π β (πΉππΊ)) & β’ (π β π β (πΊππ»)) β β’ (π β (π(β¨πΉ, πΊβ© β π»)π ) = (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπΉ)βπ₯), ((1st βπΊ)βπ₯)β© Β· ((1st βπ»)βπ₯))(π βπ₯)))) | ||
Theorem | fuccoval 17918 | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ π΄ = (BaseβπΆ) & β’ Β· = (compβπ·) & β’ β = (compβπ) & β’ (π β π β (πΉππΊ)) & β’ (π β π β (πΊππ»)) & β’ (π β π β π΄) β β’ (π β ((π(β¨πΉ, πΊβ© β π»)π )βπ) = ((πβπ)(β¨((1st βπΉ)βπ), ((1st βπΊ)βπ)β© Β· ((1st βπ»)βπ))(π βπ))) | ||
Theorem | fuccocl 17919 | The composition of two natural transformations is a natural transformation. Remark 6.14(a) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ β = (compβπ) & β’ (π β π β (πΉππΊ)) & β’ (π β π β (πΊππ»)) β β’ (π β (π(β¨πΉ, πΊβ© β π»)π ) β (πΉππ»)) | ||
Theorem | fucidcl 17920 | The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ 1 = (Idβπ·) & β’ (π β πΉ β (πΆ Func π·)) β β’ (π β ( 1 β (1st βπΉ)) β (πΉππΉ)) | ||
Theorem | fuclid 17921 | Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ β = (compβπ) & β’ 1 = (Idβπ·) & β’ (π β π β (πΉππΊ)) β β’ (π β (( 1 β (1st βπΊ))(β¨πΉ, πΊβ© β πΊ)π ) = π ) | ||
Theorem | fucrid 17922 | Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ β = (compβπ) & β’ 1 = (Idβπ·) & β’ (π β π β (πΉππΊ)) β β’ (π β (π (β¨πΉ, πΉβ© β πΊ)( 1 β (1st βπΉ))) = π ) | ||
Theorem | fucass 17923 | Associativity of natural transformation composition. Remark 6.14(b) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π = (πΆ Nat π·) & β’ β = (compβπ) & β’ (π β π β (πΉππΊ)) & β’ (π β π β (πΊππ»)) & β’ (π β π β (π»ππΎ)) β β’ (π β ((π(β¨πΊ, π»β© β πΎ)π)(β¨πΉ, πΊβ© β πΎ)π ) = (π(β¨πΉ, π»β© β πΎ)(π(β¨πΉ, πΊβ© β π»)π ))) | ||
Theorem | fuccatid 17924* | The functor category is a category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) & β’ 1 = (Idβπ·) β β’ (π β (π β Cat β§ (Idβπ) = (π β (πΆ Func π·) β¦ ( 1 β (1st βπ))))) | ||
Theorem | fuccat 17925 | The functor category is a category. Remark 6.16 in [Adamek] p. 88. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β π β Cat) | ||
Theorem | fucid 17926 | The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ πΌ = (Idβπ) & β’ 1 = (Idβπ·) & β’ (π β πΉ β (πΆ Func π·)) β β’ (π β (πΌβπΉ) = ( 1 β (1st βπΉ))) | ||
Theorem | fucsect 17927* | Two natural transformations are in a section iff all the components are in a section relation. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (BaseβπΆ) & β’ π = (πΆ Nat π·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) & β’ π = (Sectβπ) & β’ π = (Sectβπ·) β β’ (π β (π(πΉππΊ)π β (π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π((1st βπΊ)βπ₯))(πβπ₯)))) | ||
Theorem | fucinv 17928* | Two natural transformations are inverses of each other iff all the components are inverse. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (BaseβπΆ) & β’ π = (πΆ Nat π·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) & β’ πΌ = (Invβπ) & β’ π½ = (Invβπ·) β β’ (π β (π(πΉπΌπΊ)π β (π β (πΉππΊ) β§ π β (πΊππΉ) β§ βπ₯ β π΅ (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))(πβπ₯)))) | ||
Theorem | invfuc 17929* | If π(π₯) is an inverse to π(π₯) for each π₯, and π is a natural transformation, then π is also a natural transformation, and they are inverse in the functor category. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (BaseβπΆ) & β’ π = (πΆ Nat π·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) & β’ πΌ = (Invβπ) & β’ π½ = (Invβπ·) & β’ (π β π β (πΉππΊ)) & β’ ((π β§ π₯ β π΅) β (πβπ₯)(((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))π) β β’ (π β π(πΉπΌπΊ)(π₯ β π΅ β¦ π)) | ||
Theorem | fuciso 17930* | A natural transformation is an isomorphism of functors iff all its components are isomorphisms. (Contributed by Mario Carneiro, 28-Jan-2017.) |
β’ π = (πΆ FuncCat π·) & β’ π΅ = (BaseβπΆ) & β’ π = (πΆ Nat π·) & β’ (π β πΉ β (πΆ Func π·)) & β’ (π β πΊ β (πΆ Func π·)) & β’ πΌ = (Isoβπ) & β’ π½ = (Isoβπ·) β β’ (π β (π΄ β (πΉπΌπΊ) β (π΄ β (πΉππΊ) β§ βπ₯ β π΅ (π΄βπ₯) β (((1st βπΉ)βπ₯)π½((1st βπΊ)βπ₯))))) | ||
Theorem | natpropd 17931 | If two categories have the same set of objects, morphisms, and compositions, then they have the same natural transformations. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ (π β (Homf βπ΄) = (Homf βπ΅)) & β’ (π β (compfβπ΄) = (compfβπ΅)) & β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) & β’ (π β π΄ β Cat) & β’ (π β π΅ β Cat) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β (π΄ Nat πΆ) = (π΅ Nat π·)) | ||
Theorem | fucpropd 17932 | If two categories have the same set of objects, morphisms, and compositions, then they have the same functor categories. (Contributed by Mario Carneiro, 26-Jan-2017.) |
β’ (π β (Homf βπ΄) = (Homf βπ΅)) & β’ (π β (compfβπ΄) = (compfβπ΅)) & β’ (π β (Homf βπΆ) = (Homf βπ·)) & β’ (π β (compfβπΆ) = (compfβπ·)) & β’ (π β π΄ β Cat) & β’ (π β π΅ β Cat) & β’ (π β πΆ β Cat) & β’ (π β π· β Cat) β β’ (π β (π΄ FuncCat πΆ) = (π΅ FuncCat π·)) | ||
Syntax | cinito 17933 | Extend class notation with the class of initial objects of a category. |
class InitO | ||
Syntax | ctermo 17934 | Extend class notation with the class of terminal objects of a category. |
class TermO | ||
Syntax | czeroo 17935 | Extend class notation with the class of zero objects of a category. |
class ZeroO | ||
Definition | df-inito 17936* | An object A is said to be an initial object provided that for each object B there is exactly one morphism from A to B. Definition 7.1 in [Adamek] p. 101, or definition in [Lang] p. 57 (called "a universally repelling object" there). See dfinito2 17955 and dfinito3 17957 for alternate definitions depending on df-termo 17937. (Contributed by AV, 3-Apr-2020.) |
β’ InitO = (π β Cat β¦ {π β (Baseβπ) β£ βπ β (Baseβπ)β!β β β (π(Hom βπ)π)}) | ||
Definition | df-termo 17937* | An object A is called a terminal object provided that for each object B there is exactly one morphism from B to A. Definition 7.4 in [Adamek] p. 102, or definition in [Lang] p. 57 (called "a universally attracting object" there). See dftermo2 17956 and dftermo3 17958 for alternate definitions depending on df-inito 17936. (Contributed by AV, 3-Apr-2020.) |
β’ TermO = (π β Cat β¦ {π β (Baseβπ) β£ βπ β (Baseβπ)β!β β β (π(Hom βπ)π)}) | ||
Definition | df-zeroo 17938 | An object A is called a zero object provided that it is both an initial object and a terminal object. Definition 7.7 of [Adamek] p. 103. (Contributed by AV, 3-Apr-2020.) |
β’ ZeroO = (π β Cat β¦ ((InitOβπ) β© (TermOβπ))) | ||
Theorem | initofn 17939 | InitO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.) |
β’ InitO Fn Cat | ||
Theorem | termofn 17940 | TermO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.) |
β’ TermO Fn Cat | ||
Theorem | zeroofn 17941 | ZeroO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.) |
β’ ZeroO Fn Cat | ||
Theorem | initorcl 17942 | Reverse closure for an initial object: If a class has an initial object, the class is a category. (Contributed by AV, 4-Apr-2020.) |
β’ (πΌ β (InitOβπΆ) β πΆ β Cat) | ||
Theorem | termorcl 17943 | Reverse closure for a terminal object: If a class has a terminal object, the class is a category. (Contributed by AV, 4-Apr-2020.) |
β’ (π β (TermOβπΆ) β πΆ β Cat) | ||
Theorem | zeroorcl 17944 | Reverse closure for a zero object: If a class has a zero object, the class is a category. (Contributed by AV, 4-Apr-2020.) |
β’ (π β (ZeroOβπΆ) β πΆ β Cat) | ||
Theorem | initoval 17945* | The value of the initial object function, i.e. the set of all initial objects of a category. (Contributed by AV, 3-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) β β’ (π β (InitOβπΆ) = {π β π΅ β£ βπ β π΅ β!β β β (ππ»π)}) | ||
Theorem | termoval 17946* | The value of the terminal object function, i.e. the set of all terminal objects of a category. (Contributed by AV, 3-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) β β’ (π β (TermOβπΆ) = {π β π΅ β£ βπ β π΅ β!β β β (ππ»π)}) | ||
Theorem | zerooval 17947 | The value of the zero object function, i.e. the set of all zero objects of a category. (Contributed by AV, 3-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) β β’ (π β (ZeroOβπΆ) = ((InitOβπΆ) β© (TermOβπΆ))) | ||
Theorem | isinito 17948* | The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) & β’ (π β πΌ β π΅) β β’ (π β (πΌ β (InitOβπΆ) β βπ β π΅ β!β β β (πΌπ»π))) | ||
Theorem | istermo 17949* | The predicate "is a terminal object" of a category. (Contributed by AV, 3-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) & β’ (π β πΌ β π΅) β β’ (π β (πΌ β (TermOβπΆ) β βπ β π΅ β!β β β (ππ»πΌ))) | ||
Theorem | iszeroo 17950 | The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) & β’ (π β πΌ β π΅) β β’ (π β (πΌ β (ZeroOβπΆ) β (πΌ β (InitOβπΆ) β§ πΌ β (TermOβπΆ)))) | ||
Theorem | isinitoi 17951* | Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) β β’ ((π β§ π β (InitOβπΆ)) β (π β π΅ β§ βπ β π΅ β!β β β (ππ»π))) | ||
Theorem | istermoi 17952* | Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) β β’ ((π β§ π β (TermOβπΆ)) β (π β π΅ β§ βπ β π΅ β!β β β (ππ»π))) | ||
Theorem | initoid 17953 | For an initial object, the identity arrow is the one and only morphism of the object to the object itself. (Contributed by AV, 6-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) β β’ ((π β§ π β (InitOβπΆ)) β (ππ»π) = {((IdβπΆ)βπ)}) | ||
Theorem | termoid 17954 | For a terminal object, the identity arrow is the one and only morphism of the object to the object itself. (Contributed by AV, 18-Apr-2020.) |
β’ π΅ = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ (π β πΆ β Cat) β β’ ((π β§ π β (TermOβπΆ)) β (ππ»π) = {((IdβπΆ)βπ)}) | ||
Theorem | dfinito2 17955 | An initial object is a terminal object in the opposite category. An alternate definition of df-inito 17936 depending on df-termo 17937. (Contributed by Zhi Wang, 29-Aug-2024.) |
β’ InitO = (π β Cat β¦ (TermOβ(oppCatβπ))) | ||
Theorem | dftermo2 17956 | A terminal object is an initial object in the opposite category. An alternate definition of df-termo 17937 depending on df-inito 17936. (Contributed by Zhi Wang, 29-Aug-2024.) |
β’ TermO = (π β Cat β¦ (InitOβ(oppCatβπ))) | ||
Theorem | dfinito3 17957 | An alternate definition of df-inito 17936 depending on df-termo 17937, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.) |
β’ InitO = (TermO β (oppCat βΎ Cat)) | ||
Theorem | dftermo3 17958 | An alternate definition of df-termo 17937 depending on df-inito 17936, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.) |
β’ TermO = (InitO β (oppCat βΎ Cat)) | ||
Theorem | initoo 17959 | An initial object is an object. (Contributed by AV, 14-Apr-2020.) |
β’ (πΆ β Cat β (π β (InitOβπΆ) β π β (BaseβπΆ))) | ||
Theorem | termoo 17960 | A terminal object is an object. (Contributed by AV, 18-Apr-2020.) |
β’ (πΆ β Cat β (π β (TermOβπΆ) β π β (BaseβπΆ))) | ||
Theorem | iszeroi 17961 | Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020.) |
β’ ((πΆ β Cat β§ π β (ZeroOβπΆ)) β (π β (BaseβπΆ) β§ (π β (InitOβπΆ) β§ π β (TermOβπΆ)))) | ||
Theorem | 2initoinv 17962 | Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ (π β π΄ β (InitOβπΆ)) & β’ (π β π΅ β (InitOβπΆ)) β β’ ((π β§ πΊ β (π΅(Hom βπΆ)π΄) β§ πΉ β (π΄(Hom βπΆ)π΅)) β πΉ(π΄(InvβπΆ)π΅)πΊ) | ||
Theorem | initoeu1 17963* | Initial objects are essentially unique (strong form), i.e. there is a unique isomorphism between two initial objects, see statement in [Lang] p. 58 ("... if P, P' are two universal objects [...] then there exists a unique isomorphism between them.". (Proposed by BJ, 14-Apr-2020.) (Contributed by AV, 14-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ (π β π΄ β (InitOβπΆ)) & β’ (π β π΅ β (InitOβπΆ)) β β’ (π β β!π π β (π΄(IsoβπΆ)π΅)) | ||
Theorem | initoeu1w 17964 | Initial objects are essentially unique (weak form), i.e. if A and B are initial objects, then A and B are isomorphic. Proposition 7.3 (1) of [Adamek] p. 102. (Contributed by AV, 6-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ (π β π΄ β (InitOβπΆ)) & β’ (π β π΅ β (InitOβπΆ)) β β’ (π β π΄( βπ βπΆ)π΅) | ||
Theorem | initoeu2lem0 17965 | Lemma 0 for initoeu2 17968. (Contributed by AV, 9-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ (π β π΄ β (InitOβπΆ)) & β’ π = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ πΌ = (IsoβπΆ) & β’ β¬ = (compβπΆ) β β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)) | ||
Theorem | initoeu2lem1 17966* | Lemma 1 for initoeu2 17968. (Contributed by AV, 9-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ (π β π΄ β (InitOβπΆ)) & β’ π = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ πΌ = (IsoβπΆ) & β’ β¬ = (compβπΆ) β β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π) β§ (πΎ β (π΅πΌπ΄) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·))) β ((β!π π β (π΄π»π·) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))) | ||
Theorem | initoeu2lem2 17967* | Lemma 2 for initoeu2 17968. (Contributed by AV, 10-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ (π β π΄ β (InitOβπΆ)) & β’ π = (BaseβπΆ) & β’ π» = (Hom βπΆ) & β’ πΌ = (IsoβπΆ) & β’ β¬ = (compβπΆ) β β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅π»π·))) β (β!π π β (π΄π»π·) β β!π π β (π΅π»π·))) | ||
Theorem | initoeu2 17968 | Initial objects are essentially unique, if A is an initial object, then so is every object that is isomorphic to A. Proposition 7.3 (2) in [Adamek] p. 102. (Contributed by AV, 10-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ (π β π΄ β (InitOβπΆ)) & β’ (π β π΄( βπ βπΆ)π΅) β β’ (π β π΅ β (InitOβπΆ)) | ||
Theorem | 2termoinv 17969 | Morphisms between two terminal objects are inverses. (Contributed by AV, 18-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ (π β π΄ β (TermOβπΆ)) & β’ (π β π΅ β (TermOβπΆ)) β β’ ((π β§ πΊ β (π΅(Hom βπΆ)π΄) β§ πΉ β (π΄(Hom βπΆ)π΅)) β πΉ(π΄(InvβπΆ)π΅)πΊ) | ||
Theorem | termoeu1 17970* | Terminal objects are essentially unique (strong form), i.e. there is a unique isomorphism between two terminal objects, see statement in [Lang] p. 58 ("... if P, P' are two universal objects [...] then there exists a unique isomorphism between them.". (Proposed by BJ, 14-Apr-2020.) (Contributed by AV, 18-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ (π β π΄ β (TermOβπΆ)) & β’ (π β π΅ β (TermOβπΆ)) β β’ (π β β!π π β (π΄(IsoβπΆ)π΅)) | ||
Theorem | termoeu1w 17971 | Terminal objects are essentially unique (weak form), i.e. if A and B are terminal objects, then A and B are isomorphic. Proposition 7.6 of [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.) |
β’ (π β πΆ β Cat) & β’ (π β π΄ β (TermOβπΆ)) & β’ (π β π΅ β (TermOβπΆ)) β β’ (π β π΄( βπ βπΆ)π΅) | ||
Syntax | cdoma 17972 | Extend class notation to include the domain extractor for an arrow. |
class doma | ||
Syntax | ccoda 17973 | Extend class notation to include the codomain extractor for an arrow. |
class coda | ||
Syntax | carw 17974 | Extend class notation to include the collection of all arrows of a category. |
class Arrow | ||
Syntax | choma 17975 | Extend class notation to include the set of all arrows with a specific domain and codomain. |
class Homa | ||
Definition | df-doma 17976 | Definition of the domain extractor for an arrow. (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.) |
β’ doma = (1st β 1st ) | ||
Definition | df-coda 17977 | Definition of the codomain extractor for an arrow. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.) |
β’ coda = (2nd β 1st ) | ||
Definition | df-homa 17978* | Definition of the hom-set extractor for arrows, which tags the morphisms of the underlying hom-set with domain and codomain, which can then be extracted using df-doma 17976 and df-coda 17977. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.) |
β’ Homa = (π β Cat β¦ (π₯ β ((Baseβπ) Γ (Baseβπ)) β¦ ({π₯} Γ ((Hom βπ)βπ₯)))) | ||
Definition | df-arw 17979 | Definition of the set of arrows of a category. We will use the term "arrow" to denote a morphism tagged with its domain and codomain, as opposed to Hom, which allows hom-sets for distinct objects to overlap. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ Arrow = (π β Cat β¦ βͺ ran (Homaβπ)) | ||
Theorem | homarcl 17980 | Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) β β’ (πΉ β (ππ»π) β πΆ β Cat) | ||
Theorem | homafval 17981* | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ π½ = (Hom βπΆ) β β’ (π β π» = (π₯ β (π΅ Γ π΅) β¦ ({π₯} Γ (π½βπ₯)))) | ||
Theorem | homaf 17982 | Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) β β’ (π β π»:(π΅ Γ π΅)βΆπ« ((π΅ Γ π΅) Γ V)) | ||
Theorem | homaval 17983 | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ π½ = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (ππ»π) = ({β¨π, πβ©} Γ (ππ½π))) | ||
Theorem | elhoma 17984 | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ π½ = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π(ππ»π)πΉ β (π = β¨π, πβ© β§ πΉ β (ππ½π)))) | ||
Theorem | elhomai 17985 | Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ π½ = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππ½π)) β β’ (π β β¨π, πβ©(ππ»π)πΉ) | ||
Theorem | elhomai2 17986 | Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) & β’ π΅ = (BaseβπΆ) & β’ (π β πΆ β Cat) & β’ π½ = (Hom βπΆ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΉ β (ππ½π)) β β’ (π β β¨π, π, πΉβ© β (ππ»π)) | ||
Theorem | homarcl2 17987 | Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) & β’ π΅ = (BaseβπΆ) β β’ (πΉ β (ππ»π) β (π β π΅ β§ π β π΅)) | ||
Theorem | homarel 17988 | An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) β β’ Rel (ππ»π) | ||
Theorem | homa1 17989 | The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) β β’ (π(ππ»π)πΉ β π = β¨π, πβ©) | ||
Theorem | homahom2 17990 | The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) & β’ π½ = (Hom βπΆ) β β’ (π(ππ»π)πΉ β πΉ β (ππ½π)) | ||
Theorem | homahom 17991 | The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) & β’ π½ = (Hom βπΆ) β β’ (πΉ β (ππ»π) β (2nd βπΉ) β (ππ½π)) | ||
Theorem | homadm 17992 | The domain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) β β’ (πΉ β (ππ»π) β (domaβπΉ) = π) | ||
Theorem | homacd 17993 | The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) β β’ (πΉ β (ππ»π) β (codaβπΉ) = π) | ||
Theorem | homadmcd 17994 | Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π» = (HomaβπΆ) β β’ (πΉ β (ππ»π) β πΉ = β¨π, π, (2nd βπΉ)β©) | ||
Theorem | arwval 17995 | The set of arrows is the union of all the disjointified hom-sets. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π΄ = (ArrowβπΆ) & β’ π» = (HomaβπΆ) β β’ π΄ = βͺ ran π» | ||
Theorem | arwrcl 17996 | The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π΄ = (ArrowβπΆ) β β’ (πΉ β π΄ β πΆ β Cat) | ||
Theorem | arwhoma 17997 | An arrow is contained in the hom-set corresponding to its domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π΄ = (ArrowβπΆ) & β’ π» = (HomaβπΆ) β β’ (πΉ β π΄ β πΉ β ((domaβπΉ)π»(codaβπΉ))) | ||
Theorem | homarw 17998 | A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π΄ = (ArrowβπΆ) & β’ π» = (HomaβπΆ) β β’ (ππ»π) β π΄ | ||
Theorem | arwdm 17999 | The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π΄ = (ArrowβπΆ) & β’ π΅ = (BaseβπΆ) β β’ (πΉ β π΄ β (domaβπΉ) β π΅) | ||
Theorem | arwcd 18000 | The codomain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
β’ π΄ = (ArrowβπΆ) & β’ π΅ = (BaseβπΆ) β β’ (πΉ β π΄ β (codaβπΉ) β π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |