Documentation

LeanPool.CompositionAlgebrasOverRings.QuadraticForm.Isotropic

GPR-sense isotropy #

Defines QuadraticMap.IsGPRIsotropic: Q is isotropic iff it has a unimodular null vector (GPR 11.17), not merely a nonzero one.

⚠ This is not mathlib's QuadraticMap.Anisotropic. ¬ Q.Anisotropic unfolds to "there is a nonzero x with Q x = 0". GPR's isotropy demands a unimodular null vector — strictly stronger over a general ring, since unimodularity (mathlib's Module.IsUnimodular: some functional takes the value 1 at u, equivalently R·u is a free rank-1 direct summand, GPR 9.13) asks for more than u ≠ 0. The two notions coincide over a field, and GPR Exc. 12.38(c) shows they also coincide for finitely generated projective (that is, finite free) modules over a PID (the module hypothesis is needed: the zero form on the ℤ-module ℤ/2 has a nonzero null vector but no unimodular element); in general they do not, and the reduced-composition-algebra layer (GPR 22.9 ff.) needs the GPR notion specifically. See overview §6(c).

The name carries its source, as for the regularity ladder (QuadraticForm.IsGPRNondegenerate, IsGPRNonsingular, IsGPRRegular in QuadraticForm/Regularity.lean): there is no bare IsIsotropic here, precisely because "isotropic" means two different things in mathlib and in GPR and a bare name would hide which one is meant.

Main definitions #

GPR 11.17: isotropic vectors extend to hyperbolic pairs #

GPR 11.17 proves that for a quadratic space — a regular form in the sense of QuadraticForm.IsGPRRegular — a vector is isotropic exactly when it is the first member of a hyperbolic pair. That is QuadraticForm.isGPRIsotropic_iff_exists_isHyperbolicPair below, with exists_isHyperbolicPair_of_isUnimodular for the substantive direction: regularity solves l = q(·, w) for the functional l witnessing unimodularity, and then -q(w) • u + w completes u to a pair.

⚠ Over a field, non-singularity is enough and regularity is not necessary: a non-singular form of odd rank in characteristic 2 is not regular (QuadraticForm.rankOne), yet its isotropic vectors still extend. So exists_isHyperbolicPair_of_radical_eq_bot is not a special case of GPR 11.17; it is the version the Witt-cancellation chain consumes at each residue field, where the forms being cancelled are only assumed non-singular (GN 6.5, not GPR 11.27).

Main results #

GPR Exc. 12.38(c) — that the two notions already coincide for a finitely generated projective, hence finite free, module over a PID, more generally than a field — is proved below by generating the ideal of the coordinates of a nonzero vector. A generator divides every coordinate; dividing by it gives a primitive, hence unimodular, vector. Homogeneity and the domain hypothesis preserve the null-vector equation.

References #

source
def QuadraticMap.IsGPRIsotropic {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (Q : QuadraticMap R M N) :
Prop

Q is isotropic in the GPR sense: it has a unimodular null vector (GPR 11.17).

Equations
Instances For
    source
    theorem QuadraticMap.IsGPRIsotropic.map_isometryEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {Q₁ : QuadraticMap R M N} {M' : Type u_1} [AddCommGroup M'] [Module R M'] {Q₂ : QuadraticMap R M' N} (h : Q₁.IsGPRIsotropic) (e : Q₁.IsometryEquiv Q₂) :
    Q₂.IsGPRIsotropic

    GPR-sense isotropy transports along an isometry equivalence. The null vector is carried by the underlying linear equivalence, which also preserves unimodularity.

    source
    theorem QuadraticMap.IsGPRIsotropic.not_anisotropic {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] [Nontrivial R] {Q : QuadraticMap R M N} (h : Q.IsGPRIsotropic) :
    ¬Q.Anisotropic
    source
    theorem QuadraticMap.isGPRIsotropic_of_not_anisotropic {K : Type u} [Field K] {M : Type v} [AddCommGroup M] [Module K M] {N : Type w} [AddCommGroup N] [Module K N] {Q : QuadraticMap K M N} (h : ¬Q.Anisotropic) :
    Q.IsGPRIsotropic

    Over a field, a not-anisotropic quadratic map is GPR-isotropic: the nonzero null vector mathlib gives you is automatically unimodular.

    source
    theorem QuadraticMap.isGPRIsotropic_iff_not_anisotropic {K : Type u} [Field K] {M : Type v} [AddCommGroup M] [Module K M] {N : Type w} [AddCommGroup N] [Module K N] {Q : QuadraticMap K M N} :
    Q.IsGPRIsotropic ↔ ¬Q.Anisotropic

    Over a field, GPR-sense isotropy and mathlib's ¬ Anisotropic are the same notion.

    GPR Exc. 12.38(c): isotropy over a PID #

    source
    theorem QuadraticMap.isGPRIsotropic_iff_not_anisotropic_of_pid {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {Q : QuadraticForm R M} :
    IsGPRIsotropic Q ↔ ¬Anisotropic Q

    GPR Exc. 12.38(c), for quadratic forms and with its trivial converse: over a PID, a quadratic form has a unimodular null vector if and only if it has a nonzero null vector. The module is only assumed finitely generated projective, which over a PID means finite free. GPR 22.19 applies this to the norm of a composition algebra (its conditions (ii) and (iii)).

    GPR 11.17: isotropic vectors and hyperbolic pairs #

    source
    theorem QuadraticForm.isGPRIsotropic_dualProd {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {m : M} (hm : Module.IsUnimodular R m) :
    QuadraticMap.IsGPRIsotropic (dualProd R M)

    The hyperbolic form dualProd R M is GPR-isotropic as soon as M contains a unimodular element m. The null vector is (0, m); a functional taking m to 1 extends across the product by the second projection.

    source
    theorem QuadraticForm.exists_isHyperbolicPair_of_isUnimodular {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (hQ : Q.IsGPRRegular) {u : M} (hu : Module.IsUnimodular R u) (hqu : Q u = 0) :
    ∃ (v : M), QuadraticMap.IsHyperbolicPair Q u v

    GPR 11.17, (i) ⇒ (ii). In a regular quadratic module an isotropic vector — a unimodular u with q u = 0 — extends to a hyperbolic pair.

    Regularity is used exactly once, to solve l = q(·, w) for the functional l with l u = 1 supplied by unimodularity (GPR 9.13); then GPR's formula v = -q(w) • u + w finishes the job (QuadraticMap.isHyperbolicPair_neg_smul_add).

    source
    theorem QuadraticForm.isUnimodular_of_isHyperbolicPair {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (h : QuadraticMap.IsHyperbolicPair Q u v) :
    Module.IsUnimodular R u

    GPR 11.17, (ii) ⇒ (i). The first member of a hyperbolic pair is isotropic in the GPR sense: it is unimodular, since q(·, v) sends it to 1. No hypothesis on Q.

    source
    theorem QuadraticForm.isGPRIsotropic_iff_exists_isHyperbolicPair {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (hQ : Q.IsGPRRegular) :
    QuadraticMap.IsGPRIsotropic Q ↔ ∃ (u : M) (v : M), QuadraticMap.IsHyperbolicPair Q u v

    GPR 11.17. A regular quadratic module is isotropic in the GPR sense exactly when it contains a hyperbolic pair.

    source
    theorem QuadraticForm.exists_isHyperbolicPair_of_radical_eq_bot {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] {q : QuadraticForm F V} (hq : QuadraticMap.radical q = ⊥) {u : V} (hu : u ≠ 0) (hqu : q u = 0) :
    ∃ (v : V), QuadraticMap.IsHyperbolicPair q u v

    The non-singular analogue of GPR 11.17 over a field. A nonzero null vector of a form with vanishing radical extends to a hyperbolic pair.

    ⚠ This is not an instance of GPR 11.17: over a field of characteristic 2 a non-singular form of odd rank has a degenerate polar form, so it is not regular, and GPR 11.17 does not apply. What replaces regularity is that u ∉ radical Q while Q u = 0, which forces q(u, ·) ≠ 0 directly. This is the form of the statement that the Witt-cancellation chain uses at each residue field (Dias II.6.1), where the forms being cancelled are only non-singular.