![]() |
Metamath
Proof Explorer Theorem List (p. 173 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fullres2c 17201 | 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 17202 | 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 17203 | Extend class notation to include the collection of natural transformations. |
class Nat | ||
Syntax | cfuc 17204 | Extend class notation to include the functor category. |
class FuncCat | ||
Definition | df-nat 17205* | 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 17206* | 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 17207 | The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ FuncCat Fn (Cat × Cat) | ||
Theorem | natfval 17208* | Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) ⇒ ⊢ 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ 𝐵 ((𝑟‘𝑥)𝐽(𝑠‘𝑥)) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉 · (𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉 · (𝑠‘𝑦))(𝑎‘𝑥))}) | ||
Theorem | isnat 17209* | Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) ⇒ ⊢ (𝜑 → (𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥))))) | ||
Theorem | isnat2 17210* | 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 17211 | The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) | ||
Theorem | natrcl 17212 | Reverse closure for a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ (𝐴 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) | ||
Theorem | nat1st2nd 17213 | Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (〈(1st ‘𝐹), (2nd ‘𝐹)〉𝑁〈(1st ‘𝐺), (2nd ‘𝐺)〉)) | ||
Theorem | natixp 17214* | 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 17215 | A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) ∈ ((𝐹‘𝑋)𝐽(𝐾‘𝑋))) | ||
Theorem | natfn 17216 | A natural transformation is a function on the objects of 𝐶. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → 𝐴 Fn 𝐵) | ||
Theorem | nati 17217 | Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝐴‘𝑌)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉 · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(〈(𝐹‘𝑋), (𝐾‘𝑋)〉 · (𝐾‘𝑌))(𝐴‘𝑋))) | ||
Theorem | wunnat 17218 | A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐶 Nat 𝐷) ∈ 𝑈) | ||
Theorem | catstr 17219 | A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ {〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉} Struct 〈1, ;15〉 | ||
Theorem | fucval 17220* | 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 17221* | 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 17222 | 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 17223 | The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ 𝑁 = (Hom ‘𝑄) | ||
Theorem | fucco 17224* | Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) ⇒ ⊢ (𝜑 → (𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅) = (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st ‘𝐻)‘𝑥))(𝑅‘𝑥)))) | ||
Theorem | fuccoval 17225 | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅)‘𝑋) = ((𝑆‘𝑋)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)〉 · ((1st ‘𝐻)‘𝑋))(𝑅‘𝑋))) | ||
Theorem | fuccocl 17226 | 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 17227 | The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → ( 1 ∘ (1st ‘𝐹)) ∈ (𝐹𝑁𝐹)) | ||
Theorem | fuclid 17228 | Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → (( 1 ∘ (1st ‘𝐺))(〈𝐹, 𝐺〉 ∙ 𝐺)𝑅) = 𝑅) | ||
Theorem | fucrid 17229 | Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → (𝑅(〈𝐹, 𝐹〉 ∙ 𝐺)( 1 ∘ (1st ‘𝐹))) = 𝑅) | ||
Theorem | fucass 17230 | 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 17231* | 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 17232 | 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 17233 | The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝐼‘𝐹) = ( 1 ∘ (1st ‘𝐹))) | ||
Theorem | fucsect 17234* | 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 17235* | 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 17236* | 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 17237* | 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 17238 | 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 17239 | 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 17240 | Extend class notation with the class of initial objects of a category. |
class InitO | ||
Syntax | ctermo 17241 | Extend class notation with the class of terminal objects of a category. |
class TermO | ||
Syntax | czeroo 17242 | Extend class notation with the class of zero objects of a category. |
class ZeroO | ||
Definition | df-inito 17243* | 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 17244* | 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 17245 | 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 17246 | 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 17247 | 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 17248 | 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 17249* | 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 17250* | 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 17251 | 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 17252* | The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝐼𝐻𝑏))) | ||
Theorem | istermo 17253* | The predicate "is a terminal object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (TermO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝐼))) | ||
Theorem | iszeroo 17254 | The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (ZeroO‘𝐶) ↔ (𝐼 ∈ (InitO‘𝐶) ∧ 𝐼 ∈ (TermO‘𝐶)))) | ||
Theorem | isinitoi 17255* | Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑏))) | ||
Theorem | istermoi 17256* | Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑂))) | ||
Theorem | initoid 17257 | 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 17258 | 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 17259 | An initial object is an object. (Contributed by AV, 14-Apr-2020.) |
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ (Base‘𝐶))) | ||
Theorem | termoo 17260 | A terminal object is an object. (Contributed by AV, 18-Apr-2020.) |
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ (Base‘𝐶))) | ||
Theorem | iszeroi 17261 | Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (ZeroO‘𝐶)) → (𝑂 ∈ (Base‘𝐶) ∧ (𝑂 ∈ (InitO‘𝐶) ∧ 𝑂 ∈ (TermO‘𝐶)))) | ||
Theorem | 2initoinv 17262 | Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶)) ⇒ ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺) | ||
Theorem | initoeu1 17263* | 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 17264 | 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 17265 | Lemma 0 for initoeu2 17268. (Contributed by AV, 9-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ (((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) ∧ ((𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾)(〈𝐴, 𝐵〉 ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(〈𝐴, 𝐵〉 ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) → 𝐺 = (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾)) | ||
Theorem | initoeu2lem1 17266* | Lemma 1 for initoeu2 17268. (Contributed by AV, 9-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 = (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾))) | ||
Theorem | initoeu2lem2 17267* | Lemma 2 for initoeu2 17268. (Contributed by AV, 10-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → (∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) → ∃!𝑔 𝑔 ∈ (𝐵𝐻𝐷))) | ||
Theorem | initoeu2 17268 | 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 17269 | Morphisms between two terminal objects are inverses. (Contributed by AV, 18-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶)) ⇒ ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺) | ||
Theorem | termoeu1 17270* | 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 17271 | 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 17272 | Extend class notation to include the domain extractor for an arrow. |
class doma | ||
Syntax | ccoda 17273 | Extend class notation to include the codomain extractor for an arrow. |
class coda | ||
Syntax | carw 17274 | Extend class notation to include the collection of all arrows of a category. |
class Arrow | ||
Syntax | choma 17275 | Extend class notation to include the set of all arrows with a specific domain and codomain. |
class Homa | ||
Definition | df-doma 17276 | 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 17277 | 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 17278* | 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 17276 and df-coda 17277. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.) |
⊢ Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥)))) | ||
Definition | df-arw 17279 | 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 17280 | Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐶 ∈ Cat) | ||
Theorem | homafval 17281* | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐻 = (𝑥 ∈ (𝐵 × 𝐵) ↦ ({𝑥} × (𝐽‘𝑥)))) | ||
Theorem | homaf 17282 | Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐻:(𝐵 × 𝐵)⟶𝒫 ((𝐵 × 𝐵) × V)) | ||
Theorem | homaval 17283 | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = ({〈𝑋, 𝑌〉} × (𝑋𝐽𝑌))) | ||
Theorem | elhoma 17284 | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑍(𝑋𝐻𝑌)𝐹 ↔ (𝑍 = 〈𝑋, 𝑌〉 ∧ 𝐹 ∈ (𝑋𝐽𝑌)))) | ||
Theorem | elhomai 17285 | Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌)) ⇒ ⊢ (𝜑 → 〈𝑋, 𝑌〉(𝑋𝐻𝑌)𝐹) | ||
Theorem | elhomai2 17286 | Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌)) ⇒ ⊢ (𝜑 → 〈𝑋, 𝑌, 𝐹〉 ∈ (𝑋𝐻𝑌)) | ||
Theorem | homarcl2 17287 | Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
Theorem | homarel 17288 | An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ Rel (𝑋𝐻𝑌) | ||
Theorem | homa1 17289 | The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝑍(𝑋𝐻𝑌)𝐹 → 𝑍 = 〈𝑋, 𝑌〉) | ||
Theorem | homahom2 17290 | 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 17291 | 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 17292 | The domain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (doma‘𝐹) = 𝑋) | ||
Theorem | homacd 17293 | The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (coda‘𝐹) = 𝑌) | ||
Theorem | homadmcd 17294 | Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹 = 〈𝑋, 𝑌, (2nd ‘𝐹)〉) | ||
Theorem | arwval 17295 | 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 17296 | 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 17297 | 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 17298 | A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝑋𝐻𝑌) ⊆ 𝐴 | ||
Theorem | arwdm 17299 | The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → (doma‘𝐹) ∈ 𝐵) | ||
Theorem | arwcd 17300 | 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 > |