pi — Mathlib · SciLib

English

Define a quadratic form on a finite family of modules by summing the quadratic forms on each component after projecting onto that component.

Русский

Определим квадратичную форму на конечной семье модулей как сумму квадратичных форм по компонентам после проекции на соответствующую компоненту.

LaTeX

$$$ \\pi\\_ι Q = \\sum_{i} Q_i \\circ \\mathrm{proj}_i. $$$

Lean4

/-- Construct a quadratic form on a family of modules from the quadratic form on each module. -/
def pi [Fintype ι] (Q : ∀ i, QuadraticMap R (Mᵢ i) P) : QuadraticMap R (∀ i, Mᵢ i) P :=
  ∑ i, (Q i).comp (LinearMap.proj i : _ →ₗ[R] Mᵢ i)

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