![]() |
Metamath
Proof Explorer Theorem List (p. 179 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | issect2 17801 | Property of being a section. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑋)) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐺(〈𝑋, 𝑌〉 · 𝑋)𝐹) = ( 1 ‘𝑋))) | ||
Theorem | sectcan 17802 | 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 17803 | Composition of two sections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) & ⊢ (𝜑 → 𝐻(𝑌𝑆𝑍)𝐾) ⇒ ⊢ (𝜑 → (𝐻(〈𝑋, 𝑌〉 · 𝑍)𝐹)(𝑋𝑆𝑍)(𝐺(〈𝑍, 𝑌〉 · 𝑋)𝐾)) | ||
Theorem | isofval 17804* | Function value of the function returning the isomorphisms of a category. (Contributed by AV, 5-Apr-2017.) |
⊢ (𝐶 ∈ Cat → (Iso‘𝐶) = ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶))) | ||
Theorem | invffval 17805* | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥𝑆𝑦) ∩ ◡(𝑦𝑆𝑥)))) | ||
Theorem | invfval 17806 | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑁𝑌) = ((𝑋𝑆𝑌) ∩ ◡(𝑌𝑆𝑋))) | ||
Theorem | isinv 17807 | Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹))) | ||
Theorem | invss 17808 | The inverse relation is a relation between morphisms 𝐹:𝑋⟶𝑌 and their inverses 𝐺:𝑌⟶𝑋. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑁𝑌) ⊆ ((𝑋𝐻𝑌) × (𝑌𝐻𝑋))) | ||
Theorem | invsym 17809 | The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ 𝐺(𝑌𝑁𝑋)𝐹)) | ||
Theorem | invsym2 17810 | The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ◡(𝑋𝑁𝑌) = (𝑌𝑁𝑋)) | ||
Theorem | invfun 17811 | 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 17812 | 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 17813 | If 𝐺 is an inverse to 𝐹, then 𝐹 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) | ||
Theorem | inviso2 17814 | If 𝐺 is an inverse to 𝐹, then 𝐺 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑋)) | ||
Theorem | invf 17815 | The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑁𝑌):(𝑋𝐼𝑌)⟶(𝑌𝐼𝑋)) | ||
Theorem | invf1o 17816 | 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 17817 | 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 17818 | 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 17819* | 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 17820* | 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 17821 | 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 17822 | 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 17823 | An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋𝐻𝑌)) | ||
Theorem | isoco 17824 | 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 17825 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝑂) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑇𝑌)𝐺 ↔ 𝐺(𝑋𝑆𝑌)𝐹)) | ||
Theorem | oppcsect2 17826 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝑂) ⇒ ⊢ (𝜑 → (𝑋𝑇𝑌) = ◡(𝑋𝑆𝑌)) | ||
Theorem | oppcinv 17827 | An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Inv‘𝐶) & ⊢ 𝐽 = (Inv‘𝑂) ⇒ ⊢ (𝜑 → (𝑋𝐽𝑌) = (𝑌𝐼𝑋)) | ||
Theorem | oppciso 17828 | 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 17829 | 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 17830 | 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 17831 | 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 17832 | 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 17833 | The identity is a section of itself. (Contributed by AV, 8-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Sect‘𝐶)𝑋)(𝐼‘𝑋)) | ||
Theorem | invid 17834 | The inverse of the identity is the identity. (Contributed by AV, 8-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Inv‘𝐶)𝑋)(𝐼‘𝑋)) | ||
Theorem | idiso 17835 | The identity is an isomorphism. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 8-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋(Iso‘𝐶)𝑋)) | ||
Theorem | idinv 17836 | 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 17837 | The inverse of an isomorphism 𝐹 (which is unique because of invf 17815 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 17838 | The inverse of an isomorphism is invers to the isomorphism. (Contributed by AV, 9-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹)) | ||
Theorem | invcoisoid 17839 | 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 17840 | 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 17841 | 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 17843). It is shown that this relation is an equivalence relation, see cicer 17853. | ||
Syntax | ccic 17842 | Extend class notation to include the category isomorphism relation. |
class ≃𝑐 | ||
Definition | df-cic 17843 | 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 19290. (Contributed by AV, 4-Apr-2020.) |
⊢ ≃𝑐 = (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅)) | ||
Theorem | cicfval 17844 | The set of isomorphic objects of the category 𝑐. (Contributed by AV, 4-Apr-2020.) |
⊢ (𝐶 ∈ Cat → ( ≃𝑐 ‘𝐶) = ((Iso‘𝐶) supp ∅)) | ||
Theorem | brcic 17845 | The relation "is isomorphic to" for categories. (Contributed by AV, 5-Apr-2020.) |
⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ (𝑋𝐼𝑌) ≠ ∅)) | ||
Theorem | cic 17846* | 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 17847 | Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020.) |
⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌) | ||
Theorem | cicref 17848 | Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (Base‘𝐶)) → 𝑂( ≃𝑐 ‘𝐶)𝑂) | ||
Theorem | ciclcl 17849 | Isomorphism implies the left side is an object. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑅 ∈ (Base‘𝐶)) | ||
Theorem | cicrcl 17850 | Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆 ∈ (Base‘𝐶)) | ||
Theorem | cicsym 17851 | Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆( ≃𝑐 ‘𝐶)𝑅) | ||
Theorem | cictr 17852 | Isomorphism is transitive. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆 ∧ 𝑆( ≃𝑐 ‘𝐶)𝑇) → 𝑅( ≃𝑐 ‘𝐶)𝑇) | ||
Theorem | cicer 17853 | 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 17854 | Extend class notation to include the subset relation for subcategories. |
class ⊆cat | ||
Syntax | cresc 17855 | Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms). |
class ↾cat | ||
Syntax | csubc 17856 | Extend class notation to include the collection of subcategories of a category. |
class Subcat | ||
Definition | df-ssc 17857* | 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 17859, 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 17858* | 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 17859* | (Subcat‘𝐶) is the set of all the subcategory specifications of the category 𝐶. Like df-subg 19153, 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 17858) 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 17860 | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ Rel ⊆cat | ||
Theorem | brssc 17861* | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) | ||
Theorem | sscpwex 17862* | An analogue of pwex 5385 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 17863 | Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat) | ||
Theorem | sscfn1 17864 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑆 = dom dom 𝐻) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) | ||
Theorem | sscfn2 17865 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑇 = dom dom 𝐽) ⇒ ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) | ||
Theorem | ssclem 17866 | Lemma for ssc1 17868 and similar theorems. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (𝐻 ∈ V ↔ 𝑆 ∈ V)) | ||
Theorem | isssc 17867* | Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) | ||
Theorem | ssc1 17868 | Infer subset relation on objects from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝐻 ⊆cat 𝐽) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝑇) | ||
Theorem | ssc2 17869 | Infer subset relation on morphisms from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) ⊆ (𝑋𝐽𝑌)) | ||
Theorem | sscres 17870 | 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 17871 | The subcategory subset relation is reflexive. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → 𝐻 ⊆cat 𝐻) | ||
Theorem | ssctr 17872 | The subcategory subset relation is transitive. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶) → 𝐴 ⊆cat 𝐶) | ||
Theorem | ssceq 17873 | The subcategory subset relation is antisymmetric. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴) → 𝐴 = 𝐵) | ||
Theorem | rescval 17874 | Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) ⇒ ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → 𝐷 = ((𝐶 ↾s dom dom 𝐻) sSet 〈(Hom ‘ndx), 𝐻〉)) | ||
Theorem | rescval2 17875 | Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → 𝐷 = ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉)) | ||
Theorem | rescbas 17876 | 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 | rescbasOLD 17877 | Obsolete version of rescbas 17876 as of 18-Oct-2024. Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 = (Base‘𝐷)) | ||
Theorem | reschom 17878 | Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐻 = (Hom ‘𝐷)) | ||
Theorem | reschomf 17879 | Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐻 = (Homf ‘𝐷)) | ||
Theorem | rescco 17880 | 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 | resccoOLD 17881 | Obsolete version of rescco 17880 as of 14-Oct-2024. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → · = (comp‘𝐷)) | ||
Theorem | rescabs 17882 | Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 9-Nov-2024.) |
⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) | ||
Theorem | rescabsOLD 17883 | Obsolete version of seqp1d 14055 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 17884 | Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → ((𝐶 ↾s 𝑆) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) | ||
Theorem | issubc 17885* | 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 17886* | Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐽𝑧))))) | ||
Theorem | 0ssc 17887 | For any category 𝐶, the empty set is a subcategory subset of 𝐶. (Contributed by AV, 23-Apr-2020.) |
⊢ (𝐶 ∈ Cat → ∅ ⊆cat (Homf ‘𝐶)) | ||
Theorem | 0subcat 17888 | 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 17889 | 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 17890 | 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 17891 | An element in the set of subcategories is a binary function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝑆 = dom dom 𝐽) ⇒ ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) | ||
Theorem | subcss1 17892 | 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 17893 | 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 17894 | 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 17895 | A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐽𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐽𝑍)) | ||
Theorem | subccatid 17896* | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ∧ (Id‘𝐷) = (𝑥 ∈ 𝑆 ↦ ( 1 ‘𝑥)))) | ||
Theorem | subcid 17897 | 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 17898 | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → 𝐷 ∈ Cat) | ||
Theorem | issubc3 17899* | 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 18829, 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 17900 | 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‘𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |