Home | Metamath
Proof Explorer Theorem List (p. 163 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | oppcbas 16201 | Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ 𝐵 = (Base‘𝑂) | ||
Theorem | oppccatid 16202 | Lemma for oppccat 16205. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧ (Id‘𝑂) = (Id‘𝐶))) | ||
Theorem | oppchomf 16203 | Hom-sets of the opposite category. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) ⇒ ⊢ tpos 𝐻 = (Homf ‘𝑂) | ||
Theorem | oppcid 16204 | Identity function of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐵 = (Id‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → (Id‘𝑂) = 𝐵) | ||
Theorem | oppccat 16205 | An opposite category is a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) | ||
Theorem | 2oppcbas 16206 | The double opposite category has the same objects as the original category. Intended for use with property lemmas such as monpropd 16220. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ 𝐵 = (Base‘(oppCat‘𝑂)) | ||
Theorem | 2oppchomf 16207 | The double opposite category has the same morphisms as the original category. Intended for use with property lemmas such as monpropd 16220. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (Homf ‘𝐶) = (Homf ‘(oppCat‘𝑂)) | ||
Theorem | 2oppccomf 16208 | The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd 16220. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (compf‘𝐶) = (compf‘(oppCat‘𝑂)) | ||
Theorem | oppchomfpropd 16209 | 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 16210 | 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 16211 | Extend class notation with the class of all monomorphisms. |
class Mono | ||
Syntax | cepi 16212 | Extend class notation with the class of all epimorphisms. |
class Epi | ||
Definition | df-mon 16213* | 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 16214 | 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 16215* | Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝑀 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(〈𝑧, 𝑥〉 · 𝑦)𝑔))})) | ||
Theorem | ismon 16216* | Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔))))) | ||
Theorem | ismon2 16217* | Write out the monomorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑧𝐻𝑋)∀ℎ ∈ (𝑧𝐻𝑋)((𝐹(〈𝑧, 𝑋〉 · 𝑌)𝑔) = (𝐹(〈𝑧, 𝑋〉 · 𝑌)ℎ) → 𝑔 = ℎ)))) | ||
Theorem | monhom 16218 | A monomorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝑀𝑌) ⊆ (𝑋𝐻𝑌)) | ||
Theorem | moni 16219 | Property of a monomorphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝑀𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑋)) ⇒ ⊢ (𝜑 → ((𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐺) = (𝐹(〈𝑍, 𝑋〉 · 𝑌)𝐾) ↔ 𝐺 = 𝐾)) | ||
Theorem | monpropd 16220 | 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 16221 | A monomorphism in the opposite category is an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝑀 = (Mono‘𝑂) & ⊢ 𝐸 = (Epi‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑀𝑌) = (𝑌𝐸𝑋)) | ||
Theorem | oppcepi 16222 | An epimorphism in the opposite category is a monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐸 = (Epi‘𝑂) & ⊢ 𝑀 = (Mono‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) = (𝑌𝑀𝑋)) | ||
Theorem | isepi 16223* | Definition of an epimorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑌𝐻𝑧) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹))))) | ||
Theorem | isepi2 16224* | Write out the epimorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑔 ∈ (𝑌𝐻𝑧)∀ℎ ∈ (𝑌𝐻𝑧)((𝑔(〈𝑋, 𝑌〉 · 𝑧)𝐹) = (ℎ(〈𝑋, 𝑌〉 · 𝑧)𝐹) → 𝑔 = ℎ)))) | ||
Theorem | epihom 16225 | An epimorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐸𝑌) ⊆ (𝑋𝐻𝑌)) | ||
Theorem | epii 16226 | Property of an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐸𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → 𝐾 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → ((𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐾(〈𝑋, 𝑌〉 · 𝑍)𝐹) ↔ 𝐺 = 𝐾)) | ||
Syntax | csect 16227 | Extend class notation with the sections of a morphism. |
class Sect | ||
Syntax | cinv 16228 | Extend class notation with the inverses of a morphism. |
class Inv | ||
Syntax | ciso 16229 | Extend class notation with the class of all isomorphisms. |
class Iso | ||
Definition | df-sect 16230* | 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 16231* | 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 16232* | 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 16233* | Value of the section operation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑥)) ∧ (𝑔(〈𝑥, 𝑦〉 · 𝑥)𝑓) = ( 1 ‘𝑥))})) | ||
Theorem | sectfval 16234* | Value of the section relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝑆𝑌) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑋𝐻𝑌) ∧ 𝑔 ∈ (𝑌𝐻𝑋)) ∧ (𝑔(〈𝑋, 𝑌〉 · 𝑋)𝑓) = ( 1 ‘𝑋))}) | ||
Theorem | sectss 16235 | The section relation is a relation between morphisms from 𝑋 to 𝑌 and morphisms from 𝑌 to 𝑋. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝑆𝑌) ⊆ ((𝑋𝐻𝑌) × (𝑌𝐻𝑋))) | ||
Theorem | issect 16236 | The property "𝐹 is a section of 𝐺". (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑋) ∧ (𝐺(〈𝑋, 𝑌〉 · 𝑋)𝐹) = ( 1 ‘𝑋)))) | ||
Theorem | issect2 16237 | Property of being a section. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑋)) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐺(〈𝑋, 𝑌〉 · 𝑋)𝐹) = ( 1 ‘𝑋))) | ||
Theorem | sectcan 16238 | If 𝐺 is a section of 𝐹 and 𝐹 is a section of 𝐻, then 𝐺 = 𝐻. Proposition 3.10 of [Adamek] p. 28. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐺(𝑋𝑆𝑌)𝐹) & ⊢ (𝜑 → 𝐹(𝑌𝑆𝑋)𝐻) ⇒ ⊢ (𝜑 → 𝐺 = 𝐻) | ||
Theorem | sectco 16239 | Composition of two sections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) & ⊢ (𝜑 → 𝐻(𝑌𝑆𝑍)𝐾) ⇒ ⊢ (𝜑 → (𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋𝑆𝑍)(𝐺(〈𝑍, 𝑌〉 · 𝑋)𝐾)) | ||
Theorem | isofval 16240* | Function value of the function returning the isomorphisms of a category. (Contributed by AV, 5-Apr-2017.) |
⊢ (𝐶 ∈ Cat → (Iso‘𝐶) = ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶))) | ||
Theorem | invffval 16241* | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝑆𝑦) ∩ ◡(𝑦𝑆𝑥)))) | ||
Theorem | invfval 16242 | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑁𝑌) = ((𝑋𝑆𝑌) ∩ ◡(𝑌𝑆𝑋))) | ||
Theorem | isinv 16243 | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹))) | ||
Theorem | invss 16244 | The inverse relation is a relation between morphisms 𝐹:𝑋⟶𝑌 and their inverses 𝐺:𝑌⟶𝑋. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑁𝑌) ⊆ ((𝑋𝐻𝑌) × (𝑌𝐻𝑋))) | ||
Theorem | invsym 16245 | The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ 𝐺(𝑌𝑁𝑋)𝐹)) | ||
Theorem | invsym2 16246 | The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ◡(𝑋𝑁𝑌) = (𝑌𝑁𝑋)) | ||
Theorem | invfun 16247 | The inverse relation is a function, which is to say that every morphism has at most one inverse. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → Fun (𝑋𝑁𝑌)) | ||
Theorem | isoval 16248 | The isomorphisms are the domain of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof shortened by AV, 21-May-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌)) | ||
Theorem | inviso1 16249 | If 𝐺 is an inverse to 𝐹, then 𝐹 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) | ||
Theorem | inviso2 16250 | If 𝐺 is an inverse to 𝐹, then 𝐺 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑋)) | ||
Theorem | invf 16251 | The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑁𝑌):(𝑋𝐼𝑌)⟶(𝑌𝐼𝑋)) | ||
Theorem | invf1o 16252 | The inverse relation is a bijection from isomorphisms to isomorphisms. This means that every isomorphism 𝐹 ∈ (𝑋𝐼𝑌) has a unique inverse, denoted by ((Inv‘𝐶)‘𝐹). Remark 3.12 of [Adamek] p. 28. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑁𝑌):(𝑋𝐼𝑌)–1-1-onto→(𝑌𝐼𝑋)) | ||
Theorem | invinv 16253 | The inverse of the inverse of an isomorphism is itself. Proposition 3.14(1) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → ((𝑌𝑁𝑋)‘((𝑋𝑁𝑌)‘𝐹)) = 𝐹) | ||
Theorem | invco 16254 | The composition of two isomorphisms is an isomorphism, and the inverse is the composition of the individual inverses. Proposition 3.14(2) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋𝑁𝑍)(((𝑋𝑁𝑌)‘𝐹)(〈𝑍, 𝑌〉 · 𝑋)((𝑌𝑁𝑍)‘𝐺))) | ||
Theorem | dfiso2 16255* | Alternate definition of an isomorphism of a category, according to definition 3.8 in [Adamek] p. 28. (Contributed by AV, 10-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ 1 = (Id‘𝐶) & ⊢ ⚬ = (〈𝑋, 𝑌〉(comp‘𝐶)𝑋) & ⊢ ∗ = (〈𝑌, 𝑋〉(comp‘𝐶)𝑌) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔 ⚬ 𝐹) = ( 1 ‘𝑋) ∧ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌)))) | ||
Theorem | dfiso3 16256* | Alternate definition of an isomorphism of a category as a section in both directions. (Contributed by AV, 11-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)(𝑔(𝑌𝑆𝑋)𝐹 ∧ 𝐹(𝑋𝑆𝑌)𝑔))) | ||
Theorem | inveq 16257 | If there are two inverses of an morphism, these inverses are equal. Corollary 3.11 of [Adamek] p. 28. (Contributed by AV, 10-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹(𝑋𝑁𝑌)𝐺 ∧ 𝐹(𝑋𝑁𝑌)𝐾) → 𝐺 = 𝐾)) | ||
Theorem | isofn 16258 | The function value of the function returning the isomorphisms of a category is a function over the square product of the base set of the category. (Contributed by AV, 5-Apr-2017.) |
⊢ (𝐶 ∈ Cat → (Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))) | ||
Theorem | isohom 16259 | An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋𝐻𝑌)) | ||
Theorem | isoco 16260 | The composition of two isomorphisms is an isomorphism. Proposition 3.14(2) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐼𝑍)) | ||
Theorem | oppcsect 16261 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝑂) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑇𝑌)𝐺 ↔ 𝐺(𝑋𝑆𝑌)𝐹)) | ||
Theorem | oppcsect2 16262 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝑂) ⇒ ⊢ (𝜑 → (𝑋𝑇𝑌) = ◡(𝑋𝑆𝑌)) | ||
Theorem | oppcinv 16263 | An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Inv‘𝐶) & ⊢ 𝐽 = (Inv‘𝑂) ⇒ ⊢ (𝜑 → (𝑋𝐽𝑌) = (𝑌𝐼𝑋)) | ||
Theorem | oppciso 16264 | An isomorphism in the opposite category. See also remark 3.9 in [Adamek] p. 28. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐽 = (Iso‘𝑂) ⇒ ⊢ (𝜑 → (𝑋𝐽𝑌) = (𝑌𝐼𝑋)) | ||
Theorem | sectmon 16265 | If 𝐹 is a section of 𝐺, then 𝐹 is a monomorphism. A monomorphism that arises from a section is also known as a split monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑋𝑀𝑌)) | ||
Theorem | monsect 16266 | If 𝐹 is a monomorphism and 𝐺 is a section of 𝐹, then 𝐺 is an inverse of 𝐹 and they are both isomorphisms. This is also stated as "a monomorphism which is also a split epimorphism is an isomorphism". (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑀 = (Mono‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝑀𝑌)) & ⊢ (𝜑 → 𝐺(𝑌𝑆𝑋)𝐹) ⇒ ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) | ||
Theorem | sectepi 16267 | If 𝐹 is a section of 𝐺, then 𝐺 is an epimorphism. An epimorphism that arises from a section is also known as a split epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐸𝑋)) | ||
Theorem | episect 16268 | If 𝐹 is an epimorphism and 𝐹 is a section of 𝐺, then 𝐺 is an inverse of 𝐹 and they are both isomorphisms. This is also stated as "an epimorphism which is also a split monomorphism is an isomorphism". (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐸 = (Epi‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐸𝑌)) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) | ||
Theorem | sectid 16269 | The identity is a section of itself. (Contributed by AV, 8-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Sect‘𝐶)𝑋)(𝐼‘𝑋)) | ||
Theorem | invid 16270 | The inverse of the identity is the identity. (Contributed by AV, 8-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Inv‘𝐶)𝑋)(𝐼‘𝑋)) | ||
Theorem | idiso 16271 | The identity is an isomorphism. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 8-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋(Iso‘𝐶)𝑋)) | ||
Theorem | idinv 16272 | The inverse of the identity is the identity. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 9-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋(Inv‘𝐶)𝑋)‘(𝐼‘𝑋)) = (𝐼‘𝑋)) | ||
Theorem | invisoinvl 16273 | The inverse of an isomorphism 𝐹 (which is unique because of invf 16251 and is therefore denoted by ((𝑋𝑁𝑌)‘𝐹), see also remark 3.12 in [Adamek] p. 28) is invers to the isomorphism. (Contributed by AV, 9-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → ((𝑋𝑁𝑌)‘𝐹)(𝑌𝑁𝑋)𝐹) | ||
Theorem | invisoinvr 16274 | The inverse of an isomorphism is invers to the isomorphism. (Contributed by AV, 9-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹)) | ||
Theorem | invcoisoid 16275 | The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 5-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ 1 = (Id‘𝐶) & ⊢ ⚬ = (〈𝑋, 𝑌〉(comp‘𝐶)𝑋) ⇒ ⊢ (𝜑 → (((𝑋𝑁𝑌)‘𝐹) ⚬ 𝐹) = ( 1 ‘𝑋)) | ||
Theorem | isocoinvid 16276 | The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 10-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ 1 = (Id‘𝐶) & ⊢ ⚬ = (〈𝑌, 𝑋〉(comp‘𝐶)𝑌) ⇒ ⊢ (𝜑 → (𝐹 ⚬ ((𝑋𝑁𝑌)‘𝐹)) = ( 1 ‘𝑌)) | ||
Theorem | rcaninv 16277 | Right cancellation of an inverse of an isomorphism. (Contributed by AV, 5-Apr-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑌(Iso‘𝐶)𝑋)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌(Hom ‘𝐶)𝑍)) & ⊢ (𝜑 → 𝐻 ∈ (𝑌(Hom ‘𝐶)𝑍)) & ⊢ 𝑅 = ((𝑌𝑁𝑋)‘𝐹) & ⊢ ⚬ = (〈𝑋, 𝑌〉(comp‘𝐶)𝑍) ⇒ ⊢ (𝜑 → ((𝐺 ⚬ 𝑅) = (𝐻 ⚬ 𝑅) → 𝐺 = 𝐻)) | ||
In this subsection, the "is isomorphic to" relation between objects of a category ≃𝑐 is defined (see df-cic 16279). It is shown that this relation is an equivalence relation, see cicer 16289. | ||
Syntax | ccic 16278 | Extend class notation to include the category isomorphism relation. |
class ≃𝑐 | ||
Definition | df-cic 16279 | Function returning the set of isomorphic objects for each category 𝑐. Definition 3.15 of [Adamek] p. 29. Analogous to the definition of the group isomorphism relation ≃𝑔, see df-gic 17525. (Contributed by AV, 4-Apr-2020.) |
⊢ ≃𝑐 = (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅)) | ||
Theorem | cicfval 16280 | The set of isomorphic objects of the category 𝑐. (Contributed by AV, 4-Apr-2020.) |
⊢ (𝐶 ∈ Cat → ( ≃𝑐 ‘𝐶) = ((Iso‘𝐶) supp ∅)) | ||
Theorem | brcic 16281 | The relation "is isomorphic to" for categories. (Contributed by AV, 5-Apr-2020.) |
⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ (𝑋𝐼𝑌) ≠ ∅)) | ||
Theorem | cic 16282* | Objects 𝑋 and 𝑌 in a category are isomorphic provided that there is an isomorphism 𝑓:𝑋⟶𝑌, see definition 3.15 of [Adamek] p. 29. (Contributed by AV, 4-Apr-2020.) |
⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ ∃𝑓 𝑓 ∈ (𝑋𝐼𝑌))) | ||
Theorem | brcici 16283 | Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020.) |
⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌) | ||
Theorem | cicref 16284 | Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (Base‘𝐶)) → 𝑂( ≃𝑐 ‘𝐶)𝑂) | ||
Theorem | ciclcl 16285 | Isomorphism implies the left side is an object. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑅 ∈ (Base‘𝐶)) | ||
Theorem | cicrcl 16286 | Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆 ∈ (Base‘𝐶)) | ||
Theorem | cicsym 16287 | Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆( ≃𝑐 ‘𝐶)𝑅) | ||
Theorem | cictr 16288 | Isomorphism is transitive. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆 ∧ 𝑆( ≃𝑐 ‘𝐶)𝑇) → 𝑅( ≃𝑐 ‘𝐶)𝑇) | ||
Theorem | cicer 16289 | Isomorphism is an equivalence relation on objects of a category. Remark 3.16 in [Adamek] p. 29. (Contributed by AV, 5-Apr-2020.) |
⊢ (𝐶 ∈ Cat → ( ≃𝑐 ‘𝐶) Er (Base‘𝐶)) | ||
Syntax | cssc 16290 | Extend class notation to include the subset relation for subcategories. |
class ⊆cat | ||
Syntax | cresc 16291 | Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms). |
class ↾cat | ||
Syntax | csubc 16292 | Extend class notation to include the collection of subcategories of a category. |
class Subcat | ||
Definition | df-ssc 16293* | Define the subset relation for subcategories. Despite the name, this is not really a "category-aware" definition, which is to say it makes no explicit references to homsets or composition; instead this is a subset-like relation on the functions that are used as subcategory specifications in df-subc 16295, which makes it play an analogous role to the subset relation applied to the subgroups of a group. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ⊆cat = {〈ℎ, 𝑗〉 ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))} | ||
Definition | df-resc 16294* | Define the restriction of a category to a given set of arrows. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ ↾cat = (𝑐 ∈ V, ℎ ∈ V ↦ ((𝑐 ↾s dom dom ℎ) sSet 〈(Hom ‘ndx), ℎ〉)) | ||
Definition | df-subc 16295* | (Subcat‘𝐶) is the set of all the subcategory specifications of the category 𝐶. Like df-subg 17414, this is not actually a collection of categories (as in definition 4.1(a) of [Adamek] p. 48), but only sets which when given operations from the base category (using df-resc 16294) form a category. All the objects and all the morphisms of the subcategory belong to the supercategory. The identity of an object, the domain and the codomain of a morphism are the same in the subcategory and the supercategory. The composition of the subcategory is a restriction of the composition of the supercategory. (Contributed by FL, 17-Sep-2009.) (Revised by Mario Carneiro, 4-Jan-2017.) |
⊢ Subcat = (𝑐 ∈ Cat ↦ {ℎ ∣ (ℎ ⊆cat (Homf ‘𝑐) ∧ [dom dom ℎ / 𝑠]∀𝑥 ∈ 𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥ℎ𝑥) ∧ ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)))}) | ||
Theorem | sscrel 16296 | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ Rel ⊆cat | ||
Theorem | brssc 16297* | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) | ||
Theorem | sscpwex 16298* | An analogue of pwex 4774 for the subcategory subset relation: The collection of subcategory subsets of a given set 𝐽 is a set. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ {ℎ ∣ ℎ ⊆cat 𝐽} ∈ V | ||
Theorem | subcrcl 16299 | Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat) | ||
Theorem | sscfn1 16300 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑆 = dom dom 𝐻) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |