Module

MateComparison.lean

Nyll.EtaleCohomology.Sites.MateComparison

2 declarations indexed from sourceView source ↗

Module documentation

Independence of inverse mates from the choice of left adjoints

For a fixed square of right adjoints, changing the chosen left adjoints conjugates the inverse mate by the canonical comparison isomorphisms. Consequently, invertibility of the inverse mate is independent of these choices. This permits comparison of directly constructed stalk adjunctions with composites of inverse-image and stalk adjunctions.

Imports3

Mathlib.CategoryTheory.Adjunction.Mates
Mathlib.CategoryTheory.Functor.TwoSquare
Mathlib.CategoryTheory.Iso

Imported by2

lemma

inverseMate_change_leftAdjoints

L35 ↗

EtaleCohomology.Sites.inverseMate_change_leftAdjoints

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Functor
universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
namespace EtaleCohomology.Sites
variable {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄}
  [Category.{v₁} A] [Category.{v₂} B] [Category.{v₃} C] [Category.{v₄} D]
  {G : A ⥤ C} {H : B ⥤ D}
  {L₁ L₁' : A ⥤ B} {R₁ : B ⥤ A} {L₂ L₂' : C ⥤ D} {R₂ : D ⥤ C}
  (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₁' : L₁' ⊣ R₁) (adj₂' : L₂' ⊣ R₂)

Lean source · statement

lemma inverseMate_change_leftAdjoints (β : TwoSquare R₁ H G R₂) :
    (mateEquiv adj₁' adj₂').symm β =
      (((mateEquiv adj₁ adj₂).symm β).whiskerLeft
        ((conjugateEquiv adj₁' adj₁).symm (𝟙 R₁))).whiskerRight
          ((conjugateEquiv adj₂ adj₂').symm (𝟙 R₂))

lemma

isIso_inverseMate_iff

L53 ↗

EtaleCohomology.Sites.isIso_inverseMate_iff

Documentation

Invertibility of the inverse mate of a fixed right square is unchanged when its two left adjoints are replaced by other adjoints to the same functors.