English
In ModuleCat(R), the limit cone for a discrete diagram exists and can be realized as ModuleCat.of R (∀ j, f j) with projections from the product.
Русский
В ModuleCat(R) существует предел для дискретного диаграммного вида: предел реализуется как ModuleCat.of(R, ∀ j, f_j) с проекциями из произведения.
LaTeX
$$$\text{Limits.LimitCone}(\mathrm{Discrete.functor}(f))$, with $\mathrm{pt} = \mathrm{ModuleCat.of}(R, \forall j, f_j)$ and projections $\pi_j$.$$
Lean4
/-- Construct limit data for a product in `ModuleCat R`, using `ModuleCat.of R (∀ j, F.obj j)`.
-/
@[simps]
def productLimitCone : Limits.LimitCone (Discrete.functor f)
where
cone :=
{ pt := ModuleCat.of R (∀ j, f j)
π := Discrete.natTrans fun j => ofHom (LinearMap.proj j.as : (∀ j, f j) →ₗ[R] f j.as) }
isLimit :=
{ lift := lift.{_, v} f
fac := fun _ _ => rfl
uniq := fun s m w => by
ext x j
exact congr_arg (fun g : s.pt ⟶ f j => (g : s.pt → f j) x) (w ⟨j⟩) }
