pullback_snd_isIso_of_range_subset

English

Two open immersions with equal left image are isomorphic; there is a canonical isomorphism X ≅ Y determined by the common image.

Русский

Два открытых вложения с одинаковым изображением слева изоморфны; существует каноническое изоморождение X ≅ Y, определяемое общим изображением.

LaTeX

$$$X \cong Y$$$

Lean4

theorem pullback_snd_isIso_of_range_subset (H : Set.range g.base ⊆ Set.range f.base) : IsIso (pullback.snd f g) :=
  by
  haveI := TopCat.snd_iso_of_left_embedding_range_subset hf.base_open.isEmbedding g.base H
  have : IsIso (pullback.snd f g).base := by
    delta pullback.snd
    rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
    change IsIso (_ ≫ pullback.snd _ _)
    infer_instance
  apply to_iso

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