productCone — Mathlib

English

The product cone in ModuleCat agrees with the usual module-theoretic product; projections are the standard projections to each Z_i.

Русский

Произведение в ModuleCat совпадает с обычным модульным произведением; проекции — стандартные проекции на Z_i.

LaTeX

$$$ \text{The concrete product cone is the usual product: } \prod_i Z_i. $$$

Lean4

/-- The product cone induced by the concrete product. -/
def productCone : Fan Z :=
  Fan.mk (ModuleCat.of R (∀ i : ι, Z i)) fun i => ofHom (LinearMap.proj i : (∀ i : ι, Z i) →ₗ[R] Z i)

Похожие утверждения