uniq — Mathlib

English

Any two arrows χ', π with the same pullback square must coincide: χ' = χ m.

Русский

Любые два стрелки χ', π с равной диаграммой вытягивания совпадают: χ' = χ m.

LaTeX

$$IsPullback m π χ' h.Ω₀.arrow → χ' = h.χ m$$

Lean4

theorem uniq {χ' : X ⟶ Ω} {π : U ⟶ h.Ω₀} (sq : IsPullback m π χ' h.Ω₀.arrow) : χ' = h.χ m :=
  by
  apply h.homEquiv.injective
  simp only [χ, Equiv.apply_symm_apply, homEquiv_eq]
  simpa using Subobject.pullback_obj_mk sq.flip

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