snd_iso_of_left_embedding_range_subset

English

If f is an embedding and range g is contained in range f, then pullback.snd f g is an isomorphism.

Русский

Если f — вложение и диапазон g ⊆ диапазон f, тогда pullback.snd f g — изоморфизм.

LaTeX

$$$ \text{IsIso}\big( \mathrm{pullback.snd} f g \big) $$$

Lean4

theorem snd_iso_of_left_embedding_range_subset {X Y S : TopCat} {f : X ⟶ S} (hf : IsEmbedding f) (g : Y ⟶ S)
    (H : Set.range g ⊆ Set.range f) : IsIso (pullback.snd f g) :=
  by
  let esto : (pullback f g : TopCat) ≃ₜ Y :=
    (snd_isEmbedding_of_left hf g).toHomeomorph.trans
      { toFun := Subtype.val
        invFun := fun x =>
          ⟨x, by
            rw [pullback_snd_range]
            exact ⟨_, (H (Set.mem_range_self x)).choose_spec⟩⟩ }
  convert (isoOfHomeo esto).isIso_hom

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