![]() |
Metamath
Proof Explorer Theorem List (p. 175 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 | funcsetcestrclem5 17401* | Lemma 5 for funcsetcestrc 17406. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌) = ( I ↾ (𝑌 ↑m 𝑋))) | ||
Theorem | funcsetcestrclem6 17402* | Lemma 6 for funcsetcestrc 17406. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝐻 ∈ (𝑌 ↑m 𝑋)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻) | ||
Theorem | funcsetcestrclem7 17403* | Lemma 7 for funcsetcestrc 17406. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑋𝐺𝑋)‘((Id‘𝑆)‘𝑋)) = ((Id‘𝐸)‘(𝐹‘𝑋))) | ||
Theorem | funcsetcestrclem8 17404* | Lemma 8 for funcsetcestrc 17406. (Contributed by AV, 28-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑆)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝐸)(𝐹‘𝑌))) | ||
Theorem | funcsetcestrclem9 17405* | Lemma 9 for funcsetcestrc 17406. (Contributed by AV, 28-Mar-2020.) |
⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶 ↦ {〈(Base‘ndx), 𝑥〉})) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐶 ↦ ( I ↾ (𝑦 ↑m 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑆)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑆)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝑆)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝐸)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻))) | ||
Theorem | funcsetcestrc 17406* | 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 ↾ (𝑦 ↑m 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ (𝜑 → 𝐹(𝑆 Func 𝐸)𝐺) | ||
Theorem | fthsetcestrc 17407* | 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 ↾ (𝑦 ↑m 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ (𝜑 → 𝐹(𝑆 Faith 𝐸)𝐺) | ||
Theorem | fullsetcestrc 17408* | 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 ↾ (𝑦 ↑m 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) ⇒ ⊢ (𝜑 → 𝐹(𝑆 Full 𝐸)𝐺) | ||
Theorem | embedsetcestrc 17409* | 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 ↾ (𝑦 ↑m 𝑥)))) & ⊢ 𝐸 = (ExtStrCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐸) ⇒ ⊢ (𝜑 → (𝐹(𝑆 Faith 𝐸)𝐺 ∧ 𝐹:𝐶–1-1→𝐵)) | ||
Syntax | cxpc 17410 | Extend class notation with the product of two categories. |
class ×c | ||
Syntax | c1stf 17411 | Extend class notation with the first projection functor. |
class 1stF | ||
Syntax | c2ndf 17412 | Extend class notation with the second projection functor. |
class 2ndF | ||
Syntax | cprf 17413 | Extend class notation with the functor pairing operation. |
class 〈,〉F | ||
Definition | df-xpc 17414* | 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 17415* | 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 17416* | 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 17417* | 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 17418 | The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ ×c Fn (V × V) | ||
Theorem | xpcval 17419* | 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 17420 | Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝑋 = (Base‘𝐶) & ⊢ 𝑌 = (Base‘𝐷) ⇒ ⊢ (𝑋 × 𝑌) = (Base‘𝑇) | ||
Theorem | xpchomfval 17421* | Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ 𝐾 = (Hom ‘𝑇) ⇒ ⊢ 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))) | ||
Theorem | xpchom 17422 | 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 17423 | A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐾 = (Hom ‘𝑇) ⇒ ⊢ Rel (𝑋𝐾𝑌) | ||
Theorem | xpccofval 17424* | Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.) (Proof shortened by AV, 2-Mar-2024.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐾 = (Hom ‘𝑇) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐷) & ⊢ 𝑂 = (comp‘𝑇) ⇒ ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))〉 · (1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))〉 ∙ (2nd ‘𝑦))(2nd ‘𝑓))〉)) | ||
Theorem | xpcco 17425 | 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 17426 | 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 17427 | 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 17428 | 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 17429 | 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 17430* | 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 17431 | 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 17432 | The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑇 ∈ Cat) | ||
Theorem | 1stfval 17433* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑃 = (𝐶 1stF 𝐷) ⇒ ⊢ (𝜑 → 𝑃 = 〈(1st ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (1st ↾ (𝑥𝐻𝑦)))〉) | ||
Theorem | 1stf1 17434 | 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 17435 | 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 17436* | Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ 𝑇 = (𝐶 ×c 𝐷) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ 𝐻 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝑄 = (𝐶 2ndF 𝐷) ⇒ ⊢ (𝜑 → 𝑄 = 〈(2nd ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (2nd ↾ (𝑥𝐻𝑦)))〉) | ||
Theorem | 2ndf1 17437 | 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 17438 | 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 17439 | 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 17440 | 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 17441* | Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → 𝑃 = 〈(𝑥 ∈ 𝐵 ↦ 〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (ℎ ∈ (𝑥𝐻𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉) | ||
Theorem | prf1 17442 | Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((1st ‘𝑃)‘𝑋) = 〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐺)‘𝑋)〉) | ||
Theorem | prf2fval 17443* | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋(2nd ‘𝑃)𝑌) = (ℎ ∈ (𝑋𝐻𝑌) ↦ 〈((𝑋(2nd ‘𝐹)𝑌)‘ℎ), ((𝑋(2nd ‘𝐺)𝑌)‘ℎ)〉)) | ||
Theorem | prf2 17444 | Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝑃)𝑌)‘𝐾) = 〈((𝑋(2nd ‘𝐹)𝑌)‘𝐾), ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)〉) | ||
Theorem | prfcl 17445 | The pairing of functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐷 is a functor 〈𝐹, 𝐺〉:𝐶⟶(𝐷 × 𝐸). (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ 𝑇 = (𝐷 ×c 𝐸) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇)) | ||
Theorem | prf1st 17446 | Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → ((𝐷 1stF 𝐸) ∘func 𝑃) = 𝐹) | ||
Theorem | prf2nd 17447 | Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) ⇒ ⊢ (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = 𝐺) | ||
Theorem | 1st2ndprf 17448 | 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 17449 | 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 17450 | 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 17451 | Extend class notation with the evaluation functor. |
class evalF | ||
Syntax | ccurf 17452 | Extend class notation with the currying of a functor. |
class curryF | ||
Syntax | cuncf 17453 | Extend class notation with the uncurrying of a functor. |
class uncurryF | ||
Syntax | cdiag 17454 | Extend class notation to include the diagonal functor. |
class Δfunc | ||
Definition | df-evlf 17455* | 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 17456* | 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 17457* | 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 17458* | 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 17459* | 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 17460* | 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 17461 | 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 17462 | Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = (𝐶 evalF 𝐷) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹(1st ‘𝐸)𝑋) = ((1st ‘𝐹)‘𝑋)) | ||
Theorem | evlfcllem 17463 | Lemma for evlfcl 17464. (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 17464 | 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 17465* | 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 17466* | 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 17467* | 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 17468 | 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 17469 | 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 17470 | 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 17471* | 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 17472 | 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 17473 | 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 17474 | 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 17475 | 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 17476 | 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 17477 | 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 17478 | 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 17479 | 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 17480 | Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐸 ∈ Cat) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) ⇒ ⊢ (𝜑 → (〈𝐶, 𝐷〉 curryF 𝐹) = 𝐺) | ||
Theorem | uncfcurf 17481 | Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) ⇒ ⊢ (𝜑 → (〈“𝐶𝐷𝐸”〉 uncurryF 𝐺) = 𝐹) | ||
Theorem | diagval 17482 | 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 17483 | 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 17484 | 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 17485 | 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 17486 | 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 17487 | Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ 𝐿 = (𝐶Δfunc𝐷) & ⊢ 𝐴 = (Base‘𝐶) & ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → ((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = (𝐵 × {𝐹})) | ||
Theorem | diag2cl 17488 | 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 17489 | As shown in diagval 17482, 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 17490 | Extend class notation with the Hom functor. |
class HomF | ||
Syntax | cyon 17491 | Extend class notation with the Yoneda embedding. |
class Yon | ||
Definition | df-hof 17492* | 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 17493 | 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 17494* | 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 17495 | 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 17496 | 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 17497* | 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 17498* | 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 17499 | 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 17500 | Lemma for hofcl 17501. (Contributed by Mario Carneiro, 15-Jan-2017.) |
⊢ 𝑀 = (HomF‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐷 = (SetCat‘𝑈) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑊)) & ⊢ (𝜑 → 𝑃 ∈ (𝑆𝐻𝑍)) & ⊢ (𝜑 → 𝑄 ∈ (𝑊𝐻𝑇)) ⇒ ⊢ (𝜑 → ((𝐾(〈𝑆, 𝑍〉(comp‘𝐶)𝑋)𝑃)(〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑆, 𝑇〉)(𝑄(〈𝑌, 𝑊〉(comp‘𝐶)𝑇)𝐿)) = ((𝑃(〈𝑍, 𝑊〉(2nd ‘𝑀)〈𝑆, 𝑇〉)𝑄)(〈(𝑋𝐻𝑌), (𝑍𝐻𝑊)〉(comp‘𝐷)(𝑆𝐻𝑇))(𝐾(〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑍, 𝑊〉)𝐿))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |