English
If Q is a quadratic map between R-modules M→N and S is a base of scalars with R an S-algebra, then restricting scalars yields a quadratic map S M N with the same underlying function and adjusted scalar action.
Русский
Если Q — квадратичная карта между R-модулями M→N и S является базой скаляров, причём R является S-алгеброй, то ограничение скаляров даёт квадратичную карту S M N с той же базовой функцией и соответствующим действием скаляров.
LaTeX
$$$\\text{restrictScalars}(Q) : \\ QuadraticMap(S,M,N)$, with $\\text{restrictScalars}(Q)(x)=Q(x)$ and appropriate scalar-tower compatibility.$$
Lean4
/-- Compose a quadratic map with a linear function on the left. -/
@[simps +simpRhs]
def _root_.LinearMap.compQuadraticMap (f : N →ₗ[R] P) (Q : QuadraticMap R M N) : QuadraticMap R M P
where
toFun x := f (Q x)
toFun_smul b x := by simp only [Q.map_smul, map_smul]
exists_companion' :=
let ⟨B, h⟩ := Q.exists_companion
⟨B.compr₂ f, fun x y => by simp only [h, map_add, LinearMap.compr₂_apply]⟩
