English
The fst projection in pullback cone of left lift preserves the first component.
Русский
Проекция fst в предельной схеме левого подъема сохраняет первую компоненту.
LaTeX
$$pullbackConeOfLeftLift f g s ≫ pullbackConeOfLeft f g).fst = s.fst$$
Lean4
/-- An open immersion is an iso if the underlying continuous map is epi. -/
theorem to_iso [h' : Epi f.base] : IsIso f :=
by
have : ∀ (U : (Opens Y)ᵒᵖ), IsIso (f.c.app U) := by
intro U
have : U = op (opensFunctor f |>.obj ((Opens.map f.base).obj (unop U))) :=
by
induction U with
| op U => ?_
cases U
dsimp only [Functor.op, Opens.map]
congr
exact (Set.image_preimage_eq _ ((TopCat.epi_iff_surjective _).mp h')).symm
convert H.c_iso (Opens.map f.base |>.obj <| unop U)
have : IsIso f.c := NatIso.isIso_of_isIso_app _
apply (config := { allowSynthFailures := true }) isIso_of_components
let t : X ≃ₜ Y :=
H.base_open.isEmbedding.toHomeomorph.trans
{ toFun := Subtype.val
invFun := fun x => ⟨x, by rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp h')]; trivial⟩ }
exact (TopCat.isoOfHomeo t).isIso_hom
