English
For each j, the projection from the limit cone to F(j) is an R-linear map.
Русский
Для каждого j проекция из предельного конуса к F(j) является R-линейным отображением.
LaTeX
$$$\text{limit}\\pi_{j}: \mathrm{Types.Small.limitCone}(F).pt \to (F \downarrow \mathrm{forget}(\mathrm{ModuleCat}\,R)).obj(j)$ является линейным отображением над R.$$
Lean4
/-- `limit.π (F ⋙ forget (ModuleCat.{w} R)) j` as an `R`-linear map. -/
def limitπLinearMap (j) :
(Types.Small.limitCone (F ⋙ forget (ModuleCat.{w} R))).pt →ₗ[R] (F ⋙ forget (ModuleCat R)).obj j
where
toFun := (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j
map_smul' _
_ :=
by
simp only [Types.Small.limitCone_π_app, ← Shrink.linearEquiv_apply R (F ⋙ forget (ModuleCat R)).sections, map_smul]
simp only [Shrink.linearEquiv_apply]
rfl
map_add' _
_ := by
simp only [Types.Small.limitCone_π_app, ← Equiv.addEquiv_apply, map_add]
rfl
