pullbackCone — Mathlib

English

There is a canonical isomorphism between the pullback pb(f,g) and the subtype TopCat.of { p: X×Y | f p.1 = g p.2 }.

Русский

Существует каноническое изоморфизм pb(f,g) и подмножество-структура TopCat.of { p: X×Y | f p.1 = g p.2 }.

LaTeX

$$$\\mathrm{pullbackIsoProdSubtype}(f,g) : pb(f,g) \\cong TopCat.of\\{ p:\\,X\\times Y \\mid f p.1 = g p.2\\}$$$

Lean4

/-- The explicit pullback cone of `X, Y` given by `{ p : X × Y // f p.1 = g p.2 }`. -/
def pullbackCone (f : X ⟶ Z) (g : Y ⟶ Z) : PullbackCone f g :=
  PullbackCone.mk (pullbackFst f g) (pullbackSnd f g)
    (by
      dsimp [pullbackFst, pullbackSnd, Function.comp_def]
      ext ⟨x, h⟩
      simpa)

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