isPullback_aux — Mathlib

English

There is a map between Subobject induced by an isomorphism e: A ≅ B, i.e., Subobject.mapIso.

Русский

Существует отображение между подобъектами, индуцированное изоморфизмом e: A ≅ B, то есть Subobject.mapIso.

LaTeX

$$$\mathrm{map} : A \cong B \Rightarrow \mathrm{Subobject}(A) \simeq \mathrm{Subobject}(B)$$$

Lean4

theorem isPullback_aux (f : X ⟶ Y) (y : Subobject Y) : ∃ φ, IsPullback φ ((pullback f).obj y).arrow y.arrow f :=
  by
  obtain ⟨A, i, ⟨_, rfl⟩⟩ := mk_surjective y
  rw [pullback_obj]
  exists (underlyingIso (pullback.snd (mk i).arrow f)).hom ≫ pullback.fst (mk i).arrow f
  exact
    IsPullback.of_iso (IsPullback.of_hasPullback (mk i).arrow f) (underlyingIso (pullback.snd (mk i).arrow f)).symm
      (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp) (by simp) (by simp)

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