sheafComposeNatTrans — Mathlib

Lean4
/-- The canonical natural transformation
`(whiskeringRight Cᵒᵖ A B).obj F ⋙ G₂ ⟶ G₁ ⋙ sheafCompose J F`
when `F : A ⥤ B` is such that `J.HasSheafCompose F`, and that `G₁` and `G₂` are
left adjoints to the forget functors `sheafToPresheaf`. -/
def sheafComposeNatTrans : (whiskeringRight Cᵒᵖ A B).obj F ⋙ G₂ ⟶ G₁ ⋙ sheafCompose J F
    where
  app P := (adj₂.homEquiv _ _).symm (whiskerRight (adj₁.unit.app P) F)
  naturality {P Q}
    f := by
    dsimp
    erw [← adj₂.homEquiv_naturality_left_symm, ← adj₂.homEquiv_naturality_right_symm]
    dsimp
    rw [← whiskerRight_comp, ← whiskerRight_comp]
    erw [adj₁.unit.naturality f]
    rfl
Похожие утверждения