From 0d7d128377ca246afafa94dee1f6f1ba2ea11583 Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Wed, 10 Jul 2024 18:10:45 +0000 Subject: [PATCH] feat (Category Theory): redefine and extend mates (#13840) The mates bijection between natural transformations inhabiting a certain dual pairs of squares (the duality in the sense of a parallel pair of adjunctions) can be defined in a more direct way: using pasting composition on 2-cells. This pull request: (i) proposes a new definition of `Mates` to replace and rename the existing `transferNatTrans` (ii) proposes a new definition of `Conjugates` to replace and rename the existing `transferNatTransSelf` (iii) proves that the mates correspondence commutes with horizontal and vertical composition of squares, as well as some coherences relating mates to conjugates (iv) updates the files that depends on this, involving two new proofs about exponentiation in cartesian closed categories --- Mathlib/CategoryTheory/Adjunction/Mates.lean | 702 +++++++++++++----- Mathlib/CategoryTheory/Closed/Cartesian.lean | 8 +- Mathlib/CategoryTheory/Closed/Functor.lean | 89 ++- Mathlib/CategoryTheory/Closed/Monoidal.lean | 10 +- .../Limits/Shapes/BinaryProducts.lean | 17 +- 5 files changed, 610 insertions(+), 216 deletions(-) diff --git a/Mathlib/CategoryTheory/Adjunction/Mates.lean b/Mathlib/CategoryTheory/Adjunction/Mates.lean index a16de6016fa72..0605105cd80cf 100644 --- a/Mathlib/CategoryTheory/Adjunction/Mates.lean +++ b/Mathlib/CategoryTheory/Adjunction/Mates.lean @@ -1,10 +1,16 @@ /- Copyright (c) 2020 Bhavik Mehta. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Bhavik Mehta +Authors: Bhavik Mehta, Emily Riehl -/ import Mathlib.CategoryTheory.Adjunction.Basic import Mathlib.CategoryTheory.Conj +import Mathlib.CategoryTheory.Category.Basic +import Mathlib.CategoryTheory.Functor.Basic +import Mathlib.CategoryTheory.Functor.Category +import Mathlib.CategoryTheory.Whiskering + +import Mathlib.Tactic.ApplyFun #align_import category_theory.adjunction.mates from "leanprover-community/mathlib"@"cea27692b3fdeb328a2ddba6aabf181754543184" @@ -19,18 +25,17 @@ This file establishes the bijection between the 2-cells E --→ F E ←-- F L₂ R₂ -where `L₁ ⊣ R₁` and `L₂ ⊣ R₂`, and shows that in the special case where `G,H` are identity 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). +where `L₁ ⊣ R₁` and `L₂ ⊣ R₂`. The corresponding natural transformations are called mates. -On its own, this bijection is not particularly useful but it includes a number of interesting cases -as specializations. +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₂`). -For instance, this generalises the fact that adjunctions are unique (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 +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 @@ -39,31 +44,27 @@ This also relates to Grothendieck's yoga of six operations, though this is not s mathlib: https://ncatlab.org/nlab/show/six+operations. -/ - -universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄ - +universe v₁ v₂ v₃ v₄ v₅ v₆ v₇ v₈ v₉ u₁ u₂ u₃ u₄ u₅ u₆ u₇ u₈ u₉ namespace CategoryTheory -open Category +open Category Functor Adjunction NatTrans -variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] +section mateEquiv -section Square - -variable {E : Type u₃} {F : Type u₄} [Category.{v₃} E] [Category.{v₄} F] +variable {C : Type u₁} {D : Type u₂}{E : Type u₃} {F : Type u₄} +variable [Category.{v₁} C] [Category.{v₂} D][Category.{v₃} E] [Category.{v₄} F] variable {G : C ⥤ E} {H : D ⥤ F} {L₁ : C ⥤ D} {R₁ : D ⥤ C} {L₂ : E ⥤ F} {R₂ : F ⥤ E} variable (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). +/-- 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: +`R₁ ⋙ G ⟶ H ⋙ R₂`. This can be seen as a bijection of the 2-cells: L₁ R₁ C --→ D C ←-- D @@ -73,199 +74,558 @@ This can be seen as a bijection of the 2-cells: Note that if one of the transformations is an iso, it does not imply the other is an iso. -/ -def transferNatTrans : (G ⋙ L₂ ⟶ L₁ ⋙ H) ≃ (R₁ ⋙ G ⟶ H ⋙ R₂) where - toFun h := - { app := fun X => adj₂.unit.app _ ≫ R₂.map (h.app _ ≫ H.map (adj₁.counit.app _)) - naturality := fun X Y f => by - dsimp - rw [assoc, ← R₂.map_comp, assoc, ← H.map_comp, ← adj₁.counit_naturality, H.map_comp, ← - Functor.comp_map L₁, ← h.naturality_assoc] - simp } - invFun h := - { app := fun X => L₂.map (G.map (adj₁.unit.app _) ≫ h.app _) ≫ adj₂.counit.app _ - naturality := fun X Y f => by - dsimp - rw [← L₂.map_comp_assoc, ← G.map_comp_assoc, ← adj₁.unit_naturality, G.map_comp_assoc, ← - Functor.comp_map, h.naturality] - simp } - left_inv h := by - ext X - dsimp - simp only [L₂.map_comp, assoc, adj₂.counit_naturality, adj₂.left_triangle_components_assoc, ← - Functor.comp_map G L₂, h.naturality_assoc, Functor.comp_map L₁, ← H.map_comp, - adj₁.left_triangle_components] - dsimp - simp only [id_comp, ← Functor.comp_map, ← Functor.comp_obj, NatTrans.naturality_assoc] - simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp] - have : Prefunctor.map L₁.toPrefunctor (NatTrans.app adj₁.unit X) ≫ - NatTrans.app adj₁.counit (Prefunctor.obj L₁.toPrefunctor X) = 𝟙 _ := by simp - simp [this] - -- See library note [dsimp, simp]. - right_inv h := by - ext X - dsimp - simp [-Functor.comp_map, ← Functor.comp_map H, Functor.comp_map R₁, -NatTrans.naturality, ← - h.naturality, -Functor.map_comp, ← Functor.map_comp_assoc G, R₂.map_comp] -#align category_theory.transfer_nat_trans CategoryTheory.transferNatTrans - -theorem transferNatTrans_counit (f : G ⋙ L₂ ⟶ L₁ ⋙ H) (Y : D) : - L₂.map ((transferNatTrans adj₁ adj₂ f).app _) ≫ adj₂.counit.app _ = - f.app _ ≫ H.map (adj₁.counit.app Y) := by - erw [Functor.map_comp] - simp -#align category_theory.transfer_nat_trans_counit CategoryTheory.transferNatTrans_counit - -theorem unit_transferNatTrans (f : G ⋙ L₂ ⟶ L₁ ⋙ H) (X : C) : - G.map (adj₁.unit.app X) ≫ (transferNatTrans adj₁ adj₂ f).app _ = - adj₂.unit.app _ ≫ R₂.map (f.app _) := by - dsimp [transferNatTrans] - rw [← adj₂.unit_naturality_assoc, ← R₂.map_comp, ← Functor.comp_map G L₂, f.naturality_assoc, - Functor.comp_map, ← H.map_comp] - dsimp; simp -#align category_theory.unit_transfer_nat_trans CategoryTheory.unit_transferNatTrans - --- See library note [dsimp, simp] -end Square - -section Self +@[simps] +def mateEquiv : (G ⋙ L₂ ⟶ L₁ ⋙ H) ≃ (R₁ ⋙ G ⟶ H ⋙ R₂) where + toFun α := + whiskerLeft (R₁ ⋙ G) adj₂.unit ≫ + whiskerRight (whiskerLeft R₁ α) R₂ ≫ + whiskerRight adj₁.counit (H ⋙ R₂) + invFun β := + whiskerRight adj₁.unit (G ⋙ L₂) ≫ + whiskerRight (whiskerLeft L₁ β) L₂ ≫ + whiskerLeft (L₁ ⋙ H) adj₂.counit + left_inv α := by + ext + unfold whiskerRight whiskerLeft + simp only [comp_obj, id_obj, Functor.comp_map, comp_app, map_comp, assoc, counit_naturality, + counit_naturality_assoc, left_triangle_components_assoc] + rw [← assoc, ← Functor.comp_map, α.naturality, Functor.comp_map, assoc, ← H.map_comp, + left_triangle_components, map_id] + simp only [comp_obj, comp_id] + right_inv β := by + ext + unfold whiskerLeft whiskerRight + simp only [comp_obj, id_obj, Functor.comp_map, comp_app, map_comp, assoc, + unit_naturality_assoc, right_triangle_components_assoc] + rw [← assoc, ← Functor.comp_map, assoc, ← β.naturality, ← assoc, Functor.comp_map, + ← G.map_comp, right_triangle_components, map_id, id_comp] + +@[deprecated (since := "2024-07-09")] alias transferNatTrans := mateEquiv + +/-- A component of a transposed version of the mates correspondence. -/ +theorem mateEquiv_counit (α : G ⋙ L₂ ⟶ L₁ ⋙ H) (d : D) : + L₂.map ((mateEquiv adj₁ adj₂ α).app _) ≫ adj₂.counit.app _ = + α.app _ ≫ H.map (adj₁.counit.app d) := by + erw [Functor.map_comp]; simp + +/-- A component of a transposed version of the inverse mates correspondence. -/ +theorem mateEquiv_counit_symm (α : R₁ ⋙ G ⟶ H ⋙ R₂) (d : D) : + L₂.map (α.app _) ≫ adj₂.counit.app _ = + ((mateEquiv adj₁ adj₂).symm α).app _ ≫ H.map (adj₁.counit.app d) := by + conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α] + exact (mateEquiv_counit adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) d) + +/- A component of a transposed version of the mates correspondence. -/ +theorem unit_mateEquiv (α : G ⋙ L₂ ⟶ L₁ ⋙ H) (c : C) : + G.map (adj₁.unit.app c) ≫ (mateEquiv adj₁ adj₂ α).app _ = + adj₂.unit.app _ ≫ R₂.map (α.app _) := by + dsimp [mateEquiv] + rw [← adj₂.unit_naturality_assoc] + slice_lhs 2 3 => + rw [← R₂.map_comp, ← Functor.comp_map G L₂, α.naturality] + rw [R₂.map_comp] + slice_lhs 3 4 => + { + rw [← R₂.map_comp, Functor.comp_map L₁ H, ← H.map_comp, left_triangle_components] + } + simp only [comp_obj, map_id, comp_id] + +/-- A component of a transposed version of the inverse mates correspondence. -/ +theorem unit_mateEquiv_symm (α : R₁ ⋙ G ⟶ H ⋙ R₂) (c : C) : + G.map (adj₁.unit.app c) ≫ α.app _ = + adj₂.unit.app _ ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app _) := by + conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α] + exact (unit_mateEquiv adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) c) + +end mateEquiv + +section mateEquivVComp + +variable {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} +variable [Category.{v₁} A] [Category.{v₂} B][Category.{v₃} C] +variable [Category.{v₄} D] [Category.{v₅} E][Category.{v₆} F] +variable {G₁ : A ⥤ C}{G₂ : C ⥤ E}{H₁ : B ⥤ D}{H₂ : D ⥤ F} +variable {L₁ : A ⥤ B}{R₁ : B ⥤ A} {L₂ : C ⥤ D}{R₂ : D ⥤ C}{L₃ : E ⥤ F}{R₃ : F ⥤ E} +variable (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) -variable {L₁ L₂ L₃ : C ⥤ D} {R₁ R₂ R₃ : D ⥤ C} +/-- Squares between left adjoints can be composed "vertically" by pasting. -/ +def leftAdjointSquare.vcomp : + (G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁) → (G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂) → ((G₁ ⋙ G₂) ⋙ L₃ ⟶ L₁ ⋙ (H₁ ⋙ H₂)) := + fun α β ↦ (whiskerLeft G₁ β) ≫ (whiskerRight α H₂) + +/-- Squares between right adjoints can be composed "vertically" by pasting. -/ +def rightAdjointSquare.vcomp : + (R₁ ⋙ G₁ ⟶ H₁ ⋙ R₂) → (R₂ ⋙ G₂ ⟶ H₂ ⋙ R₃) → (R₁ ⋙ (G₁ ⋙ G₂) ⟶ (H₁ ⋙ H₂) ⋙ R₃) := + fun α β ↦ (whiskerRight α G₂) ≫ (whiskerLeft H₁ β) + +/-- The mates equivalence commutes with vertical composition. -/ +theorem mateEquiv_vcomp + (α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁) (β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂) : + (mateEquiv (G := G₁ ⋙ G₂) (H := H₁ ⋙ H₂) adj₁ adj₃) (leftAdjointSquare.vcomp α β) = + rightAdjointSquare.vcomp (mateEquiv adj₁ adj₂ α) (mateEquiv adj₂ adj₃ β) := by + unfold leftAdjointSquare.vcomp rightAdjointSquare.vcomp mateEquiv + ext b + simp only [comp_obj, Equiv.coe_fn_mk, whiskerLeft_comp, whiskerLeft_twice, whiskerRight_comp, + assoc, comp_app, whiskerLeft_app, whiskerRight_app, id_obj, Functor.comp_map, + whiskerRight_twice] + slice_rhs 1 4 => + { + rw [← assoc, ← assoc, ← unit_naturality (adj₃)] + } + rw [L₃.map_comp, R₃.map_comp] + slice_rhs 2 4 => + { + rw [← R₃.map_comp, ← R₃.map_comp, ← assoc, ← L₃.map_comp, ← G₂.map_comp, ← G₂.map_comp] + rw [← Functor.comp_map G₂ L₃, β.naturality] + } + rw [(L₂ ⋙ H₂).map_comp, R₃.map_comp, R₃.map_comp] + slice_rhs 4 5 => + { + rw [← R₃.map_comp, Functor.comp_map L₂ _, ← Functor.comp_map _ L₂, ← H₂.map_comp] + rw [adj₂.counit.naturality] + } + simp only [comp_obj, Functor.comp_map, map_comp, id_obj, Functor.id_map, assoc] + slice_rhs 4 5 => + { + rw [← R₃.map_comp, ← H₂.map_comp, ← Functor.comp_map _ L₂, adj₂.counit.naturality] + } + simp only [comp_obj, id_obj, Functor.id_map, map_comp, assoc] + slice_rhs 3 4 => + { + rw [← R₃.map_comp, ← H₂.map_comp, left_triangle_components] + } + simp only [map_id, id_comp] + +end mateEquivVComp + +section mateEquivHComp + +variable {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} +variable [Category.{v₁} A] [Category.{v₂} B][Category.{v₃} C] +variable [Category.{v₄} D] [Category.{v₅} E][Category.{v₆} F] +variable {G : A ⥤ D}{H : B ⥤ E}{K : C ⥤ F} +variable {L₁ : A ⥤ B}{R₁ : B ⥤ A} {L₂ : D ⥤ E}{R₂ : E ⥤ D} +variable {L₃ : B ⥤ C}{R₃ : C ⥤ B} {L₄ : E ⥤ F}{R₄ : F ⥤ E} +variable (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (adj₄ : L₄ ⊣ R₄) + +/-- Squares between left adjoints can be composed "horizontally" by pasting. -/ +def leftAdjointSquare.hcomp : + (G ⋙ L₂ ⟶ L₁ ⋙ H) → (H ⋙ L₄ ⟶ L₃ ⋙ K) → (G ⋙ (L₂ ⋙ L₄) ⟶ (L₁ ⋙ L₃) ⋙ K) := fun α β ↦ + (whiskerRight α L₄) ≫ (whiskerLeft L₁ β) + +/-- Squares between right adjoints can be composed "horizontally" by pasting. -/ +def rightAdjointSquare.hcomp : + (R₁ ⋙ G ⟶ H ⋙ R₂) → (R₃ ⋙ H ⟶ K ⋙ R₄) → ((R₃ ⋙ R₁) ⋙ G ⟶ K ⋙ (R₄ ⋙ R₂)) := fun α β ↦ + (whiskerLeft R₃ α) ≫ (whiskerRight β R₂) + +/-- The mates equivalence commutes with horizontal composition of squares. -/ +theorem mateEquiv_hcomp + (α : G ⋙ L₂ ⟶ L₁ ⋙ H) (β : H ⋙ L₄ ⟶ L₃ ⋙ K) : + (mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (leftAdjointSquare.hcomp α β) = + rightAdjointSquare.hcomp (mateEquiv adj₁ adj₂ α) (mateEquiv adj₃ adj₄ β) := by + unfold leftAdjointSquare.hcomp rightAdjointSquare.hcomp mateEquiv Adjunction.comp + ext c + simp only [comp_obj, whiskerLeft_comp, whiskerLeft_twice, whiskerRight_comp, assoc, + Equiv.coe_fn_mk, comp_app, whiskerLeft_app, whiskerRight_app, id_obj, associator_inv_app, + Functor.comp_map, associator_hom_app, map_id, id_comp, whiskerRight_twice] + slice_rhs 2 4 => + { + rw [← R₂.map_comp, ← R₂.map_comp, ← assoc, ← unit_naturality (adj₄)] + } + rw [R₂.map_comp, L₄.map_comp, R₄.map_comp, R₂.map_comp] + slice_rhs 4 5 => + { + rw [← R₂.map_comp, ← R₄.map_comp, ← Functor.comp_map _ L₄ , β.naturality] + } + simp only [comp_obj, Functor.comp_map, map_comp, assoc] + +end mateEquivHComp + +section mateEquivSquareComp + +variable {A : Type u₁} {B : Type u₂} {C : Type u₃} +variable {D : Type u₄} {E : Type u₅} {F : Type u₆} +variable {X : Type u₇} {Y : Type u₈} {Z : Type u₉} +variable [Category.{v₁} A] [Category.{v₂} B][Category.{v₃} C] +variable [Category.{v₄} D] [Category.{v₅} E][Category.{v₆} F] +variable [Category.{v₇} X] [Category.{v₈} Y][Category.{v₉} Z] +variable {G₁ : A ⥤ D} {H₁ : B ⥤ E} {K₁ : C ⥤ F} {G₂ : D ⥤ X} {H₂ : E ⥤ Y} {K₂ : F ⥤ Z} +variable {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : B ⥤ C} {R₂ : C ⥤ B} {L₃ : D ⥤ E} {R₃ : E ⥤ D} +variable {L₄ : E ⥤ F} {R₄ : F ⥤ E} {L₅ : X ⥤ Y} {R₅ : Y ⥤ X} {L₆ : Y ⥤ Z} {R₆ : Z ⥤ Y} variable (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) +variable (adj₄ : L₄ ⊣ R₄) (adj₅ : L₅ ⊣ R₅) (adj₆ : L₆ ⊣ R₆) + +/-- Squares of squares between left adjoints can be composed by iterating vertical and horizontal +composition. +-/ +def leftAdjointSquare.comp + (α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁) (β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁) + (γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂) (δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂) : + ((G₁ ⋙ G₂) ⋙ (L₅ ⋙ L₆)) ⟶ ((L₁ ⋙ L₂) ⋙ (K₁ ⋙ K₂)) := + leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ) +#align category_theory.leftadjointsquare_comp CategoryTheory.leftAdjointSquare.comp + +theorem leftAdjointSquare.comp_vhcomp + (α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁) (β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁) + (γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂) (δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂) : + leftAdjointSquare.comp α β γ δ = + leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ) := rfl + +/-- Horizontal and vertical composition of squares commutes.-/ +theorem leftAdjointSquare.comp_hvcomp + (α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁) (β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁) + (γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂) (δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂) : + leftAdjointSquare.comp α β γ δ = + leftAdjointSquare.hcomp (leftAdjointSquare.vcomp α γ) (leftAdjointSquare.vcomp β δ) := by + unfold leftAdjointSquare.comp leftAdjointSquare.hcomp leftAdjointSquare.vcomp + unfold whiskerLeft whiskerRight + ext a + simp only [comp_obj, comp_app, map_comp, assoc] + slice_rhs 2 3 => + { + rw [← Functor.comp_map _ L₆, δ.naturality] + } + simp only [comp_obj, Functor.comp_map, assoc] + +/-- Squares of squares between right adjoints can be composed by iterating vertical and horizontal +composition. +-/ +def rightAdjointSquare.comp + (α : R₁ ⋙ G₁ ⟶ H₁ ⋙ R₃) (β : R₂ ⋙ H₁ ⟶ K₁ ⋙ R₄) + (γ : R₃ ⋙ G₂ ⟶ H₂ ⋙ R₅) (δ : R₄ ⋙ H₂ ⟶ K₂ ⋙ R₆) : + ((R₂ ⋙ R₁) ⋙ (G₁ ⋙ G₂) ⟶ (K₁ ⋙ K₂) ⋙ (R₆ ⋙ R₅)) := + rightAdjointSquare.vcomp (rightAdjointSquare.hcomp α β) (rightAdjointSquare.hcomp γ δ) +#align category_theory.rightadjointsquare_comp CategoryTheory.rightAdjointSquare.comp + +theorem rightAdjointSquare.comp_vhcomp + (α : R₁ ⋙ G₁ ⟶ H₁ ⋙ R₃) (β : R₂ ⋙ H₁ ⟶ K₁ ⋙ R₄) + (γ : R₃ ⋙ G₂ ⟶ H₂ ⋙ R₅) (δ : R₄ ⋙ H₂ ⟶ K₂ ⋙ R₆) : + rightAdjointSquare.comp α β γ δ = + rightAdjointSquare.vcomp (rightAdjointSquare.hcomp α β) (rightAdjointSquare.hcomp γ δ) := rfl + +/-- Horizontal and vertical composition of squares commutes.-/ +theorem rightAdjointSquare.comp_hvcomp + (α : R₁ ⋙ G₁ ⟶ H₁ ⋙ R₃) (β : R₂ ⋙ H₁ ⟶ K₁ ⋙ R₄) + (γ : R₃ ⋙ G₂ ⟶ H₂ ⋙ R₅) (δ : R₄ ⋙ H₂ ⟶ K₂ ⋙ R₆) : + rightAdjointSquare.comp α β γ δ = + rightAdjointSquare.hcomp (rightAdjointSquare.vcomp α γ) (rightAdjointSquare.vcomp β δ) := by + unfold rightAdjointSquare.comp rightAdjointSquare.hcomp rightAdjointSquare.vcomp + unfold whiskerLeft whiskerRight + ext c + simp only [comp_obj, comp_app, map_comp, assoc] + slice_rhs 2 3 => + { + rw [← Functor.comp_map _ R₅, ← γ.naturality] + } + simp only [comp_obj, Functor.comp_map, assoc] + +/-- 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. +-/ +theorem mateEquiv_square + (α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁) (β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁) + (γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂) (δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂) : + (mateEquiv (G := G₁ ⋙ G₂) (H := K₁ ⋙ K₂) (adj₁.comp adj₂) (adj₅.comp adj₆)) + (leftAdjointSquare.comp α β γ δ) = + rightAdjointSquare.comp + (mateEquiv adj₁ adj₃ α) (mateEquiv adj₂ adj₄ β) + (mateEquiv adj₃ adj₅ γ) (mateEquiv adj₄ adj₆ δ) := by + have vcomp := + mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆) + (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ) + have hcomp1 := mateEquiv_hcomp adj₁ adj₃ adj₂ adj₄ α β + have hcomp2 := mateEquiv_hcomp adj₃ adj₅ adj₄ adj₆ γ δ + rw [hcomp1, hcomp2] at vcomp + exact vcomp + +end mateEquivSquareComp + +section conjugateEquiv + +variable {C : Type u₁} {D : Type u₂} +variable [Category.{v₁} C] [Category.{v₂} D] +variable {L₁ L₂ : C ⥤ D} {R₁ R₂ : D ⥤ C} +variable (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 `transferNatTrans`, where the two "vertical" functors are -identity. +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.transferNatTransSelf_iso`. -This is in contrast to the general case `transferNatTrans` which does not in general have this -property. +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. -/ -def transferNatTransSelf : (L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂) := +def conjugateEquiv : (L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂) := calc (L₂ ⟶ L₁) ≃ _ := (Iso.homCongr L₂.leftUnitor L₁.rightUnitor).symm - _ ≃ _ := transferNatTrans adj₁ adj₂ + _ ≃ _ := mateEquiv adj₁ adj₂ _ ≃ (R₁ ⟶ R₂) := R₁.rightUnitor.homCongr R₂.leftUnitor -#align category_theory.transfer_nat_trans_self CategoryTheory.transferNatTransSelf -theorem transferNatTransSelf_counit (f : L₂ ⟶ L₁) (X) : - L₂.map ((transferNatTransSelf adj₁ adj₂ f).app _) ≫ adj₂.counit.app X = - f.app _ ≫ adj₁.counit.app X := by - dsimp [transferNatTransSelf] +@[deprecated (since := "2024-07-09")] alias transferNatTransSelf := conjugateEquiv + +/-- A component of a transposed form of the conjugation definition. -/ +theorem conjugateEquiv_counit (α : L₂ ⟶ L₁) (d : D) : + L₂.map ((conjugateEquiv adj₁ adj₂ α).app _) ≫ adj₂.counit.app d = + α.app _ ≫ adj₁.counit.app d := by + dsimp [conjugateEquiv] rw [id_comp, comp_id] - have := transferNatTrans_counit adj₁ adj₂ (L₂.leftUnitor.hom ≫ f ≫ L₁.rightUnitor.inv) X + have := mateEquiv_counit adj₁ adj₂ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) d dsimp at this rw [this] - simp -#align category_theory.transfer_nat_trans_self_counit CategoryTheory.transferNatTransSelf_counit + simp only [comp_id, id_comp] -theorem unit_transferNatTransSelf (f : L₂ ⟶ L₁) (X) : - adj₁.unit.app _ ≫ (transferNatTransSelf adj₁ adj₂ f).app _ = - adj₂.unit.app X ≫ R₂.map (f.app _) := by - dsimp [transferNatTransSelf] +/-- A component of a transposed form of the inverse conjugation definition. -/ +theorem conjugateEquiv_counit_symm (α : R₁ ⟶ R₂) (d : D) : + L₂.map (α.app _) ≫ adj₂.counit.app d = + ((conjugateEquiv adj₁ adj₂).symm α).app _ ≫ adj₁.counit.app d := by + conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α] + exact (conjugateEquiv_counit adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) d) + +/-- A component of a transposed form of the conjugation definition. -/ +theorem unit_conjugateEquiv (α : L₂ ⟶ L₁) (c : C) : + adj₁.unit.app _ ≫ (conjugateEquiv adj₁ adj₂ α).app _ = + adj₂.unit.app c ≫ R₂.map (α.app _) := by + dsimp [conjugateEquiv] rw [id_comp, comp_id] - have := unit_transferNatTrans adj₁ adj₂ (L₂.leftUnitor.hom ≫ f ≫ L₁.rightUnitor.inv) X + have := unit_mateEquiv adj₁ adj₂ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) c dsimp at this rw [this] simp -#align category_theory.unit_transfer_nat_trans_self CategoryTheory.unit_transferNatTransSelf + +/-- A component of a transposed form of the inverse conjugation definition. -/ +theorem unit_conjugateEquiv_symm (α : R₁ ⟶ R₂) (c : C) : + adj₁.unit.app _ ≫ α.app _ = + adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app _) := by + conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α] + exact (unit_conjugateEquiv adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) c) @[simp] -theorem transferNatTransSelf_id : transferNatTransSelf adj₁ adj₁ (𝟙 _) = 𝟙 _ := by +theorem conjugateEquiv_id : conjugateEquiv adj₁ adj₁ (𝟙 _) = 𝟙 _ := by ext - dsimp [transferNatTransSelf, transferNatTrans] - simp -#align category_theory.transfer_nat_trans_self_id CategoryTheory.transferNatTransSelf_id + dsimp [conjugateEquiv, mateEquiv] + simp only [comp_id, map_id, id_comp, right_triangle_components] --- See library note [dsimp, simp] @[simp] -theorem transferNatTransSelf_symm_id : (transferNatTransSelf adj₁ adj₁).symm (𝟙 _) = 𝟙 _ := by +theorem conjugateEquiv_symm_id : (conjugateEquiv adj₁ adj₁).symm (𝟙 _) = 𝟙 _ := by rw [Equiv.symm_apply_eq] - simp -#align category_theory.transfer_nat_trans_self_symm_id CategoryTheory.transferNatTransSelf_symm_id + simp only [conjugateEquiv_id] +#align category_theory.conjugates_symm_id CategoryTheory.conjugateEquiv_symm_id -theorem transferNatTransSelf_comp (f g) : - transferNatTransSelf adj₁ adj₂ f ≫ transferNatTransSelf adj₂ adj₃ g = - transferNatTransSelf adj₁ adj₃ (g ≫ f) := by - ext - dsimp [transferNatTransSelf, transferNatTrans] - simp only [id_comp, comp_id] - rw [← adj₃.unit_naturality_assoc, ← R₃.map_comp, g.naturality_assoc, L₂.map_comp, assoc, - adj₂.counit_naturality, adj₂.left_triangle_components_assoc, assoc] -#align category_theory.transfer_nat_trans_self_comp CategoryTheory.transferNatTransSelf_comp - -theorem transferNatTransSelf_adjunction_id {L R : C ⥤ C} (adj : L ⊣ R) (f : 𝟭 C ⟶ L) (X : C) : - (transferNatTransSelf adj Adjunction.id f).app X = f.app (R.obj X) ≫ adj.counit.app X := by - dsimp [transferNatTransSelf, transferNatTrans, Adjunction.id] +theorem conjugateEquiv_adjunction_id {L R : C ⥤ C} (adj : L ⊣ R) (α : 𝟭 C ⟶ L) (c : C) : + (conjugateEquiv adj Adjunction.id α).app c = α.app (R.obj c) ≫ adj.counit.app c := by + dsimp [conjugateEquiv, mateEquiv, Adjunction.id] simp only [comp_id, id_comp] -#align category_theory.transfer_nat_trans_self_adjunction_id CategoryTheory.transferNatTransSelf_adjunction_id -theorem transferNatTransSelf_adjunction_id_symm {L R : C ⥤ C} (adj : L ⊣ R) (g : R ⟶ 𝟭 C) (X : C) : - ((transferNatTransSelf adj Adjunction.id).symm g).app X = adj.unit.app X ≫ g.app (L.obj X) := by - dsimp [transferNatTransSelf, transferNatTrans, Adjunction.id] +theorem conjugateEquiv_adjunction_id_symm {L R : C ⥤ C} (adj : L ⊣ R) (α : R ⟶ 𝟭 C) (c : C) : + ((conjugateEquiv adj Adjunction.id).symm α).app c = adj.unit.app c ≫ α.app (L.obj c) := by + dsimp [conjugateEquiv, mateEquiv, Adjunction.id] simp only [comp_id, id_comp] -#align category_theory.transfer_nat_trans_self_adjunction_id_symm CategoryTheory.transferNatTransSelf_adjunction_id_symm +end conjugateEquiv -theorem transferNatTransSelf_symm_comp (f g) : - (transferNatTransSelf adj₂ adj₁).symm f ≫ (transferNatTransSelf adj₃ adj₂).symm g = - (transferNatTransSelf adj₃ adj₁).symm (g ≫ f) := by - rw [Equiv.eq_symm_apply, ← transferNatTransSelf_comp _ adj₂] - simp -#align category_theory.transfer_nat_trans_self_symm_comp CategoryTheory.transferNatTransSelf_symm_comp -theorem transferNatTransSelf_comm {f g} (gf : g ≫ f = 𝟙 _) : - transferNatTransSelf adj₁ adj₂ f ≫ transferNatTransSelf adj₂ adj₁ g = 𝟙 _ := by - rw [transferNatTransSelf_comp, gf, transferNatTransSelf_id] -#align category_theory.transfer_nat_trans_self_comm CategoryTheory.transferNatTransSelf_comm +section ConjugateComposition +variable {C : Type u₁} {D : Type u₂} +variable [Category.{v₁} C] [Category.{v₂} D] +variable {L₁ L₂ L₃ : C ⥤ D} {R₁ R₂ R₃ : D ⥤ C} +variable (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) -theorem transferNatTransSelf_symm_comm {f g} (gf : g ≫ f = 𝟙 _) : - (transferNatTransSelf adj₁ adj₂).symm f ≫ (transferNatTransSelf adj₂ adj₁).symm g = 𝟙 _ := by - rw [transferNatTransSelf_symm_comp, gf, transferNatTransSelf_symm_id] -#align category_theory.transfer_nat_trans_self_symm_comm CategoryTheory.transferNatTransSelf_symm_comm +theorem conjugateEquiv_comp (α : L₂ ⟶ L₁) (β : L₃ ⟶ L₂) : + conjugateEquiv adj₁ adj₂ α ≫ conjugateEquiv adj₂ adj₃ β = + conjugateEquiv adj₁ adj₃ (β ≫ α) := by + ext d + dsimp [conjugateEquiv, mateEquiv] + have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃ + (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) + (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) + have vcompd := congr_app vcomp d + dsimp [mateEquiv, leftAdjointSquare.vcomp, rightAdjointSquare.vcomp] at vcompd + simp at vcompd + simp only [comp_id, id_comp, assoc, map_comp] + rw [vcompd] + +theorem conjugateEquiv_symm_comp (α : R₁ ⟶ R₂) (β : R₂ ⟶ R₃) : + (conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = + (conjugateEquiv adj₁ adj₃).symm (α ≫ β) := by + rw [Equiv.eq_symm_apply, ← conjugateEquiv_comp _ adj₂] + simp only [Equiv.apply_symm_apply] + +theorem conjugateEquiv_comm {α : L₂ ⟶ L₁} {β : L₁ ⟶ L₂} (βα : β ≫ α = 𝟙 _) : + conjugateEquiv adj₁ adj₂ α ≫ conjugateEquiv adj₂ adj₁ β = 𝟙 _ := by + rw [conjugateEquiv_comp, βα, conjugateEquiv_id] + +theorem conjugateEquiv_symm_comm {α : R₁ ⟶ R₂}{β : R₂ ⟶ R₁} (αβ : α ≫ β = 𝟙 _) : + (conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 _ := by + rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id] + +end ConjugateComposition + +section ConjugateIsomorphism + +variable {C : Type u₁} {D : Type u₂} +variable [Category.{v₁} C] [Category.{v₂} D] +variable {L₁ L₂ : C ⥤ D} {R₁ R₂ : D ⥤ C} +variable (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) -/-- If `f` is an isomorphism, then the transferred natural transformation is an isomorphism. -The converse is given in `transferNatTransSelf_of_iso`. +/-- If `α` is an isomorphism between left adjoints, then its conjugate transformation is an +isomorphism. The converse is given in `conjugateEquiv_of_iso`. -/ -instance transferNatTransSelf_iso (f : L₂ ⟶ L₁) [IsIso f] : - IsIso (transferNatTransSelf adj₁ adj₂ f) := - ⟨⟨transferNatTransSelf adj₂ adj₁ (inv f), - ⟨transferNatTransSelf_comm _ _ (by simp), transferNatTransSelf_comm _ _ (by simp)⟩⟩⟩ -#align category_theory.transfer_nat_trans_self_iso CategoryTheory.transferNatTransSelf_iso - -/-- If `f` is an isomorphism, then the un-transferred natural transformation is an isomorphism. -The converse is given in `transferNatTransSelf_symm_of_iso`. +instance conjugateEquiv_iso (α : L₂ ⟶ L₁) [IsIso α] : + IsIso (conjugateEquiv adj₁ adj₂ α) := + ⟨⟨conjugateEquiv adj₂ adj₁ (inv α), + ⟨conjugateEquiv_comm _ _ (by simp), conjugateEquiv_comm _ _ (by simp)⟩⟩⟩ + +/-- If `α` is an isomorphism between right adjoints, then its conjugate transformation is an +isomorphism. The converse is given in `conjugateEquiv_symm_of_iso`. -/ -instance transferNatTransSelf_symm_iso (f : R₁ ⟶ R₂) [IsIso f] : - IsIso ((transferNatTransSelf adj₁ adj₂).symm f) := - ⟨⟨(transferNatTransSelf adj₂ adj₁).symm (inv f), - ⟨transferNatTransSelf_symm_comm _ _ (by simp), transferNatTransSelf_symm_comm _ _ (by simp)⟩⟩⟩ -#align category_theory.transfer_nat_trans_self_symm_iso CategoryTheory.transferNatTransSelf_symm_iso - -/-- If `f` is a natural transformation whose transferred natural transformation is an isomorphism, -then `f` is an isomorphism. -The converse is given in `transferNatTransSelf_iso`. +instance conjugateEquiv_symm_iso (α : R₁ ⟶ R₂) [IsIso α] : + IsIso ((conjugateEquiv adj₁ adj₂).symm α) := + ⟨⟨(conjugateEquiv adj₂ adj₁).symm (inv α), + ⟨conjugateEquiv_symm_comm _ _ (by simp), conjugateEquiv_symm_comm _ _ (by simp)⟩⟩⟩ + +/-- 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 transferNatTransSelf_of_iso (f : L₂ ⟶ L₁) [IsIso (transferNatTransSelf adj₁ adj₂ f)] : - IsIso f := by - suffices IsIso ((transferNatTransSelf adj₁ adj₂).symm (transferNatTransSelf adj₁ adj₂ f)) +theorem conjugateEquiv_of_iso (α : L₂ ⟶ L₁) [IsIso (conjugateEquiv adj₁ adj₂ α)] : + IsIso α := by + suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α)) by simpa using this infer_instance -#align category_theory.transfer_nat_trans_self_of_iso CategoryTheory.transferNatTransSelf_of_iso /-- -If `f` is a natural transformation whose un-transferred natural transformation is an isomorphism, -then `f` is an isomorphism. -The converse is given in `transferNatTransSelf_symm_iso`. +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`. -/ -theorem transferNatTransSelf_symm_of_iso (f : R₁ ⟶ R₂) - [IsIso ((transferNatTransSelf adj₁ adj₂).symm f)] : IsIso f := by - suffices IsIso ((transferNatTransSelf adj₁ adj₂) ((transferNatTransSelf adj₁ adj₂).symm f)) +theorem conjugateEquiv_symm_of_iso (α : R₁ ⟶ R₂) + [IsIso ((conjugateEquiv adj₁ adj₂).symm α)] : IsIso α := by + suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α)) by simpa using this infer_instance -#align category_theory.transfer_nat_trans_self_symm_of_iso CategoryTheory.transferNatTransSelf_symm_of_iso -end Self +/-- Thus conjugation defines an equivalence between natural isomorphisms. -/ +noncomputable def conjugateIsoEquiv : (L₂ ≅ L₁) ≃ (R₁ ≅ R₂) where + toFun α := asIso (conjugateEquiv adj₁ adj₂ α.hom) + invFun β := asIso ((conjugateEquiv adj₁ adj₂).symm β.hom) + left_inv := by aesop_cat + right_inv := by aesop_cat + +end ConjugateIsomorphism + +section IteratedmateEquiv +variable {A : Type u₁} {B : Type u₂}{C : Type u₃} {D : Type u₄} +variable [Category.{v₁} A] [Category.{v₂} B][Category.{v₃} C] [Category.{v₄} D] +variable {F₁ : A ⥤ C}{U₁ : C ⥤ A} {F₂ : B ⥤ D} {U₂ : D ⥤ B} +variable {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : C ⥤ D} {R₂ : D ⥤ C} +variable (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : F₁ ⊣ U₁)(adj₄ : F₂ ⊣ U₂) + +/-- 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 iterated_mateEquiv_conjugateEquiv (α : F₁ ⋙ L₂ ⟶ L₁ ⋙ F₂) : + mateEquiv adj₄ adj₃ (mateEquiv adj₁ adj₂ α) = + conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂) α := by + ext d + unfold conjugateEquiv mateEquiv Adjunction.comp + simp only [comp_obj, Equiv.coe_fn_mk, whiskerLeft_comp, whiskerLeft_twice, whiskerRight_comp, + assoc, comp_app, whiskerLeft_app, whiskerRight_app, id_obj, Functor.comp_map, Iso.homCongr_symm, + Equiv.instTrans_trans, Equiv.trans_apply, Iso.homCongr_apply, Iso.symm_inv, Iso.symm_hom, + rightUnitor_inv_app, associator_inv_app, leftUnitor_hom_app, map_id, associator_hom_app, + Functor.id_map, comp_id, id_comp] + +theorem iterated_mateEquiv_conjugateEquiv_symm (α : U₂ ⋙ R₁ ⟶ R₂ ⋙ U₁) : + (mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α) = + (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm α := by + rw [Equiv.eq_symm_apply, ← iterated_mateEquiv_conjugateEquiv] + simp only [Equiv.apply_symm_apply] + +end IteratedmateEquiv + +section mateEquivconjugateEquivVComp + +variable {A : Type u₁} {B : Type u₂} {C : Type u₃}{D : Type u₄} +variable [Category.{v₁} A] [Category.{v₂} B][Category.{v₃} C] +variable [Category.{v₄} D] +variable {G : A ⥤ C} {H : B ⥤ D} +variable {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : C ⥤ D} {R₂ : D ⥤ C} {L₃ : C ⥤ D}{R₃ : D ⥤ C} +variable (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) + +/-- Composition of a squares between left adjoints with a conjugate square. -/ +def leftAdjointSquareConjugate.vcomp : + (G ⋙ L₂ ⟶ L₁ ⋙ H) → (L₃ ⟶ L₂) → (G ⋙ L₃ ⟶ L₁ ⋙ H) := + fun α β ↦ (whiskerLeft G β) ≫ α + +/-- Composition of a squares between right adjoints with a conjugate square. -/ +def rightAdjointSquareConjugate.vcomp : + (R₁ ⋙ G ⟶ H ⋙ R₂) → (R₂ ⟶ R₃) → (R₁ ⋙ G ⟶ H ⋙ R₃) := + fun α β ↦ α ≫ (whiskerLeft H β) + +/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`. -/ +theorem mateEquiv_conjugateEquiv_vcomp + (α : G ⋙ L₂ ⟶ L₁ ⋙ H) (β : L₃ ⟶ L₂) : + (mateEquiv adj₁ adj₃) (leftAdjointSquareConjugate.vcomp α β) = + rightAdjointSquareConjugate.vcomp (mateEquiv adj₁ adj₂ α) (conjugateEquiv adj₂ adj₃ β) := by + ext b + have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃ α (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) + unfold leftAdjointSquare.vcomp rightAdjointSquare.vcomp at vcomp + unfold leftAdjointSquareConjugate.vcomp rightAdjointSquareConjugate.vcomp conjugateEquiv + have vcompb := congr_app vcomp b + simp at vcompb + unfold mateEquiv + simp only [comp_obj, Equiv.coe_fn_mk, whiskerLeft_comp, whiskerLeft_twice, whiskerRight_comp, + assoc, comp_app, whiskerLeft_app, whiskerRight_app, id_obj, Functor.comp_map, Iso.homCongr_symm, + Equiv.instTrans_trans, Equiv.trans_apply, Iso.homCongr_apply, Iso.symm_inv, Iso.symm_hom, + rightUnitor_inv_app, leftUnitor_hom_app, map_id, Functor.id_map, comp_id, id_comp] + exact vcompb + +end mateEquivconjugateEquivVComp + +section conjugateEquivmateEquivVComp + +variable {A : Type u₁} {B : Type u₂} {C : Type u₃}{D : Type u₄} +variable [Category.{v₁} A] [Category.{v₂} B][Category.{v₃} C] +variable [Category.{v₄} D] +variable {G : A ⥤ C} {H : B ⥤ D} +variable {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : A ⥤ B} {R₂ : B ⥤ A} {L₃ : C ⥤ D} {R₃ : D ⥤ C} +variable (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) + +/-- Composition of a conjugate square with a squares between left adjoints. -/ +def leftAdjointConjugateSquare.vcomp : + (L₂ ⟶ L₁) → (G ⋙ L₃ ⟶ L₂ ⋙ H) → (G ⋙ L₃ ⟶ L₁ ⋙ H) := + fun α β ↦ β ≫ (whiskerRight α H) + +/-- Composition of a conjugate square with a squares between right adjoints. -/ +def rightAdjointConjugateSquare.vcomp : + (R₁ ⟶ R₂) → (R₂ ⋙ G ⟶ H ⋙ R₃) → (R₁ ⋙ G ⟶ H ⋙ R₃) := + fun α β ↦ (whiskerRight α G) ≫ β + +/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`. -/ +theorem conjugateEquiv_mateEquiv_vcomp + (α : L₂ ⟶ L₁) (β : G ⋙ L₃ ⟶ L₂ ⋙ H) : + (mateEquiv adj₁ adj₃) (leftAdjointConjugateSquare.vcomp α β) = + rightAdjointConjugateSquare.vcomp (conjugateEquiv adj₁ adj₂ α) (mateEquiv adj₂ adj₃ β) := by + ext b + have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) β + unfold leftAdjointSquare.vcomp rightAdjointSquare.vcomp at vcomp + unfold leftAdjointConjugateSquare.vcomp rightAdjointConjugateSquare.vcomp conjugateEquiv + have vcompb := congr_app vcomp b + simp at vcompb + unfold mateEquiv + simp only [comp_obj, Equiv.coe_fn_mk, whiskerLeft_comp, whiskerLeft_twice, whiskerRight_comp, + assoc, comp_app, whiskerLeft_app, whiskerRight_app, id_obj, Functor.comp_map, Iso.homCongr_symm, + Equiv.instTrans_trans, Equiv.trans_apply, Iso.homCongr_apply, Iso.symm_inv, Iso.symm_hom, + rightUnitor_inv_app, leftUnitor_hom_app, map_id, Functor.id_map, comp_id, id_comp] + exact vcompb + +end conjugateEquivmateEquivVComp end CategoryTheory diff --git a/Mathlib/CategoryTheory/Closed/Cartesian.lean b/Mathlib/CategoryTheory/Closed/Cartesian.lean index 2b4b97544d0fe..129918fc14ff1 100644 --- a/Mathlib/CategoryTheory/Closed/Cartesian.lean +++ b/Mathlib/CategoryTheory/Closed/Cartesian.lean @@ -284,13 +284,13 @@ variable {B} /-- Pre-compose an internal hom with an external hom. -/ def pre (f : B ⟶ A) [Exponentiable B] : exp A ⟶ exp B := - transferNatTransSelf (exp.adjunction _) (exp.adjunction _) (prod.functor.map f) + conjugateEquiv (exp.adjunction _) (exp.adjunction _) (prod.functor.map f) #align category_theory.pre CategoryTheory.pre theorem prod_map_pre_app_comp_ev (f : B ⟶ A) [Exponentiable B] (X : C) : Limits.prod.map (𝟙 B) ((pre f).app X) ≫ (exp.ev B).app X = Limits.prod.map f (𝟙 (A ⟹ X)) ≫ (exp.ev A).app X := - transferNatTransSelf_counit _ _ (prod.functor.map f) X + conjugateEquiv_counit _ _ (prod.functor.map f) X #align category_theory.prod_map_pre_app_comp_ev CategoryTheory.prod_map_pre_app_comp_ev theorem uncurry_pre (f : B ⟶ A) [Exponentiable B] (X : C) : @@ -301,7 +301,7 @@ theorem uncurry_pre (f : B ⟶ A) [Exponentiable B] (X : C) : theorem coev_app_comp_pre_app (f : B ⟶ A) [Exponentiable B] : (exp.coev A).app X ≫ (pre f).app (A ⨯ X) = (exp.coev B).app X ≫ (exp B).map (Limits.prod.map f (𝟙 _)) := - unit_transferNatTransSelf _ _ (prod.functor.map f) X + unit_conjugateEquiv _ _ (prod.functor.map f) X #align category_theory.coev_app_comp_pre_app CategoryTheory.coev_app_comp_pre_app @[simp] @@ -311,7 +311,7 @@ theorem pre_id (A : C) [Exponentiable A] : pre (𝟙 A) = 𝟙 _ := by simp [pre @[simp] theorem pre_map {A₁ A₂ A₃ : C} [Exponentiable A₁] [Exponentiable A₂] [Exponentiable A₃] (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) : pre (f ≫ g) = pre g ≫ pre f := by - rw [pre, pre, pre, transferNatTransSelf_comp, prod.functor.map_comp] + rw [pre, pre, pre, conjugateEquiv_comp, prod.functor.map_comp] #align category_theory.pre_map CategoryTheory.pre_map end Pre diff --git a/Mathlib/CategoryTheory/Closed/Functor.lean b/Mathlib/CategoryTheory/Closed/Functor.lean index 57d3c39435053..6ef96f8eaa95f 100644 --- a/Mathlib/CategoryTheory/Closed/Functor.lean +++ b/Mathlib/CategoryTheory/Closed/Functor.lean @@ -77,13 +77,13 @@ variable [PreservesLimitsOfShape (Discrete WalkingPair) F] `F` is a cartesian closed functor if this is an iso for all `A`. -/ def expComparison (A : C) : exp A ⋙ F ⟶ F ⋙ exp (F.obj A) := - transferNatTrans (exp.adjunction A) (exp.adjunction (F.obj A)) (prodComparisonNatIso F A).inv + mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A)) (prodComparisonNatIso F A).inv #align category_theory.exp_comparison CategoryTheory.expComparison theorem expComparison_ev (A B : C) : Limits.prod.map (𝟙 (F.obj A)) ((expComparison F A).app B) ≫ (exp.ev (F.obj A)).app (F.obj B) = inv (prodComparison F _ _) ≫ F.map ((exp.ev _).app _) := by - convert transferNatTrans_counit _ _ (prodComparisonNatIso F A).inv B using 2 + convert mateEquiv_counit _ _ (prodComparisonNatIso F A).inv B using 2 apply IsIso.inv_eq_of_hom_inv_id -- Porting note: was `ext` simp only [Limits.prodComparisonNatIso_inv, asIso_inv, NatIso.isIso_inv_app, IsIso.hom_inv_id] #align category_theory.exp_comparison_ev CategoryTheory.expComparison_ev @@ -91,7 +91,7 @@ theorem expComparison_ev (A B : C) : theorem coev_expComparison (A B : C) : F.map ((exp.coev A).app B) ≫ (expComparison F A).app (A ⨯ B) = (exp.coev _).app (F.obj B) ≫ (exp (F.obj A)).map (inv (prodComparison F A B)) := by - convert unit_transferNatTrans _ _ (prodComparisonNatIso F A).inv B using 3 + convert unit_mateEquiv _ _ (prodComparisonNatIso F A).inv B using 3 apply IsIso.inv_eq_of_hom_inv_id -- Porting note: was `ext` dsimp simp @@ -107,13 +107,23 @@ theorem uncurry_expComparison (A B : C) : theorem expComparison_whiskerLeft {A A' : C} (f : A' ⟶ A) : expComparison F A ≫ whiskerLeft _ (pre (F.map f)) = whiskerRight (pre f) _ ≫ expComparison F A' := by + unfold expComparison pre + have vcomp1 := mateEquiv_conjugateEquiv_vcomp + (exp.adjunction A) (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A')) + ((prodComparisonNatIso F A).inv) ((prod.functor.map (F.map f))) + have vcomp2 := conjugateEquiv_mateEquiv_vcomp + (exp.adjunction A) (exp.adjunction A') (exp.adjunction (F.obj A')) + ((prod.functor.map f)) ((prodComparisonNatIso F A').inv) + unfold leftAdjointSquareConjugate.vcomp rightAdjointSquareConjugate.vcomp at vcomp1 + unfold leftAdjointConjugateSquare.vcomp rightAdjointConjugateSquare.vcomp at vcomp2 + rw [← vcomp1, ← vcomp2] + apply congr_arg ext B - dsimp - apply uncurry_injective - rw [uncurry_natural_left, uncurry_natural_left, uncurry_expComparison, uncurry_pre, - prod.map_swap_assoc, ← F.map_id, expComparison_ev, ← F.map_id, ← - prodComparison_inv_natural_assoc, ← prodComparison_inv_natural_assoc, ← F.map_comp, ← - F.map_comp, prod_map_pre_app_comp_ev] + simp only [Functor.comp_obj, prod.functor_obj_obj, prodComparisonNatIso_inv, asIso_inv, + NatTrans.comp_app, whiskerLeft_app, prod.functor_map_app, NatIso.isIso_inv_app, + whiskerRight_app] + rw [← F.map_id] + exact (prodComparison_inv_natural F f (𝟙 B)).symm #align category_theory.exp_comparison_whisker_left CategoryTheory.expComparison_whiskerLeft /-- The functor `F` is cartesian closed (ie preserves exponentials) if each natural transformation @@ -126,27 +136,39 @@ class CartesianClosedFunctor : Prop where attribute [instance] CartesianClosedFunctor.comparison_iso theorem frobeniusMorphism_mate (h : L ⊣ F) (A : C) : - transferNatTransSelf (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h) + conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h) (frobeniusMorphism F h A) = expComparison F A := by - rw [← Equiv.eq_symm_apply] - ext B : 2 - dsimp [frobeniusMorphism, transferNatTransSelf, transferNatTrans, Adjunction.comp] - simp only [id_comp, comp_id] - rw [← L.map_comp_assoc, prod.map_id_comp, assoc] - -- Porting note: need to use `erw` here. - -- https://github.com/leanprover-community/mathlib4/issues/5164 - erw [expComparison_ev] - rw [prod.map_id_comp, assoc, ← F.map_id, ← prodComparison_inv_natural_assoc, ← F.map_comp] - -- Porting note: need to use `erw` here. - -- https://github.com/leanprover-community/mathlib4/issues/5164 - erw [exp.ev_coev] - rw [F.map_id (A ⨯ L.obj B), comp_id] - ext - · rw [assoc, assoc, ← h.counit_naturality, ← L.map_comp_assoc, assoc, inv_prodComparison_map_fst] - simp - · rw [assoc, assoc, ← h.counit_naturality, ← L.map_comp_assoc, assoc, inv_prodComparison_map_snd] - simp + unfold expComparison frobeniusMorphism + have conjeq := iterated_mateEquiv_conjugateEquiv h h + (exp.adjunction (F.obj A)) (exp.adjunction A) + (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A))) + rw [← conjeq] + apply congr_arg + ext B + unfold mateEquiv + simp only [Functor.comp_obj, prod.functor_obj_obj, Functor.id_obj, Equiv.coe_fn_mk, + whiskerLeft_comp, whiskerLeft_twice, whiskerRight_comp, assoc, NatTrans.comp_app, + whiskerLeft_app, whiskerRight_app, prodComparisonNatTrans_app, prod.functor_map_app, + Functor.comp_map, prod.functor_obj_map, prodComparisonNatIso_inv, asIso_inv, + NatIso.isIso_inv_app] + rw [← F.map_comp, ← F.map_comp] + simp only [prod.map_map, comp_id, id_comp] + apply IsIso.eq_inv_of_inv_hom_id + rw [F.map_comp, assoc, assoc, prodComparison_natural] + slice_lhs 2 3 => + { + rw [← prodComparison_comp] + } + rw [← assoc] + unfold prodComparison + have ηlemma : (h.unit.app (F.obj A ⨯ F.obj B) ≫ + prod.lift ((L ⋙ F).map prod.fst) ((L ⋙ F).map prod.snd)) = + prod.map (h.unit.app (F.obj A)) (h.unit.app (F.obj B)) := by + ext <;> simp + rw [ηlemma] + simp only [Functor.id_obj, Functor.comp_obj, prod.map_map, Adjunction.right_triangle_components, + prod.map_id_id] #align category_theory.frobenius_morphism_mate CategoryTheory.frobeniusMorphism_mate /-- @@ -156,8 +178,9 @@ at `A` is an isomorphism. theorem frobeniusMorphism_iso_of_expComparison_iso (h : L ⊣ F) (A : C) [i : IsIso (expComparison F A)] : IsIso (frobeniusMorphism F h A) := by rw [← frobeniusMorphism_mate F h] at i - exact @transferNatTransSelf_of_iso _ _ _ _ _ _ _ _ _ _ _ i -#align category_theory.frobenius_morphism_iso_of_exp_comparison_iso CategoryTheory.frobeniusMorphism_iso_of_expComparison_iso + exact @conjugateEquiv_of_iso _ _ _ _ _ _ _ _ _ _ _ i +#align category_theory.frobenius_morphism_iso_of_exp_comparison_iso +CategoryTheory.frobeniusMorphism_iso_of_expComparison_iso /-- If the Frobenius morphism at `A` is an isomorphism, then the exponential comparison transformation @@ -166,7 +189,8 @@ If the Frobenius morphism at `A` is an isomorphism, then the exponential compari theorem expComparison_iso_of_frobeniusMorphism_iso (h : L ⊣ F) (A : C) [i : IsIso (frobeniusMorphism F h A)] : IsIso (expComparison F A) := by rw [← frobeniusMorphism_mate F h]; infer_instance -#align category_theory.exp_comparison_iso_of_frobenius_morphism_iso CategoryTheory.expComparison_iso_of_frobeniusMorphism_iso +#align category_theory.exp_comparison_iso_of_frobenius_morphism_iso +CategoryTheory.expComparison_iso_of_frobeniusMorphism_iso /-- If `F` is full and faithful, and has a left adjoint which preserves binary products, then it is cartesian closed. @@ -177,6 +201,7 @@ products, then it is full and faithful. theorem cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts (h : L ⊣ F) [F.Full] [F.Faithful] [PreservesLimitsOfShape (Discrete WalkingPair) L] : CartesianClosedFunctor F where comparison_iso _ := expComparison_iso_of_frobeniusMorphism_iso F h _ -#align category_theory.cartesian_closed_functor_of_left_adjoint_preserves_binary_products CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts +#align category_theory.cartesian_closed_functor_of_left_adjoint_preserves_binary_products +CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts end CategoryTheory diff --git a/Mathlib/CategoryTheory/Closed/Monoidal.lean b/Mathlib/CategoryTheory/Closed/Monoidal.lean index 8308ad4035c01..817522bdce459 100644 --- a/Mathlib/CategoryTheory/Closed/Monoidal.lean +++ b/Mathlib/CategoryTheory/Closed/Monoidal.lean @@ -237,13 +237,13 @@ variable [Closed B] /-- Pre-compose an internal hom with an external hom. -/ def pre (f : B ⟶ A) : ihom A ⟶ ihom B := - transferNatTransSelf (ihom.adjunction _) (ihom.adjunction _) ((tensoringLeft C).map f) + conjugateEquiv (ihom.adjunction _) (ihom.adjunction _) ((tensoringLeft C).map f) #align category_theory.monoidal_closed.pre CategoryTheory.MonoidalClosed.pre @[reassoc (attr := simp)] theorem id_tensor_pre_app_comp_ev (f : B ⟶ A) (X : C) : B ◁ (pre f).app X ≫ (ihom.ev B).app X = f ▷ (A ⟶[C] X) ≫ (ihom.ev A).app X := - transferNatTransSelf_counit _ _ ((tensoringLeft C).map f) X + conjugateEquiv_counit _ _ ((tensoringLeft C).map f) X #align category_theory.monoidal_closed.id_tensor_pre_app_comp_ev CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev @[simp] @@ -255,19 +255,19 @@ theorem uncurry_pre (f : B ⟶ A) (X : C) : @[reassoc (attr := simp)] theorem coev_app_comp_pre_app (f : B ⟶ A) : (ihom.coev A).app X ≫ (pre f).app (A ⊗ X) = (ihom.coev B).app X ≫ (ihom B).map (f ▷ _) := - unit_transferNatTransSelf _ _ ((tensoringLeft C).map f) X + unit_conjugateEquiv _ _ ((tensoringLeft C).map f) X #align category_theory.monoidal_closed.coev_app_comp_pre_app CategoryTheory.MonoidalClosed.coev_app_comp_pre_app @[simp] theorem pre_id (A : C) [Closed A] : pre (𝟙 A) = 𝟙 _ := by rw [pre, Functor.map_id] - apply transferNatTransSelf_id + apply conjugateEquiv_id #align category_theory.monoidal_closed.pre_id CategoryTheory.MonoidalClosed.pre_id @[simp] theorem pre_map {A₁ A₂ A₃ : C} [Closed A₁] [Closed A₂] [Closed A₃] (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) : pre (f ≫ g) = pre g ≫ pre f := by - rw [pre, pre, pre, transferNatTransSelf_comp, (tensoringLeft C).map_comp] + rw [pre, pre, pre, conjugateEquiv_comp, (tensoringLeft C).map_comp] #align category_theory.monoidal_closed.pre_map CategoryTheory.MonoidalClosed.pre_map theorem pre_comm_ihom_map {W X Y Z : C} [Closed W] [Closed X] (f : W ⟶ X) (g : Y ⟶ Z) : diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean index acd0a8e98a919..85baa68c32ade 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean @@ -1238,12 +1238,15 @@ end CoprodFunctor section ProdComparison -universe w +universe w w' u₃ -variable {C} {D : Type u₂} [Category.{w} D] -variable (F : C ⥤ D) {A A' B B' : C} +variable {C} {D : Type u₂} [Category.{w} D] {E : Type u₃} [Category.{w'} E] +variable (F : C ⥤ D) (G : D ⥤ E) {A A' B B' : C} variable [HasBinaryProduct A B] [HasBinaryProduct A' B'] -variable [HasBinaryProduct (F.obj A) (F.obj B)] [HasBinaryProduct (F.obj A') (F.obj B')] +variable [HasBinaryProduct (F.obj A) (F.obj B)] +variable [HasBinaryProduct (F.obj A') (F.obj B')] +variable [HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))] +variable [HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)] /-- The product comparison morphism. @@ -1324,6 +1327,12 @@ def prodComparisonNatIso [HasBinaryProducts C] [HasBinaryProducts D] (A : C) apply NatIso.isIso_of_isIso_app #align category_theory.limits.prod_comparison_nat_iso CategoryTheory.Limits.prodComparisonNatIso +theorem prodComparison_comp : + prodComparison (F ⋙ G) A B = + G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B) := by + unfold prodComparison + ext <;> simp <;> rw [← G.map_comp] <;> simp + end ProdComparison section CoprodComparison