proj — Mathlib

English

For each i, there is a canonical isometry from pi (Pi.single i Q) to Q_i, called Isometry.proj.

Русский

Для каждой i существует каноническая изометрия от pi(Pi.single i Q) к Q_i, обозначаемая Isometry.proj.

LaTeX

$$$ \\text{Isometry.proj}_{i} : \\mathrm{pi}(\\mathrm{Pi.single}_{i} Q) \\to Q_i. $$$

Lean4

/-- `LinearMap.proj` as an isometry, when all but one quadratic form is zero. -/
@[simps!]
def proj [Fintype ι] [DecidableEq ι] (i : ι) (Q : QuadraticMap R (Mᵢ i) P) : pi (Pi.single i Q) →qᵢ Q
    where
  toLinearMap := LinearMap.proj i
  map_app'
    m := by
    dsimp
    rw [pi_apply, Fintype.sum_eq_single i (fun j hij => ?_), Pi.single_eq_same]
    rw [Pi.single_eq_of_ne hij, zero_apply]

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