frobeniusMorphism_iso_of_preserves_binary_products

English

For a left adjoint L ⊣ F and A, the mate of FrobeniusMorphism F h A under conjugateEquiv equals expComparison F A.

Русский

Для левого пары L ⊣ F и A мари FrobeniusMorphism F h A через сопряжённость эквивалентности равна expComparison F A.

LaTeX

$$$\text{conjugateEquiv} (h \cdot (\exp.adjunction A)) ((\exp.adjunction (F.obj A)).\cdot h) (\mathrm{frobeniusMorphism}\; F\; h\; A).\mathrm{natTrans} = (\expComparison\; F\; A).\mathrm{natTrans}$$$

Lean4

/-- If `F` is full and faithful and has a left adjoint `L` which preserves binary products, then the
Frobenius morphism is an isomorphism.
-/
instance frobeniusMorphism_iso_of_preserves_binary_products (h : L ⊣ F) (A : C)
    [Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) L] [F.Full] [F.Faithful] :
    IsIso (frobeniusMorphism F h A).natTrans :=
  suffices ∀ (X : D), IsIso ((frobeniusMorphism F h A).natTrans.app X) from NatIso.isIso_of_isIso_app _
  fun B ↦ by dsimp [frobeniusMorphism]; infer_instance

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