to_iso — Mathlib

English

Under epi condition on base, open immersion is an isomorphism.

Русский

При условии эпиморфизма на базе открытого вложения — это изоморфизм.

LaTeX

$$$[\text{epi}(f.base)] \Rightarrow IsIso(f)$$$

Lean4

theorem to_iso [h' : Epi f.base] : IsIso f :=
  by
  suffices IsIso (LocallyRingedSpace.forgetToSheafedSpace.map f) from
    isIso_of_reflects_iso _ LocallyRingedSpace.forgetToSheafedSpace
  exact SheafedSpace.IsOpenImmersion.to_iso f.1

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