Home | Metamath
Proof Explorer Theorem List (p. 165 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fthi 16401 | The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑆 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (((𝑋𝐺𝑌)‘𝑅) = ((𝑋𝐺𝑌)‘𝑆) ↔ 𝑅 = 𝑆)) | ||
Theorem | ffthf1o 16402 | The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)–1-1-onto→((𝐹‘𝑋)𝐽(𝐹‘𝑌))) | ||
Theorem | fullpropd 16403 | If two categories have the same set of objects, morphisms, and compositions, then they have the same full functors. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 Full 𝐶) = (𝐵 Full 𝐷)) | ||
Theorem | fthpropd 16404 | If two categories have the same set of objects, morphisms, and compositions, then they have the same faithful functors. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 Faith 𝐶) = (𝐵 Faith 𝐷)) | ||
Theorem | fulloppc 16405 | The opposite functor of a full functor is also full. Proposition 3.43(d) in [Adamek] p. 39. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝑂 Full 𝑃)tpos 𝐺) | ||
Theorem | fthoppc 16406 | The opposite functor of a faithful functor is also faithful. Proposition 3.43(c) in [Adamek] p. 39. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝑂 Faith 𝑃)tpos 𝐺) | ||
Theorem | ffthoppc 16407 | The opposite functor of a fully faithful functor is also full and faithful. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑃 = (oppCat‘𝐷) & ⊢ (𝜑 → 𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺) ⇒ ⊢ (𝜑 → 𝐹((𝑂 Full 𝑃) ∩ (𝑂 Faith 𝑃))tpos 𝐺) | ||
Theorem | fthsect 16408 | A faithful functor reflects sections. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑋)) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝐷) ⇒ ⊢ (𝜑 → (𝑀(𝑋𝑆𝑌)𝑁 ↔ ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝑇(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁))) | ||
Theorem | fthinv 16409 | A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑋)) & ⊢ 𝐼 = (Inv‘𝐶) & ⊢ 𝐽 = (Inv‘𝐷) ⇒ ⊢ (𝜑 → (𝑀(𝑋𝐼𝑌)𝑁 ↔ ((𝑋𝐺𝑌)‘𝑀)((𝐹‘𝑋)𝐽(𝐹‘𝑌))((𝑌𝐺𝑋)‘𝑁))) | ||
Theorem | fthmon 16410 | A faithful functor reflects monomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ 𝑁 = (Mono‘𝐷) & ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑁(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → 𝑅 ∈ (𝑋𝑀𝑌)) | ||
Theorem | fthepi 16411 | A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ 𝑃 = (Epi‘𝐷) & ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝑃(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐸𝑌)) | ||
Theorem | ffthiso 16412 | A fully faithful functor reflects isomorphisms. Corollary 3.32 of [Adamek] p. 35. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹(𝐶 Faith 𝐷)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐹(𝐶 Full 𝐷)𝐺) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐽 = (Iso‘𝐷) ⇒ ⊢ (𝜑 → (𝑅 ∈ (𝑋𝐼𝑌) ↔ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))) | ||
Theorem | fthres2b 16413* | Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑅 ∈ (Subcat‘𝐷)) & ⊢ (𝜑 → 𝑅 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦))) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ 𝐹(𝐶 Faith (𝐷 ↾cat 𝑅))𝐺)) | ||
Theorem | fthres2c 16414 | Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) |
⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐸 = (𝐷 ↾s 𝑆) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ 𝐹(𝐶 Faith 𝐸)𝐺)) | ||
Theorem | fthres2 16415 | A faithful functor into a restricted category is also a faithful functor into the whole category. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ (𝑅 ∈ (Subcat‘𝐷) → (𝐶 Faith (𝐷 ↾cat 𝑅)) ⊆ (𝐶 Faith 𝐷)) | ||
Theorem | idffth 16416 | The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐼 = (idfunc‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → 𝐼 ∈ ((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶))) | ||
Theorem | cofull 16417 | The composition of two full functors is full. Proposition 3.30(d) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ (𝐶 Full 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Full 𝐸)) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Full 𝐸)) | ||
Theorem | cofth 16418 | The composition of two faithful functors is faithful. Proposition 3.30(c) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ (𝐶 Faith 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐷 Faith 𝐸)) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Faith 𝐸)) | ||
Theorem | coffth 16419 | The composition of two fully faithful functors is fully faithful. (Contributed by Mario Carneiro, 28-Jan-2017.) |
⊢ (𝜑 → 𝐹 ∈ ((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))) & ⊢ (𝜑 → 𝐺 ∈ ((𝐷 Full 𝐸) ∩ (𝐷 Faith 𝐸))) ⇒ ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ ((𝐶 Full 𝐸) ∩ (𝐶 Faith 𝐸))) | ||
Theorem | rescfth 16420 | The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ 𝐼 = (idfunc‘𝐷) ⇒ ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 ∈ (𝐷 Faith 𝐶)) | ||
Theorem | ressffth 16421 | The inclusion functor from a full subcategory is a full and faithful functor, see also remark 4.4(2) in [Adamek] p. 49. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾s 𝑆) & ⊢ 𝐼 = (idfunc‘𝐷) ⇒ ⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))) | ||
Theorem | fullres2c 16422 | Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) |
⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐸 = (𝐷 ↾s 𝑆) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) ⇒ ⊢ (𝜑 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ 𝐹(𝐶 Full 𝐸)𝐺)) | ||
Theorem | ffthres2c 16423 | Condition for a fully faithful functor to also be a fully faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐸 = (𝐷 ↾s 𝑆) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) ⇒ ⊢ (𝜑 → (𝐹((𝐶 Full 𝐷) ∩ (𝐶 Faith 𝐷))𝐺 ↔ 𝐹((𝐶 Full 𝐸) ∩ (𝐶 Faith 𝐸))𝐺)) | ||
Syntax | cnat 16424 | Extend class notation to include the collection of natural transformations. |
class Nat | ||
Syntax | cfuc 16425 | Extend class notation to include the functor category. |
class FuncCat | ||
Definition | df-nat 16426* | Definition of a natural transformation between two functors. A natural transformation 𝐴:𝐹⟶𝐺 is a collection of arrows 𝐴(𝑥):𝐹(𝑥)⟶𝐺(𝑥), such that 𝐴(𝑦) ∘ 𝐹(ℎ) = 𝐺(ℎ) ∘ 𝐴(𝑥) for each morphism ℎ:𝑥⟶𝑦. Definition 6.1 in [Adamek] p. 83, and definition in [Lang] p. 65. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ Nat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))})) | ||
Definition | df-fuc 16427* | Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ FuncCat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {〈(Base‘ndx), (𝑡 Func 𝑢)〉, 〈(Hom ‘ndx), (𝑡 Nat 𝑢)〉, 〈(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉}) | ||
Theorem | fnfuc 16428 | The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ FuncCat Fn (Cat × Cat) | ||
Theorem | natfval 16429* | Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) ⇒ ⊢ 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ 𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) | ||
Theorem | isnat 16430* | Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) ⇒ ⊢ (𝜑 → (𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥))))) | ||
Theorem | isnat2 16431* | 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 16432 | The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) | ||
Theorem | natrcl 16433 | Reverse closure for a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ (𝐴 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) | ||
Theorem | nat1st2nd 16434 | Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (〈(1st ‘𝐹), (2nd ‘𝐹)〉𝑁〈(1st ‘𝐺), (2nd ‘𝐺)〉)) | ||
Theorem | natixp 16435* | 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 16436 | A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) ∈ ((𝐹‘𝑋)𝐽(𝐾‘𝑋))) | ||
Theorem | natfn 16437 | A natural transformation is a function on the objects of 𝐶. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → 𝐴 Fn 𝐵) | ||
Theorem | nati 16438 | Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝐴‘𝑌)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉 · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(〈(𝐹‘𝑋), (𝐾‘𝑋)〉 · (𝐾‘𝑌))(𝐴‘𝑋))) | ||
Theorem | wunnat 16439 | A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐶 Nat 𝐷) ∈ 𝑈) | ||
Theorem | catstr 16440 | A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ {〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉} Struct 〈1, ;15〉 | ||
Theorem | fucval 16441* | 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 16442* | 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 16443 | 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 16444 | The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ 𝑁 = (Hom ‘𝑄) | ||
Theorem | fucco 16445* | Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) ⇒ ⊢ (𝜑 → (𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅) = (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st ‘𝐻)‘𝑥))(𝑅‘𝑥)))) | ||
Theorem | fuccoval 16446 | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅)‘𝑋) = ((𝑆‘𝑋)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)〉 · ((1st ‘𝐻)‘𝑋))(𝑅‘𝑋))) | ||
Theorem | fuccocl 16447 | 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 16448 | The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → ( 1 ∘ (1st ‘𝐹)) ∈ (𝐹𝑁𝐹)) | ||
Theorem | fuclid 16449 | Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → (( 1 ∘ (1st ‘𝐺))(〈𝐹, 𝐺〉 ∙ 𝐺)𝑅) = 𝑅) | ||
Theorem | fucrid 16450 | Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → (𝑅(〈𝐹, 𝐹〉 ∙ 𝐺)( 1 ∘ (1st ‘𝐹))) = 𝑅) | ||
Theorem | fucass 16451 | 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 16452* | 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 16453 | 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 16454 | The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝐼‘𝐹) = ( 1 ∘ (1st ‘𝐹))) | ||
Theorem | fucsect 16455* | 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 16456* | 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 16457* | 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 16458* | 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 16459 | 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 16460 | 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 16461 | Extend class notation with the class of initial objects of a category. |
class InitO | ||
Syntax | ctermo 16462 | Extend class notation with the class of terminal objects of a category. |
class TermO | ||
Syntax | czeroo 16463 | Extend class notation with the class of zero objects of a category. |
class ZeroO | ||
Definition | df-inito 16464* | 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). (Contributed by AV, 3-Apr-2020.) |
⊢ InitO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)}) | ||
Definition | df-termo 16465* | 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). (Contributed by AV, 3-Apr-2020.) |
⊢ TermO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑏(Hom ‘𝑐)𝑎)}) | ||
Definition | df-zeroo 16466 | 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 | initorcl 16467 | 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 16468 | 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 16469 | 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 16470* | 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 16471* | 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 16472 | 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 16473* | The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝐼𝐻𝑏))) | ||
Theorem | istermo 16474* | The predicate "is a terminal object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (TermO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝐼))) | ||
Theorem | iszeroo 16475 | The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (ZeroO‘𝐶) ↔ (𝐼 ∈ (InitO‘𝐶) ∧ 𝐼 ∈ (TermO‘𝐶)))) | ||
Theorem | isinitoi 16476* | Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑏))) | ||
Theorem | istermoi 16477* | Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑂))) | ||
Theorem | initoid 16478 | 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 16479 | 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 | initoo 16480 | An initial object is an object. (Contributed by AV, 14-Apr-2020.) |
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ (Base‘𝐶))) | ||
Theorem | termoo 16481 | A terminal object is an object. (Contributed by AV, 18-Apr-2020.) |
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ (Base‘𝐶))) | ||
Theorem | iszeroi 16482 | Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (ZeroO‘𝐶)) → (𝑂 ∈ (Base‘𝐶) ∧ (𝑂 ∈ (InitO‘𝐶) ∧ 𝑂 ∈ (TermO‘𝐶)))) | ||
Theorem | 2initoinv 16483 | Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶)) ⇒ ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺) | ||
Theorem | initoeu1 16484* | 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 16485 | 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 16486 | Lemma 0 for initoeu2 16489. (Contributed by AV, 9-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ (((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) ∧ ((𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾)(〈𝐴, 𝐵〉 ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(〈𝐴, 𝐵〉 ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) → 𝐺 = (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾)) | ||
Theorem | initoeu2lem1 16487* | Lemma 1 for initoeu2 16489. (Contributed by AV, 9-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 = (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾))) | ||
Theorem | initoeu2lem2 16488* | Lemma 2 for initoeu2 16489. (Contributed by AV, 10-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → (∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) → ∃!𝑔 𝑔 ∈ (𝐵𝐻𝐷))) | ||
Theorem | initoeu2 16489 | 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 16490 | Morphisms between two terminal objects are inverses. (Contributed by AV, 18-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶)) ⇒ ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺) | ||
Theorem | termoeu1 16491* | 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 16492 | 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 16493 | Extend class notation to include the domain extractor for an arrow. |
class doma | ||
Syntax | ccoda 16494 | Extend class notation to include the codomain extractor for an arrow. |
class coda | ||
Syntax | carw 16495 | Extend class notation to include the collection of all arrows of a category. |
class Arrow | ||
Syntax | choma 16496 | Extend class notation to include the set of all arrows with a specific domain and codomain. |
class Homa | ||
Definition | df-doma 16497 | 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 16498 | 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 16499* | 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 16497 and df-coda 16498. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.) |
⊢ Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥)))) | ||
Definition | df-arw 16500 | 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‘𝑐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |