English
Twice the associated bilinear map equals the polar bilinear form.
Русский
Дважды ассоциированное билинейное отображение равно полярной билинейной форме.
LaTeX
$$$ 2 \cdot \mathrm{associatedHom} \, S \, Q = Q \;\mathrm{polarBilin} $$$
Lean4
/-- `associatedHom` is the map that sends a quadratic map on a module `M` over `R` to its
associated symmetric bilinear map. As provided here, this has the structure of an `S`-linear map
where `S` is a commutative ring and `R` is an `S`-algebra.
Over a commutative ring, use `QuadraticMap.associated`, which gives an `R`-linear map. Over a
general ring with no nontrivial distinguished commutative subring, use `QuadraticMap.associated'`,
which gives an additive homomorphism (or more precisely a `ℤ`-linear map.) -/
def associatedHom : QuadraticMap R M N →ₗ[S] (BilinMap R M N)
where
toFun Q := ⅟(2 : Module.End R N) • polarBilin Q
map_add' _ _ := LinearMap.ext₂ fun _ _ ↦ by simp [polar_add]
map_smul' _ _ := LinearMap.ext₂ fun _ _ ↦ by simp [polar_smul]
