English
If P is stable under composition and base change and has postcomposition property, then the Over ⊤ X subcategory is closed under pullbacks.
Русский
Если P стабильна под композицией и базовым изменением и обладает свойством посткомпозиции, то подкатегория Over ⊤ X замкнута по pullbacks.
LaTeX
$$$$ \\operatorname{ClosedUnderLimitsOfShape}\\Bigl( \\text{WalkingCospan}, P.\\mathrm{overObj}(X) \\Bigr) $$$$
Lean4
/-- Let `P` be stable under composition and base change. If `P` satisfies cancellation on the right,
the subcategory of `Over X` defined by `P` is closed under pullbacks.
Without the cancellation property, this does not in general. Consider for example
`P = Function.Surjective` on `Type`. -/
theorem closedUnderLimitsOfShape_pullback [HasPullbacks T] [P.IsStableUnderComposition] [P.IsStableUnderBaseChange]
[P.HasOfPostcompProperty P] : ClosedUnderLimitsOfShape WalkingCospan (P.overObj (X := X)) :=
by
intro D c hc hf
have h :
IsPullback (c.π.app .left).left (c.π.app .right).left (D.map WalkingCospan.Hom.inl).left
(D.map WalkingCospan.Hom.inr).left :=
IsPullback.of_isLimit_cone <| Limits.isLimitOfPreserves (CategoryTheory.Over.forget X) hc
rw [P.overObj_iff, show c.pt.hom = (c.π.app .left).left ≫ (D.obj .left).hom by simp]
apply P.comp_mem _ _ (P.of_isPullback h.flip ?_) (hf _)
exact P.of_postcomp _ (D.obj WalkingCospan.one).hom (hf .one) (by simpa using hf .right)
