pullbackIsoProdSubtype — Mathlib

English

Equivalence of the canonical pullback-isomorphism with the limit-cone iso from the cospan, under the wide pullback framework.

Русский

Эквивалентность канонического изоморфизма pullback и subtype с пределом в рамках широкого вытягивания.

LaTeX

$$$\\mathrm{pullbackIsoProdSubtype}(f,g) = (\\mathrm{limit.isLimit}(\\mathrm{cospan} f g)).conePointUniqueUpToIso(\\mathrm{pullbackConeIsLimit} f g)$$$

Lean4

/-- The pullback of two maps can be identified as a subspace of `X × Y`. -/
def pullbackIsoProdSubtype (f : X ⟶ Z) (g : Y ⟶ Z) : pullback f g ≅ TopCat.of { p : X × Y // f p.1 = g p.2 } :=
  (limit.isLimit _).conePointUniqueUpToIso (pullbackConeIsLimit f g)

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