CategoryTheory.transferNatTransSelf_counit
theorem CategoryTheory.transferNatTransSelf_counit :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : L₂ ⟶ L₁) (X : D),
CategoryTheory.CategoryStruct.comp (L₂.map (((CategoryTheory.transferNatTransSelf adj₁ adj₂) f).app X))
(adj₂.counit.app X) =
CategoryTheory.CategoryStruct.comp (f.app (R₁.obj X)) (adj₁.counit.app X)
This theorem, named `CategoryTheory.transferNatTransSelf_counit`, establishes a property of natural transformations in category theory. Given two categories `C` and `D` with respective functors `L₁`, `L₂`, `R₁` and `R₂`, and where `L₁` is left adjoint to `R₁` and `L₂` is left adjoint to `R₂`, the theorem states that for any natural transformation `f` from `L₂` to `L₁` and any object `X` in `D`, the composition of the mapping of the application of the transferred natural transformation at `X` through `L₂` and the application of the counit of the adjunction at `X` in `adj₂` is equal to the composition of the application of `f` at the object `R₁.obj X` and the application of the counit of the adjunction at `X` in `adj₁`. This is a key property of transferred natural transformations between adjunctions in category theory.
More concisely: For natural transformations `f` from the left adjoint `L₂` to the left adjoint `L₁` of functors `L₁`, `L₂`, `R₁`, and `R₂` between categories `C` and `D`, with adjunctions `adj₁` and `adj₂`, the composition of `L₂.apply f X` and `adj₂.counit X` equals the composition of `f.apply (R₁.obj X)` and `adj₁.counit X`.
|
CategoryTheory.transferNatTransSelf_of_iso
theorem CategoryTheory.transferNatTransSelf_of_iso :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : L₂ ⟶ L₁)
[inst_2 : CategoryTheory.IsIso ((CategoryTheory.transferNatTransSelf adj₁ adj₂) f)], CategoryTheory.IsIso f
This theorem states that if `f` is a natural transformation and the natural transformation transferred from `f` is an isomorphism in the context of category theory, then `f` itself is an isomorphism. It operates within two categories, `C` and `D`, with functors `L₁`, `L₂`, `R₁`, and `R₂` from `C` to `D` and `D` to `C`, respectively. The theorem also assumes that `L₁` is adjoint to `R₁` and `L₂` is adjoint to `R₂`. The converse of this theorem is provided by `transferNatTransSelf_iso`.
More concisely: If `f` is a natural transformation between categories `C` and `D` with adjoint functors `L₁ ⊣ R₁` and `L₂ ⊣ R₂`, and the transferred natural transformation `L₂ �circ f �circ R₁` is an isomorphism, then `f` is an isomorphism.
|
CategoryTheory.transferNatTransSelf_symm_of_iso
theorem CategoryTheory.transferNatTransSelf_symm_of_iso :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : R₁ ⟶ R₂)
[inst_2 : CategoryTheory.IsIso ((CategoryTheory.transferNatTransSelf adj₁ adj₂).symm f)],
CategoryTheory.IsIso f
This theorem states that if `f` is a natural transformation between two functors `R₁` and `R₂` from category `D` to category `C`, and the natural transformation that results from transferring `f` using two adjunctions `adj₁ : L₁ ⊣ R₁` and `adj₂ : L₂ ⊣ R₂` is an isomorphism, then `f` itself is also an isomorphism. In other words, the ability to reverse the transfer of a natural transformation from one adjunction to another implies that the original transformation is an isomorphism. The reverse statement is provided by the theorem `transferNatTransSelf_symm_iso`.
More concisely: If natural transformation `f` between functors `R₁` and `R₂` is the isomorphism image of itself under the adjunction transformations `adj₁` and `adj₂`, then `f` is an isomorphism.
|
CategoryTheory.unit_transferNatTransSelf
theorem CategoryTheory.unit_transferNatTransSelf :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : L₂ ⟶ L₁) (X : C),
CategoryTheory.CategoryStruct.comp (adj₁.unit.app X)
(((CategoryTheory.transferNatTransSelf adj₁ adj₂) f).app (L₁.obj X)) =
CategoryTheory.CategoryStruct.comp (adj₂.unit.app X) (R₂.map (f.app X))
The theorem `CategoryTheory.unit_transferNatTransSelf` states that for any two categories `C` and `D`, with `C` of type `u₁` and `D` of type `u₂`, and with category structures given by `inst` and `inst_1` respectively, for any two functors `L₁`, `L₂` from `C` to `D` and any two functors `R₁`, `R₂` from `D` to `C`, and for any natural transformations `f : L₂ ⟶ L₁`, if `L₁` is left adjoint to `R₁` (denoted `L₁ ⊣ R₁`) and `L₂` is left adjoint to `R₂` (denoted `L₂ ⊣ R₂`), then for any object `X` of `C`, the composition of the unit of the adjunction `adj₁` at `X` with the application of the natural transformation resulting from transferring `adj₁` to `adj₂` via `f` to `L₁.obj X` is equal to the composition of the unit of the adjunction `adj₂` at `X` with the mapping of the functor `R₂` applied to `f.app X`.
More concisely: For categories C and D, functors L₁, L₂, R₁, R₂ between them, and given left adjoints L₁ ⊣ R₁ and L₂ ⊣ R₂, the unit of the adjunction at an object X in C, applied to L₁.obj X and transferred via f, equals the unit of the adjunction at X in D, composed with R₂.app f.app X.
|
CategoryTheory.transferNatTransSelf_comp
theorem CategoryTheory.transferNatTransSelf_comp :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L₁ L₂ L₃ : CategoryTheory.Functor C D}
{R₁ R₂ R₃ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (f : L₂ ⟶ L₁)
(g : L₃ ⟶ L₂),
CategoryTheory.CategoryStruct.comp ((CategoryTheory.transferNatTransSelf adj₁ adj₂) f)
((CategoryTheory.transferNatTransSelf adj₂ adj₃) g) =
(CategoryTheory.transferNatTransSelf adj₁ adj₃) (CategoryTheory.CategoryStruct.comp g f)
This theorem, `CategoryTheory.transferNatTransSelf_comp`, concerns the composition of natural transformations in the context of category theory. More specifically, for any two categories `C` and `D`, and functors `L₁`, `L₂`, `L₃`, `R₁`, `R₂`, `R₃` between these categories, if `L₁`, `L₂`, `L₃` are left adjoint to `R₁`, `R₂`, `R₃` respectively, and there exist morphisms `f : L₂ ⟶ L₁` and `g : L₃ ⟶ L₂`, then the composition of the transferred natural transformations from `adj₁` to `adj₂` and from `adj₂` to `adj₃` is equal to the transferred natural transformation from `adj₁` to `adj₃` of the composition of the morphisms `g` and `f`. This highlights that the operation of transferring natural transformations respects the composition of morphisms.
More concisely: Given functors `L₁`, `L₂`, `L₃`, `R₁`, `R₂`, `R₃` between categories `C` and `D` with `L₁ ⊣ R₁`, `L₂ ⊣ R₂`, `L₃ ⊣ R₃`, if there exist morphisms `f : L₂ ⟶ L₁` and `g : L₃ ⟶ L₂`, then the transferred natural transformations `adj₁ ∘ adj₂` and `adj₁ ∘ adj₃ ∘ (g ∘ f)` are equal.
|
CategoryTheory.transferNatTransSelf_id
theorem CategoryTheory.transferNatTransSelf_id :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁),
(CategoryTheory.transferNatTransSelf adj₁ adj₁) (CategoryTheory.CategoryStruct.id L₁) =
CategoryTheory.CategoryStruct.id R₁
This theorem states that for any two categories `C` and `D` of types `u₁` and `u₂` respectively, and any two functors `L₁` and `R₁` from `C` to `D` and from `D` to `C` respectively, if `L₁` is left adjoint to `R₁` (denoted as `L₁ ⊣ R₁`), then the natural transformation associated with the identity morphism on `L₁` under the transfer operation (i.e., `CategoryTheory.transferNatTransSelf adj₁ adj₁ (CategoryTheory.CategoryStruct.id L₁)`) is equal to the identity morphism on `R₁` (`CategoryTheory.CategoryStruct.id R₁`). In other words, the identity morphism on a functor is preserved under the adjunction transfer operation.
More concisely: For any functors `L₁ : C → D` and `R₁ : D → C` with `L₁` left adjoint to `R₁`, the natural transformation `transferNatTransSelf adj₁ adj₁ (id L₁)` equals `id R₁`.
|