Mate of natural transformations #
This file establishes the bijection between the 2-cells
L₁ R₁
C --→ D C ←-- D
G ↓ ↗ ↓ H G ↓ ↘ ↓ H
E --→ F E ←-- F
L₂ R₂
where L₁ ⊣ R₁ and L₂ ⊣ R₂. The corresponding natural transformations are called mates.
This bijection includes a number of interesting cases as specializations. For instance, in the
special case where G,H are identity functors then the bijection preserves and reflects
isomorphisms (i.e. we have bijections(L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂), and if either side is an iso then the
other side is as well). This demonstrates that adjoints to a given functor are unique up to
isomorphism (since if L₁ ≅ L₂ then we deduce R₁ ≅ R₂).
Another example arises from considering the square representing that a functor H preserves
products, in particular the morphism HA ⨯ H- ⟶ H(A ⨯ -). Then provided (A ⨯ -) and HA ⨯ -
have left adjoints (for instance if the relevant categories are cartesian closed), the transferred
natural transformation is the exponential comparison morphism: H(A ^ -) ⟶ HA ^ H-.
Furthermore if H has a left adjoint L, this morphism is an isomorphism iff its mate
L(HA ⨯ -) ⟶ A ⨯ L- is an isomorphism, see
https://ncatlab.org/nlab/show/Frobenius+reciprocity#InCategoryTheory.
This also relates to Grothendieck's yoga of six operations, though this is not spelled out in
mathlib: https://ncatlab.org/nlab/show/six+operations.
def
CategoryTheory.mateEquiv
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
{F : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Category.{v₄, u₄} F]
{G : CategoryTheory.Functor C E}
{H : CategoryTheory.Functor D F}
{L₁ : CategoryTheory.Functor C D}
{R₁ : CategoryTheory.Functor D C}
{L₂ : CategoryTheory.Functor E F}
{R₂ : CategoryTheory.Functor F E}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
:
Suppose we have a square of functors (where the top and bottom are adjunctions L₁ ⊣ R₁
and L₂ ⊣ R₂ respectively).
C ↔ D
G ↓ ↓ H
E ↔ F
Then we have a bijection between natural transformations G ⋙ L₂ ⟶ L₁ ⋙ H and
R₁ ⋙ G ⟶ H ⋙ R₂. This can be seen as a bijection of the 2-cells:
L₁ R₁
C --→ D C ←-- D
G ↓ ↗ ↓ H G ↓ ↘ ↓ H
E --→ F E ←-- F
L₂ R₂
Note that if one of the transformations is an iso, it does not imply the other is an iso.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.mateEquiv_apply
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
{F : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Category.{v₄, u₄} F]
{G : CategoryTheory.Functor C E}
{H : CategoryTheory.Functor D F}
{L₁ : CategoryTheory.Functor C D}
{R₁ : CategoryTheory.Functor D C}
{L₂ : CategoryTheory.Functor E F}
{R₂ : CategoryTheory.Functor F E}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : G.comp L₂ ⟶ L₁.comp H)
:
(CategoryTheory.mateEquiv adj₁ adj₂) α = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (R₁.comp G) adj₂.unit)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft R₁ α) R₂)
(CategoryTheory.whiskerRight adj₁.counit (H.comp R₂)))
@[simp]
theorem
CategoryTheory.mateEquiv_symm_apply
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
{F : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Category.{v₄, u₄} F]
{G : CategoryTheory.Functor C E}
{H : CategoryTheory.Functor D F}
{L₁ : CategoryTheory.Functor C D}
{R₁ : CategoryTheory.Functor D C}
{L₂ : CategoryTheory.Functor E F}
{R₂ : CategoryTheory.Functor F E}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(β : R₁.comp G ⟶ H.comp R₂)
:
(CategoryTheory.mateEquiv adj₁ adj₂).symm β = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight adj₁.unit (G.comp L₂))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft L₁ β) L₂)
(CategoryTheory.whiskerLeft (L₁.comp H) adj₂.counit))
@[deprecated CategoryTheory.mateEquiv]
def
CategoryTheory.transferNatTrans
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
{F : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Category.{v₄, u₄} F]
{G : CategoryTheory.Functor C E}
{H : CategoryTheory.Functor D F}
{L₁ : CategoryTheory.Functor C D}
{R₁ : CategoryTheory.Functor D C}
{L₂ : CategoryTheory.Functor E F}
{R₂ : CategoryTheory.Functor F E}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
:
Alias of CategoryTheory.mateEquiv.
Suppose we have a square of functors (where the top and bottom are adjunctions L₁ ⊣ R₁
and L₂ ⊣ R₂ respectively).
C ↔ D
G ↓ ↓ H
E ↔ F
Then we have a bijection between natural transformations G ⋙ L₂ ⟶ L₁ ⋙ H and
R₁ ⋙ G ⟶ H ⋙ R₂. This can be seen as a bijection of the 2-cells:
L₁ R₁
C --→ D C ←-- D
G ↓ ↗ ↓ H G ↓ ↘ ↓ H
E --→ F E ←-- F
L₂ R₂
Note that if one of the transformations is an iso, it does not imply the other is an iso.
Instances For
theorem
CategoryTheory.mateEquiv_counit
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
{F : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Category.{v₄, u₄} F]
{G : CategoryTheory.Functor C E}
{H : CategoryTheory.Functor D F}
{L₁ : CategoryTheory.Functor C D}
{R₁ : CategoryTheory.Functor D C}
{L₂ : CategoryTheory.Functor E F}
{R₂ : CategoryTheory.Functor F E}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : G.comp L₂ ⟶ L₁.comp H)
(d : D)
:
CategoryTheory.CategoryStruct.comp (L₂.map (((CategoryTheory.mateEquiv adj₁ adj₂) α).app d))
(adj₂.counit.app (H.obj d)) = CategoryTheory.CategoryStruct.comp (α.app (R₁.obj d)) (H.map (adj₁.counit.app d))
A component of a transposed version of the mates correspondence.
theorem
CategoryTheory.mateEquiv_counit_symm
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
{F : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Category.{v₄, u₄} F]
{G : CategoryTheory.Functor C E}
{H : CategoryTheory.Functor D F}
{L₁ : CategoryTheory.Functor C D}
{R₁ : CategoryTheory.Functor D C}
{L₂ : CategoryTheory.Functor E F}
{R₂ : CategoryTheory.Functor F E}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : R₁.comp G ⟶ H.comp R₂)
(d : D)
:
CategoryTheory.CategoryStruct.comp (L₂.map (α.app d)) (adj₂.counit.app (H.obj d)) = CategoryTheory.CategoryStruct.comp (((CategoryTheory.mateEquiv adj₁ adj₂).symm α).app (R₁.obj d))
(H.map (adj₁.counit.app d))
A component of a transposed version of the inverse mates correspondence.
theorem
CategoryTheory.unit_mateEquiv
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
{F : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Category.{v₄, u₄} F]
{G : CategoryTheory.Functor C E}
{H : CategoryTheory.Functor D F}
{L₁ : CategoryTheory.Functor C D}
{R₁ : CategoryTheory.Functor D C}
{L₂ : CategoryTheory.Functor E F}
{R₂ : CategoryTheory.Functor F E}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : G.comp L₂ ⟶ L₁.comp H)
(c : C)
:
CategoryTheory.CategoryStruct.comp (G.map (adj₁.unit.app c)) (((CategoryTheory.mateEquiv adj₁ adj₂) α).app (L₁.obj c)) = CategoryTheory.CategoryStruct.comp (adj₂.unit.app (G.obj ((CategoryTheory.Functor.id C).obj c)))
(R₂.map (α.app ((CategoryTheory.Functor.id C).obj c)))
theorem
CategoryTheory.unit_mateEquiv_symm
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
{F : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Category.{v₄, u₄} F]
{G : CategoryTheory.Functor C E}
{H : CategoryTheory.Functor D F}
{L₁ : CategoryTheory.Functor C D}
{R₁ : CategoryTheory.Functor D C}
{L₂ : CategoryTheory.Functor E F}
{R₂ : CategoryTheory.Functor F E}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : R₁.comp G ⟶ H.comp R₂)
(c : C)
:
CategoryTheory.CategoryStruct.comp (G.map (adj₁.unit.app c)) (α.app (L₁.obj c)) = CategoryTheory.CategoryStruct.comp (adj₂.unit.app (G.obj ((CategoryTheory.Functor.id C).obj c)))
(R₂.map (((CategoryTheory.mateEquiv adj₁ adj₂).symm α).app ((CategoryTheory.Functor.id C).obj c)))
A component of a transposed version of the inverse mates correspondence.
def
CategoryTheory.leftAdjointSquare.vcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
{G₁ : CategoryTheory.Functor A C}
{G₂ : CategoryTheory.Functor C E}
{H₁ : CategoryTheory.Functor B D}
{H₂ : CategoryTheory.Functor D F}
{L₁ : CategoryTheory.Functor A B}
{L₂ : CategoryTheory.Functor C D}
{L₃ : CategoryTheory.Functor E F}
:
Squares between left adjoints can be composed "vertically" by pasting.
Equations
Instances For
def
CategoryTheory.rightAdjointSquare.vcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
{G₁ : CategoryTheory.Functor A C}
{G₂ : CategoryTheory.Functor C E}
{H₁ : CategoryTheory.Functor B D}
{H₂ : CategoryTheory.Functor D F}
{R₁ : CategoryTheory.Functor B A}
{R₂ : CategoryTheory.Functor D C}
{R₃ : CategoryTheory.Functor F E}
:
Squares between right adjoints can be composed "vertically" by pasting.
Equations
Instances For
theorem
CategoryTheory.mateEquiv_vcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
{G₁ : CategoryTheory.Functor A C}
{G₂ : CategoryTheory.Functor C E}
{H₁ : CategoryTheory.Functor B D}
{H₂ : CategoryTheory.Functor D F}
{L₁ : CategoryTheory.Functor A B}
{R₁ : CategoryTheory.Functor B A}
{L₂ : CategoryTheory.Functor C D}
{R₂ : CategoryTheory.Functor D C}
{L₃ : CategoryTheory.Functor E F}
{R₃ : CategoryTheory.Functor F E}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(adj₃ : L₃ ⊣ R₃)
(α : G₁.comp L₂ ⟶ L₁.comp H₁)
(β : G₂.comp L₃ ⟶ L₂.comp H₂)
:
(CategoryTheory.mateEquiv adj₁ adj₃) (CategoryTheory.leftAdjointSquare.vcomp α β) = CategoryTheory.rightAdjointSquare.vcomp ((CategoryTheory.mateEquiv adj₁ adj₂) α)
((CategoryTheory.mateEquiv adj₂ adj₃) β)
The mates equivalence commutes with vertical composition.
def
CategoryTheory.leftAdjointSquare.hcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
{G : CategoryTheory.Functor A D}
{H : CategoryTheory.Functor B E}
{K : CategoryTheory.Functor C F}
{L₁ : CategoryTheory.Functor A B}
{L₂ : CategoryTheory.Functor D E}
{L₃ : CategoryTheory.Functor B C}
{L₄ : CategoryTheory.Functor E F}
:
Squares between left adjoints can be composed "horizontally" by pasting.
Equations
Instances For
def
CategoryTheory.rightAdjointSquare.hcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
{G : CategoryTheory.Functor A D}
{H : CategoryTheory.Functor B E}
{K : CategoryTheory.Functor C F}
{R₁ : CategoryTheory.Functor B A}
{R₂ : CategoryTheory.Functor E D}
{R₃ : CategoryTheory.Functor C B}
{R₄ : CategoryTheory.Functor F E}
:
Squares between right adjoints can be composed "horizontally" by pasting.
Equations
Instances For
theorem
CategoryTheory.mateEquiv_hcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
{G : CategoryTheory.Functor A D}
{H : CategoryTheory.Functor B E}
{K : CategoryTheory.Functor C F}
{L₁ : CategoryTheory.Functor A B}
{R₁ : CategoryTheory.Functor B A}
{L₂ : CategoryTheory.Functor D E}
{R₂ : CategoryTheory.Functor E D}
{L₃ : CategoryTheory.Functor B C}
{R₃ : CategoryTheory.Functor C B}
{L₄ : CategoryTheory.Functor E F}
{R₄ : CategoryTheory.Functor F E}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(adj₃ : L₃ ⊣ R₃)
(adj₄ : L₄ ⊣ R₄)
(α : G.comp L₂ ⟶ L₁.comp H)
(β : H.comp L₄ ⟶ L₃.comp K)
:
(CategoryTheory.mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (CategoryTheory.leftAdjointSquare.hcomp α β) = CategoryTheory.rightAdjointSquare.hcomp ((CategoryTheory.mateEquiv adj₁ adj₂) α)
((CategoryTheory.mateEquiv adj₃ adj₄) β)
The mates equivalence commutes with horizontal composition of squares.
def
CategoryTheory.leftAdjointSquare.comp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
{X : Type u₇}
{Y : Type u₈}
{Z : Type u₉}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
[CategoryTheory.Category.{v₇, u₇} X]
[CategoryTheory.Category.{v₈, u₈} Y]
[CategoryTheory.Category.{v₉, u₉} Z]
{G₁ : CategoryTheory.Functor A D}
{H₁ : CategoryTheory.Functor B E}
{K₁ : CategoryTheory.Functor C F}
{G₂ : CategoryTheory.Functor D X}
{H₂ : CategoryTheory.Functor E Y}
{K₂ : CategoryTheory.Functor F Z}
{L₁ : CategoryTheory.Functor A B}
{L₂ : CategoryTheory.Functor B C}
{L₃ : CategoryTheory.Functor D E}
{L₄ : CategoryTheory.Functor E F}
{L₅ : CategoryTheory.Functor X Y}
{L₆ : CategoryTheory.Functor Y Z}
(α : G₁.comp L₃ ⟶ L₁.comp H₁)
(β : H₁.comp L₄ ⟶ L₂.comp K₁)
(γ : G₂.comp L₅ ⟶ L₃.comp H₂)
(δ : H₂.comp L₆ ⟶ L₄.comp K₂)
:
(G₁.comp G₂).comp (L₅.comp L₆) ⟶ (L₁.comp L₂).comp (K₁.comp K₂)
Squares of squares between left adjoints can be composed by iterating vertical and horizontal composition.
Equations
Instances For
theorem
CategoryTheory.leftAdjointSquare.comp_vhcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
{X : Type u₇}
{Y : Type u₈}
{Z : Type u₉}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
[CategoryTheory.Category.{v₇, u₇} X]
[CategoryTheory.Category.{v₈, u₈} Y]
[CategoryTheory.Category.{v₉, u₉} Z]
{G₁ : CategoryTheory.Functor A D}
{H₁ : CategoryTheory.Functor B E}
{K₁ : CategoryTheory.Functor C F}
{G₂ : CategoryTheory.Functor D X}
{H₂ : CategoryTheory.Functor E Y}
{K₂ : CategoryTheory.Functor F Z}
{L₁ : CategoryTheory.Functor A B}
{L₂ : CategoryTheory.Functor B C}
{L₃ : CategoryTheory.Functor D E}
{L₄ : CategoryTheory.Functor E F}
{L₅ : CategoryTheory.Functor X Y}
{L₆ : CategoryTheory.Functor Y Z}
(α : G₁.comp L₃ ⟶ L₁.comp H₁)
(β : H₁.comp L₄ ⟶ L₂.comp K₁)
(γ : G₂.comp L₅ ⟶ L₃.comp H₂)
(δ : H₂.comp L₆ ⟶ L₄.comp K₂)
:
theorem
CategoryTheory.leftAdjointSquare.comp_hvcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
{X : Type u₇}
{Y : Type u₈}
{Z : Type u₉}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
[CategoryTheory.Category.{v₇, u₇} X]
[CategoryTheory.Category.{v₈, u₈} Y]
[CategoryTheory.Category.{v₉, u₉} Z]
{G₁ : CategoryTheory.Functor A D}
{H₁ : CategoryTheory.Functor B E}
{K₁ : CategoryTheory.Functor C F}
{G₂ : CategoryTheory.Functor D X}
{H₂ : CategoryTheory.Functor E Y}
{K₂ : CategoryTheory.Functor F Z}
{L₁ : CategoryTheory.Functor A B}
{L₂ : CategoryTheory.Functor B C}
{L₃ : CategoryTheory.Functor D E}
{L₄ : CategoryTheory.Functor E F}
{L₅ : CategoryTheory.Functor X Y}
{L₆ : CategoryTheory.Functor Y Z}
(α : G₁.comp L₃ ⟶ L₁.comp H₁)
(β : H₁.comp L₄ ⟶ L₂.comp K₁)
(γ : G₂.comp L₅ ⟶ L₃.comp H₂)
(δ : H₂.comp L₆ ⟶ L₄.comp K₂)
:
Horizontal and vertical composition of squares commutes.
def
CategoryTheory.rightAdjointSquare.comp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
{X : Type u₇}
{Y : Type u₈}
{Z : Type u₉}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
[CategoryTheory.Category.{v₇, u₇} X]
[CategoryTheory.Category.{v₈, u₈} Y]
[CategoryTheory.Category.{v₉, u₉} Z]
{G₁ : CategoryTheory.Functor A D}
{H₁ : CategoryTheory.Functor B E}
{K₁ : CategoryTheory.Functor C F}
{G₂ : CategoryTheory.Functor D X}
{H₂ : CategoryTheory.Functor E Y}
{K₂ : CategoryTheory.Functor F Z}
{R₁ : CategoryTheory.Functor B A}
{R₂ : CategoryTheory.Functor C B}
{R₃ : CategoryTheory.Functor E D}
{R₄ : CategoryTheory.Functor F E}
{R₅ : CategoryTheory.Functor Y X}
{R₆ : CategoryTheory.Functor Z Y}
(α : R₁.comp G₁ ⟶ H₁.comp R₃)
(β : R₂.comp H₁ ⟶ K₁.comp R₄)
(γ : R₃.comp G₂ ⟶ H₂.comp R₅)
(δ : R₄.comp H₂ ⟶ K₂.comp R₆)
:
(R₂.comp R₁).comp (G₁.comp G₂) ⟶ (K₁.comp K₂).comp (R₆.comp R₅)
Squares of squares between right adjoints can be composed by iterating vertical and horizontal composition.
Equations
Instances For
theorem
CategoryTheory.rightAdjointSquare.comp_vhcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
{X : Type u₇}
{Y : Type u₈}
{Z : Type u₉}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
[CategoryTheory.Category.{v₇, u₇} X]
[CategoryTheory.Category.{v₈, u₈} Y]
[CategoryTheory.Category.{v₉, u₉} Z]
{G₁ : CategoryTheory.Functor A D}
{H₁ : CategoryTheory.Functor B E}
{K₁ : CategoryTheory.Functor C F}
{G₂ : CategoryTheory.Functor D X}
{H₂ : CategoryTheory.Functor E Y}
{K₂ : CategoryTheory.Functor F Z}
{R₁ : CategoryTheory.Functor B A}
{R₂ : CategoryTheory.Functor C B}
{R₃ : CategoryTheory.Functor E D}
{R₄ : CategoryTheory.Functor F E}
{R₅ : CategoryTheory.Functor Y X}
{R₆ : CategoryTheory.Functor Z Y}
(α : R₁.comp G₁ ⟶ H₁.comp R₃)
(β : R₂.comp H₁ ⟶ K₁.comp R₄)
(γ : R₃.comp G₂ ⟶ H₂.comp R₅)
(δ : R₄.comp H₂ ⟶ K₂.comp R₆)
:
theorem
CategoryTheory.rightAdjointSquare.comp_hvcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
{X : Type u₇}
{Y : Type u₈}
{Z : Type u₉}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
[CategoryTheory.Category.{v₇, u₇} X]
[CategoryTheory.Category.{v₈, u₈} Y]
[CategoryTheory.Category.{v₉, u₉} Z]
{G₁ : CategoryTheory.Functor A D}
{H₁ : CategoryTheory.Functor B E}
{K₁ : CategoryTheory.Functor C F}
{G₂ : CategoryTheory.Functor D X}
{H₂ : CategoryTheory.Functor E Y}
{K₂ : CategoryTheory.Functor F Z}
{R₁ : CategoryTheory.Functor B A}
{R₂ : CategoryTheory.Functor C B}
{R₃ : CategoryTheory.Functor E D}
{R₄ : CategoryTheory.Functor F E}
{R₅ : CategoryTheory.Functor Y X}
{R₆ : CategoryTheory.Functor Z Y}
(α : R₁.comp G₁ ⟶ H₁.comp R₃)
(β : R₂.comp H₁ ⟶ K₁.comp R₄)
(γ : R₃.comp G₂ ⟶ H₂.comp R₅)
(δ : R₄.comp H₂ ⟶ K₂.comp R₆)
:
Horizontal and vertical composition of squares commutes.
theorem
CategoryTheory.mateEquiv_square
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
{E : Type u₅}
{F : Type u₆}
{X : Type u₇}
{Y : Type u₈}
{Z : Type u₉}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
[CategoryTheory.Category.{v₅, u₅} E]
[CategoryTheory.Category.{v₆, u₆} F]
[CategoryTheory.Category.{v₇, u₇} X]
[CategoryTheory.Category.{v₈, u₈} Y]
[CategoryTheory.Category.{v₉, u₉} Z]
{G₁ : CategoryTheory.Functor A D}
{H₁ : CategoryTheory.Functor B E}
{K₁ : CategoryTheory.Functor C F}
{G₂ : CategoryTheory.Functor D X}
{H₂ : CategoryTheory.Functor E Y}
{K₂ : CategoryTheory.Functor F Z}
{L₁ : CategoryTheory.Functor A B}
{R₁ : CategoryTheory.Functor B A}
{L₂ : CategoryTheory.Functor B C}
{R₂ : CategoryTheory.Functor C B}
{L₃ : CategoryTheory.Functor D E}
{R₃ : CategoryTheory.Functor E D}
{L₄ : CategoryTheory.Functor E F}
{R₄ : CategoryTheory.Functor F E}
{L₅ : CategoryTheory.Functor X Y}
{R₅ : CategoryTheory.Functor Y X}
{L₆ : CategoryTheory.Functor Y Z}
{R₆ : CategoryTheory.Functor Z Y}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(adj₃ : L₃ ⊣ R₃)
(adj₄ : L₄ ⊣ R₄)
(adj₅ : L₅ ⊣ R₅)
(adj₆ : L₆ ⊣ R₆)
(α : G₁.comp L₃ ⟶ L₁.comp H₁)
(β : H₁.comp L₄ ⟶ L₂.comp K₁)
(γ : G₂.comp L₅ ⟶ L₃.comp H₂)
(δ : H₂.comp L₆ ⟶ L₄.comp K₂)
:
(CategoryTheory.mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (CategoryTheory.leftAdjointSquare.comp α β γ δ) = CategoryTheory.rightAdjointSquare.comp ((CategoryTheory.mateEquiv adj₁ adj₃) α)
((CategoryTheory.mateEquiv adj₂ adj₄) β) ((CategoryTheory.mateEquiv adj₃ adj₅) γ)
((CategoryTheory.mateEquiv adj₄ adj₆) δ)
The mates equivalence commutes with composition of squares of squares. These results form the basis for an isomorphism of double categories to be proven later.
def
CategoryTheory.conjugateEquiv
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
:
Given two adjunctions L₁ ⊣ R₁ and L₂ ⊣ R₂ both between categories C, D, there is a
bijection between natural transformations L₂ ⟶ L₁ and natural transformations R₁ ⟶ R₂. This is
defined as a special case of mateEquiv, where the two "vertical" functors are identity, modulo
composition with the unitors. Corresponding natural transformations are called conjugateEquiv.
TODO: Generalise to when the two vertical functors are equivalences rather than being exactly 𝟭.
Furthermore, this bijection preserves (and reflects) isomorphisms, i.e. a transformation is an iso
iff its image under the bijection is an iso, see eg CategoryTheory.conjugateIsoEquiv.
This is in contrast to the general case mateEquiv which does not in general have this property.
Equations
- CategoryTheory.conjugateEquiv adj₁ adj₂ = Trans.trans (Trans.trans (L₂.leftUnitor.homCongr L₁.rightUnitor).symm (CategoryTheory.mateEquiv adj₁ adj₂)) (R₁.rightUnitor.homCongr R₂.leftUnitor)
Instances For
@[simp]
theorem
CategoryTheory.conjugateEquiv_apply_app
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(a✝ : L₂ ⟶ L₁)
(X : D)
:
((CategoryTheory.conjugateEquiv adj₁ adj₂) a✝).app X = CategoryTheory.CategoryStruct.comp (adj₂.unit.app (R₁.obj X))
(CategoryTheory.CategoryStruct.comp (R₂.map (a✝.app (R₁.obj X))) (R₂.map (adj₁.counit.app X)))
@[simp]
theorem
CategoryTheory.conjugateEquiv_symm_apply_app
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(a✝ : R₁ ⟶ R₂)
(X : C)
:
((CategoryTheory.conjugateEquiv adj₁ adj₂).symm a✝).app X = CategoryTheory.CategoryStruct.comp (L₂.map (adj₁.unit.app X))
(CategoryTheory.CategoryStruct.comp (L₂.map (a✝.app (L₁.obj X))) (adj₂.counit.app (L₁.obj X)))
@[deprecated CategoryTheory.conjugateEquiv]
def
CategoryTheory.transferNatTransSelf
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
:
Alias of CategoryTheory.conjugateEquiv.
Given two adjunctions L₁ ⊣ R₁ and L₂ ⊣ R₂ both between categories C, D, there is a
bijection between natural transformations L₂ ⟶ L₁ and natural transformations R₁ ⟶ R₂. This is
defined as a special case of mateEquiv, where the two "vertical" functors are identity, modulo
composition with the unitors. Corresponding natural transformations are called conjugateEquiv.
TODO: Generalise to when the two vertical functors are equivalences rather than being exactly 𝟭.
Furthermore, this bijection preserves (and reflects) isomorphisms, i.e. a transformation is an iso
iff its image under the bijection is an iso, see eg CategoryTheory.conjugateIsoEquiv.
This is in contrast to the general case mateEquiv which does not in general have this property.
Instances For
theorem
CategoryTheory.conjugateEquiv_counit
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : L₂ ⟶ L₁)
(d : D)
:
CategoryTheory.CategoryStruct.comp (L₂.map (((CategoryTheory.conjugateEquiv adj₁ adj₂) α).app d)) (adj₂.counit.app d) = CategoryTheory.CategoryStruct.comp (α.app (R₁.obj d)) (adj₁.counit.app d)
A component of a transposed form of the conjugation definition.
theorem
CategoryTheory.conjugateEquiv_counit_symm
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : R₁ ⟶ R₂)
(d : D)
:
CategoryTheory.CategoryStruct.comp (L₂.map (α.app d)) (adj₂.counit.app d) = CategoryTheory.CategoryStruct.comp (((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α).app (R₁.obj d))
(adj₁.counit.app d)
A component of a transposed form of the inverse conjugation definition.
theorem
CategoryTheory.unit_conjugateEquiv
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : L₂ ⟶ L₁)
(c : C)
:
CategoryTheory.CategoryStruct.comp (adj₁.unit.app c) (((CategoryTheory.conjugateEquiv adj₁ adj₂) α).app (L₁.obj c)) = CategoryTheory.CategoryStruct.comp (adj₂.unit.app c) (R₂.map (α.app c))
A component of a transposed form of the conjugation definition.
theorem
CategoryTheory.unit_conjugateEquiv_symm
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : R₁ ⟶ R₂)
(c : C)
:
CategoryTheory.CategoryStruct.comp (adj₁.unit.app c) (α.app (L₁.obj c)) = CategoryTheory.CategoryStruct.comp (adj₂.unit.app c)
(R₂.map (((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α).app c))
A component of a transposed form of the inverse conjugation definition.
@[simp]
theorem
CategoryTheory.conjugateEquiv_id
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ : CategoryTheory.Functor C D}
{R₁ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
:
@[simp]
theorem
CategoryTheory.conjugateEquiv_symm_id
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ : CategoryTheory.Functor C D}
{R₁ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
:
(CategoryTheory.conjugateEquiv adj₁ adj₁).symm (CategoryTheory.CategoryStruct.id R₁) = CategoryTheory.CategoryStruct.id L₁
theorem
CategoryTheory.conjugateEquiv_adjunction_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{L R : CategoryTheory.Functor C C}
(adj : L ⊣ R)
(α : CategoryTheory.Functor.id C ⟶ L)
(c : C)
:
((CategoryTheory.conjugateEquiv adj CategoryTheory.Adjunction.id) α).app c = CategoryTheory.CategoryStruct.comp (α.app (R.obj c)) (adj.counit.app c)
theorem
CategoryTheory.conjugateEquiv_adjunction_id_symm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{L R : CategoryTheory.Functor C C}
(adj : L ⊣ R)
(α : R ⟶ CategoryTheory.Functor.id C)
(c : C)
:
((CategoryTheory.conjugateEquiv adj CategoryTheory.Adjunction.id).symm α).app c = CategoryTheory.CategoryStruct.comp (adj.unit.app c) (α.app (L.obj c))
@[simp]
theorem
CategoryTheory.conjugateEquiv_comp
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[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₃)
(α : L₂ ⟶ L₁)
(β : L₃ ⟶ L₂)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)
((CategoryTheory.conjugateEquiv adj₂ adj₃) β) = (CategoryTheory.conjugateEquiv adj₁ adj₃) (CategoryTheory.CategoryStruct.comp β α)
@[simp]
theorem
CategoryTheory.conjugateEquiv_symm_comp
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[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₃)
(α : R₁ ⟶ R₂)
(β : R₂ ⟶ R₃)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₂ adj₃).symm β)
((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α) = (CategoryTheory.conjugateEquiv adj₁ adj₃).symm (CategoryTheory.CategoryStruct.comp α β)
theorem
CategoryTheory.conjugateEquiv_comm
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
{α : L₂ ⟶ L₁}
{β : L₁ ⟶ L₂}
(βα : CategoryTheory.CategoryStruct.comp β α = CategoryTheory.CategoryStruct.id L₁)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)
((CategoryTheory.conjugateEquiv adj₂ adj₁) β) = CategoryTheory.CategoryStruct.id R₁
theorem
CategoryTheory.conjugateEquiv_symm_comm
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
{α : R₁ ⟶ R₂}
{β : R₂ ⟶ R₁}
(αβ : CategoryTheory.CategoryStruct.comp α β = CategoryTheory.CategoryStruct.id R₁)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₂ adj₁).symm β)
((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α) = CategoryTheory.CategoryStruct.id L₁
instance
CategoryTheory.conjugateEquiv_iso
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : L₂ ⟶ L₁)
[CategoryTheory.IsIso α]
:
CategoryTheory.IsIso ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)
If α is an isomorphism between left adjoints, then its conjugate transformation is an
isomorphism. The converse is given in conjugateEquiv_of_iso.
Equations
- ⋯ = ⋯
instance
CategoryTheory.conjugateEquiv_symm_iso
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : R₁ ⟶ R₂)
[CategoryTheory.IsIso α]
:
CategoryTheory.IsIso ((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α)
If α is an isomorphism between right adjoints, then its conjugate transformation is an
isomorphism. The converse is given in conjugateEquiv_symm_of_iso.
Equations
- ⋯ = ⋯
theorem
CategoryTheory.conjugateEquiv_of_iso
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : L₂ ⟶ L₁)
[CategoryTheory.IsIso ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)]
:
If α is a natural transformation between left adjoints whose conjugate natural transformation
is an isomorphism, then α is an isomorphism. The converse is given in Conjugate_iso.
theorem
CategoryTheory.conjugateEquiv_symm_of_iso
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : R₁ ⟶ R₂)
[CategoryTheory.IsIso ((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α)]
:
If α is a natural transformation between right adjoints whose conjugate natural transformation is
an isomorphism, then α is an isomorphism. The converse is given in conjugateEquiv_symm_iso.
def
CategoryTheory.conjugateIsoEquiv
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
:
Thus conjugation defines an equivalence between natural isomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.conjugateIsoEquiv_apply_hom
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : L₂ ≅ L₁)
:
((CategoryTheory.conjugateIsoEquiv adj₁ adj₂) α).hom = (CategoryTheory.conjugateEquiv adj₁ adj₂) α.hom
@[simp]
theorem
CategoryTheory.conjugateIsoEquiv_symm_apply_inv
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(β : R₁ ≅ R₂)
:
((CategoryTheory.conjugateIsoEquiv adj₁ adj₂).symm β).inv = (CategoryTheory.conjugateEquiv adj₂ adj₁).symm β.inv
@[simp]
theorem
CategoryTheory.conjugateIsoEquiv_symm_apply_hom
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(β : R₁ ≅ R₂)
:
((CategoryTheory.conjugateIsoEquiv adj₁ adj₂).symm β).hom = (CategoryTheory.conjugateEquiv adj₁ adj₂).symm β.hom
@[simp]
theorem
CategoryTheory.conjugateIsoEquiv_apply_inv
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L₁ L₂ : CategoryTheory.Functor C D}
{R₁ R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(α : L₂ ≅ L₁)
:
((CategoryTheory.conjugateIsoEquiv adj₁ adj₂) α).inv = (CategoryTheory.conjugateEquiv adj₂ adj₁) α.inv
theorem
CategoryTheory.iterated_mateEquiv_conjugateEquiv
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
{F₁ : CategoryTheory.Functor A C}
{U₁ : CategoryTheory.Functor C A}
{F₂ : CategoryTheory.Functor B D}
{U₂ : CategoryTheory.Functor D B}
{L₁ : CategoryTheory.Functor A B}
{R₁ : CategoryTheory.Functor B A}
{L₂ : CategoryTheory.Functor C D}
{R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(adj₃ : F₁ ⊣ U₁)
(adj₄ : F₂ ⊣ U₂)
(α : F₁.comp L₂ ⟶ L₁.comp F₂)
:
(CategoryTheory.mateEquiv adj₄ adj₃) ((CategoryTheory.mateEquiv adj₁ adj₂) α) = (CategoryTheory.conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α
When all four functors in a sequare are left adjoints, the mates operation can be iterated:
L₁ R₁ R₁
C --→ D C ←-- D C ←-- D
F₁ ↓ ↗ ↓ F₂ F₁ ↓ ↘ ↓ F₂ U₁ ↑ ↙ ↑ U₂ E --→ F E ←-- F E ←-- F L₂ R₂ R₂
In this case the iterated mate equals the conjugate of the original transformation and is thus an isomorphism if and only if the original transformation is. This explains why some Beck-Chevalley natural transformations are natural isomorphisms.
theorem
CategoryTheory.iterated_mateEquiv_conjugateEquiv_symm
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
{F₁ : CategoryTheory.Functor A C}
{U₁ : CategoryTheory.Functor C A}
{F₂ : CategoryTheory.Functor B D}
{U₂ : CategoryTheory.Functor D B}
{L₁ : CategoryTheory.Functor A B}
{R₁ : CategoryTheory.Functor B A}
{L₂ : CategoryTheory.Functor C D}
{R₂ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(adj₃ : F₁ ⊣ U₁)
(adj₄ : F₂ ⊣ U₂)
(α : U₂.comp R₁ ⟶ R₂.comp U₁)
:
(CategoryTheory.mateEquiv adj₁ adj₂).symm ((CategoryTheory.mateEquiv adj₄ adj₃).symm α) = (CategoryTheory.conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm α
def
CategoryTheory.leftAdjointSquareConjugate.vcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
{G : CategoryTheory.Functor A C}
{H : CategoryTheory.Functor B D}
{L₁ : CategoryTheory.Functor A B}
{L₂ L₃ : CategoryTheory.Functor C D}
:
Composition of a squares between left adjoints with a conjugate square.
Equations
Instances For
def
CategoryTheory.rightAdjointSquareConjugate.vcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
{G : CategoryTheory.Functor A C}
{H : CategoryTheory.Functor B D}
{R₁ : CategoryTheory.Functor B A}
{R₂ R₃ : CategoryTheory.Functor D C}
:
Composition of a squares between right adjoints with a conjugate square.
Equations
Instances For
theorem
CategoryTheory.mateEquiv_conjugateEquiv_vcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
{G : CategoryTheory.Functor A C}
{H : CategoryTheory.Functor B D}
{L₁ : CategoryTheory.Functor A B}
{R₁ : CategoryTheory.Functor B A}
{L₂ : CategoryTheory.Functor C D}
{R₂ : CategoryTheory.Functor D C}
{L₃ : CategoryTheory.Functor C D}
{R₃ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(adj₃ : L₃ ⊣ R₃)
(α : G.comp L₂ ⟶ L₁.comp H)
(β : L₃ ⟶ L₂)
:
(CategoryTheory.mateEquiv adj₁ adj₃) (CategoryTheory.leftAdjointSquareConjugate.vcomp α β) = CategoryTheory.rightAdjointSquareConjugate.vcomp ((CategoryTheory.mateEquiv adj₁ adj₂) α)
((CategoryTheory.conjugateEquiv adj₂ adj₃) β)
The mates equivalence commutes with this composition, essentially by mateEquiv_vcomp.
def
CategoryTheory.leftAdjointConjugateSquare.vcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
{G : CategoryTheory.Functor A C}
{H : CategoryTheory.Functor B D}
{L₁ L₂ : CategoryTheory.Functor A B}
{L₃ : CategoryTheory.Functor C D}
:
Composition of a conjugate square with a squares between left adjoints.
Equations
Instances For
def
CategoryTheory.rightAdjointConjugateSquare.vcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
{G : CategoryTheory.Functor A C}
{H : CategoryTheory.Functor B D}
{R₁ R₂ : CategoryTheory.Functor B A}
{R₃ : CategoryTheory.Functor D C}
:
Composition of a conjugate square with a squares between right adjoints.
Equations
Instances For
theorem
CategoryTheory.conjugateEquiv_mateEquiv_vcomp
{A : Type u₁}
{B : Type u₂}
{C : Type u₃}
{D : Type u₄}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Category.{v₃, u₃} C]
[CategoryTheory.Category.{v₄, u₄} D]
{G : CategoryTheory.Functor A C}
{H : CategoryTheory.Functor B D}
{L₁ : CategoryTheory.Functor A B}
{R₁ : CategoryTheory.Functor B A}
{L₂ : CategoryTheory.Functor A B}
{R₂ : CategoryTheory.Functor B A}
{L₃ : CategoryTheory.Functor C D}
{R₃ : CategoryTheory.Functor D C}
(adj₁ : L₁ ⊣ R₁)
(adj₂ : L₂ ⊣ R₂)
(adj₃ : L₃ ⊣ R₃)
(α : L₂ ⟶ L₁)
(β : G.comp L₃ ⟶ L₂.comp H)
:
(CategoryTheory.mateEquiv adj₁ adj₃) (CategoryTheory.leftAdjointConjugateSquare.vcomp α β) = CategoryTheory.rightAdjointConjugateSquare.vcomp ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)
((CategoryTheory.mateEquiv adj₂ adj₃) β)
The mates equivalence commutes with this composition, essentially by mateEquiv_vcomp.