pullbackConeIsLimit — Mathlib

English

The isomorphism pullbackIsoProdSubtype f g equals the limit-cone point unique up to iso map derived from the cospan limit construction.

Русский

Изоморфизм pullbackIsoProdSubtype f g эквивалентен конструктору ограничений через ограничение по пределу для коспонной диаграммы.

LaTeX

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

Lean4

/-- The constructed cone is a limit. -/
def pullbackConeIsLimit (f : X ⟶ Z) (g : Y ⟶ Z) : IsLimit (pullbackCone f g) :=
  PullbackCone.isLimitAux' _
    (by
      intro S
      constructor; swap
      ·
        exact
          ofHom
            { toFun := fun x => ⟨⟨S.fst x, S.snd x⟩, by simpa using ConcreteCategory.congr_hom S.condition x⟩
              continuous_toFun := by fun_prop }
      refine ⟨?_, ?_, ?_⟩
      · delta pullbackCone
        ext a
        dsimp
      · delta pullbackCone
        ext a
        dsimp
      · intro m h₁ h₂
        ext x
        apply Subtype.ext
        apply Prod.ext
        · simpa using ConcreteCategory.congr_hom h₁ x
        · simpa using ConcreteCategory.congr_hom h₂ x)

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