CategoryTheory.Adjunction.homEquiv_naturality_right_symm
theorem CategoryTheory.Adjunction.homEquiv_naturality_right_symm :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'),
(adj.homEquiv X Y').symm (CategoryTheory.CategoryStruct.comp f (G.map g)) =
CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y).symm f) g
The theorem `CategoryTheory.Adjunction.homEquiv_naturality_right_symm` expresses a fundamental property of adjunctions in category theory. Specifically, it states that for any two categories `C` and `D`, and functors `F` from `C` to `D` and `G` from `D` to `C` forming an adjunction, the mapping of morphisms (homEquiv) between objects is natural in the right argument. This naturality condition ensures that for any objects `X` in `C`, `Y` and `Y'` in `D`, and morphisms `f` from `X` to `G(Y)` and `g` from `Y` to `Y'`, the composition of `f` with the functor image of `g` under `G` and then applying the inverse of homEquiv at `X` and `Y'`, is the same as first applying the inverse of homEquiv at `X` and `Y` to `f`, and then composing the result with `g`. This theorem is a cornerstone of the theory of adjoint functors, which are a key concept in category theory.
More concisely: Given categories `C` and `D`, functors `F: C → D` and `G: D → C` forming an adjunction, the homomorphism equivalence `map_comp` between `F(f)` and `G(g)` for morphisms `f: X → G(Y)` in `C` and `g: Y → Y'` in `D`, is natural in `Y` and `Y'`.
|
CategoryTheory.Adjunction.homEquiv_apply_eq
theorem CategoryTheory.Adjunction.homEquiv_apply_eq :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B),
(adj.homEquiv A B) f = g ↔ f = (adj.homEquiv A B).symm g
This theorem states that for any categories `C` and `D`, their functors `F` and `G` that form an adjunction `adj`, along with objects `A` in `C` and `B` in `D`, and morphisms `f` from `F.obj A` to `B` and `g` from `A` to `G.obj B`, the morphism `f` is equal to the application of the inverse of `adj.homEquiv` at `A` and `B` to `g` if and only if the application of `adj.homEquiv` at `A` and `B` to `f` is equal to `g`. In other words, the adjunction homomorphism equivalence `adj.homEquiv` provides a bijective correspondence between the morphisms `f` and `g`.
More concisely: For any categories `C`, `D`, functors `F: C -> D`, `G: D -> C`, and their adjunction `adj: (F, G)`, the natural transformation `adj.homEquiv` is a bijective correspondence between morphisms `f: F(A) -> B` and `g: A -> G(B)` in `C` and `D`, respectively.
|
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm
theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(self : CategoryTheory.Adjunction.CoreHomEquiv F G) {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
(self.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
CategoryTheory.CategoryStruct.comp (F.map f) ((self.homEquiv X Y).symm g)
The theorem `CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm` describes a property about the effect of applying the inverse (`symm`) of a hom-set equivalence (`homEquiv`) in the context of category theory adjunctions. Specifically, it states that for any categories `C` and `D`, functors `F` from `C` to `D` and `G` from `D` to `C`, an adjunction core of `F` and `G`, and morphisms `f` and `g` in category `C` and the image of `G` respectively, the inverse of `homEquiv` on the composition of `f` and `g` is equal to the composition of the image of `f` under functor `F` and the inverse of `homEquiv` on `g`. In simpler terms, this theorem defines the compatibility between the hom-set equivalence and the composition of morphisms in a category, under the inverse operation.
More concisely: For any adjunction between functors F from C to D and G from D to C, and morphisms f in C and g in D with f ≈ g, the inverse of the hom-set equivalence homEquiv(F, G) on the composite f · G(g) is equal to G(g) · homEquiv(F, G).inverse(f).
|
CategoryTheory.Adjunction.homEquiv_naturality_left
theorem CategoryTheory.Adjunction.homEquiv_naturality_left :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) {X' X : C} {Y : D} (f : X' ⟶ X) (g : F.obj X ⟶ Y),
(adj.homEquiv X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) =
CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y) g)
The theorem `CategoryTheory.Adjunction.homEquiv_naturality_left` states that for any two categories `C` and `D`, and functors `F` from `C` to `D` and `G` from `D` to `C` that form an adjunction, and given two objects `X'` and `X` in `C` and an object `Y` in `D`, with a morphism `f` from `X'` to `X` in `C` and a morphism `g` from `F(X)` to `Y` in `D`, the equivalence of hom-sets given by the adjunction commutes with the composition of morphisms. More specifically, applying the equivalence to the composition of `F.map f` and `g` is the same as first applying the morphism `f` and then applying the equivalence to `g`. This theorem demonstrates one of the key properties that adjunctions in category theory must satisfy, namely, naturality with respect to the morphisms in the categories involved.
More concisely: For any adjunction between functors F from category C to D and G from D to C, and given objects X, X' in C and Y in D, morphisms f: X' -> X in C and g: F(X) -> Y in D, the commutativity of the hom-set equivalence: (∘)⁃₁(F.map f ∘ g) ≡ g ∘ F.map(f).
|
CategoryTheory.Adjunction.left_triangle_components
theorem CategoryTheory.Adjunction.left_triangle_components :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) (X : C),
CategoryTheory.CategoryStruct.comp (F.map (adj.unit.app X)) (adj.counit.app (F.obj X)) =
CategoryTheory.CategoryStruct.id (F.obj X)
This theorem, called `CategoryTheory.Adjunction.left_triangle_components`, states that for any categories `C` and `D`, with functors `F : C -> D` and `G : D -> C` forming an adjunction (denoted `F ⊣ G`), and any object `X` in `C`, the composition of `F.map (adj.unit.app X)` and `adj.counit.app (F.obj X)` is equal to the identity on `F.obj X`.
In simpler terms, this theorem is a part of the definition of an adjunction in category theory, more specifically, it is the statement of one of the conditions in the so-called "triangle identities". It says that if you start with an object in `C`, apply `F`, then apply the unit at `X`, then apply `F` again, then apply the counit at `F.obj X`, you end up back at `F.obj X`, i.e., doing all these operations is the same as doing nothing.
More concisely: For any adjunction `F ⊣ G` between categories `C` and `D`, and for any object `X` in `C`, the diagram `F(X) ♂ adj.unit.app X ♂ F(X)` commutes, where `♂` denotes composition.
|
CategoryTheory.Adjunction.unit_naturality_assoc
theorem CategoryTheory.Adjunction.unit_naturality_assoc :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) {X Y : C} (f : X ⟶ Y) {Z : C} (h : G.obj (F.obj Y) ⟶ Z),
CategoryTheory.CategoryStruct.comp (adj.unit.app X) (CategoryTheory.CategoryStruct.comp (G.map (F.map f)) h) =
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (adj.unit.app Y) h)
This theorem states that for any two categories `C` and `D` with a pair of functors `F` (from `C` to `D`) and `G` (from `D` to `C`) that form an adjunction, and for any two objects `X` and `Y` in `C` with a morphism `f` from `X` to `Y`, the unit of the adjunction behaves naturally. Specifically, for any object `Z` in `C` and a morphism `h` from `G(F(Y))` to `Z`, the composition of the unit at `X` with the composition of the `G`-image of the `F`-image of `f` and `h`, is the same as the composition of `f` with the composition of the unit at `Y` and `h`.
In other words, this theorem is saying that the following square commutes in category `C`:
```
F(X) --(unit at X)--> G(F(X)) --(G(F(f)))--> G(F(Y))
| |
F(f) (unit at Y)
| |
v v
F(Y) --(unit at Y)--> G(F(Y)) --(h)--> Z
```
Here, the vertical arrows are given by the functor `F` and `h`, and the horizontal arrows are given by the unit of the adjunction. The theorem is stating that going from `F(X)` to `Z` via the top path yields the same result as going via the bottom path.
More concisely: For any adjunction between categories `C` and `D` given by functors `F: C -> D` and `G: D -> C`, and for any objects `X, Y in C` and morphisms `f: X -> Y` and `h: G(F(Y)) -> Z` in `C`, the unit of the adjunction at `X` and composition with `h` is equal to composition with `F(f)` and the unit at `Y` and `h`. In other words, the following square commutes:
```
F(X) ---- (unit at X) ---- G(F(X)) ----> G(F(Y))
| | |
| v v
| F(f) h
| | |
| v v
F(Y) ---- (unit at Y) ---- G(F(Y)) ----> Z
```
|
CategoryTheory.Adjunction.unit_naturality
theorem CategoryTheory.Adjunction.unit_naturality :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) {X Y : C} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map (F.map f)) =
CategoryTheory.CategoryStruct.comp f (adj.unit.app Y)
This theorem, `CategoryTheory.Adjunction.unit_naturality`, states that for any two categories `C` and `D`, with functors `F` from `C` to `D` and `G` from `D` to `C` forming an adjunction denoted by `adj`, and for any two objects `X` and `Y` in category `C` with a morphism `f` from `X` to `Y`, the composition of the unit of the adjunction at `X` and the map from `G` applied to the map from `F` applied to `f`, is equal to the composition of `f` and the unit of the adjunction at `Y`.
In simpler terms, it shows the naturality of the unit of an adjunction in the context of category theory.
More concisely: For any adjunction between categories `C` and `D` given by functors `F: C -> D` and `G: D -> C`, and for any objects `X, Y in C` and morphism `f: X -> Y`, the units `ηx: X -> F(X)` and `ηy: Y -> G(Y)` satisfy `F(f) ∘ ηx = ηy ∘ f`.
|
CategoryTheory.Adjunction.eq_homEquiv_apply
theorem CategoryTheory.Adjunction.eq_homEquiv_apply :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B),
g = (adj.homEquiv A B) f ↔ (adj.homEquiv A B).symm g = f
This theorem states that for any given two categories `C` and `D`, and functors `F : C -> D` and `G : D -> C` creating an adjunction `F ⊣ G`, then for any objects `A` in `C` and `B` in `D`, and morphisms `f : F.obj A ⟶ B` in `D` and `g : A ⟶ G.obj B` in `C`, the morphism `g` is equivalent to the application of `adj.homEquiv A B` on `f` if and only if the morphism `f` is equal to the application of the inverse of `adj.homEquiv A B` on `g`.
In other words, this theorem tells us that in the context of adjunctions in category theory, going from `C` to `D` using `F` and then comparing to a morphism in `D` is the same as going the other way from `D` to `C` using `G` and then comparing to a morphism in `C`.
More concisely: For any adjunction `F ⊣ G` between categories `C` and `D`, the natural transformation `adj.homEquiv A B` is an equivalence between `F(g)` and `g · adj.homEquiv A B.symm`, for any objects `A` in `C` and `B` in `D` and morphisms `g : A ⟶ G(B)`.
|
CategoryTheory.Adjunction.left_triangle_components_assoc
theorem CategoryTheory.Adjunction.left_triangle_components_assoc :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) (X : C) {Z : D} (h : F.obj X ⟶ Z),
CategoryTheory.CategoryStruct.comp (F.map (adj.unit.app X))
(CategoryTheory.CategoryStruct.comp (adj.counit.app (F.obj X)) h) =
h
This theorem is about the "left triangle identity" in category theory. It states that, given categories `C` and `D` with functors `F` from `C` to `D` and `G` from `D` to `C` forming an adjunction (that is, `F` is left adjoint to `G`), for any object `X` in `C` and morphism `h` from the image of `X` under `F` to some object `Z` in `D`, composing the morphism given by applying `F` to the unit of the adjunction at `X` with the composition of the counit of the adjunction at `F(X)` and `h`, is the same as `h` itself. In terms of the usual diagrammatic formulation of the triangle identities, this corresponds to the fact that one can go directly from `F(X)` to `Z`, or alternatively first go via `G(F(F(X)))` and then to `Z`, and the two routes give the same result.
More concisely: Given functors `F: C -> D` and `G: D -> C` forming an adjunction, for any object `X` in `C` and morphism `h: F(X) -> Z` in `D`, the composition of `F(μX)` and `h`, and the composition of `h` with `γ(F(X))`, are equal in `D`, where `μX` is the unit of the adjunction at `X` and `γ(F(X))` is the counit of the adjunction at `F(X)`.
|
CategoryTheory.Adjunction.homEquiv_naturality_left_symm
theorem CategoryTheory.Adjunction.homEquiv_naturality_left_symm :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
(adj.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y).symm g)
The theorem `CategoryTheory.Adjunction.homEquiv_naturality_left_symm` states that for any categories `C` and `D`, functors `F` from `C` to `D` and `G` from `D` to `C`, and an adjunction `adj` between `F` and `G`, if we have objects `X` and `X'` in `C` and `Y` in `D`, and morphisms `f` from `X'` to `X` and `g` from `X` to `G.obj Y`, then applying the inverse of the `homEquiv` function of the adjunction to the composition of `f` and `g` is equal to the composition of the `F.map` of `f` and the inverse of the `homEquiv` function applied to `g`. This theorem describes a property of the hom-set bijection in an adjunction, specifically its compatibility with morphism composition in the 'left-naturality' sense when considering the inverse of the bijection.
More concisely: For any adjunction between functors and objects in categories, the application of the inverse of the adjunction's hom-set bijection to the composition of a morphism from one object to another in the source category followed by a morphism from the image of the first to the second in the target category, is equal to the composition of the functor's mapping of the first morphism and the inverse of the hom-set bijection applied to the second morphism.
|
CategoryTheory.Adjunction.right_triangle
theorem CategoryTheory.Adjunction.right_triangle :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G),
CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G adj.unit)
(CategoryTheory.whiskerRight adj.counit G) =
CategoryTheory.CategoryStruct.id (G.comp (CategoryTheory.Functor.id C))
The theorem `CategoryTheory.Adjunction.right_triangle` in Lean 4 states the right triangle identity in the context of category theory. Specifically, given any two categories `C` and `D`, and a pair of functors `F` from `C` to `D` and `G` from `D` to `C` forming an adjunction, the composition of the unit of the adjunction whiskered on the left with `G` and the counit of the adjunction whiskered on the right with `G` is equal to the identity morphism on the composition of `G` with the identity functor on `C`. In mathematical notation, this theorem can be expressed as $(G \dashv F) \Rightarrow G \eta \circ \epsilon G = 1_{G \circ 1_{C}}$, where $\eta$ and $\epsilon$ are the unit and counit of the adjunction respectively.
More concisely: Given an adjunction between functors F : C -> D and G : D -> C, the composition of G with the unit η and followed by the counit ε is equal to the identity morphism on the composition of G and the identity functor on C: G η . εG = 1\_(G . Id\_C).
|
CategoryTheory.Adjunction.CoreUnitCounit.left_triangle
theorem CategoryTheory.Adjunction.CoreUnitCounit.left_triangle :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(self : CategoryTheory.Adjunction.CoreUnitCounit F G),
CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight self.unit F)
(CategoryTheory.CategoryStruct.comp (F.associator G F).hom (CategoryTheory.whiskerLeft F self.counit)) =
CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F)
The theorem `CategoryTheory.Adjunction.CoreUnitCounit.left_triangle` states that for any two categories `C` and `D`, and functors `F` from `C` to `D` and `G` from `D` to `C` that are adjoint (as described by the structure `CategoryTheory.Adjunction.CoreUnitCounit F G`), the composition of the left unit transformation, the associator transformation, and the right counit transformation is equal to the identity natural transformation on the functor `F`. This composition represents one of the triangle identities in an adjunction between two categories in category theory. In terms of category theory, this can be written as `F ⟶ (F G) F ⟶ F (G F) ⟶ F = NatTrans.id F`.
More concisely: In the category theory of Lean 4, given an adjunction `F ⊣ G` between categories `C` and `D`, the left triangle identity holds, that is, `F ∘ unit (F, G) ∘ assoc (F, G) ∘ counit (F, G) = id F`.
|
CategoryTheory.Adjunction.homEquiv_counit
theorem CategoryTheory.Adjunction.homEquiv_counit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(self : F ⊣ G) {X : C} {Y : D} {g : X ⟶ G.obj Y},
(self.homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (self.counit.app Y)
This theorem states the naturality of the counit of an adjunction in category theory. Specifically, for any categories `C` and `D`, and functors `F` from `C` to `D` and `G` from `D` to `C` such that `F` is left adjoint to `G`, the theorem asserts that for any objects `X` in `C` and `Y` in `D`, and any morphism `g` from `X` to `G(Y)`, the inverse of the hom-set bijection (`homEquiv`) associated with the adjunction, evaluated at `g`, is equal to the composition of `F.map g` and the application of the counit of the adjunction to `Y`. This statement is a common property of adjunctions in category theory, encapsulating the interaction between the adjunction and the structure of the categories.
More concisely: For any left adjoint functor F : C -> D and right adjoint functor G : D -> C, and for any objects X in C and Y in D, and morphism g : X -> G(Y), the inverse of the adjunction hom-set bijection is equal to F.map g . counit(Y).
|
CategoryTheory.Adjunction.right_triangle_components
theorem CategoryTheory.Adjunction.right_triangle_components :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) (Y : D),
CategoryTheory.CategoryStruct.comp (adj.unit.app (G.obj Y)) (G.map (adj.counit.app Y)) =
CategoryTheory.CategoryStruct.id (G.obj Y)
This theorem is about the right triangle identity in the context of an adjunction in category theory. For any two categories `C` and `D`, and a pair of functors `F` (from `C` to `D`) and `G` (from `D` to `C`) that form an adjunction, the theorem asserts the following: for any object `Y` in `D`, the composition of the unit of the adjunction (applied to `G(Y)`) and the morphism `G` applied to the counit of the adjunction (applied to `Y`) is equal to the identity morphism on `G(Y)`. This is one of the defining properties of adjunctions in category theory, expressed in the language of Lean 4. This theorem is a formalization of the following diagrammatic identity for an adjunction, commonly referred to as the "right triangle identity":
```
G(F(G(Y))) ---> G(Y)
| |
| | id_{G(Y)}
V V
G(Y) ---> G(Y)
```
More concisely: For any adjunction between categories `C` and `D` given by functors `F: C -> D` and `G: D -> C`, and for any object `Y` in `D`, the composition of the unit `G(η_Y)` and the counit `η_G(Y)` is equal to the identity morphism `id_{G Y}`, i.e., `G(η_Y) ∘ η_G(Y) = id_ {G Y}`.
|
CategoryTheory.Adjunction.homEquiv_unit
theorem CategoryTheory.Adjunction.homEquiv_unit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(self : F ⊣ G) {X : C} {Y : D} {f : F.obj X ⟶ Y},
(self.homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (self.unit.app X) (G.map f)
This theorem, called "Naturality of the unit of an adjunction", states that for any categories `C` and `D`, functors `F` from `C` to `D` and `G` from `D` to `C` (such that `F` is left adjoint to `G`), and any objects `X` in `C` and `Y` in `D`, and morphism `f` from the object `F.obj X` to `Y` in `D`, the application of the hom-set equivalence (`homEquiv`) of the adjunction to `f` is equal to the composition of the application of the unit natural transformation of the adjunction to `X` and the image of `f` under the functor `G`. In mathematical terms, for an adjunction `F ⊣ G` and a morphism `f` in category `D`, the theorem is stating that `homEquiv(f) = unit(X) ∘ G(f)`.
More concisely: For any adjunction F ⊣ G between categories C and D, and any object X in C, morphism f from F(X) to Y in D, the hom-set equivalence of the adjunction applied to f equals the composition of the unit natural transformation of the adjunction evaluated at X with G(f): homEquiv(f) = unit(X) ∘ G(f).
|
CategoryTheory.Adjunction.counit_naturality
theorem CategoryTheory.Adjunction.counit_naturality :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) {X Y : D} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (F.map (G.map f)) (adj.counit.app Y) =
CategoryTheory.CategoryStruct.comp (adj.counit.app X) f
This theorem, `CategoryTheory.Adjunction.counit_naturality`, is about the properties of adjunctions in category theory. Specifically, for any categories `C` and `D`, a pair of functors `F : C -> D` and `G : D -> C` forming an adjunction `adj : F ⊣ G`, and any morphism `f : X ⟶ Y` in `D`, the theorem states that the composition of the `F`-mapped version of `G.map f` and the counit of the adjunction at `Y` is the same as the composition of the counit of the adjunction at `X` and `f`.
In mathematical terms, this corresponds to the naturality condition for the counit of an adjunction, which can be written as `F(G(f)) ⋅ counit_Y = counit_X ⋅ f` in the notation of category theory. This property is central to the definition of an adjunction in category theory.
More concisely: For any adjunction `F ⊣ G` between categories `C` and `D` and morphism `f : X ⟶ Y` in `D`, the composition of `F(G(f))` and the counit of `F` at `Y` equals the composition of the counit of `G` at `X` and `f`.
|
CategoryTheory.Adjunction.left_triangle
theorem CategoryTheory.Adjunction.left_triangle :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G),
CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight adj.unit F)
(CategoryTheory.whiskerLeft F adj.counit) =
CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).comp F)
This theorem is known as the "left triangle identity" for adjunctions in category theory. It states that for any two categories `C` and `D`, and for any two functors `F : C → D` and `G : D → C` forming an adjunction `F ⊣ G`, the composition of the morphism `adj.unit` whiskered on the right with `F` and the morphism `adj.counit` whiskered on the left with `F`, is equal to the identity morphism on the composition of the identity functor on `C` and the functor `F`. This is a fundamental property satisfied by all adjunctions in category theory.
More concisely: For any adjunction `F ⊣ G` between categories `C` and `D`, the composition of `F(adj.unit)` and `G` is equal to the identity function on `F`. In Lean syntax: `(F ∘ adj.unit) = id_on_fc : ∀{C : Type u1} {D : Type u2} [Category C] [Category D] (F : C → D) (G : D → C) (adj : F ⊣ G), F (adj.unit X) = X`.
|
CategoryTheory.Adjunction.CoreUnitCounit.right_triangle
theorem CategoryTheory.Adjunction.CoreUnitCounit.right_triangle :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(self : CategoryTheory.Adjunction.CoreUnitCounit F G),
CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G self.unit)
(CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.whiskerRight self.counit G)) =
CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C))
This theorem, named `CategoryTheory.Adjunction.CoreUnitCounit.right_triangle`, states that in the context of category theory, for any two categories `C` and `D`, and functors `F` from `C` to `D` and `G` from `D` to `C`, with an adjunction given by the `CoreUnitCounit` structure, the composition of the unit, the associator, and the counit is equal to the identity natural transformation.
More specifically, given the functors `F` and `G` creating an adjunction, the composition in question is `(G ⟶ G (F G) ⟶ (F G) F ⟶ G)`, where `G` is whiskered on the left by the unit of the adjunction, followed by the inverse of the associator for `F` and `G` whiskered on the right by the counit, resulting in the functor `G`. This composition is proven to be equal to the identity natural transformation on the composition of `G` and the identity functor on `C`.
More concisely: In the context of category theory, for any adjunction between functors F from C to D and G from D to C, the composition of unit, associator, and counit is equal to the identity natural transformation on the composition of G and the identity functor on C.
|
CategoryTheory.Adjunction.homEquiv_naturality_right
theorem CategoryTheory.Adjunction.homEquiv_naturality_right :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(adj : F ⊣ G) {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
(adj.homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) =
CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y) f) (G.map g)
This theorem states that given two categories `C` and `D`, with functors `F` and `G` forming an adjunction `F ⊣ G`, and morphisms `f : F.obj X ⟶ Y` and `g : Y ⟶ Y'`, the hom-set equivalence provided by the adjunction obeys a naturalness condition. This condition says that applying the hom-set equivalence to the composition `f ≫ g` is equivalent to first applying it to `f`, then post-composing with the morphism `G.map g`. This is a general property of adjunctions in category theory. In more mathematical terms, we could write it as `(adj.homEquiv X Y') (f ≫ g) = (adj.homEquiv X Y f) ≫ (G.map g)`.
More concisely: Given an adjunction between categories `F ⊣ G` and morphisms `f : F(X) → Y` and `g : Y → Y'`, the naturalness condition holds, that is, `(adj.homEquiv X Y' (f ≫ g)) = (adj.homEquiv X Y f) ≫ (G.map g)`.
|
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right
theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
(self : CategoryTheory.Adjunction.CoreHomEquiv F G) {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
(self.homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) =
CategoryTheory.CategoryStruct.comp ((self.homEquiv X Y) f) (G.map g)
This theorem, `CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right`, is a property that describes how the `homEquiv` function of an adjunction in category theory transforms compositions of morphisms from `F X` to `Y` to `Y'`. Given any two categories `C` and `D`, functors `F` from `C` to `D` and `G` from `D` to `C`, an adjunction between `F` and `G`, objects `X` in `C` and `Y`, `Y'` in `D`, and morphisms `f` from `F X` to `Y` and `g` from `Y` to `Y'`, it states that the hom-set equivalence for `X` and `Y'` applied to the composition of `f` and `g` is equivalent to the composition of the hom-set equivalence for `X` and `Y` applied to `f` and the mapping of `g` under `G`. This property is crucial in ensuring that the adjunction respects the categorical structure, in particular the composition of morphisms.
More concisely: Given an adjunction between functors F and G, the hom-set equivalence for compositions of morphisms F(X) → Y and Y → Y' is equivalent to the composition of the hom-set equivalence for F(X) → Y and the application of G on morphism Y → Y'.
|