English
Given a cone s over a diagram f: J → ModuleCat R, there is a canonical morphism from the cone point to the product object ModuleCat.of R (∀ j, f j), whose j-th component equals the j-th leg of the cone, i.e., the lift is defined by (lift s)ᵢ = s.π.app ⟨i⟩. This exhibits the product as a limit of the diagram.
Русский
Пусть дан конус s над диаграммой f: J → ModuleCat R. Существует каноническое отображение из вершины конуса к объекту произведения ModuleCat.of R (∀ j, f j), такое что его j-я компонента равна j-й ноге конуса: lift s определяется как (lift s)ⱼ = s.π.app ⟨j⟩. Это демонстрирует, что произведение является пределом диаграммы.
LaTeX
$$$$ \text{lift}(s): s.pt \to \mathrm{ModuleCat.of}\,R\bigl(\forall j, f(j)\bigr), \quad \pi_j \circ \text{lift}(s) = s.\pi.app\langle j \rangle \quad \text{for all } j \in J. $$$$
Lean4
/-- The map from an arbitrary cone over an indexed family of abelian groups
to the Cartesian product of those groups.
-/
@[simps!]
def lift (s : Fan f) : s.pt ⟶ ModuleCat.of R (∀ j, f j) :=
ofHom
{ toFun := fun x j => s.π.app ⟨j⟩ x
map_add' := fun x y => by
simp only [Functor.const_obj_obj, map_add]
rfl
map_smul' := fun r x => by
simp only [Functor.const_obj_obj, map_smul]
rfl }
