Isometries of quadratic maps

This file records general properties of quadratic-map isometries. It also reindexes a weighted sum of squares along an equivalence of its index type, which complements Mathlib's QuadraticForm.weightedSumSquaresCongr for equal weights and QuadraticForm.isometryEquivWeightedSumSquaresWeightedSumSquares for weights rescaled by squares.

Main results

• QuadraticMap.Isometry.polar_apply: an isometry preserves polarization.
• QuadraticForm.isIsometry_polarBilin_of_forall_map_app: a form-preserving linear map preserves the polar bilinear form.
• QuadraticMap.IsometryEquiv.polar_apply: an isometric equivalence preserves polarization.
• QuadraticMap.IsometryEquiv.polarKernelEquiv: an isometric equivalence restricts to an equivalence of the kernels of polarization against corresponding vectors.
• QuadraticMap.IsometryEquiv.trans_apply: composition of isometries acts by composition.
• QuadraticMap.IsometryEquiv.nondegenerate_iff: nondegeneracy is invariant under isometry.
• QuadraticForm.isometryEquivWeightedSumSquaresReindex: reindexing the weights of a weighted sum of squares along an equivalence of index types gives an isometric quadratic form.
• QuadraticForm.equivalent_weightedSumSquares_of_comp_eq: weighted sums of squares whose weights agree after reindexing are equivalent.

@[simp]

theorem QuadraticMap.Isometry.polar_apply {R : Type u} {M₁ : Type v} {M₂ : Type u_1} {N : Type w} [CommSemiring R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁ →qᵢ Q₂) (x y : M₁) : polar (⇑Q₂) (f x) (f y) = polar (⇑Q₁) x y

An isometry preserves the polarization of a quadratic map.

theorem QuadraticForm.isIsometry_polarBilin_of_forall_map_app {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {f : Module.End R M} (hf : ∀ (x : M), Q (f x) = Q x) : TauCeti.BilinForm.IsIsometry (QuadraticMap.polarBilin Q) f

A linear map preserving a quadratic form is an isometry of its polar bilinear form.

@[simp]

theorem QuadraticMap.IsometryEquiv.polar_apply {R : Type u} {M₁ : Type v} {M₂ : Type u_1} {N : Type w} [CommSemiring R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (x y : M₁) : polar (⇑Q₂) (e x) (e y) = polar (⇑Q₁) x y

An isometric equivalence preserves the polarization of a quadratic map.

@[simp]

theorem QuadraticMap.IsometryEquiv.map_polarKernel {R : Type u} {M₁ : Type v} {M₂ : Type u_1} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (x : M₁) : Submodule.map (↑e.toLinearEquiv) (Q₁.polarBilin x).ker = (Q₂.polarBilin (e x)).ker

An isometric equivalence maps the kernel of polarization against x onto the kernel of polarization against its image.

def QuadraticMap.IsometryEquiv.polarKernelEquiv {R : Type u} {M₁ : Type v} {M₂ : Type u_1} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (x : M₁) : ↥(Q₁.polarBilin x).ker ≃ₗ[R] ↥(Q₂.polarBilin (e x)).ker

The restriction of an isometric equivalence to the kernels of polarization against corresponding vectors.

Equations

• e.polarKernelEquiv x = e.ofSubmodules (Q₁.polarBilin x).ker (Q₂.polarBilin (e x)).ker ⋯

@[simp]

theorem QuadraticMap.IsometryEquiv.coe_polarKernelEquiv_apply {R : Type u} {M₁ : Type v} {M₂ : Type u_1} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (x : M₁) (y : ↥(Q₁.polarBilin x).ker) : ↑((e.polarKernelEquiv x) y) = e ↑y

The equivalence between polar kernels acts through the original isometry.

@[simp]

theorem QuadraticMap.IsometryEquiv.coe_polarKernelEquiv_symm_apply {R : Type u} {M₁ : Type v} {M₂ : Type u_1} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (x : M₁) (y : ↥(Q₂.polarBilin (e x)).ker) : ↑((e.polarKernelEquiv x).symm y) = e.symm ↑y

The inverse equivalence between polar kernels acts through the inverse isometry.

@[simp]

theorem QuadraticMap.IsometryEquiv.trans_apply {R : Type u} {M₁ : Type v} {M₂ : Type u_1} {M₃ : Type u_2} {N : Type w} [CommSemiring R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N} (f : Q₁.IsometryEquiv Q₂) (g : Q₂.IsometryEquiv Q₃) (x : M₁) : (f.trans g) x = g (f x)

The composition of two isometric equivalences acts by composing their underlying maps.

theorem QuadraticMap.IsometryEquiv.nondegenerate_iff {R : Type u} {M₁ : Type v} {M₂ : Type u_1} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) : Nondegenerate ↔ Nondegenerate

Nondegeneracy of a quadratic map is invariant under an isometric equivalence.

def QuadraticForm.isometryEquivWeightedSumSquaresReindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype ι] [Fintype ι'] [CommSemiring R] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) (e : ι' ≃ ι) : (QuadraticMap.weightedSumSquares R w).IsometryEquiv (QuadraticMap.weightedSumSquares R (w ∘ ⇑e))

Reindexing the weights of a weighted sum of squares along an equivalence of the index types gives an isometric quadratic form. The isometry is precomposition with the equivalence.

Equations

• QuadraticForm.isometryEquivWeightedSumSquaresReindex w e = { toLinearEquiv := LinearEquiv.funCongrLeft R R e, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.isometryEquivWeightedSumSquaresReindex_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype ι] [Fintype ι'] [CommSemiring R] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) (e : ι' ≃ ι) (x : ι → R) (i : ι') : (isometryEquivWeightedSumSquaresReindex w e) x i = x (e i)

The reindexing isometry acts on a vector by precomposition with the equivalence.

theorem QuadraticForm.equivalent_weightedSumSquares_of_comp_eq {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype ι] [Fintype ι'] [CommSemiring R] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] {w : ι → S} {w' : ι' → S} (e : ι' ≃ ι) (h : w ∘ ⇑e = w') : (QuadraticMap.weightedSumSquares R w').Equivalent (QuadraticMap.weightedSumSquares R w)

Weighted sums of squares whose weights agree after reindexing are equivalent.