expComparison_iso_of_frobeniusMorphism_iso

English

If expComparison is an isomorphism, then Frobenius morphism is an isomorphism.

Русский

Если expComparison является изоморфизмом, тогда морфизм Фробениуса является изоморфизмом.

LaTeX

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

Lean4

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

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