English
Restating the limit cone definition: for t a limit cone and s any cone, there exists a unique morphism l: s.pt ⟶ t.pt with l ≫ t.π.app j = s.π.app j for all j.
Русский
Переформулируя определение предельного конуса: для t — предел конуса и любого конуса s существует уникальный морфизм l: s.pt ⟶ t.pt такой, что l ≫ t.π.app j = s.π.app j для всех j.
LaTeX
$$$\\exists! l : s.pt \\to t.pt, \\forall j,\\; l \\gg t.π.app j = s.π.app j$$$
Lean4
/-- If `P` is stable under composition, base change and satisfies post-cancellation,
`P.Over ⊤ X` has pullbacks -/
instance (priority := 900) hasPullbacks [HasPullbacks T] [P.IsStableUnderComposition] [P.IsStableUnderBaseChange]
[P.HasOfPostcompProperty P] : HasPullbacks (P.Over ⊤ X) :=
haveI : HasLimitsOfShape WalkingCospan (Comma (𝟭 T) (Functor.fromPUnit X)) :=
inferInstanceAs <| HasLimitsOfShape WalkingCospan (Over X)
hasLimitsOfShape_of_closedUnderLimitsOfShape P (Over.closedUnderLimitsOfShape_pullback P)
