English
For W, W.IsStableUnderLimitsOfShape J holds if and only if W.limitsOfShape J ≤ W in the lattice of properties.
Русский
Для W выполняется равенство: устойчивость относительно пределов формы J эквивалентна W.limitsOfShape J ≤ W в решётке свойств.
LaTeX
$$$W.IsStableUnderLimitsOfShape J \iff W.limitsOfShape J \le W$$$
Lean4
instance : (W.limitsOfShape J).RespectsIso :=
RespectsIso.of_respects_arrow_iso _
(by
rintro ⟨_, _, f⟩ ⟨Y₁, Y₂, g⟩ e ⟨X₁, X₂, c₁, c₂, h₁, h₂, f, hf⟩
let e₁ := Arrow.leftFunc.mapIso e
let e₂ := Arrow.rightFunc.mapIso e
have fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift (Cone.mk _ (c₁.π ≫ f)) := e.inv.w.symm
let c₁' : Cone X₁ := { pt := Y₁, π := (Functor.const _).map e₁.inv ≫ c₁.π }
let c₂' : Cone X₂ := { pt := Y₂, π := (Functor.const _).map e₂.inv ≫ c₂.π }
have h₁' : IsLimit c₁' := IsLimit.ofIsoLimit h₁ (Cones.ext e₁)
have h₂' : IsLimit c₂' := IsLimit.ofIsoLimit h₂ (Cones.ext e₂)
obtain hg : h₂'.lift (Cone.mk _ (c₁'.π ≫ f)) = g :=
h₂'.hom_ext
(fun j ↦ by
rw [h₂'.fac]
simp [reassoc_of% fac, c₁', c₂'])
rw [← hg]
exact ⟨_, _, _, _, h₁', _, _, hf⟩)
