| Metamath
Proof Explorer Theorem List (p. 179 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | isofval 17801* | Function value of the function returning the isomorphisms of a category. (Contributed by AV, 5-Apr-2017.) |
| ⊢ (𝐶 ∈ Cat → (Iso‘𝐶) = ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶))) | ||
| Theorem | invffval 17802* | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝑆𝑦) ∩ ◡(𝑦𝑆𝑥)))) | ||
| Theorem | invfval 17803 | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑁𝑌) = ((𝑋𝑆𝑌) ∩ ◡(𝑌𝑆𝑋))) | ||
| Theorem | isinv 17804 | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹))) | ||
| Theorem | invss 17805 | The inverse relation is a relation between morphisms 𝐹:𝑋⟶𝑌 and their inverses 𝐺:𝑌⟶𝑋. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑁𝑌) ⊆ ((𝑋𝐻𝑌) × (𝑌𝐻𝑋))) | ||
| Theorem | invsym 17806 | The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ 𝐺(𝑌𝑁𝑋)𝐹)) | ||
| Theorem | invsym2 17807 | The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ◡(𝑋𝑁𝑌) = (𝑌𝑁𝑋)) | ||
| Theorem | invfun 17808 | 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 17809 | 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 17810 | If 𝐺 is an inverse to 𝐹, then 𝐹 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) | ||
| Theorem | inviso2 17811 | If 𝐺 is an inverse to 𝐹, then 𝐺 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑋)) | ||
| Theorem | invf 17812 | The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑁𝑌):(𝑋𝐼𝑌)⟶(𝑌𝐼𝑋)) | ||
| Theorem | invf1o 17813 | 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 17814 | 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 17815 | 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 17816* | Alternate definition of an isomorphism of a category, according to definition 3.8 in [Adamek] p. 28. (Contributed by AV, 10-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ 1 = (Id‘𝐶) & ⊢ ⚬ = (〈𝑋, 𝑌〉(comp‘𝐶)𝑋) & ⊢ ∗ = (〈𝑌, 𝑋〉(comp‘𝐶)𝑌) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔 ⚬ 𝐹) = ( 1 ‘𝑋) ∧ (𝐹 ∗ 𝑔) = ( 1 ‘𝑌)))) | ||
| Theorem | dfiso3 17817* | Alternate definition of an isomorphism of a category as a section in both directions. (Contributed by AV, 11-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)(𝑔(𝑌𝑆𝑋)𝐹 ∧ 𝐹(𝑋𝑆𝑌)𝑔))) | ||
| Theorem | inveq 17818 | If there are two inverses of a morphism, these inverses are equal. Corollary 3.11 of [Adamek] p. 28. (Contributed by AV, 10-Apr-2020.) (Revised by AV, 3-Jul-2022.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹(𝑋𝑁𝑌)𝐺 ∧ 𝐹(𝑋𝑁𝑌)𝐾) → 𝐺 = 𝐾)) | ||
| Theorem | isofn 17819 | 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-2020.) |
| ⊢ (𝐶 ∈ Cat → (Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))) | ||
| Theorem | isohom 17820 | An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋𝐻𝑌)) | ||
| Theorem | isoco 17821 | 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 17822 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝑂) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑇𝑌)𝐺 ↔ 𝐺(𝑋𝑆𝑌)𝐹)) | ||
| Theorem | oppcsect2 17823 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝑂) ⇒ ⊢ (𝜑 → (𝑋𝑇𝑌) = ◡(𝑋𝑆𝑌)) | ||
| Theorem | oppcinv 17824 | An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Inv‘𝐶) & ⊢ 𝐽 = (Inv‘𝑂) ⇒ ⊢ (𝜑 → (𝑋𝐽𝑌) = (𝑌𝐼𝑋)) | ||
| Theorem | oppciso 17825 | 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 17826 | 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 17827 | 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 17828 | 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 17829 | 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 17830 | The identity is a section of itself. (Contributed by AV, 8-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Sect‘𝐶)𝑋)(𝐼‘𝑋)) | ||
| Theorem | invid 17831 | The inverse of the identity is the identity. (Contributed by AV, 8-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Inv‘𝐶)𝑋)(𝐼‘𝑋)) | ||
| Theorem | idiso 17832 | The identity is an isomorphism. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 8-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋(Iso‘𝐶)𝑋)) | ||
| Theorem | idinv 17833 | The inverse of the identity is the identity. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 9-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋(Inv‘𝐶)𝑋)‘(𝐼‘𝑋)) = (𝐼‘𝑋)) | ||
| Theorem | invisoinvl 17834 | The inverse of an isomorphism 𝐹 (which is unique because of invf 17812 and is therefore denoted by ((𝑋𝑁𝑌)‘𝐹), see also remark 3.12 in [Adamek] p. 28) is invers to the isomorphism. (Contributed by AV, 9-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → ((𝑋𝑁𝑌)‘𝐹)(𝑌𝑁𝑋)𝐹) | ||
| Theorem | invisoinvr 17835 | The inverse of an isomorphism is invers to the isomorphism. (Contributed by AV, 9-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹)) | ||
| Theorem | invcoisoid 17836 | The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 5-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ 1 = (Id‘𝐶) & ⊢ ⚬ = (〈𝑋, 𝑌〉(comp‘𝐶)𝑋) ⇒ ⊢ (𝜑 → (((𝑋𝑁𝑌)‘𝐹) ⚬ 𝐹) = ( 1 ‘𝑋)) | ||
| Theorem | isocoinvid 17837 | The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 10-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ 1 = (Id‘𝐶) & ⊢ ⚬ = (〈𝑌, 𝑋〉(comp‘𝐶)𝑌) ⇒ ⊢ (𝜑 → (𝐹 ⚬ ((𝑋𝑁𝑌)‘𝐹)) = ( 1 ‘𝑌)) | ||
| Theorem | rcaninv 17838 | Right cancellation of an inverse of an isomorphism. (Contributed by AV, 5-Apr-2020.) |
| ⊢ 𝐵 = (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 17840). It is shown that this relation is an equivalence relation, see cicer 17850. | ||
| Syntax | ccic 17839 | Extend class notation to include the category isomorphism relation. |
| class ≃𝑐 | ||
| Definition | df-cic 17840 | 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 19278. (Contributed by AV, 4-Apr-2020.) |
| ⊢ ≃𝑐 = (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅)) | ||
| Theorem | cicfval 17841 | The set of isomorphic objects of the category 𝑐. (Contributed by AV, 4-Apr-2020.) |
| ⊢ (𝐶 ∈ Cat → ( ≃𝑐 ‘𝐶) = ((Iso‘𝐶) supp ∅)) | ||
| Theorem | brcic 17842 | The relation "is isomorphic to" for categories. (Contributed by AV, 5-Apr-2020.) |
| ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ (𝑋𝐼𝑌) ≠ ∅)) | ||
| Theorem | cic 17843* | 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 17844 | Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020.) |
| ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌) | ||
| Theorem | cicref 17845 | Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020.) |
| ⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (Base‘𝐶)) → 𝑂( ≃𝑐 ‘𝐶)𝑂) | ||
| Theorem | ciclcl 17846 | Isomorphism implies the left side is an object. (Contributed by AV, 5-Apr-2020.) |
| ⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑅 ∈ (Base‘𝐶)) | ||
| Theorem | cicrcl 17847 | Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020.) |
| ⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆 ∈ (Base‘𝐶)) | ||
| Theorem | cicsym 17848 | Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020.) |
| ⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆( ≃𝑐 ‘𝐶)𝑅) | ||
| Theorem | cictr 17849 | Isomorphism is transitive. (Contributed by AV, 5-Apr-2020.) |
| ⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆 ∧ 𝑆( ≃𝑐 ‘𝐶)𝑇) → 𝑅( ≃𝑐 ‘𝐶)𝑇) | ||
| Theorem | cicer 17850 | 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 17851 | Extend class notation to include the subset relation for subcategories. |
| class ⊆cat | ||
| Syntax | cresc 17852 | Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms). |
| class ↾cat | ||
| Syntax | csubc 17853 | Extend class notation to include the collection of subcategories of a category. |
| class Subcat | ||
| Definition | df-ssc 17854* | 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 17856, 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 17855* | 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 17856* | (Subcat‘𝐶) is the set of all the subcategory specifications of the category 𝐶. Like df-subg 19141, 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 17855) 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 17857 | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ Rel ⊆cat | ||
| Theorem | brssc 17858* | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) | ||
| Theorem | sscpwex 17859* | An analogue of pwex 5380 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 17860 | Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat) | ||
| Theorem | sscfn1 17861 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑆 = dom dom 𝐻) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) | ||
| Theorem | sscfn2 17862 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑇 = dom dom 𝐽) ⇒ ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) | ||
| Theorem | ssclem 17863 | Lemma for ssc1 17865 and similar theorems. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (𝐻 ∈ V ↔ 𝑆 ∈ V)) | ||
| Theorem | isssc 17864* | Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) | ||
| Theorem | ssc1 17865 | Infer subset relation on objects from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝐻 ⊆cat 𝐽) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝑇) | ||
| Theorem | ssc2 17866 | Infer subset relation on morphisms from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) ⊆ (𝑋𝐽𝑌)) | ||
| Theorem | sscres 17867 | Any function restricted to a square domain is a subcategory subset of the original. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → (𝐻 ↾ (𝑇 × 𝑇)) ⊆cat 𝐻) | ||
| Theorem | sscid 17868 | The subcategory subset relation is reflexive. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → 𝐻 ⊆cat 𝐻) | ||
| Theorem | ssctr 17869 | The subcategory subset relation is transitive. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶) → 𝐴 ⊆cat 𝐶) | ||
| Theorem | ssceq 17870 | The subcategory subset relation is antisymmetric. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴) → 𝐴 = 𝐵) | ||
| Theorem | rescval 17871 | Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐻) ⇒ ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → 𝐷 = ((𝐶 ↾s dom dom 𝐻) sSet 〈(Hom ‘ndx), 𝐻〉)) | ||
| Theorem | rescval2 17872 | Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → 𝐷 = ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉)) | ||
| Theorem | rescbas 17873 | Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by AV, 18-Oct-2024.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 = (Base‘𝐷)) | ||
| Theorem | reschom 17874 | Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐻 = (Hom ‘𝐷)) | ||
| Theorem | reschomf 17875 | Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐻 = (Homf ‘𝐷)) | ||
| Theorem | rescco 17876 | Composition in the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by AV, 13-Oct-2024.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → · = (comp‘𝐷)) | ||
| Theorem | rescabs 17877 | Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 9-Nov-2024.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) | ||
| Theorem | rescabsOLD 17878 | Obsolete version of seqp1d 14059 as of 10-Nov-2024. Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) | ||
| Theorem | rescabs2 17879 | Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → ((𝐶 ↾s 𝑆) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) | ||
| Theorem | issubc 17880* | Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑆 = dom dom 𝐽) ⇒ ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐽𝑧))))) | ||
| Theorem | issubc2 17881* | Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐽𝑧))))) | ||
| Theorem | 0ssc 17882 | For any category 𝐶, the empty set is a subcategory subset of 𝐶. (Contributed by AV, 23-Apr-2020.) |
| ⊢ (𝐶 ∈ Cat → ∅ ⊆cat (Homf ‘𝐶)) | ||
| Theorem | 0subcat 17883 | For any category 𝐶, the empty set is a (full) subcategory of 𝐶, see example 4.3(1.a) in [Adamek] p. 48. (Contributed by AV, 23-Apr-2020.) |
| ⊢ (𝐶 ∈ Cat → ∅ ∈ (Subcat‘𝐶)) | ||
| Theorem | catsubcat 17884 | For any category 𝐶, 𝐶 itself is a (full) subcategory of 𝐶, see example 4.3(1.b) in [Adamek] p. 48. (Contributed by AV, 23-Apr-2020.) |
| ⊢ (𝐶 ∈ Cat → (Homf ‘𝐶) ∈ (Subcat‘𝐶)) | ||
| Theorem | subcssc 17885 | An element in the set of subcategories is a subset of the category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ 𝐻 = (Homf ‘𝐶) ⇒ ⊢ (𝜑 → 𝐽 ⊆cat 𝐻) | ||
| Theorem | subcfn 17886 | An element in the set of subcategories is a binary function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝑆 = dom dom 𝐽) ⇒ ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) | ||
| Theorem | subcss1 17887 | The objects of a subcategory are a subset of the objects of the original. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝐵) | ||
| Theorem | subcss2 17888 | The morphisms of a subcategory are a subset of the morphisms of the original. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐽𝑌) ⊆ (𝑋𝐻𝑌)) | ||
| Theorem | subcidcl 17889 | The identity of the original category is contained in each subcategory. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐽𝑋)) | ||
| Theorem | subccocl 17890 | A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐽𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐽𝑍)) | ||
| Theorem | subccatid 17891* | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ∧ (Id‘𝐷) = (𝑥 ∈ 𝑆 ↦ ( 1 ‘𝑥)))) | ||
| Theorem | subcid 17892 | The identity in a subcategory is the same as the original category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) = ((Id‘𝐷)‘𝑋)) | ||
| Theorem | subccat 17893 | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → 𝐷 ∈ Cat) | ||
| Theorem | issubc3 17894* | Alternate definition of a subcategory, as a subset of the category which is itself a category. The assumption that the identity be closed is necessary just as in the case of a monoid, issubm2 18817, for the same reasons, since categories are a generalization of monoids. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat))) | ||
| Theorem | fullsubc 17895 | The full subcategory generated by a subset of objects is the category with these objects and the same morphisms as the original. The result is always a subcategory (and it is full, meaning that all morphisms of the original category between objects in the subcategory is also in the subcategory), see definition 4.1(2) of [Adamek] p. 48. (Contributed by Mario Carneiro, 4-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ↾ (𝑆 × 𝑆)) ∈ (Subcat‘𝐶)) | ||
| Theorem | fullresc 17896 | The category formed by structure restriction is the same as the category restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ 𝐷 = (𝐶 ↾s 𝑆) & ⊢ 𝐸 = (𝐶 ↾cat (𝐻 ↾ (𝑆 × 𝑆))) ⇒ ⊢ (𝜑 → ((Homf ‘𝐷) = (Homf ‘𝐸) ∧ (compf‘𝐷) = (compf‘𝐸))) | ||
| Theorem | resscat 17897 | A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐶 ↾s 𝑆) ∈ Cat) | ||
| Theorem | subsubc 17898 | A subcategory of a subcategory is a subcategory. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾cat 𝐻) ⇒ ⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻))) | ||
| Syntax | cfunc 17899 | Extend class notation with the class of all functors. |
| class Func | ||
| Syntax | cidfu 17900 | Extend class notation with identity functor. |
| class idfunc | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |