frobeniusMorphism_iso_of_expComparison_iso

English

If the Frobenius morphism at A is an isomorphism, then the exponential comparison at A is an isomorphism.

Русский

Если морфизм Фробениуса в A изоморфизм, то экспоненциальное сравнение в A изоморфизм.

LaTeX

$$$\text{IsIso}(\mathrm{frobeniusMorphism}\; F\; h\; A).\mathrm{natTrans} \Rightarrow \text{IsIso}(\mathrm{expComparison}\; F\; A).\mathrm{natTrans}$$$

Lean4

/-- If the exponential comparison transformation (at `A`) is an isomorphism, then the Frobenius morphism
at `A` is an isomorphism.
-/
theorem frobeniusMorphism_iso_of_expComparison_iso (h : L ⊣ F) (A : C) [i : IsIso (expComparison F A).natTrans] :
    IsIso (frobeniusMorphism F h A).natTrans :=
  by
  rw [← frobeniusMorphism_mate F h] at i
  exact @conjugateEquiv_of_iso _ _ _ _ _ _ _ _ _ _ _ i

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