ι_sq_scalar — Mathlib

English

A scalar relation holds for the square of the graded embedding, matching the quadratic form value via the graded algebra map.

Русский

Скалярая связь для квадрата вложения сохраняется: квадрат ι_Q(m) соответствуют значению Q(m) через алгебраическую передачу.

LaTeX

$$$ι_Q(m)^{2} = algebraMap_R(Q(m))$$$

Lean4

nonrec theorem ι_sq_scalar (m : M) : GradedAlgebra.ι Q m * GradedAlgebra.ι Q m = algebraMap R _ (Q m) :=
  by
  rw [GradedAlgebra.ι_apply Q, DirectSum.of_mul_of, DirectSum.algebraMap_apply]
  exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext rfl <| ι_sq_scalar _ _)

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