Home | Metamath
Proof Explorer Theorem List (p. 174 of 463) | < 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-29031) |
Hilbert Space Explorer
(29032-30554) |
Users' Mathboxes
(30555-46226) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | invsym2 17301 | The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ◡(𝑋𝑁𝑌) = (𝑌𝑁𝑋)) | ||
Theorem | invfun 17302 | 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 17303 | 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 17304 | If 𝐺 is an inverse to 𝐹, then 𝐹 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) | ||
Theorem | inviso2 17305 | If 𝐺 is an inverse to 𝐹, then 𝐺 is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐼𝑋)) | ||
Theorem | invf 17306 | The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝑋𝑁𝑌):(𝑋𝐼𝑌)⟶(𝑌𝐼𝑋)) | ||
Theorem | invf1o 17307 | 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 17308 | 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 17309 | 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 17310* | 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 17311* | 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 17312 | 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 17313 | 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 17314 | An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋𝐻𝑌)) | ||
Theorem | isoco 17315 | 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 17316 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝑂) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑇𝑌)𝐺 ↔ 𝐺(𝑋𝑆𝑌)𝐹)) | ||
Theorem | oppcsect2 17317 | A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑆 = (Sect‘𝐶) & ⊢ 𝑇 = (Sect‘𝑂) ⇒ ⊢ (𝜑 → (𝑋𝑇𝑌) = ◡(𝑋𝑆𝑌)) | ||
Theorem | oppcinv 17318 | An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Inv‘𝐶) & ⊢ 𝐽 = (Inv‘𝑂) ⇒ ⊢ (𝜑 → (𝑋𝐽𝑌) = (𝑌𝐼𝑋)) | ||
Theorem | oppciso 17319 | 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 17320 | 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 17321 | 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 17322 | 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 17323 | 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 17324 | The identity is a section of itself. (Contributed by AV, 8-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Sect‘𝐶)𝑋)(𝐼‘𝑋)) | ||
Theorem | invid 17325 | The inverse of the identity is the identity. (Contributed by AV, 8-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋)(𝑋(Inv‘𝐶)𝑋)(𝐼‘𝑋)) | ||
Theorem | idiso 17326 | The identity is an isomorphism. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 8-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝑋(Iso‘𝐶)𝑋)) | ||
Theorem | idinv 17327 | 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 17328 | The inverse of an isomorphism 𝐹 (which is unique because of invf 17306 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 17329 | The inverse of an isomorphism is invers to the isomorphism. (Contributed by AV, 9-Apr-2020.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)((𝑋𝑁𝑌)‘𝐹)) | ||
Theorem | invcoisoid 17330 | 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 17331 | 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 17332 | 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 17334). It is shown that this relation is an equivalence relation, see cicer 17344. | ||
Syntax | ccic 17333 | Extend class notation to include the category isomorphism relation. |
class ≃𝑐 | ||
Definition | df-cic 17334 | 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 18697. (Contributed by AV, 4-Apr-2020.) |
⊢ ≃𝑐 = (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅)) | ||
Theorem | cicfval 17335 | The set of isomorphic objects of the category 𝑐. (Contributed by AV, 4-Apr-2020.) |
⊢ (𝐶 ∈ Cat → ( ≃𝑐 ‘𝐶) = ((Iso‘𝐶) supp ∅)) | ||
Theorem | brcic 17336 | The relation "is isomorphic to" for categories. (Contributed by AV, 5-Apr-2020.) |
⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐶)𝑌 ↔ (𝑋𝐼𝑌) ≠ ∅)) | ||
Theorem | cic 17337* | 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 17338 | Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020.) |
⊢ 𝐼 = (Iso‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐶)𝑌) | ||
Theorem | cicref 17339 | Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑂 ∈ (Base‘𝐶)) → 𝑂( ≃𝑐 ‘𝐶)𝑂) | ||
Theorem | ciclcl 17340 | Isomorphism implies the left side is an object. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑅 ∈ (Base‘𝐶)) | ||
Theorem | cicrcl 17341 | Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆 ∈ (Base‘𝐶)) | ||
Theorem | cicsym 17342 | Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆) → 𝑆( ≃𝑐 ‘𝐶)𝑅) | ||
Theorem | cictr 17343 | Isomorphism is transitive. (Contributed by AV, 5-Apr-2020.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐 ‘𝐶)𝑆 ∧ 𝑆( ≃𝑐 ‘𝐶)𝑇) → 𝑅( ≃𝑐 ‘𝐶)𝑇) | ||
Theorem | cicer 17344 | 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 17345 | Extend class notation to include the subset relation for subcategories. |
class ⊆cat | ||
Syntax | cresc 17346 | Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms). |
class ↾cat | ||
Syntax | csubc 17347 | Extend class notation to include the collection of subcategories of a category. |
class Subcat | ||
Definition | df-ssc 17348* | 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 17350, 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 17349* | 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 17350* | (Subcat‘𝐶) is the set of all the subcategory specifications of the category 𝐶. Like df-subg 18573, 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 17349) 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 17351 | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ Rel ⊆cat | ||
Theorem | brssc 17352* | The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) | ||
Theorem | sscpwex 17353* | An analogue of pwex 5290 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 17354 | Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat) | ||
Theorem | sscfn1 17355 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑆 = dom dom 𝐻) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) | ||
Theorem | sscfn2 17356 | The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑇 = dom dom 𝐽) ⇒ ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) | ||
Theorem | ssclem 17357 | Lemma for ssc1 17359 and similar theorems. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (𝐻 ∈ V ↔ 𝑆 ∈ V)) | ||
Theorem | isssc 17358* | Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) | ||
Theorem | ssc1 17359 | Infer subset relation on objects from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝐻 ⊆cat 𝐽) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝑇) | ||
Theorem | ssc2 17360 | Infer subset relation on morphisms from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) ⊆ (𝑋𝐽𝑌)) | ||
Theorem | sscres 17361 | 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 17362 | The subcategory subset relation is reflexive. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → 𝐻 ⊆cat 𝐻) | ||
Theorem | ssctr 17363 | The subcategory subset relation is transitive. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶) → 𝐴 ⊆cat 𝐶) | ||
Theorem | ssceq 17364 | The subcategory subset relation is antisymmetric. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴) → 𝐴 = 𝐵) | ||
Theorem | rescval 17365 | Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) ⇒ ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊) → 𝐷 = ((𝐶 ↾s dom dom 𝐻) sSet 〈(Hom ‘ndx), 𝐻〉)) | ||
Theorem | rescval2 17366 | Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → 𝐷 = ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉)) | ||
Theorem | rescbas 17367 | Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 = (Base‘𝐷)) | ||
Theorem | reschom 17368 | Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐻 = (Hom ‘𝐷)) | ||
Theorem | reschomf 17369 | Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐻 = (Homf ‘𝐷)) | ||
Theorem | rescco 17370 | 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 17371 | Obsolete proof of rescco 17370 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 17372 | Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) | ||
Theorem | rescabs2 17373 | Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → ((𝐶 ↾s 𝑆) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) | ||
Theorem | issubc 17374* | 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 17375* | Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐻 = (Homf ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) ⇒ ⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐽𝑧))))) | ||
Theorem | 0ssc 17376 | For any category 𝐶, the empty set is a subcategory subset of 𝐶. (Contributed by AV, 23-Apr-2020.) |
⊢ (𝐶 ∈ Cat → ∅ ⊆cat (Homf ‘𝐶)) | ||
Theorem | 0subcat 17377 | 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 17378 | 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 17379 | 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 17380 | An element in the set of subcategories is a binary function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝑆 = dom dom 𝐽) ⇒ ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) | ||
Theorem | subcss1 17381 | 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 17382 | 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 17383 | 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 17384 | A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐽𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐽𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐽𝑍)) | ||
Theorem | subccatid 17385* | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → (𝐷 ∈ Cat ∧ (Id‘𝐷) = (𝑥 ∈ 𝑆 ↦ ( 1 ‘𝑥)))) | ||
Theorem | subcid 17386 | 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 17387 | A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐽) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → 𝐷 ∈ Cat) | ||
Theorem | issubc3 17388* | 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 18264, 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 17389 | 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 17390 | 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 17391 | A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐶 ↾s 𝑆) ∈ Cat) | ||
Theorem | subsubc 17392 | A subcategory of a subcategory is a subcategory. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾cat 𝐻) ⇒ ⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻))) | ||
Syntax | cfunc 17393 | Extend class notation with the class of all functors. |
class Func | ||
Syntax | cidfu 17394 | Extend class notation with identity functor. |
class idfunc | ||
Syntax | ccofu 17395 | Extend class notation with functor composition. |
class ∘func | ||
Syntax | cresf 17396 | Extend class notation to include restriction of a functor to a subcategory. |
class ↾f | ||
Definition | df-func 17397* | Function returning all the functors from a category 𝑡 to a category 𝑢. Definition 3.17 of [Adamek] p. 29, and definition in [Lang] p. 62 ("covariant functor"). Intuitively a functor associates any morphism of 𝑡 to a morphism of 𝑢, any object of 𝑡 to an object of 𝑢, and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of 𝑡 to an object of 𝑢 we write it associates any identity of 𝑡 to an identity of 𝑢 which simplifies the definition. According to remark 3.19 in [Adamek] p. 30, "a functor F : A -> B is technically a family of functions; one from Ob(A) to Ob(B) [here: f, called "the object part" in the following], and for each pair (A,A') of A-objects, one from hom(A,A') to hom(FA, FA') [here: g, called "the morphism part" in the following]". (Contributed by FL, 10-Feb-2008.) (Revised by Mario Carneiro, 2-Jan-2017.) |
⊢ Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {〈𝑓, 𝑔〉 ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}) | ||
Definition | df-idfu 17398* | Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ idfunc = (𝑡 ∈ Cat ↦ ⦋(Base‘𝑡) / 𝑏⦌〈( I ↾ 𝑏), (𝑧 ∈ (𝑏 × 𝑏) ↦ ( I ↾ ((Hom ‘𝑡)‘𝑧)))〉) | ||
Definition | df-cofu 17399* | Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ ∘func = (𝑔 ∈ V, 𝑓 ∈ V ↦ 〈((1st ‘𝑔) ∘ (1st ‘𝑓)), (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))〉) | ||
Definition | df-resf 17400* | Define the restriction of a functor to a subcategory (analogue of df-res 5581). (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ ↾f = (𝑓 ∈ V, ℎ ∈ V ↦ 〈((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))〉) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |