Home | Metamath
Proof Explorer Theorem List (p. 167 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cnat 16601 | Extend class notation to include the collection of natural transformations. |
class Nat | ||
Syntax | cfuc 16602 | Extend class notation to include the functor category. |
class FuncCat | ||
Definition | df-nat 16603* | 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 16604* | 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 16605 | The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ FuncCat Fn (Cat × Cat) | ||
Theorem | natfval 16606* | 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 16607* | Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) ⇒ ⊢ (𝜑 → (𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)𝐽(𝐾‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀ℎ ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥))))) | ||
Theorem | isnat2 16608* | 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 16609 | The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) | ||
Theorem | natrcl 16610 | Reverse closure for a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ (𝐴 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) | ||
Theorem | nat1st2nd 16611 | Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (〈(1st ‘𝐹), (2nd ‘𝐹)〉𝑁〈(1st ‘𝐺), (2nd ‘𝐺)〉)) | ||
Theorem | natixp 16612* | 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 16613 | A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) ∈ ((𝐹‘𝑋)𝐽(𝐾‘𝑋))) | ||
Theorem | natfn 16614 | A natural transformation is a function on the objects of 𝐶. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → 𝐴 Fn 𝐵) | ||
Theorem | nati 16615 | Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝐴‘𝑌)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉 · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(〈(𝐹‘𝑋), (𝐾‘𝑋)〉 · (𝐾‘𝑌))(𝐴‘𝑋))) | ||
Theorem | wunnat 16616 | A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐶 Nat 𝐷) ∈ 𝑈) | ||
Theorem | catstr 16617 | A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ {〈(Base‘ndx), 𝑈〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉} Struct 〈1, ;15〉 | ||
Theorem | fucval 16618* | 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 16619* | 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 16620 | 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 16621 | The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ 𝑁 = (Hom ‘𝑄) | ||
Theorem | fucco 16622* | Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) ⇒ ⊢ (𝜑 → (𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅) = (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st ‘𝐻)‘𝑥))(𝑅‘𝑥)))) | ||
Theorem | fuccoval 16623 | Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅)‘𝑋) = ((𝑆‘𝑋)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)〉 · ((1st ‘𝐻)‘𝑋))(𝑅‘𝑋))) | ||
Theorem | fuccocl 16624 | 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 16625 | The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → ( 1 ∘ (1st ‘𝐹)) ∈ (𝐹𝑁𝐹)) | ||
Theorem | fuclid 16626 | Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → (( 1 ∘ (1st ‘𝐺))(〈𝐹, 𝐺〉 ∙ 𝐺)𝑅) = 𝑅) | ||
Theorem | fucrid 16627 | Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ ∙ = (comp‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) ⇒ ⊢ (𝜑 → (𝑅(〈𝐹, 𝐹〉 ∙ 𝐺)( 1 ∘ (1st ‘𝐹))) = 𝑅) | ||
Theorem | fucass 16628 | 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 16629* | 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 16630 | 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 16631 | The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ 𝐼 = (Id‘𝑄) & ⊢ 1 = (Id‘𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) ⇒ ⊢ (𝜑 → (𝐼‘𝐹) = ( 1 ∘ (1st ‘𝐹))) | ||
Theorem | fucsect 16632* | 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 16633* | 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 16634* | 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 16635* | 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 16636 | 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 16637 | 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 16638 | Extend class notation with the class of initial objects of a category. |
class InitO | ||
Syntax | ctermo 16639 | Extend class notation with the class of terminal objects of a category. |
class TermO | ||
Syntax | czeroo 16640 | Extend class notation with the class of zero objects of a category. |
class ZeroO | ||
Definition | df-inito 16641* | 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 16642* | 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 16643 | 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 16644 | 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 16645 | 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 16646 | 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 16647* | 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 16648* | 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 16649 | 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 16650* | The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (InitO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝐼𝐻𝑏))) | ||
Theorem | istermo 16651* | The predicate "is a terminal object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (TermO‘𝐶) ↔ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝐼))) | ||
Theorem | iszeroo 16652 | The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ∈ (ZeroO‘𝐶) ↔ (𝐼 ∈ (InitO‘𝐶) ∧ 𝐼 ∈ (TermO‘𝐶)))) | ||
Theorem | isinitoi 16653* | Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑏))) | ||
Theorem | istermoi 16654* | Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑏𝐻𝑂))) | ||
Theorem | initoid 16655 | 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 16656 | 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 16657 | An initial object is an object. (Contributed by AV, 14-Apr-2020.) |
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (InitO‘𝐶) → 𝑂 ∈ (Base‘𝐶))) | ||
Theorem | termoo 16658 | A terminal object is an object. (Contributed by AV, 18-Apr-2020.) |
⊢ (𝐶 ∈ Cat → (𝑂 ∈ (TermO‘𝐶) → 𝑂 ∈ (Base‘𝐶))) | ||
Theorem | iszeroi 16659 | Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (ZeroO‘𝐶)) → (𝑂 ∈ (Base‘𝐶) ∧ (𝑂 ∈ (InitO‘𝐶) ∧ 𝑂 ∈ (TermO‘𝐶)))) | ||
Theorem | 2initoinv 16660 | Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (InitO‘𝐶)) ⇒ ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺) | ||
Theorem | initoeu1 16661* | 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 16662 | 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 16663 | Lemma 0 for initoeu2 16666. (Contributed by AV, 9-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ (((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) ∧ ((𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾)(〈𝐴, 𝐵〉 ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(〈𝐴, 𝐵〉 ⚬ 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) → 𝐺 = (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾)) | ||
Theorem | initoeu2lem1 16664* | Lemma 1 for initoeu2 16666. (Contributed by AV, 9-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 = (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾))) | ||
Theorem | initoeu2lem2 16665* | Lemma 2 for initoeu2 16666. (Contributed by AV, 10-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (InitO‘𝐶)) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ ⚬ = (comp‘𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ (𝐹(〈𝐵, 𝐴〉 ⚬ 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → (∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) → ∃!𝑔 𝑔 ∈ (𝐵𝐻𝐷))) | ||
Theorem | initoeu2 16666 | 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 16667 | Morphisms between two terminal objects are inverses. (Contributed by AV, 18-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 ∈ (TermO‘𝐶)) & ⊢ (𝜑 → 𝐵 ∈ (TermO‘𝐶)) ⇒ ⊢ ((𝜑 ∧ 𝐺 ∈ (𝐵(Hom ‘𝐶)𝐴) ∧ 𝐹 ∈ (𝐴(Hom ‘𝐶)𝐵)) → 𝐹(𝐴(Inv‘𝐶)𝐵)𝐺) | ||
Theorem | termoeu1 16668* | 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 16669 | 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 16670 | Extend class notation to include the domain extractor for an arrow. |
class doma | ||
Syntax | ccoda 16671 | Extend class notation to include the codomain extractor for an arrow. |
class coda | ||
Syntax | carw 16672 | Extend class notation to include the collection of all arrows of a category. |
class Arrow | ||
Syntax | choma 16673 | Extend class notation to include the set of all arrows with a specific domain and codomain. |
class Homa | ||
Definition | df-doma 16674 | 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 16675 | 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 16676* | 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 16674 and df-coda 16675. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.) |
⊢ Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥)))) | ||
Definition | df-arw 16677 | 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 16678 | Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐶 ∈ Cat) | ||
Theorem | homafval 16679* | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐻 = (𝑥 ∈ (𝐵 × 𝐵) ↦ ({𝑥} × (𝐽‘𝑥)))) | ||
Theorem | homaf 16680 | Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐻:(𝐵 × 𝐵)⟶𝒫 ((𝐵 × 𝐵) × V)) | ||
Theorem | homaval 16681 | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = ({〈𝑋, 𝑌〉} × (𝑋𝐽𝑌))) | ||
Theorem | elhoma 16682 | Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑍(𝑋𝐻𝑌)𝐹 ↔ (𝑍 = 〈𝑋, 𝑌〉 ∧ 𝐹 ∈ (𝑋𝐽𝑌)))) | ||
Theorem | elhomai 16683 | Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌)) ⇒ ⊢ (𝜑 → 〈𝑋, 𝑌〉(𝑋𝐻𝑌)𝐹) | ||
Theorem | elhomai2 16684 | Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐽 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌)) ⇒ ⊢ (𝜑 → 〈𝑋, 𝑌, 𝐹〉 ∈ (𝑋𝐻𝑌)) | ||
Theorem | homarcl2 16685 | Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
Theorem | homarel 16686 | An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ Rel (𝑋𝐻𝑌) | ||
Theorem | homa1 16687 | The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝑍(𝑋𝐻𝑌)𝐹 → 𝑍 = 〈𝑋, 𝑌〉) | ||
Theorem | homahom2 16688 | 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 16689 | 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 16690 | The domain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (doma‘𝐹) = 𝑋) | ||
Theorem | homacd 16691 | The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (coda‘𝐹) = 𝑌) | ||
Theorem | homadmcd 16692 | Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹 = 〈𝑋, 𝑌, (2nd ‘𝐹)〉) | ||
Theorem | arwval 16693 | 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 16694 | 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 16695 | 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 16696 | A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐻 = (Homa‘𝐶) ⇒ ⊢ (𝑋𝐻𝑌) ⊆ 𝐴 | ||
Theorem | arwdm 16697 | The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → (doma‘𝐹) ∈ 𝐵) | ||
Theorem | arwcd 16698 | The codomain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝐹 ∈ 𝐴 → (coda‘𝐹) ∈ 𝐵) | ||
Theorem | dmaf 16699 | The domain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (doma ↾ 𝐴):𝐴⟶𝐵 | ||
Theorem | cdaf 16700 | The codomain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝐴 = (Arrow‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (coda ↾ 𝐴):𝐴⟶𝐵 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |