English
Let Q be a quadratic form on a module M over a commutative ring R, and let A be a commutative ring with a compatible R-algebra structure (so that 2 is invertible in A). Then the polar bilinear form after base change to A satisfies polarBilin(Q.baseChange A) = BilinForm.baseChange A (polarBilin Q).
Русский
Пусть Q — квадратичная форма на модуле M над кольцом R, и пусть A — кольцо, над которым задана совместимая структура скаляров (так, что 2 обратимо в A). Тогда полярная билинейная форма квадратичной формы Q после базового изменения скаляров на A удовлетворяет равенству polarBilin(Q.baseChange A) = BilinForm.baseChange A(polarBilin Q).
LaTeX
$$$$ \\operatorname{polarBilin}(Q^{\\text{baseChange } A}) = \\operatorname{BilinForm.baseChange}_A\\bigl(\\operatorname{polarBilin} Q\\bigr). $$$$
Lean4
theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) :
polarBilin (Q.baseChange A) = BilinForm.baseChange A (polarBilin Q) := by
rw [QuadraticForm.baseChange, BilinForm.baseChange, polarBilin_tmul, BilinForm.tmul, ← LinearMap.map_smul, smul_tmul',
← two_nsmul_associated R, coe_associatedHom, associated_sq, smul_comm, ← smul_assoc, two_smul,
invOf_two_add_invOf_two, one_smul]
