![]() |
Metamath
Proof Explorer Theorem List (p. 168 of 437) | < 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-28351) |
![]() (28352-29876) |
![]() (29877-43667) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isacs 16701* | A set is an algebraic closure system iff it is specified by some function of the finite subsets, such that a set is closed iff it does not expand under the operation. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))) | ||
Theorem | acsmre 16702 | Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) | ||
Theorem | isacs2 16703* | In the definition of an algebraic closure system, we may always take the operation being closed over as the Moore closure. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑠))) | ||
Theorem | acsfiel 16704* | A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (ACS‘𝑋) → (𝑆 ∈ 𝐶 ↔ (𝑆 ⊆ 𝑋 ∧ ∀𝑦 ∈ (𝒫 𝑆 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑆))) | ||
Theorem | acsfiel2 16705* | A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑆 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑆)) | ||
Theorem | acsmred 16706 | An algebraic closure system is also a Moore system. Deduction form of acsmre 16702. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) | ||
Theorem | isacs1i 16707* | A closure system determined by a function is a closure system and algebraic. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∈ (ACS‘𝑋)) | ||
Theorem | mreacs 16708 | Algebraicity is a composable property; combining several algebraic closure properties gives another. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)) | ||
Theorem | acsfn 16709* | Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋) ∧ (𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇 ⊆ 𝑎 → 𝐾 ∈ 𝑎)} ∈ (ACS‘𝑋)) | ||
Theorem | acsfn0 16710* | Algebraicity of a point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ 𝐾 ∈ 𝑎} ∈ (ACS‘𝑋)) | ||
Theorem | acsfn1 16711* | Algebraicity of a one-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) | ||
Theorem | acsfn1c 16712* | Algebraicity of a one-argument closure condition with additional constant. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝐾 ∀𝑐 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝐾 ∀𝑐 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) | ||
Theorem | acsfn2 16713* | Algebraicity of a two-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) | ||
Syntax | ccat 16714 | Extend class notation with the class of categories. |
class Cat | ||
Syntax | ccid 16715 | Extend class notation with the identity arrow of a category. |
class Id | ||
Syntax | chomf 16716 | Extend class notation to include functionalized Hom-set extractor. |
class Homf | ||
Syntax | ccomf 16717 | Extend class notation to include functionalized composition operation. |
class compf | ||
Definition | df-cat 16718* | A category is an abstraction of a structure (a group, a topology, an order...) Category theory consists in finding new formulation of the concepts associated with those structures (product, substructure...) using morphisms instead of the belonging relation. That trick has the interesting property that heterogeneous structures like topologies or groups for instance become comparable. Definition in [Lang] p. 53. In contrast to definition 3.1 of [Adamek] p. 21, where "A category is a quadruple A = (O, hom, id, o)", a category is defined as an extensible structure consisting of three slots: the objects "O" ((Base‘𝑐)), the morphisms "hom" ((Hom ‘𝑐)) and the composition law "o" ((comp‘𝑐)). The identities "id" are defined by their properties related to morphisms and their composition, see condition 3.1(b) in [Adamek] p. 21 and df-cid 16719. (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 2-Jan-2017.) |
⊢ Cat = {𝑐 ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓))))} | ||
Definition | df-cid 16719* | Define the category identity arrow. Since it is uniquely defined when it exists, we do not need to add it to the data of the category, and instead extract it by uniqueness. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ Id = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓)))) | ||
Definition | df-homf 16720* | Define the functionalized Hom-set operator, which is exactly like Hom but is guaranteed to be a function on the base. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ Homf = (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦))) | ||
Definition | df-comf 16721* | Define the functionalized composition operator, which is exactly like comp but is guaranteed to be a function of the proper type. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ compf = (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓)))) | ||
Theorem | iscat 16722* | The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))))) | ||
Theorem | iscatd 16723* | Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → · = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 1 ∈ (𝑥𝐻𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦𝐻𝑥))) → ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) & ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
Theorem | catidex 16724* | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓)) | ||
Theorem | catideu 16725* | Each object in a category has a unique identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃!𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓)) | ||
Theorem | cidfval 16726* | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 1 = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) | ||
Theorem | cidval 16727* | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) = (℩𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓))) | ||
Theorem | cidffn 16728 | The identity arrow construction is a function on categories. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ Id Fn Cat | ||
Theorem | cidfn 16729 | The identity arrow operator is a function from objects to arrows. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → 1 Fn 𝐵) | ||
Theorem | catidd 16730* | Deduce the identity arrow in a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → · = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 1 ∈ (𝑥𝐻𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦𝐻𝑥))) → ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓) ⇒ ⊢ (𝜑 → (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ 1 )) | ||
Theorem | iscatd2 16731* | Version of iscatd 16723 with a uniform assumption list, for increased proof sharing capabilities. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → · = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1 ∈ (𝑦𝐻𝑦)) & ⊢ ((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) & ⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) & ⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) & ⊢ ((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ⇒ ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 ))) | ||
Theorem | catidcl 16732 | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐻𝑋)) | ||
Theorem | catlid 16733 | Left identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (( 1 ‘𝑌)(〈𝑋, 𝑌〉 · 𝑌)𝐹) = 𝐹) | ||
Theorem | catrid 16734 | Right identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (𝐹(〈𝑋, 𝑋〉 · 𝑌)( 1 ‘𝑋)) = 𝐹) | ||
Theorem | catcocl 16735 | Closure of a composition arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)) | ||
Theorem | catass 16736 | Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑊)) ⇒ ⊢ (𝜑 → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹))) | ||
Theorem | 0catg 16737 | Any structure with an empty set of objects is a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ Cat) | ||
Theorem | 0cat 16738 | The empty set is a category, the empty category, see example 3.3(4.c) in [Adamek] p. 24. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ ∅ ∈ Cat | ||
Theorem | homffval 16739* | Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐹 = (Homf ‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥𝐻𝑦)) | ||
Theorem | fnhomeqhomf 16740 | If the Hom-set operation is a function it is equal to the corresponding functionalized Hom-set operation. (Contributed by AV, 1-Mar-2020.) |
⊢ 𝐹 = (Homf ‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐻 Fn (𝐵 × 𝐵) → 𝐹 = 𝐻) | ||
Theorem | homfval 16741 | Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐹 = (Homf ‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑋𝐻𝑌)) | ||
Theorem | homffn 16742 | The functionalized Hom-set operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐹 = (Homf ‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ 𝐹 Fn (𝐵 × 𝐵) | ||
Theorem | homfeq 16743* | Condition for two categories with the same base to have the same hom-sets. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐷)) ⇒ ⊢ (𝜑 → ((Homf ‘𝐶) = (Homf ‘𝐷) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) = (𝑥𝐽𝑦))) | ||
Theorem | homfeqd 16744 | If two structures have the same Hom slot, they have the same Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) & ⊢ (𝜑 → (Hom ‘𝐶) = (Hom ‘𝐷)) ⇒ ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) | ||
Theorem | homfeqbas 16745 | Deduce equality of base sets from equality of Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) ⇒ ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) | ||
Theorem | homfeqval 16746 | Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋𝐽𝑌)) | ||
Theorem | comfffval 16747* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) ⇒ ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) | ||
Theorem | comffval 16748* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉𝑂𝑍) = (𝑔 ∈ (𝑌𝐻𝑍), 𝑓 ∈ (𝑋𝐻𝑌) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑍)𝑓))) | ||
Theorem | comfval 16749 | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉𝑂𝑍)𝐹) = (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)) | ||
Theorem | comfffval2 16750* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ · = (comp‘𝐶) ⇒ ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) | ||
Theorem | comffval2 16751* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉𝑂𝑍) = (𝑔 ∈ (𝑌𝐻𝑍), 𝑓 ∈ (𝑋𝐻𝑌) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑍)𝑓))) | ||
Theorem | comfval2 16752 | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉𝑂𝑍)𝐹) = (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)) | ||
Theorem | comfffn 16753 | The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ 𝑂 Fn ((𝐵 × 𝐵) × 𝐵) | ||
Theorem | comffn 16754 | The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉𝑂𝑍) Fn ((𝑌𝐻𝑍) × (𝑋𝐻𝑌))) | ||
Theorem | comfeq 16755* | Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐷)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) ⇒ ⊢ (𝜑 → ((compf‘𝐶) = (compf‘𝐷) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) | ||
Theorem | comfeqd 16756 | Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → (comp‘𝐶) = (comp‘𝐷)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) ⇒ ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) | ||
Theorem | comfeqval 16757 | Equality of two compositions. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐷) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺(〈𝑋, 𝑌〉 ∙ 𝑍)𝐹)) | ||
Theorem | catpropd 16758 | Two structures with the same base, hom-sets and composition operation are either both categories or neither. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat)) | ||
Theorem | cidpropd 16759 | Two structures with the same base, hom-sets and composition operation have the same identity function. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (Id‘𝐶) = (Id‘𝐷)) | ||
Syntax | coppc 16760 | The opposite category operation. |
class oppCat | ||
Definition | df-oppc 16761* | Define an opposite category, which is the same as the original category but with the direction of arrows the other way around. Definition 3.5 of [Adamek] p. 25. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ oppCat = (𝑓 ∈ V ↦ ((𝑓 sSet 〈(Hom ‘ndx), tpos (Hom ‘𝑓)〉) sSet 〈(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (〈𝑧, (2nd ‘𝑢)〉(comp‘𝑓)(1st ‘𝑢)))〉)) | ||
Theorem | oppcval 16762* | Value of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝐶 ∈ 𝑉 → 𝑂 = ((𝐶 sSet 〈(Hom ‘ndx), tpos 𝐻〉) sSet 〈(comp‘ndx), (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st ‘𝑢)))〉)) | ||
Theorem | oppchomfval 16763 | Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ tpos 𝐻 = (Hom ‘𝑂) | ||
Theorem | oppchom 16764 | Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝑋(Hom ‘𝑂)𝑌) = (𝑌𝐻𝑋) | ||
Theorem | oppccofval 16765 | Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉(comp‘𝑂)𝑍) = tpos (〈𝑍, 𝑌〉 · 𝑋)) | ||
Theorem | oppcco 16766 | Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑍)𝐹) = (𝐹(〈𝑍, 𝑌〉 · 𝑋)𝐺)) | ||
Theorem | oppcbas 16767 | Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ 𝐵 = (Base‘𝑂) | ||
Theorem | oppccatid 16768 | Lemma for oppccat 16771. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧ (Id‘𝑂) = (Id‘𝐶))) | ||
Theorem | oppchomf 16769 | Hom-sets of the opposite category. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) ⇒ ⊢ tpos 𝐻 = (Homf ‘𝑂) | ||
Theorem | oppcid 16770 | Identity function of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐵 = (Id‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → (Id‘𝑂) = 𝐵) | ||
Theorem | oppccat 16771 | An opposite category is a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) | ||
Theorem | 2oppcbas 16772 | The double opposite category has the same objects as the original category. Intended for use with property lemmas such as monpropd 16786. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ 𝐵 = (Base‘(oppCat‘𝑂)) | ||
Theorem | 2oppchomf 16773 | The double opposite category has the same morphisms as the original category. Intended for use with property lemmas such as monpropd 16786. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (Homf ‘𝐶) = (Homf ‘(oppCat‘𝑂)) | ||
Theorem | 2oppccomf 16774 | The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd 16786. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (compf‘𝐶) = (compf‘(oppCat‘𝑂)) | ||
Theorem | oppchomfpropd 16775 | If two categories have the same hom-sets, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) ⇒ ⊢ (𝜑 → (Homf ‘(oppCat‘𝐶)) = (Homf ‘(oppCat‘𝐷))) | ||
Theorem | oppccomfpropd 16776 | If two categories have the same hom-sets and composition, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → (compf‘(oppCat‘𝐶)) = (compf‘(oppCat‘𝐷))) | ||
Syntax | cmon 16777 | Extend class notation with the class of all monomorphisms. |
class Mono | ||
Syntax | cepi 16778 | Extend class notation with the class of all epimorphisms. |
class Epi | ||
Definition | df-mon 16779* | Function returning the monomorphisms of the category 𝑐. JFM CAT1 def. 10. (Contributed by FL, 5-Dec-2007.) (Revised by Mario Carneiro, 2-Jan-2017.) |
⊢ Mono = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(〈𝑧, 𝑥〉(comp‘𝑐)𝑦)𝑔))})) | ||
Definition | df-epi 16780 | Function returning the epimorphisms of the category 𝑐. JFM CAT1 def. 11. (Contributed by FL, 8-Aug-2008.) (Revised by Mario Carneiro, 2-Jan-2017.) |
⊢ Epi = (𝑐 ∈ Cat ↦ tpos (Mono‘(oppCat‘𝑐))) | ||
Theorem | monfval 16781* | Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑀 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))})) | ||
Theorem | ismon 16782* | Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔))))) | ||
Theorem | ismon2 16783* | Write out the monomorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑧𝐻𝑋)∀ℎ ∈ (𝑧𝐻𝑋)((𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉 · 𝑌)ℎ) → 𝑔 = ℎ)))) | ||
Theorem | monhom 16784 | A monomorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝑀𝑌) ⊆ (𝑋𝐻𝑌)) | ||
Theorem | moni 16785 | Property of a monomorphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝑀𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋)) ⇒ ⊢ (𝜑 → ((𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐺) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐾) ↔ 𝐺 = 𝐾)) | ||
Theorem | monpropd 16786 | If two categories have the same set of objects, morphisms, and compositions, then they have the same monomorphisms. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐷 ∈ Cat) ⇒ ⊢ (𝜑 → (Mono‘𝐶) = (Mono‘𝐷)) | ||
Theorem | oppcmon 16787 | A monomorphism in the opposite category is an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝑀 = (Mono‘𝑂) & ⊢ 𝐸 = (Epi‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑌𝐸𝑋)) | ||
Theorem | oppcepi 16788 | An epimorphism in the opposite category is a monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐸 = (Epi‘𝑂) & ⊢ 𝑀 = (Mono‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑌𝑀𝑋)) | ||
Theorem | isepi 16789* | Definition of an epimorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹))))) | ||
Theorem | isepi2 16790* | Write out the epimorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑌𝐻𝑧)∀ℎ ∈ (𝑌𝐻𝑧)((𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉 · 𝑧)𝐹) → 𝑔 = ℎ)))) | ||
Theorem | epihom 16791 | An epimorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) ⊆ (𝑋𝐻𝑌)) | ||
Theorem | epii 16792 | Property of an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐸𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → 𝐾 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → ((𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐾(〈𝑋, 𝑌〉 · 𝑍)𝐹) ↔ 𝐺 = 𝐾)) | ||
Syntax | csect 16793 | Extend class notation with the sections of a morphism. |
class Sect | ||
Syntax | cinv 16794 | Extend class notation with the inverses of a morphism. |
class Inv | ||
Syntax | ciso 16795 | Extend class notation with the class of all isomorphisms. |
class Iso | ||
Definition | df-sect 16796* | Function returning the section relation in a category. Given arrows 𝑓:𝑋⟶𝑌 and 𝑔:𝑌⟶𝑋, we say 𝑓Sect𝑔, that is, 𝑓 is a section of 𝑔, if 𝑔 ∘ 𝑓 = 1‘𝑋. If there there is an arrow 𝑔 with 𝑓Sect𝑔, the arrow 𝑓 is called a section, see definition 7.19 of [Adamek] p. 106. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ Sect = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {〈𝑓, 𝑔〉 ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))})) | ||
Definition | df-inv 16797* | The inverse relation in a category. Given arrows 𝑓:𝑋⟶𝑌 and 𝑔:𝑌⟶𝑋, we say 𝑔Inv𝑓, that is, 𝑔 is an inverse of 𝑓, if 𝑔 is a section of 𝑓 and 𝑓 is a section of 𝑔. Definition 3.8 of [Adamek] p. 28. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 2-Jan-2017.) |
⊢ Inv = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ ((𝑥(Sect‘𝑐)𝑦) ∩ ◡(𝑦(Sect‘𝑐)𝑥)))) | ||
Definition | df-iso 16798* | Function returning the isomorphisms of the category 𝑐. Definition 3.8 of [Adamek] p. 28, and definition in [Lang] p. 54. (Contributed by FL, 9-Jun-2014.) (Revised by Mario Carneiro, 2-Jan-2017.) |
⊢ Iso = (𝑐 ∈ Cat ↦ ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐))) | ||
Theorem | sectffval 16799* | Value of the section operation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑥)) ∧ (𝑔(〈𝑥, 𝑦〉 · 𝑥)𝑓) = ( 1 ‘𝑥))})) | ||
Theorem | sectfval 16800* | Value of the section relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝑆𝑌) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(〈𝑋, 𝑌〉 · 𝑋)𝑓) = ( 1 ‘𝑋))}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |