Linear isometries as isometries of quadratic forms

A real quadratic form Q on a normed space is a fixed multiple of the squared norm when Q v = c * ‖v‖² for all v; for example the form Q v = -‖v‖² of the Clifford algebras of the Seiberg–Witten equations. A linear isometry equivalence preserves the norm, so it is an isometry equivalence between two such forms with the same constant c.

Main definitions

• LinearIsometryEquiv.toQuadraticIsometryEquiv: a linear isometry equivalence f : V ≃ V' as an isometry equivalence Q ≃ Q' of quadratic forms with Q v = c * ‖v‖² and Q' v = c * ‖v‖².

def LinearIsometryEquiv.toQuadraticIsometryEquiv {V : Type u_1} {V' : Type u_2} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [SeminormedAddCommGroup V'] [NormedSpace ℝ V'] {Q : QuadraticForm ℝ V} {Q' : QuadraticForm ℝ V'} {c : ℝ} (f : V ≃ₗᵢ[ℝ] V') (hQ : ∀ (v : V), Q v = c * ‖v‖ ^ 2) (hQ' : ∀ (v : V'), Q' v = c * ‖v‖ ^ 2) : QuadraticMap.IsometryEquiv Q Q'

A linear isometry equivalence is an isometry equivalence between quadratic forms that are the same multiple of the squared norm, Q v = c * ‖v‖² and Q' v = c * ‖v‖².

@[simp]

theorem LinearIsometryEquiv.coe_toQuadraticIsometryEquiv {V : Type u_1} {V' : Type u_2} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [SeminormedAddCommGroup V'] [NormedSpace ℝ V'] {Q : QuadraticForm ℝ V} {Q' : QuadraticForm ℝ V'} {c : ℝ} (f : V ≃ₗᵢ[ℝ] V') (hQ : ∀ (v : V), Q v = c * ‖v‖ ^ 2) (hQ' : ∀ (v : V'), Q' v = c * ‖v‖ ^ 2) : ⇑(f.toQuadraticIsometryEquiv hQ hQ') = ⇑f

The isometry equivalence of quadratic forms induced by f is f.

@[simp]

theorem LinearIsometryEquiv.toLinearEquiv_toQuadraticIsometryEquiv {V : Type u_1} {V' : Type u_2} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [SeminormedAddCommGroup V'] [NormedSpace ℝ V'] {Q : QuadraticForm ℝ V} {Q' : QuadraticForm ℝ V'} {c : ℝ} (f : V ≃ₗᵢ[ℝ] V') (hQ : ∀ (v : V), Q v = c * ‖v‖ ^ 2) (hQ' : ∀ (v : V'), Q' v = c * ‖v‖ ^ 2) : (f.toQuadraticIsometryEquiv hQ hQ').toLinearEquiv = f.toLinearEquiv

The underlying linear equivalence of the isometry equivalence of quadratic forms induced by f is that of f.