pullbackP1Iso_hom_ι — Mathlib

English

If every patch over X admits a pullback with Y over Z, then the global pullback f: X → Z and g: Y → Z exists.

Русский

Если на каждом участке покрытия X существуют пулбэки с Y над Z, то глобальный пулбэк f: X → Z и g: Y → Z существует.

LaTeX

$$$$ \text{HasPullback}(f,g) $$$$

Lean4

@[simp, reassoc]
theorem pullbackP1Iso_hom_ι (i : 𝒰.I₀) :
    (pullbackP1Iso 𝒰 f g i).hom ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i = pullback.fst _ _ := by
  rw [← gluing_ι, ← pullbackP1Iso_inv_fst, Iso.hom_inv_id_assoc]

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