frobeniusMorphism — Mathlib

Lean4

/-- The Frobenius morphism for an adjunction `L ⊣ F` at `A` is given by the morphism

    L(FA ⨯ B) ⟶ LFA ⨯ LB ⟶ A ⨯ LB

natural in `B`, where the first morphism is the product comparison and the latter uses the counit
of the adjunction.

We will show that if `C` and `D` are Cartesian closed, then this morphism is an isomorphism for all
`A` iff `F` is a Cartesian-closed functor, i.e. it preserves exponentials.
-/
def frobeniusMorphism (h : L ⊣ F) (A : C) : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A) :=
  prodComparisonNatTrans L (F.obj A) ≫ Functor.whiskerLeft _ ((curriedTensor C).map (h.counit.app _))

Похожие утверждения