![]() |
Metamath
Proof Explorer Theorem List (p. 181 of 486) | < 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-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | natpropd 18001 | 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 18002 | 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 18003 | Extend class notation with the class of initial objects of a category. |
class InitO | ||
Syntax | ctermo 18004 | Extend class notation with the class of terminal objects of a category. |
class TermO | ||
Syntax | czeroo 18005 | Extend class notation with the class of zero objects of a category. |
class ZeroO | ||
Definition | df-inito 18006* | 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 18025 and dfinito3 18027 for alternate definitions depending on df-termo 18007. (Contributed by AV, 3-Apr-2020.) |
⊢ InitO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)}) | ||
Definition | df-termo 18007* | 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 18026 and dftermo3 18028 for alternate definitions depending on df-inito 18006. (Contributed by AV, 3-Apr-2020.) |
⊢ TermO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎)}) | ||
Definition | df-zeroo 18008 | 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 18009 | InitO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.) |
⊢ InitO Fn Cat | ||
Theorem | termofn 18010 | TermO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.) |
⊢ TermO Fn Cat | ||
Theorem | zeroofn 18011 | ZeroO is a function on Cat. (Contributed by Zhi Wang, 29-Aug-2024.) |
⊢ ZeroO Fn Cat | ||
Theorem | initorcl 18012 | 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 18013 | 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 18014 | 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 18015* | 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 18016* | 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 18017 | 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 18018* | The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝐼𝐻𝑏))) | ||
Theorem | istermo 18019* | The predicate "is a terminal object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (TermO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝐼))) | ||
Theorem | iszeroo 18020 | The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (ZeroO‘𝐶) ↔ (𝐼 ∈ (InitO‘𝐶) ∧ 𝐼 ∈ (TermO‘𝐶)))) | ||
Theorem | isinitoi 18021* | Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑏))) | ||
Theorem | istermoi 18022* | Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑂))) | ||
Theorem | initoid 18023 | 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 18024 | 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 18025 | An initial object is a terminal object in the opposite category. An alternate definition of df-inito 18006 depending on df-termo 18007. (Contributed by Zhi Wang, 29-Aug-2024.) |
⊢ InitO = (𝑐 ∈ Cat ↦ (TermO‘(oppCat‘𝑐))) | ||
Theorem | dftermo2 18026 | A terminal object is an initial object in the opposite category. An alternate definition of df-termo 18007 depending on df-inito 18006. (Contributed by Zhi Wang, 29-Aug-2024.) |
⊢ TermO = (𝑐 ∈ Cat ↦ (InitO‘(oppCat‘𝑐))) | ||
Theorem | dfinito3 18027 | An alternate definition of df-inito 18006 depending on df-termo 18007, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.) |
⊢ InitO = (TermO ∘ (oppCat ↾ Cat)) | ||
Theorem | dftermo3 18028 | An alternate definition of df-termo 18007 depending on df-inito 18006, without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024.) |
⊢ TermO = (InitO ∘ (oppCat ↾ Cat)) | ||
Theorem | initoo 18029 | An initial object is an object. (Contributed by AV, 14-Apr-2020.) |
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ (Base‘𝐶))) | ||
Theorem | termoo 18030 | A terminal object is an object. (Contributed by AV, 18-Apr-2020.) |
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ (Base‘𝐶))) | ||
Theorem | iszeroi 18031 | Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (ZeroO‘𝐶)) → (𝑂 ∈ (Base‘𝐶) ∧ (𝑂 ∈ (InitO‘𝐶) ∧ 𝑂 ∈ (TermO‘𝐶)))) | ||
Theorem | 2initoinv 18032 | Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶)) ⇒ ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺) | ||
Theorem | initoeu1 18033* | 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 18034 | 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 18035 | Lemma 0 for initoeu2 18038. (Contributed by AV, 9-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ (((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) ∧ ((𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾)(〈𝐴, 𝐵〉 ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(〈𝐴, 𝐵〉 ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) → 𝐺 = (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾)) | ||
Theorem | initoeu2lem1 18036* | Lemma 1 for initoeu2 18038. (Contributed by AV, 9-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 = (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾))) | ||
Theorem | initoeu2lem2 18037* | Lemma 2 for initoeu2 18038. (Contributed by AV, 10-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → (∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) → ∃!𝑔 𝑔 ∈ (𝐵𝐻𝐷))) | ||
Theorem | initoeu2 18038 | 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 18039 | Morphisms between two terminal objects are inverses. (Contributed by AV, 18-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶)) ⇒ ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺) | ||
Theorem | termoeu1 18040* | 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 18041 | 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 18042 | Extend class notation to include the domain extractor for an arrow. |
class doma | ||
Syntax | ccoda 18043 | Extend class notation to include the codomain extractor for an arrow. |
class coda | ||
Syntax | carw 18044 | Extend class notation to include the collection of all arrows of a category. |
class Arrow | ||
Syntax | choma 18045 | Extend class notation to include the set of all arrows with a specific domain and codomain. |
class Homa | ||
Definition | df-doma 18046 | 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 18047 | 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 18048* | 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 18046 and df-coda 18047. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.) |
⊢ Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥)))) | ||
Definition | df-arw 18049 | 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 18050 | Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐶 ∈ Cat) | ||
Theorem | homafval 18051* | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐻 = (𝑥 ∈ (𝐵 × 𝐵) ↦ ({𝑥} × (𝐽‘𝑥)))) | ||
Theorem | homaf 18052 | Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐻:(𝐵 × 𝐵)⟶𝒫 ((𝐵 × 𝐵) × V)) | ||
Theorem | homaval 18053 | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = ({〈𝑋, 𝑌〉} × (𝑋𝐽𝑌))) | ||
Theorem | elhoma 18054 | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑍(𝑋𝐻𝑌)𝐹 ↔ (𝑍 = 〈𝑋, 𝑌〉 ∧ 𝐹 ∈ (𝑋𝐽𝑌)))) | ||
Theorem | elhomai 18055 | Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌)) ⇒ ⊢ (𝜑 → 〈𝑋, 𝑌〉(𝑋𝐻𝑌)𝐹) | ||
Theorem | elhomai2 18056 | Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌)) ⇒ ⊢ (𝜑 → 〈𝑋, 𝑌, 𝐹〉 ∈ (𝑋𝐻𝑌)) | ||
Theorem | homarcl2 18057 | Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
Theorem | homarel 18058 | An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ Rel (𝑋𝐻𝑌) | ||
Theorem | homa1 18059 | The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝑍(𝑋𝐻𝑌)𝐹 → 𝑍 = 〈𝑋, 𝑌〉) | ||
Theorem | homahom2 18060 | 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 18061 | 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 18062 | The domain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (doma‘𝐹) = 𝑋) | ||
Theorem | homacd 18063 | The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (coda‘𝐹) = 𝑌) | ||
Theorem | homadmcd 18064 | Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹 = 〈𝑋, 𝑌, (2nd ‘𝐹)〉) | ||
Theorem | arwval 18065 | 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 18066 | 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 18067 | 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 18068 | A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝑋𝐻𝑌) ⊆ 𝐴 | ||
Theorem | arwdm 18069 | The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → (doma‘𝐹) ∈ 𝐵) | ||
Theorem | arwcd 18070 | The codomain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → (coda‘𝐹) ∈ 𝐵) | ||
Theorem | dmaf 18071 | The domain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (doma ↾ 𝐴):𝐴⟶𝐵 | ||
Theorem | cdaf 18072 | The codomain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (coda ↾ 𝐴):𝐴⟶𝐵 | ||
Theorem | arwhom 18073 | The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → (2nd ‘𝐹) ∈ ((doma‘𝐹)𝐽(coda‘𝐹))) | ||
Theorem | arwdmcd 18074 | Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝐹 = 〈(doma‘𝐹), (coda‘𝐹), (2nd ‘𝐹)〉) | ||
Syntax | cida 18075 | Extend class notation to include identity for arrows. |
class Ida | ||
Syntax | ccoa 18076 | Extend class notation to include composition for arrows. |
class compa | ||
Definition | df-ida 18077* | Definition of the identity arrow, which is just the identity morphism tagged with its domain and codomain. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.) |
⊢ Ida = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ 〈𝑥, 𝑥, ((Id‘𝑐)‘𝑥)〉)) | ||
Definition | df-coa 18078* | Definition of the composition of arrows. Since arrows are tagged with domain and codomain, this does not need to be a quinary operation like the regular composition in a category comp. Instead, it is a partial binary operation on arrows, which is defined when the domain of the first arrow matches the codomain of the second. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ compa = (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ 〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓), (doma‘𝑔)〉(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))〉)) | ||
Theorem | idafval 18079* | Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵 ↦ 〈𝑥, 𝑥, ( 1 ‘𝑥)〉)) | ||
Theorem | idaval 18080 | Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) = 〈𝑋, 𝑋, ( 1 ‘𝑋)〉) | ||
Theorem | ida2 18081 | Morphism part of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (2nd ‘(𝐼‘𝑋)) = ( 1 ‘𝑋)) | ||
Theorem | idahom 18082 | Domain and codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋𝐻𝑋)) | ||
Theorem | idadm 18083 | Domain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (doma‘(𝐼‘𝑋)) = 𝑋) | ||
Theorem | idacd 18084 | Codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (coda‘(𝐼‘𝑋)) = 𝑋) | ||
Theorem | idaf 18085 | The identity arrow function is a function from objects to arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐼 = (Ida‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐴 = (Arrow‘𝐶) ⇒ ⊢ (𝜑 → 𝐼:𝐵⟶𝐴) | ||
Theorem | coafval 18086* | The value of the composition of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐴 = (Arrow‘𝐶) & ⊢ ∙ = (comp‘𝐶) ⇒ ⊢ · = (𝑔 ∈ 𝐴, 𝑓 ∈ {ℎ ∈ 𝐴 ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ 〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓), (doma‘𝑔)〉 ∙ (coda‘𝑔))(2nd ‘𝑓))〉) | ||
Theorem | eldmcoa 18087 | A pair 〈𝐺, 𝐹〉 is in the domain of the arrow composition, if the domain of 𝐺 equals the codomain of 𝐹. (In this case we say 𝐺 and 𝐹 are composable.) (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐴 = (Arrow‘𝐶) ⇒ ⊢ (𝐺dom · 𝐹 ↔ (𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ (coda‘𝐹) = (doma‘𝐺))) | ||
Theorem | dmcoass 18088 | The domain of composition is a collection of pairs of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐴 = (Arrow‘𝐶) ⇒ ⊢ dom · ⊆ (𝐴 × 𝐴) | ||
Theorem | homdmcoa 18089 | If 𝐹:𝑋⟶𝑌 and 𝐺:𝑌⟶𝑍, then 𝐺 and 𝐹 are composable. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → 𝐺dom · 𝐹) | ||
Theorem | coaval 18090 | Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ ∙ = (comp‘𝐶) ⇒ ⊢ (𝜑 → (𝐺 · 𝐹) = 〈𝑋, 𝑍, ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))〉) | ||
Theorem | coa2 18091 | The morphism part of arrow composition. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ ∙ = (comp‘𝐶) ⇒ ⊢ (𝜑 → (2nd ‘(𝐺 · 𝐹)) = ((2nd ‘𝐺)(〈𝑋, 𝑌〉 ∙ 𝑍)(2nd ‘𝐹))) | ||
Theorem | coahom 18092 | The composition of two composable arrows is an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → (𝐺 · 𝐹) ∈ (𝑋𝐻𝑍)) | ||
Theorem | coapm 18093 | Composition of arrows is a partial binary operation on arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ · = (compa‘𝐶) & ⊢ 𝐴 = (Arrow‘𝐶) ⇒ ⊢ · ∈ (𝐴 ↑pm (𝐴 × 𝐴)) | ||
Theorem | arwlid 18094 | Left identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ · = (compa‘𝐶) & ⊢ 1 = (Ida‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (( 1 ‘𝑌) · 𝐹) = 𝐹) | ||
Theorem | arwrid 18095 | Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ · = (compa‘𝐶) & ⊢ 1 = (Ida‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (𝐹 · ( 1 ‘𝑋)) = 𝐹) | ||
Theorem | arwass 18096 | Associativity of composition in a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ · = (compa‘𝐶) & ⊢ 1 = (Ida‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑊)) ⇒ ⊢ (𝜑 → ((𝐾 · 𝐺) · 𝐹) = (𝐾 · (𝐺 · 𝐹))) | ||
Syntax | csetc 18097 | Extend class notation to include the category Set. |
class SetCat | ||
Definition | df-setc 18098* | Definition of the category Set, relativized to a subset 𝑢. Example 3.3(1) of [Adamek] p. 22. This is the category of all sets in 𝑢 and functions between these sets. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by FL, 8-Nov-2013.) (Revised by Mario Carneiro, 3-Jan-2017.) |
⊢ SetCat = (𝑢 ∈ V ↦ {〈(Base‘ndx), 𝑢〉, 〈(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ (𝑦 ↑m 𝑥))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉}) | ||
Theorem | setcval 18099* | Value of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ (𝑦 ↑m 𝑥))) & ⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) ⇒ ⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) | ||
Theorem | setcbas 18100 | Set of objects of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐶 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑈 = (Base‘𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |