isLimitPullbackCone — Mathlib

English

There is a canonical IsLimit structure on pullbackCone f g pb, built from the isLimit pb i data and the universal property of the pullback.

Русский

Существует каноническая структура IsLimit на pullbackCone f g pb, объединяющая данные pb i и универсальность обратного предела.

LaTeX

$$$\\text{isLimitPullbackCone} : \\mathrm{IsLimit} (\\mathrm{pullbackCone}\\ f\\ g\\ pb)$$$

Lean4

/-- `pullbackCone f g pb` is a pullback. -/
def isLimitPullbackCone : IsLimit (pullbackCone f g pb) :=
  by
  refine
    PullbackCone.IsLimit.mk (fst := (pullbackCone f g pb).fst) (snd := (pullbackCone f g pb).snd) _
      (fun s ↦ (homPullbackEquiv f g pb hpb s.pt).2 ⟨(s.fst, s.snd), s.condition⟩)
      (fun s ↦ congrArg (·.1.fst) ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
      (fun s ↦ congrArg (·.1.snd) ((homPullbackEquiv f g pb hpb s.pt).right_inv ⟨(s.fst, s.snd), s.condition⟩))
      (fun s m h₁ h₂ ↦ ?_)
  convert ((homPullbackEquiv f g pb hpb s.pt).left_inv m).symm using 3
  rw [← h₁, ← h₂];
  rfl
    -- Arguments cannot be inferred.

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