CategoryTheory.Equivalence.counitInv_functor_comp
theorem CategoryTheory.Equivalence.counitInv_functor_comp :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (e : C ā D) (X : C),
CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (e.functor.map (e.unitInv.app X)) =
CategoryTheory.CategoryStruct.id (e.functor.obj X)
This theorem expresses a property of equivalences in category theory. More specifically, given an equivalence `e` between two categories `C` and `D`, and an object `X` of category `C`, the composition of the morphism given by the application of the counit inverse of `e` to the object obtained by applying the functor of `e` to `X`, followed by the morphism obtained by mapping through the functor of `e` the application of the unit inverse of `e` to `X`, is equal to the identity morphism on the object obtained by applying the functor of `e` to `X`. In symbols, if $e : C \simeq D$ is an equivalence of categories and $X$ is an object of $C$, then the composition $e_{\text{counitInv}}(e_{\text{functor}}(X)) \circ e_{\text{functor}}(e_{\text{unitInv}}(X)) = id_{e_{\text{functor}}(X)}$.
More concisely: Given an equivalence of categories $e : C \simeq D$ and an object $X$ in $C$, the composition of $e_{\text{counitInv}} \circ e_{\text{functor}}(X) \circ e_{\text{unitInv}}(X)$ equals the identity morphism $id_{e_{\text{functor}}(X)}$.
|
CategoryTheory.Equivalence.invFunIdAssoc_hom_app
theorem CategoryTheory.Equivalence.invFunIdAssoc_hom_app :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] {E : Type uā} [inst_2 : CategoryTheory.Category.{vā, uā} E]
(e : C ā D) (F : CategoryTheory.Functor D E) (X : D), (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)
This theorem is about category theory and deals with the concept of functors and equivalence between categories. Specifically, for any categories `C`, `D`, and `E`, and for any equivalence `e` between `C` and `D`, and any functor `F` from `D` to `E`, and any object `X` in `D`, the application of the homomorphism of the functor obtained by associating the inverse of the functor `F` with the identity functor on the equivalence `e` to the object `X` is equal to the mapping of the counit of the equivalence `e` at `X` under the functor `F`. This theorem establishes a relationship between the operations of the functor and the equivalence in the context of category theory.
More concisely: For any categories `C`, `D`, `E`, equivalence `e` between `C` and `D`, functor `F` from `D` to `E`, and object `X` in `D`, the application of the right adjoint of `F` along `e` to `X` is equal to the composition of `F` with the inverse of the counit of `e` at `X`.
|
Mathlib.CategoryTheory.Equivalence._auxLemma.1
theorem Mathlib.CategoryTheory.Equivalence._auxLemma.1 :
ā {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ā¶ Y) [inst_1 : CategoryTheory.Mono f]
{g h : Z ā¶ X}, (CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f) = (g = h)
This theorem states that in any category `C`, for any objects `X`, `Y`, `Z` of `C` and any morphism `f` from `X` to `Y` that is a monomorphism, if we have two morphisms `g` and `h` from `Z` to `X`, then the composition of `g` with `f` is equal to the composition of `h` with `f` if and only if `g` is equal to `h`. In other words, monomorphisms in a category are left-cancellative with respect to composition.
More concisely: In any category, if `f` is a monomorphism from object `X` to object `Y`, and `g` and `h` are morphisms from object `Z` to `X`, then `g ā f = h ā f` implies `g = h`.
|
CategoryTheory.Equivalence.functor_unitIso_comp
theorem CategoryTheory.Equivalence.functor_unitIso_comp :
ā {C : Type uā} {D : Type uā} [inst : CategoryTheory.Category.{vā, uā} C]
[inst_1 : CategoryTheory.Category.{vā, uā} D] (self : C ā D) (X : C),
CategoryTheory.CategoryStruct.comp (self.functor.map (self.unitIso.hom.app X))
(self.counitIso.hom.app (self.functor.obj X)) =
CategoryTheory.CategoryStruct.id (self.functor.obj X)
The theorem `CategoryTheory.Equivalence.functor_unitIso_comp` states that for any two categories `C` and `D`, given an equivalence between them (represented by `self : C ā D`), for any object `X` in category `C`, the composition of the morphism given by the natural transformation unit of the equivalence applied to `X` and the morphism given by the natural transformation co-unit of the equivalence applied to the image of `X` under the functor of the equivalence, is equal to the identity morphism on the image of `X` under the functor of the equivalence. This expresses one of the key properties of an equivalence of categories, that the functor and its quasi-inverse are related by natural isomorphisms.
More concisely: For any equivalence of categories `C ā D` and object `X` in `C`, the composition of the unit and co-unit natural transformations of the equivalence applied to `X` is equal to the identity morphism on the image of `X` under the functor of the equivalence.
|
CategoryTheory.Equivalence.inv_fun_map
theorem CategoryTheory.Equivalence.inv_fun_map :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (e : C ā D) (X Y : C) (f : X ā¶ Y),
e.inverse.map (e.functor.map f) =
CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (e.unit.app Y))
The theorem `CategoryTheory.Equivalence.inv_fun_map` states that in the setting of category theory, for any two categories `C` and `D` that are equivalent (denoted `C ā D`), and any two objects `X` and `Y` in `C`, and a morphism `f` from `X` to `Y` (denoted `X ā¶ Y`), the image of the morphism `f` under the functor associated with the equivalence, when mapped back using the inverse of the equivalence, is the same as first applying the unit inverse at `X`, then composing with `f`, and then applying the unit at `Y`.
In simpler terms, this theorem is about "going around in a loop" in a specific way within an equivalence of categories, and ending up where you started. This is a fundamental property in category theory that such a loop, involving functors and natural transformations (the 'unit' and 'unit inverse' are examples of these), doesn't change the morphism you started with.
More concisely: Given any equivalence of categories `C ā D` and morphisms `X ā¶ Y` in `C`, the image of `f` under the functor associated with the equivalence, followed by the inverse equivalence, is equivalent to applying the unit inverse at `X`, then `f`, and then the unit at `Y`.
|
CategoryTheory.Equivalence.unit_inverse_comp
theorem CategoryTheory.Equivalence.unit_inverse_comp :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (e : C ā D) (Y : D),
CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (e.inverse.map (e.counit.app Y)) =
CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
This theorem, named `CategoryTheory.Equivalence.unit_inverse_comp`, states that for any two categories `C` and `D` that are equivalent (denoted `C ā D`), and for any object `Y` in the category `D`, the composition of two morphisms ā the application of the unit component of the equivalence to the object obtained by applying the inverse of the equivalence to `Y`, and the mapping of the counit component of the equivalence applied to `Y` under the inverse of the equivalence ā is equal to the identity morphism on the object obtained by applying the inverse of the equivalence to `Y`. This theorem is related to the other triangle identity in category theory and the proof in Globular can be found at: http://globular.science/1905.001.
More concisely: Given categories `C` and `D` equivalent to each other, for any object `Y` in `D`, the composition of the unit and counit morphisms of the equivalence, applied to `Y` and its inverse, equals the identity morphism on the object obtained by applying the inverse of the equivalence to `Y`.
|
CategoryTheory.IsEquivalence.ofIso_trans
theorem CategoryTheory.IsEquivalence.ofIso_trans :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] {F G H : CategoryTheory.Functor C D} (e : F ā
G) (e' : G ā
H)
(hF : F.IsEquivalence),
CategoryTheory.Functor.IsEquivalence.ofIso e' (CategoryTheory.Functor.IsEquivalence.ofIso e hF) =
CategoryTheory.Functor.IsEquivalence.ofIso (e.trans e') hF
This theorem, `CategoryTheory.IsEquivalence.ofIso_trans`, in the category theory, states that for any three functors `F`, `G`, and `H` between categories `C` and `D`, and for any isomorphisms `e` between `F` and `G` and `e'` between `G` and `H`, if `F` is an equivalence, then the equivalence of `F` and `H` obtained by applying `ofIso` to the composition of the isomorphisms `e` and `e'` is the same as that obtained by first applying `ofIso` to the isomorphisms `e` and `e'` separately and then composing the results. This demonstrates the compatibility of `ofIso` with the composition of isomorphisms of functors.
More concisely: Given functors F, G, H between categories C and D, isomorphisms e : F ā
G and e' : G ā
H with F an equivalence, the compositions of ofIso(e) and ofIso(e') are equal.
|
CategoryTheory.Equivalence.essSurj_of_equivalence
theorem CategoryTheory.Equivalence.essSurj_of_equivalence :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence],
F.EssSurj
This theorem states that an equivalence in category theory is essentially surjective. Specifically, given any two categories `C` and `D`, and a functor `F` from `C` to `D` that is an equivalence, then `F` is essentially surjective. In category theory, a functor is essentially surjective if for every object in the codomain category (in this case, `D`), there is an object in the domain category (`C`) such that the two objects are isomorphic under the functor.
More concisely: Given any equivalence of categories `F: C ā D`, for every object `d` in `D`, there exists an object `c` in `C` such that `F(c) ā
d`.
|
CategoryTheory.Equivalence.fun_inv_map
theorem CategoryTheory.Equivalence.fun_inv_map :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (e : C ā D) (X Y : D) (f : X ā¶ Y),
e.functor.map (e.inverse.map f) =
CategoryTheory.CategoryStruct.comp (e.counit.app X)
(CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y))
The theorem `CategoryTheory.Equivalence.fun_inv_map` states that for any two categories `C` and `D` and an equivalence `e` between them, for any objects `X` and `Y` in `D` and a morphism `f` from `X` to `Y`, the mapping of the inverse of `f` under the functor of the equivalence `e` is equal to the composition of the application of the counit of the equivalence `e` to `X`, `f`, and the application of the inverse of the counit of the equivalence `e` to `Y`. This is a statement about how morphisms and objects behave under equivalences in category theory.
More concisely: For any equivalence `e` between categories `C` and `D` and morphism `f` in `D`, the inverse of `f` under the functor of `e` is equal to the composition of the counit of `e` at the source of `f`, `f`, and the counit of `e` at the target of `f` inverse.
|
CategoryTheory.Equivalence.functor_unit_comp
theorem CategoryTheory.Equivalence.functor_unit_comp :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (e : C ā D) (X : C),
CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (e.counit.app (e.functor.obj X)) =
CategoryTheory.CategoryStruct.id (e.functor.obj X)
The theorem `CategoryTheory.Equivalence.functor_unit_comp` states that for any two categories `C` and `D` and an equivalence `e` between them, the composition of the functor's map applied to the unit at `X` and the counit at the functor's object `X` is the identity on the functor's object `X`. In other words, it formalizes one of the triangle identities that are conditions for a functor to be an equivalence of categories: the composition of the unit transformation and the counit transformation is the identity transformation.
More concisely: Given an equivalence of categories `e : C ā D` between categories `C` and `D`, for any object `X` in `C`, the composition of `e.map X (e.unit X)` and `e.counit X` equals the identity on `e.obj X` in `D`.
|
CategoryTheory.Equivalence.counit_app_functor
theorem CategoryTheory.Equivalence.counit_app_functor :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (e : C ā D) (X : C),
e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)
This theorem states that for any category theory equivalence `e` between two categories `C` and `D`, and for any object `X` in category `C`, the application of the counit of `e` to the object obtained by applying the functor of `e` to `X` equals the map of the functor of `e` applied to the application of the inverse of the unit of `e` to `X`. In simpler terms, it shows a specific property of the interplay between the functor and the unit/counit of a category equivalence in category theory.
More concisely: For any category theory equivalence `e` between categories `C` and `D`, the counit of `e` applied to `e(X)` equals the functor of `e` applied to the inverse of the unit of `e` applied to `X`.
|
CategoryTheory.Equivalence.counitInv_app_functor
theorem CategoryTheory.Equivalence.counitInv_app_functor :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (e : C ā D) (X : C),
e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)
This theorem states that for any two categories `C` and `D` that are equivalent (denoted as `C ā D`), and for any object `X` in category `C`, the application of the inverse of the `counit` of the equivalence `e` to the result of applying the `functor` of the equivalence `e` to `X` is equal to the result of applying the `functor` of the equivalence `e` to the result of applying the `unit` of the equivalence `e` to `X`. In category theory terms, this theorem is expressing a key property of the units and counits of an equivalence of categories.
More concisely: For any equivalence of categories `e: C ā D` and object `X` in `C`, the following commutative diagram holds:
```
X āāāāāāāāāāā e.unit _ āāāāāāāāāāā e.obj X
ā ā
ā identity ā
ā ā
e.obj _ āāāāāāāāāāā e.counit _ āāāāāāāāāā e.obj (e.functor X)
```
|
CategoryTheory.IsEquivalence.ofIso_refl
theorem CategoryTheory.IsEquivalence.ofIso_refl :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (F : CategoryTheory.Functor C D) (hF : F.IsEquivalence),
CategoryTheory.Functor.IsEquivalence.ofIso (CategoryTheory.Iso.refl F) hF = hF
This theorem, referred to as an alias of `CategoryTheory.Functor.IsEquivalence.ofIso_refl`, states that for any categories `C` and `D`, for any functor `F` from `C` to `D` that is an equivalence of categories, applying the `ofIso` function to the identity isomorphism of `F` and the given equivalence `hF` will return `hF`. In short, the `ofIso` function is compatible with identity isomorphisms of functors.
More concisely: For any functor `F: C -> D` that is an equivalence of categories, `ofIso F id hF = hF`, where `id` is the identity isomorphism of `F` and `hF` is the given equivalence.
|