Home | Metamath
Proof Explorer Theorem List (p. 169 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 | ||
Theorem | funcsetcestrclem7 16801* | Lemma 7 for funcsetcestrc 16804. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑋𝐺𝑋)‘((Id‘𝑆)‘𝑋)) = ((Id‘𝐸)‘(𝐹‘𝑋))) | ||
Theorem | funcsetcestrclem8 16802* | Lemma 8 for funcsetcestrc 16804. (Contributed by AV, 28-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑆)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝐸)(𝐹‘𝑌))) | ||
Theorem | funcsetcestrclem9 16803* | Lemma 9 for funcsetcestrc 16804. (Contributed by AV, 28-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑆)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑆)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝑆)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻))) | ||
Theorem | funcsetcestrc 16804* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 28-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ (𝜑 → 𝐹(𝑆 Func 𝐸)𝐺) | ||
Theorem | fthsetcestrc 16805* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is faithful. (Contributed by AV, 31-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ (𝜑 → 𝐹(𝑆 Faith 𝐸)𝐺) | ||
Theorem | fullsetcestrc 16806* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is full. (Contributed by AV, 1-Apr-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ (𝜑 → 𝐹(𝑆 Full 𝐸)𝐺) | ||
Theorem | embedsetcestrc 16807* | The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is an embedding. According to definition 3.27 (1) of [Adamek] p. 34, a functor "F is called an embedding provided that F is injective on morphisms", or according to remark 3.28 (1) in [Adamek] p. 34, "a functor is an embedding if and only if it is faithful and injective on objects". (Contributed by AV, 31-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑𝑚 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) ⇒ ⊢ (𝜑 → (𝐹(𝑆 Faith 𝐸)𝐺 ∧ 𝐹:𝐶–1-1→𝐵)) | ||
Syntax | cxpc 16808 | Extend class notation with the product of two categories. |
class ×c | ||
Syntax | c1stf 16809 | Extend class notation with the first projection functor. |
class 1stF | ||
Syntax | c2ndf 16810 | Extend class notation with the second projection functor. |
class 2ndF | ||
Syntax | cprf 16811 | Extend class notation with the functor pairing operation. |
class 〈,〉F | ||
Definition | df-xpc 16812* | Define the binary product of categories, which has objects for each pair of objects of the factors, and morphisms for each pair of morphisms of the factors. Composition is componentwise. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ ×c = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) / ℎ⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx), ℎ〉, 〈(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉}) | ||
Definition | df-1stf 16813* | Define the first projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 1stF = (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌〈(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))〉) | ||
Definition | df-2ndf 16814* | Define the second projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 2ndF = (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌〈(2nd ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))〉) | ||
Definition | df-prf 16815* | Define the pairing operation for functors (which takes two functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐸 and produces (𝐹 〈,〉F 𝐺):𝐶⟶(𝐷 ×c 𝐸)). (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 〈,〉F = (𝑓 ∈ V, 𝑔 ∈ V ↦ ⦋dom (1st ‘𝑓) / 𝑏⦌〈(𝑥 ∈ 𝑏 ↦ 〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (ℎ ∈ dom (𝑥(2nd ‘𝑓)𝑦) ↦ 〈((𝑥(2nd ‘𝑓)𝑦)‘ℎ), ((𝑥(2nd ‘𝑔)𝑦)‘ℎ)〉))〉) | ||
Theorem | fnxpc 16816 | The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ ×c Fn (V × V) | ||
Theorem | xpcval 16817* | Value of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝑌 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐵 = (𝑋 × 𝑌)) & ⊢ (𝜑 → 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))) & ⊢ (𝜑 → 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))〉 · (1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))〉 ∙ (2nd ‘𝑦))(2nd ‘𝑓))〉))) ⇒ ⊢ (𝜑 → 𝑇 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐾〉, 〈(comp‘ndx), 𝑂〉}) | ||
Theorem | xpcbas 16818 | Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝑌 = (Base‘𝐷) ⇒ ⊢ (𝑋 × 𝑌) = (Base‘𝑇) | ||
Theorem | xpchomfval 16819* | Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐾 = (Hom ‘𝑇) ⇒ ⊢ 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))) | ||
Theorem | xpchom 16820 | Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐾 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐾𝑌) = (((1st ‘𝑋)𝐻(1st ‘𝑌)) × ((2nd ‘𝑋)𝐽(2nd ‘𝑌)))) | ||
Theorem | relxpchom 16821 | A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐾 = (Hom ‘𝑇) ⇒ ⊢ Rel (𝑋𝐾𝑌) | ||
Theorem | xpccofval 16822* | Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐾 = (Hom ‘𝑇) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐷) & ⊢ 𝑂 = (comp‘𝑇) ⇒ ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))〉 · (1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))〉 ∙ (2nd ‘𝑦))(2nd ‘𝑓))〉)) | ||
Theorem | xpcco 16823 | Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐾 = (Hom ‘𝑇) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐷) & ⊢ 𝑂 = (comp‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐾𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐾𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉𝑂𝑍)𝐹) = 〈((1st ‘𝐺)(〈(1st ‘𝑋), (1st ‘𝑌)〉 · (1st ‘𝑍))(1st ‘𝐹)), ((2nd ‘𝐺)(〈(2nd ‘𝑋), (2nd ‘𝑌)〉 ∙ (2nd ‘𝑍))(2nd ‘𝐹))〉) | ||
Theorem | xpcco1st 16824 | Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐾 = (Hom ‘𝑇) & ⊢ 𝑂 = (comp‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐾𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐾𝑍)) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → (1st ‘(𝐺(〈𝑋, 𝑌〉𝑂𝑍)𝐹)) = ((1st ‘𝐺)(〈(1st ‘𝑋), (1st ‘𝑌)〉 · (1st ‘𝑍))(1st ‘𝐹))) | ||
Theorem | xpcco2nd 16825 | Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐾 = (Hom ‘𝑇) & ⊢ 𝑂 = (comp‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐾𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐾𝑍)) & ⊢ · = (comp‘𝐷) ⇒ ⊢ (𝜑 → (2nd ‘(𝐺(〈𝑋, 𝑌〉𝑂𝑍)𝐹)) = ((2nd ‘𝐺)(〈(2nd ‘𝑋), (2nd ‘𝑌)〉 · (2nd ‘𝑍))(2nd ‘𝐹))) | ||
Theorem | xpchom2 16826 | Value of the set of morphisms in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝑌 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑌) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝑄 ∈ 𝑌) & ⊢ 𝐾 = (Hom ‘𝑇) ⇒ ⊢ (𝜑 → (〈𝑀, 𝑁〉𝐾〈𝑃, 𝑄〉) = ((𝑀𝐻𝑃) × (𝑁𝐽𝑄))) | ||
Theorem | xpcco2 16827 | Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝑌 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑌) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝑄 ∈ 𝑌) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐷) & ⊢ 𝑂 = (comp‘𝑇) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌) & ⊢ (𝜑 → 𝐹 ∈ (𝑀𝐻𝑃)) & ⊢ (𝜑 → 𝐺 ∈ (𝑁𝐽𝑄)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃𝐻𝑅)) & ⊢ (𝜑 → 𝐿 ∈ (𝑄𝐽𝑆)) ⇒ ⊢ (𝜑 → (〈𝐾, 𝐿〉(〈〈𝑀, 𝑁〉, 〈𝑃, 𝑄〉〉𝑂〈𝑅, 𝑆〉)〈𝐹, 𝐺〉) = 〈(𝐾(〈𝑀, 𝑃〉 · 𝑅)𝐹), (𝐿(〈𝑁, 𝑄〉 ∙ 𝑆)𝐺)〉) | ||
Theorem | xpccatid 16828* | The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝑌 = (Base‘𝐷) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ 𝐽 = (Id‘𝐷) ⇒ ⊢ (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐼‘𝑥), (𝐽‘𝑦)〉))) | ||
Theorem | xpcid 16829 | The identity morphism in the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝑌 = (Base‘𝐷) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ 𝐽 = (Id‘𝐷) & ⊢ 1 = (Id‘𝑇) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌) ⇒ ⊢ (𝜑 → ( 1 ‘〈𝑅, 𝑆〉) = 〈(𝐼‘𝑅), (𝐽‘𝑆)〉) | ||
Theorem | xpccat 16830 | The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑇 ∈ Cat) | ||
Theorem | 1stfval 16831* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑃 = (𝐶 1stF 𝐷) ⇒ ⊢ (𝜑 → 𝑃 = 〈(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) | ||
Theorem | 1stf1 16832 | Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑃 = (𝐶 1stF 𝐷) & ⊢ (𝜑 → 𝑅 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝑃)‘𝑅) = (1st ‘𝑅)) | ||
Theorem | 1stf2 16833 | Value of the first projection on a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑃 = (𝐶 1stF 𝐷) & ⊢ (𝜑 → 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑅(2nd ‘𝑃)𝑆) = (1st ↾ (𝑅𝐻𝑆))) | ||
Theorem | 2ndfval 16834* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑄 = (𝐶 2ndF 𝐷) ⇒ ⊢ (𝜑 → 𝑄 = 〈(2nd ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (2nd ↾ (𝑥𝐻𝑦)))〉) | ||
Theorem | 2ndf1 16835 | Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑄 = (𝐶 2ndF 𝐷) & ⊢ (𝜑 → 𝑅 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝑄)‘𝑅) = (2nd ‘𝑅)) | ||
Theorem | 2ndf2 16836 | Value of the first projection on a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑄 = (𝐶 2ndF 𝐷) & ⊢ (𝜑 → 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑅(2nd ‘𝑄)𝑆) = (2nd ↾ (𝑅𝐻𝑆))) | ||
Theorem | 1stfcl 16837 | The first projection functor is a functor onto the left argument. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑃 = (𝐶 1stF 𝐷) ⇒ ⊢ (𝜑 → 𝑃 ∈ (𝑇 Func 𝐶)) | ||
Theorem | 2ndfcl 16838 | The second projection functor is a functor onto the right argument. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑄 = (𝐶 2ndF 𝐷) ⇒ ⊢ (𝜑 → 𝑄 ∈ (𝑇 Func 𝐷)) | ||
Theorem | prfval 16839* | Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → 𝑃 = 〈(𝑥 ∈ 𝐵 ↦ 〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (ℎ ∈ (𝑥𝐻𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉) | ||
Theorem | prf1 16840 | Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝑃)‘𝑋) = 〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)〉) | ||
Theorem | prf2fval 16841* | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘𝑃)𝑌) = (ℎ ∈ (𝑋𝐻𝑌) ↦ 〈((𝑋(2nd ‘𝐹)𝑌)‘ℎ), ((𝑋(2nd ‘𝐺)𝑌)‘ℎ)〉)) | ||
Theorem | prf2 16842 | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝑃)𝑌)‘𝐾) = 〈((𝑋(2nd ‘𝐹)𝑌)‘𝐾), ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)〉) | ||
Theorem | prfcl 16843 | The pairing of functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐷 is a functor 〈𝐹, 𝐺〉:𝐶⟶(𝐷 × 𝐸). (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝑇 = (𝐷 ×c 𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇)) | ||
Theorem | prf1st 16844 | Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → ((𝐷 1stF 𝐸) ∘func 𝑃) = 𝐹) | ||
Theorem | prf2nd 16845 | Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = 𝐺) | ||
Theorem | 1st2ndprf 16846 | Break a functor into a product category into first and second projections. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑇 = (𝐷 ×c 𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝑇)) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐹 = (((𝐷 1stF 𝐸) ∘func 𝐹) 〈,〉F ((𝐷 2ndF 𝐸) ∘func 𝐹))) | ||
Theorem | catcxpccl 16847 | The category of categories for a weak universe is closed under the product category operation. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐶 = (CatCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑇 = (𝑋 ×c 𝑌) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑇 ∈ 𝐵) | ||
Theorem | xpcpropd 16848 | If two categories have the same set of objects, morphisms, and compositions, then they have the same product category. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 ×c 𝐶) = (𝐵 ×c 𝐷)) | ||
Syntax | cevlf 16849 | Extend class notation with the evaluation functor. |
class evalF | ||
Syntax | ccurf 16850 | Extend class notation with the currying of a functor. |
class curryF | ||
Syntax | cuncf 16851 | Extend class notation with the uncurrying of a functor. |
class uncurryF | ||
Syntax | cdiag 16852 | Extend class notation to include the diagonal functor. |
class Δfunc | ||
Definition | df-evlf 16853* | Define the evaluation functor, which is the extension of the evaluation map 𝑓, 𝑥 ↦ (𝑓‘𝑥) of functors, to a functor (𝐶⟶𝐷) × 𝐶⟶𝐷. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ evalF = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ 〈(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝑑)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉) | ||
Definition | df-curf 16854* | Define the curry functor, which maps a functor 𝐹:𝐶 × 𝐷⟶𝐸 to curryF (𝐹):𝐶⟶(𝐷⟶𝐸). (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ curryF = (𝑒 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑒) / 𝑐⦌⦋(2nd ‘𝑒) / 𝑑⦌〈(𝑥 ∈ (Base‘𝑐) ↦ 〈(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝑓)〈𝑦, 𝑧〉)((Id‘𝑑)‘𝑧)))))〉) | ||
Definition | df-uncf 16855* | Define the uncurry functor, which can be defined equationally using evalF. Strictly speaking, the third category argument is not needed, since the resulting functor is extensionally equal regardless, but it is used in the equational definition and is too much work to remove. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ uncurryF = (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓 ∘func ((𝑐‘0) 1stF (𝑐‘1))) 〈,〉F ((𝑐‘0) 2ndF (𝑐‘1))))) | ||
Definition | df-diag 16856* | Define the diagonal functor, which is the functor 𝐶⟶(𝐷 Func 𝐶) whose object part is 𝑥 ∈ 𝐶 ↦ (𝑦 ∈ 𝐷 ↦ 𝑥). The value of the functor at an object 𝑥 is the constant functor which maps all objects in 𝐷 to 𝑥 and all morphisms to 1(𝑥). The morphism part is a natural transformation between these functors, which takes 𝑓:𝑥⟶𝑦 to the natural transformation with every component equal to 𝑓. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ Δfunc = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ (〈𝑐, 𝑑〉 curryF (𝑐 1stF 𝑑))) | ||
Theorem | evlfval 16857* | Value of the evaluation functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) ⇒ ⊢ (𝜑 → 𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))〉 · ((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉) | ||
Theorem | evlf2 16858* | Value of the evaluation functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐿 = (〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐺, 𝑌〉) ⇒ ⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) | ||
Theorem | evlf2val 16859 | Value of the evaluation natural transformation at an object. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐷) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐿 = (〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐺, 𝑌〉) & ⊢ (𝜑 → 𝐴 ∈ (𝐹𝑁𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (𝐴𝐿𝐾) = ((𝐴‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st ‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝐾))) | ||
Theorem | evlf1 16860 | Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹(1st ‘𝐸)𝑋) = ((1st ‘𝐹)‘𝑋)) | ||
Theorem | evlfcllem 16861 | Lemma for evlfcl 16862. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ (Base‘𝐶))) & ⊢ (𝜑 → (𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ (Base‘𝐶))) & ⊢ (𝜑 → (𝐻 ∈ (𝐶 Func 𝐷) ∧ 𝑍 ∈ (Base‘𝐶))) & ⊢ (𝜑 → (𝐴 ∈ (𝐹𝑁𝐺) ∧ 𝐾 ∈ (𝑋(Hom ‘𝐶)𝑌))) & ⊢ (𝜑 → (𝐵 ∈ (𝐺𝑁𝐻) ∧ 𝐿 ∈ (𝑌(Hom ‘𝐶)𝑍))) ⇒ ⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐻, 𝑍〉)‘(〈𝐵, 𝐿〉(〈〈𝐹, 𝑋〉, 〈𝐺, 𝑌〉〉(comp‘(𝑄 ×c 𝐶))〈𝐻, 𝑍〉)〈𝐴, 𝐾〉)) = (((〈𝐺, 𝑌〉(2nd ‘𝐸)〈𝐻, 𝑍〉)‘〈𝐵, 𝐿〉)(〈((1st ‘𝐸)‘〈𝐹, 𝑋〉), ((1st ‘𝐸)‘〈𝐺, 𝑌〉)〉(comp‘𝐷)((1st ‘𝐸)‘〈𝐻, 𝑍〉))((〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐺, 𝑌〉)‘〈𝐴, 𝐾〉))) | ||
Theorem | evlfcl 16862 | The evaluation functor is a bifunctor (a two-argument functor) with the first parameter taking values in the set of functors 𝐶⟶𝐷, and the second parameter in 𝐷. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ 𝑄 = (𝐶 FuncCat 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝐶) Func 𝐷)) | ||
Theorem | curfval 16863* | Value of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) ⇒ ⊢ (𝜑 → 𝐺 = 〈(𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)(𝐼‘𝑧)))))〉) | ||
Theorem | curf1fval 16864* | Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → (1st ‘𝐺) = (𝑥 ∈ 𝐴 ↦ 〈(𝑦 ∈ 𝐵 ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉)) | ||
Theorem | curf1 16865* | Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 𝐾 = 〈(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))〉) | ||
Theorem | curf11 16866 | Value of the double evaluated curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝐾)‘𝑌) = (𝑋(1st ‘𝐹)𝑌)) | ||
Theorem | curf12 16867 | The partially evaluated curry functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐻 ∈ (𝑌𝐽𝑍)) ⇒ ⊢ (𝜑 → ((𝑌(2nd ‘𝐾)𝑍)‘𝐻) = (( 1 ‘𝑋)(〈𝑋, 𝑌〉(2nd ‘𝐹)〈𝑋, 𝑍〉)𝐻)) | ||
Theorem | curf1cl 16868 | The partially evaluated curry functor is a functor. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸)) | ||
Theorem | curf2 16869* | Value of the curry functor at a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) ⇒ ⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) | ||
Theorem | curf2val 16870 | Value of a component of the curry functor natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐿‘𝑍) = (𝐾(〈𝑋, 𝑍〉(2nd ‘𝐹)〈𝑌, 𝑍〉)(𝐼‘𝑍))) | ||
Theorem | curf2cl 16871 | The curry functor at a morphism is a natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Id‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾) & ⊢ 𝑁 = (𝐷 Nat 𝐸) ⇒ ⊢ (𝜑 → 𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌))) | ||
Theorem | curfcl 16872 | The curry functor of a functor 𝐹:𝐶 × 𝐷⟶𝐸 is a functor curryF (𝐹):𝐶⟶(𝐷⟶𝐸). (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ 𝑄 = (𝐷 FuncCat 𝐸) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝑄)) | ||
Theorem | curfpropd 16873 | If two categories have the same set of objects, morphisms, and compositions, then they curry the same functor to the same result. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵)) & ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐴 ∈ Cat) & ⊢ (𝜑 → 𝐵 ∈ Cat) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴 ×c 𝐶) Func 𝐸)) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐶〉 curryF 𝐹) = (〈𝐵, 𝐷〉 curryF 𝐹)) | ||
Theorem | uncfval 16874 | Value of the uncurry functor, which is the reverse of the curry functor, taking 𝐺:𝐶⟶(𝐷⟶𝐸) to uncurryF (𝐺):𝐶 × 𝐷⟶𝐸. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) ⇒ ⊢ (𝜑 → 𝐹 = ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func (𝐶 1stF 𝐷)) 〈,〉F (𝐶 2ndF 𝐷)))) | ||
Theorem | uncfcl 16875 | The uncurry operation takes a functor 𝐹:𝐶⟶(𝐷⟶𝐸) to a functor uncurryF (𝐹):𝐶 × 𝐷⟶𝐸. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) | ||
Theorem | uncf1 16876 | Value of the uncurry functor on an object. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(1st ‘𝐹)𝑌) = ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑌)) | ||
Theorem | uncf2 16877 | Value of the uncurry functor on a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑍)) & ⊢ (𝜑 → 𝑆 ∈ (𝑌𝐽𝑊)) ⇒ ⊢ (𝜑 → (𝑅(〈𝑋, 𝑌〉(2nd ‘𝐹)〈𝑍, 𝑊〉)𝑆) = ((((𝑋(2nd ‘𝐺)𝑍)‘𝑅)‘𝑊)(〈((1st ‘((1st ‘𝐺)‘𝑋))‘𝑌), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑊)〉(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑍))‘𝑊))((𝑌(2nd ‘((1st ‘𝐺)‘𝑋))𝑊)‘𝑆))) | ||
Theorem | curfuncf 16878 | Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) ⇒ ⊢ (𝜑 → (〈𝐶, 𝐷〉 curryF 𝐹) = 𝐺) | ||
Theorem | uncfcurf 16879 | Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) ⇒ ⊢ (𝜑 → (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) = 𝐹) | ||
Theorem | diagval 16880 | Define the diagonal functor, which is the functor 𝐶⟶(𝐷 Func 𝐶) whose object part is 𝑥 ∈ 𝐶 ↦ (𝑦 ∈ 𝐷 ↦ 𝑥). We can define this equationally as the currying of the first projection functor, and by expressing it this way we get a quick proof of functoriality. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐿 = (〈𝐶, 𝐷〉 curryF (𝐶 1stF 𝐷))) | ||
Theorem | diagcl 16881 | The diagonal functor is a functor from the base category to the functor category. Another way of saying this is that the constant functor (𝑦 ∈ 𝐷 ↦ 𝑋) is a construction that is natural in 𝑋 (and covariant). (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑄 = (𝐷 FuncCat 𝐶) ⇒ ⊢ (𝜑 → 𝐿 ∈ (𝐶 Func 𝑄)) | ||
Theorem | diag1cl 16882 | The constant functor of 𝑋 is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐶)) | ||
Theorem | diag11 16883 | Value of the constant functor at an object. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝐾)‘𝑌) = 𝑋) | ||
Theorem | diag12 16884 | Value of the constant functor at a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝐾 = ((1st ‘𝐿)‘𝑋) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑌𝐽𝑍)) ⇒ ⊢ (𝜑 → ((𝑌(2nd ‘𝐾)𝑍)‘𝐹) = ( 1 ‘𝑋)) | ||
Theorem | diag2 16885 | Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = (𝐵 × {𝐹})) | ||
Theorem | diag2cl 16886 | The diagonal functor at a morphism is a natural transformation between constant functors. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ 𝑁 = (𝐷 Nat 𝐶) ⇒ ⊢ (𝜑 → (𝐵 × {𝐹}) ∈ (((1st ‘𝐿)‘𝑋)𝑁((1st ‘𝐿)‘𝑌))) | ||
Theorem | curf2ndf 16887 | As shown in diagval 16880, the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is 𝑥 ∈ 𝐶 ↦ (𝑦 ∈ 𝐷 ↦ 𝑦), which is a constant functor of the identity functor at 𝐷. (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑄 = (𝐷 FuncCat 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (〈𝐶, 𝐷〉 curryF (𝐶 2ndF 𝐷)) = ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))) | ||
Syntax | chof 16888 | Extend class notation with the Hom functor. |
class HomF | ||
Syntax | cyon 16889 | Extend class notation with the Yoneda embedding. |
class Yon | ||
Definition | df-hof 16890* | Define the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat‘𝐶) × 𝐶 to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ HomF = (𝑐 ∈ Cat ↦ 〈(Homf ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝑐)(2nd ‘𝑦))𝑓))))〉) | ||
Definition | df-yon 16891 | Define the Yoneda embedding, which is the currying of the (opposite) Hom functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ Yon = (𝑐 ∈ Cat ↦ (〈𝑐, (oppCat‘𝑐)〉 curryF (HomF‘(oppCat‘𝑐)))) | ||
Theorem | hofval 16892* | Value of the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat‘𝐶) × 𝐶 to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → 𝑀 = 〈(Homf ‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉 · (2nd ‘𝑦))𝑓))))〉) | ||
Theorem | hof1fval 16893 | The object part of the Hom functor is the Homf operation, which is just a functionalized version of Hom. That is, it is a two argument function, which maps 𝑋, 𝑌 to the set of morphisms from 𝑋 to 𝑌. (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → (1st ‘𝑀) = (Homf ‘𝐶)) | ||
Theorem | hof1 16894 | The object part of the Hom functor maps 𝑋, 𝑌 to the set of morphisms from 𝑋 to 𝑌. (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(1st ‘𝑀)𝑌) = (𝑋𝐻𝑌)) | ||
Theorem | hof2fval 16895* | The morphism part of the Hom functor, for morphisms 〈𝑓, 𝑔〉:〈𝑋, 𝑌〉⟶〈𝑍, 𝑊〉 (which since the first argument is contravariant means morphisms 𝑓:𝑍⟶𝑋 and 𝑔:𝑌⟶𝑊), yields a function (a morphism of SetCat) mapping ℎ:𝑋⟶𝑌 to 𝑔 ∘ ℎ ∘ 𝑓:𝑍⟶𝑊. (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑍, 𝑊〉) = (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (𝑌𝐻𝑊) ↦ (ℎ ∈ (𝑋𝐻𝑌) ↦ ((𝑔(〈𝑋, 𝑌〉 · 𝑊)ℎ)(〈𝑍, 𝑋〉 · 𝑊)𝑓)))) | ||
Theorem | hof2val 16896* | The morphism part of the Hom functor, for morphisms 〈𝑓, 𝑔〉:〈𝑋, 𝑌〉⟶〈𝑍, 𝑊〉 (which since the first argument is contravariant means morphisms 𝑓:𝑍⟶𝑋 and 𝑔:𝑌⟶𝑊), yields a function (a morphism of SetCat) mapping ℎ:𝑋⟶𝑌 to 𝑔 ∘ ℎ ∘ 𝑓:𝑍⟶𝑊. (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑊)) ⇒ ⊢ (𝜑 → (𝐹(〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑍, 𝑊〉)𝐺) = (ℎ ∈ (𝑋𝐻𝑌) ↦ ((𝐺(〈𝑋, 𝑌〉 · 𝑊)ℎ)(〈𝑍, 𝑋〉 · 𝑊)𝐹))) | ||
Theorem | hof2 16897 | The morphism part of the Hom functor, for morphisms 〈𝑓, 𝑔〉:〈𝑋, 𝑌〉⟶〈𝑍, 𝑊〉 (which since the first argument is contravariant means morphisms 𝑓:𝑍⟶𝑋 and 𝑔:𝑌⟶𝑊), yields a function (a morphism of SetCat) mapping ℎ:𝑋⟶𝑌 to 𝑔 ∘ ℎ ∘ 𝑓:𝑍⟶𝑊. (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑀 = (HomF‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑊)) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝐹(〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑍, 𝑊〉)𝐺)‘𝐾) = ((𝐺(〈𝑋, 𝑌〉 · 𝑊)𝐾)(〈𝑍, 𝑋〉 · 𝑊)𝐹)) | ||
Theorem | hofcllem 16898 | Lemma for hofcl 16899. (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑀 = (HomF‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑊)) & ⊢ (𝜑 → 𝑃 ∈ (𝑆𝐻𝑍)) & ⊢ (𝜑 → 𝑄 ∈ (𝑊𝐻𝑇)) ⇒ ⊢ (𝜑 → ((𝐾(〈𝑆, 𝑍〉(comp‘𝐶)𝑋)𝑃)(〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑆, 𝑇〉)(𝑄(〈𝑌, 𝑊〉(comp‘𝐶)𝑇)𝐿)) = ((𝑃(〈𝑍, 𝑊〉(2nd ‘𝑀)〈𝑆, 𝑇〉)𝑄)(〈(𝑋𝐻𝑌), (𝑍𝐻𝑊)〉(comp‘𝐷)(𝑆𝐻𝑇))(𝐾(〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑍, 𝑊〉)𝐿))) | ||
Theorem | hofcl 16899 | Closure of the Hom functor. Note that the codomain is the category SetCat‘𝑈 for any universe 𝑈 which contains each Hom-set. This corresponds to the assertion that 𝐶 be locally small (with respect to 𝑈). (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑀 = (HomF‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑀 ∈ ((𝑂 ×c 𝐶) Func 𝐷)) | ||
Theorem | oppchofcl 16900 | Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝑀 = (HomF‘𝑂) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑀 ∈ ((𝐶 ×c 𝑂) Func 𝐷)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |