English
A cone in PresheafOfModules is a limit if and only if its image under each evaluation functor evaluation R X is a limit.
Русский
Конус в PresheafOfModules является пределом тогда и только тогда, когда его образ под каждым отображением через evaluation R X является пределом.
LaTeX
$$evaluationJointlyReflectsLimits$$
Lean4
/-- A cone in the category `PresheafOfModules R` is limit if it is so after the application
of the functors `evaluation R X` for all `X`. -/
def evaluationJointlyReflectsLimits (c : Cone F) (hc : ∀ (X : Cᵒᵖ), IsLimit ((evaluation R X).mapCone c)) : IsLimit c
where
lift
s :=
{ app := fun X => (hc X).lift ((evaluation R X).mapCone s)
naturality := fun {X Y} f ↦
by
apply (isLimitOfPreserves (ModuleCat.restrictScalars (R.map f).hom) (hc Y)).hom_ext
intro j
have h₁ := (c.π.app j).naturality f
have h₂ := (hc X).fac ((evaluation R X).mapCone s) j
rw [Functor.mapCone_π_app, assoc, assoc, ← Functor.map_comp, IsLimit.fac]
dsimp at h₁ h₂ ⊢
rw [h₁, reassoc_of% h₂, Hom.naturality] }
fac s
j := by
ext1 X
exact (hc X).fac ((evaluation R X).mapCone s) j
uniq s m
hm := by
ext1 X
apply (hc X).uniq ((evaluation R X).mapCone s)
intro j
dsimp
rw [← hm, comp_app]
