Documentation

TauCeti.LinearAlgebra.QuadraticForm.Radical

Radical API for quadratic forms #

This file records basic properties of the radical of a quadratic form (such as its invariance under negation and orthogonal products) and general consequences of nondegeneracy, together with the two facts about the quadratic form x ↦ B x x of a symmetric bilinear form B that a Clifford construction consumes: its polar form is 2 • B, and nondegeneracy passes from B to it as soon as 2 is invertible.

Main results #

source
theorem QuadraticMap.isSymm_polarBilin {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
LinearMap.BilinForm.IsSymm (polarBilin Q)

The polar bilinear form of a scalar-valued quadratic map is symmetric.

source
@[simp]
theorem QuadraticMap.polarBilin_restrict {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (Q : QuadraticMap R M P) (W : Submodule R M) :
(Q.restrict W).polarBilin = LinearMap.domRestrict₁₂ Q.polarBilin W W

Polarization commutes with restricting a quadratic map to a submodule.

source
@[simp]
theorem QuadraticMap.radical_neg {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (Q : QuadraticMap R M P) :
(-Q).radical = Q.radical

Negating a quadratic map does not change its radical.

source
@[simp]
theorem QuadraticMap.nondegenerate_neg {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (Q : QuadraticMap R M P) :
Nondegenerate ↔ Nondegenerate

Negating a quadratic map does not change its nondegeneracy.

source
@[simp]
theorem QuadraticMap.radical_smul {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] {a : R} (ha : IsUnit a) (Q : QuadraticMap R M P) :
(a • Q).radical = Q.radical

Scaling a quadratic map by a unit does not change its radical.

source
@[simp]
theorem QuadraticMap.nondegenerate_smul_iff {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] {a : R} (ha : IsUnit a) (Q : QuadraticMap R M P) :
Nondegenerate ↔ Nondegenerate

Scaling a quadratic map by a unit does not change its nondegeneracy.

source
@[simp]
theorem QuadraticMap.radical_prod {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] {M' : Type u_4} [AddCommGroup M'] [Module R M'] [Invertible 2] (Q : QuadraticMap R M P) (Q' : QuadraticMap R M' P) :
(Q.prod Q').radical = Q.radical.prod Q'.radical

The radical of an orthogonal product is the product of the two radicals when two is invertible.

source
theorem QuadraticMap.nondegenerate_of_ker_polarBilin_eq_bot {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] {Q : QuadraticMap R M P} (hker : LinearMap.ker Q.polarBilin = ⊥) :
Nondegenerate

A quadratic map whose polar form has trivial kernel is nondegenerate.

source
theorem QuadraticMap.Isometry.injective_of_radical_eq_bot {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] {M' : Type u_4} [AddCommGroup M'] [Module R M'] {Q₁ : QuadraticMap R M P} {Q₂ : QuadraticMap R M' P} (f : Q₁ →qᵢ Q₂) (h : Q₁.radical = ⊥) :
Function.Injective ⇑f

An isometry out of a quadratic map with trivial radical is injective. Its kernel lies in the radical: an element x killed by f has Q₁ x = Q₂ 0 = 0 and Q₁ (x + n) = Q₂ (f n) = Q₁ n.

source
theorem QuadraticMap.exists_isUnit_of_ne_zero {K : Type u_5} {V : Type u_6} [Semifield K] [AddCommMonoid V] [Module K V] {Q : QuadraticForm K V} (hQ : Q ≠ 0) :
∃ (v : V), IsUnit (Q v)

A nonzero quadratic form over a semifield has a vector of unit norm.

source
theorem QuadraticMap.isUnit_apply_smul {S : Type u_5} {N : Type u_6} [CommSemiring S] [AddCommMonoid N] [Module S N] {Q : QuadraticForm S N} {c : S} {v : N} (hc : IsUnit c) (hv : IsUnit (Q v)) :
IsUnit (Q (c • v))

Scaling a vector of unit norm by a unit preserves unit norm.

source
noncomputable def QuadraticMap.liftOfSurjective {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] {N : Type u_5} [AddCommGroup N] [Module R N] (Q : QuadraticMap R M P) (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) (h : f.ker ≤ Q.radical) :
QuadraticMap R N P

Descend a quadratic map along a surjective linear map whose kernel lies in its radical.

Mathlib's QuadraticMap.lift descends along the quotient by a submodule of the radical. A quotient is usually presented instead by a surjection onto a concrete group — reduction modulo m onto ZMod m, say — and this is that formulation.

Equations
Instances For
    source
    @[simp]
    theorem QuadraticMap.liftOfSurjective_apply {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] {N : Type u_5} [AddCommGroup N] [Module R N] (Q : QuadraticMap R M P) (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) (h : f.ker ≤ Q.radical) (x : M) :
    (Q.liftOfSurjective f hf h) (f x) = Q x

    The descended quadratic map takes the original value on every representative.

    source
    theorem QuadraticMap.Nondegenerate.polarBilin_ne_zero {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] {Q : QuadraticForm K V} {u : V} (hQ : Nondegenerate) (hu : u ≠ 0) :
    (polarBilin Q) u ≠ 0

    The polar functional of a nonzero vector is nonzero for a nondegenerate quadratic form.

    source
    theorem QuadraticMap.Nondegenerate.prod {R : Type u_1} {M : Type u_2} {M' : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [AddCommGroup P] [Module R P] [Invertible 2] {Q : QuadraticMap R M P} {Q' : QuadraticMap R M' P} (hQ : Nondegenerate) (hQ' : Nondegenerate) :
    Nondegenerate

    The orthogonal product of two nondegenerate quadratic maps is nondegenerate, when 2 is invertible in the coefficient ring.

    source
    theorem QuadraticMap.Nondegenerate.ne_zero {R : Type u_1} {M : Type u_2} {P : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] [Nontrivial M] {Q : QuadraticMap R M P} (hQ : Nondegenerate) :
    Q ≠ 0

    A nondegenerate quadratic map on a nontrivial module is nonzero.

    source
    theorem QuadraticMap.Nondegenerate.exists_isUnit {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] [Nontrivial V] {Q : QuadraticForm K V} (hQ : Nondegenerate) :
    ∃ (v : V), IsUnit (Q v)

    A nondegenerate quadratic form on a nontrivial vector space has a vector of nonzero norm.

    source
    theorem QuadraticMap.Nondegenerate.isCompl_orthogonal {K : Type u_5} [Field K] [Invertible 2] {V : Type u_6} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} {W : Submodule K V} (hW : Nondegenerate) :
    IsCompl W (LinearMap.BilinForm.orthogonal (polarBilin Q) W)

    A subspace on which a quadratic form restricts nondegenerately is complementary to its orthogonal complement.

    source
    theorem QuadraticMap.Nondegenerate.nondegenerate_restrict_orthogonal {K : Type u_5} [Field K] [Invertible 2] {V : Type u_6} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} {W : Submodule K V} (hQ : Nondegenerate) (hW : Nondegenerate) :
    Nondegenerate

    In a regular finite-dimensional quadratic space, the orthogonal complement of a regular subspace is regular.

    source
    theorem QuadraticMap.exists_orthogonal_anisotropic {V : Type u_2} {K : Type u_1} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NeZero 2] (Q : QuadraticForm K V) (hQ : Nondegenerate) (hrank : 2 ≤ Module.finrank K V) {y : V} (hy : Q y ≠ 0) :
    ∃ (z : V), IsOrtho Q z y ∧ Q z ≠ 0

    A nondegenerate quadratic space of dimension at least two has an anisotropic vector orthogonal to any given anisotropic vector.

    source
    theorem QuadraticMap.Anisotropic.radical_eq_bot {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {Q : QuadraticMap R M P} (hQ : Q.Anisotropic) :
    Q.radical = ⊥

    An anisotropic quadratic map has trivial radical.

    source
    theorem QuadraticMap.Anisotropic.nondegenerate {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] [Invertible 2] {Q : QuadraticMap R M P} (hQ : Q.Anisotropic) :
    Nondegenerate

    An anisotropic quadratic map is nondegenerate when 2 is invertible.

    source
    theorem LinearMap.BilinMap.polarBilin_toQuadraticMap_of_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {B : LinearMap.BilinMap R M N} (hB : flip B = B) :
    B.toQuadraticMap.polarBilin = 2 • B

    The polar form of the quadratic form of a symmetric bilinear form B is 2 • B. The polar form is B + B.flip, so symmetry collapses it.

    source
    theorem LinearMap.BilinForm.radical_toQuadraticMap {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (B : LinearMap.BilinForm R M) (hB : B.IsSymm) :
    (BilinMap.toQuadraticMap B).radical = ker B

    The radical of the quadratic form of a symmetric bilinear form equals the kernel of the bilinear form over a commutative ring in which 2 is invertible.

    source
    theorem LinearMap.BilinForm.Nondegenerate.toQuadraticMap {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {B : LinearMap.BilinForm R M} (hB : B.Nondegenerate) (hflip : LinearMap.flip B = B) :
    QuadraticMap.Nondegenerate

    Nondegeneracy passes from a symmetric bilinear form to its quadratic form over a ring in which 2 is invertible. Some hypothesis on 2 is needed: a quadratic form is a finer invariant than its polar form, and it is the bilinear form, not the polar form 2 • B, that is assumed nondegenerate here.

    source
    theorem TauCeti.nondegenerate_of_span_singleton_eq_top {R : Type u_1} {V : Type u_2} [CommRing R] [IsDomain R] [Invertible 2] [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} {v : V} (hspan : R ∙ v = ⊤) (hv : Q v ≠ 0) :
    QuadraticMap.Nondegenerate

    A form on a line spanned by a vector of nonzero value is nondegenerate.

    source
    theorem QuadraticMap.nondegenerate_smul_sq {R : Type u_1} [CommRing R] [IsDomain R] [Invertible 2] {a : R} (ha : a ≠ 0) :
    Nondegenerate

    The form x ↦ a x² on R is nondegenerate for a ≠ 0.