English
If e is a linear equivalence N ≃ₗ[R] P, then quadratic maps M → N are in natural bijection with quadratic maps M → P, given by Q ↦ e ∘ Q and Q' ↦ e^{-1} ∘ Q'.
Русский
Если e — линейное эквивалентность N ≃ₗ[R] P, то квадратичные отображения M → N и M → P эквивидны; Q ↦ e ∘ Q и Q' ↦ e^{-1} ∘ Q'.
LaTeX
$$$QuadraticMap\_R(M,N) \simeq_{\text{linear}} QuadraticMap\_R(M,P)$ via $Q \mapsto e\circ Q$ and $Q' \mapsto e^{-1}\circ Q'.$$$
Lean4
/-- When `N` and `P` are equivalent, quadratic maps on `M` into `N` are equivalent to quadratic
maps on `M` into `P`.
See `LinearMap.BilinMap.congr₂` for the bilinear map version. -/
@[simps]
def _root_.LinearEquiv.congrQuadraticMap (e : N ≃ₗ[R] P) : QuadraticMap R M N ≃ₗ[R] QuadraticMap R M P
where
toFun Q := e.compQuadraticMap Q
invFun Q := e.symm.compQuadraticMap Q
left_inv _ := ext fun _ => e.symm_apply_apply _
right_inv _ := ext fun _ => e.apply_symm_apply _
map_add' _ _ := ext fun _ => map_add e _ _
map_smul' _ _ := ext fun _ => e.map_smul _ _
