fst_iso_of_right_embedding_range_subset

English

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

Русский

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

LaTeX

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

Lean4

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

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