Documentation

LeanPool.CompositionAlgebrasOverRings.QuadraticForm.Representation

The representation lemma (GPR 11.26, GN Lemma C.13(a)) #

Over an LG-ring R, a non-singular quadratic form (M, q) with M finitely generated projective represents a unit — q(M) ∩ Rˣ ≠ ∅ — if and only if M has full support.

GPR 11.26 states this for q regular; GN C.13(a) observes that the same proof gives the non-singular case, which is the version formalized here (IsGPRNonsingular, from QuadraticForm/Regularity.lean).

Main definitions #

Main results #

Implementation notes #

GPR 11.8 (QuadraticForm/Polynomial.lean) writes a quadratic form on a free module as a polynomial, and M is only projective, so the hard direction looks as though it needs a basis — which is how GPR and GN proceed, reducing to the constant-rank case by the rank decomposition (GPR Exc. 9.31) and then invoking constant-rank-projective ⇒ free (GPR 11.24 = GN 2.6(b)).

That route is available in this development (Module/RankDecomposition.lean and LGRing/ConstantRank.lean), but it is not the route taken here. Choosing a presentation π : Rⁿ ↠ M and pulling q back to q ∘ π on the free module Rⁿ is enough: the polynomial of GPR 11.8 then exists outright, and the residue-field hypothesis survives the pullback because π ⊗ k is still surjective. So neither GN 2.6(b) nor the rank decomposition is needed for GPR 11.26. This is the same device that proves GN 2.6(a) in LGRing/Unimodular.lean.

The pullback is compared with base change by QuadraticForm.baseChangeOfProjective_comp.

References #

source
def Module.HasFullSupport (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] :
Prop

M has full support over R: base change to every field in R-alg is nonzero. This is condition (iv) of GPR 11.25; GPR and GN also call a finitely generated projective module with this property faithfully projective.

Equations
Instances For
    source
    theorem Module.hasFullSupport_iff_support_eq_univ {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] :
    HasFullSupport R M ↔ support R M = Set.univ

    Full support is mathlib's Module.support R M = Set.univ, for M finitely generated.

    F ⊗[R] M ≠ 0 at the residue field κ(𝔭) of every prime is membership of 𝔭 in the support (Module.mem_support_iff_nontrivial_residueField_tensorProduct, which is where finite generation is used). Conversely, a field F ∈ R-alg receives κ(𝔭) for 𝔭 = ker (R → F), and F ⊗[R] M = F ⊗[κ(𝔭)] (κ(𝔭) ⊗[R] M) is nonzero because F is faithfully flat over the field κ(𝔭).

    source
    theorem Module.HasFullSupport.nontrivial_quotient_tensor {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (h : HasFullSupport R M) (𝔪 : Ideal R) [𝔪.IsMaximal] :
    Nontrivial (TensorProduct R (R ⧸ 𝔪) M)

    Full support gives the residue-field condition — condition (iv) of GPR 11.25 implies condition (iii). This is the form the LG axiom consumes, since IsLGRing quantifies over residue fields.

    The converse also holds for M finitely generated projective (GPR 11.25), but needs the rank function on projective modules: a field F ∈ R-alg has ker (algebraMap R F) prime, and one must know that the rank at that prime agrees with the rank at a maximal ideal containing it. That is not proved here.

    source
    theorem Module.exists_isUnimodular_of_hasFullSupport {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (hLG : IsLGRing R) (hM : HasFullSupport R M) :
    ∃ (m : M), IsUnimodular R m

    GN 2.6(a), in terms of full support: over an LG-ring, a finitely generated projective module of full support contains a unimodular element. This is IsLGRing.exists_isUnimodular (LGRing/Unimodular.lean) fed through HasFullSupport.nontrivial_quotient_tensor.

    source
    theorem Module.hasFullSupport_of_isUnit_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (q : QuadraticForm R M) {m : M} (hm : IsUnit (q m)) :
    HasFullSupport R M

    GN C.13(a), (ai) ⇒ (aii). If q takes an invertible value then M has full support.

    No LG hypothesis and no freeness: the value q m ∈ Rˣ maps to a unit of F, so q_F (1 ⊗ m) ≠ 0, so 1 ⊗ m ≠ 0.

    source
    theorem QuadraticForm.exists_apply_ne_zero_of_radical_eq_bot {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] [Nontrivial V] (q : QuadraticForm F V) (h : QuadraticMap.radical q = ⊥) :
    ∃ (v : V), q v ≠ 0

    Over a field, a quadratic form with vanishing radical on a nonzero space takes a nonzero value. If it vanished identically, its polar form would too, so its radical would be all of V, contradicting radical = ⊥ on a nontrivial space.

    source
    theorem QuadraticForm.exists_isUnit_baseChange_of_hasFullSupport {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {q : QuadraticForm R M} (hq : q.IsGPRNonsingular) (hM : Module.HasFullSupport R M) (F : Type u) [Field F] [Algebra R F] :
    ∃ (x : TensorProduct R F M), IsUnit ((baseChangeOfProjective F q) x)

    The local half of GN C.13(a), (aii) ⇒ (ai). For q non-singular and M of full support, q represents a unit over every field F ∈ R-alg.

    Full support makes F ⊗[R] M nonzero and non-singularity makes the radical of q_F vanish, so q_F cannot be identically zero; over a field a nonzero value is a unit.

    This is precisely the hypothesis the LG axiom consumes — see the module docstring for what still stands between this and the global statement.

    The hard direction of GN C.13(a), (aii) ⇒ (ai) #

    source
    theorem QuadraticForm.exists_isUnit_apply_of_hasFullSupport {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (hLG : IsLGRing R) {q : QuadraticForm R M} (hq : q.IsGPRNonsingular) (hM : Module.HasFullSupport R M) :
    ∃ (m : M), IsUnit (q m)

    GN C.13(a), (aii) ⇒ (ai). Over an LG-ring, a non-singular quadratic form on a finitely generated projective module of full support represents a unit.

    This is the point where the LG axiom is applied. M need not be free, so there is no basis in which to write q as a polynomial; instead choose a presentation π : Rⁿ ↠ M and pull q back to q' := q ∘ π on the free module Rⁿ, where GPR 11.8 (QuadraticForm.aeval_toMvPolynomial) does apply. Then

    • q' represents a unit at every residue field k, because q does (exists_isUnit_baseChange_of_hasFullSupport) and π ⊗ k is still surjective, so the witness in k ⊗ M lifts to one in k ⊗ Rⁿ — which is free, so it can be expanded in coordinates to give the point of Fin n → k the LG axiom wants;
    • the axiom descends that to t : Fin n → R with q' t = q (π t) a unit.

    The comparison (q ∘ π)_k = q_k ∘ (π ⊗ k) is QuadraticForm.baseChangeOfProjective_comp.

    source
    theorem QuadraticForm.exists_isUnit_apply_iff_hasFullSupport {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (hLG : IsLGRing R) {q : QuadraticForm R M} (hq : q.IsGPRNonsingular) :
    (∃ (m : M), IsUnit (q m)) ↔ Module.HasFullSupport R M

    GPR 11.26, GN Lemma C.13(a). Over an LG-ring, a non-singular quadratic form on a finitely generated projective module represents a unit if and only if the module has full support.