enrichedOrdinaryCategorySelf_homEquiv_symm

English

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

Русский

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

LaTeX

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

Lean4

theorem enrichedOrdinaryCategorySelf_homEquiv_symm {X Y : C} (g : 𝟙_ C ⟶ (ihom X).obj Y) :
    (eHomEquiv C).symm g = uncurry' g :=
  rfl

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