Documentation

LeanPool.CompositionAlgebrasOverRings.LGRing.Unimodular

Faithfully projective modules over an LG-ring contain a unimodular element (GN 2.6(a)) #

Over an LG-ring R, a finitely generated projective module M that is nonzero at every residue field contains a unimodular element.

Main definitions #

Main results #

Proof idea #

Write M as a retract of a finite free module: π : Rⁿ ↠ M and σ : M ↪ Rⁿ with π ∘ σ = id (Module.Finite.exists_comp_eq_id_of_projective). Put e := σ ∘ π, an idempotent endomorphism of Rⁿ, and let E i j := e (Pi.single j 1) i be its matrix in the standard basis.

For t c : Fin n → R set m := π t and l := ∑ᵢ cᵢ · (proj i ∘ σ) : M →ₗ[R] R. Then

l m = ∑ᵢ cᵢ · (e t)ᵢ = ∑ᵢ ∑ⱼ Eᵢⱼ tⱼ cᵢ,

which is exactly bilinearPairing E evaluated at the point (t, c) — and by GPR 9.13 (Module.isUnimodular_of_apply_eq_one), a value of 1 produces a unimodular element. So it suffices to know that bilinearPairing E represents a unit over R, and by the LG axiom that reduces to representing a unit over every residue field k = R ⧸ 𝔪.

Over k the polynomial represents a unit as soon as some entry of E survives in k: take t and c to be the corresponding standard basis vectors, and the double sum collapses to that entry. And if every entry died in k, then e ⊗ k = 0; since π ⊗ k and σ ⊗ k still compose to the identity of k ⊗[R] M, every x there satisfies σₖ x = σₖ (πₖ (σₖ x)) = eₖ (σₖ x) = 0, hence x = πₖ (σₖ x) = 0, contradicting the hypothesis that k ⊗[R] M is nonzero.

Implementation notes #

The hypothesis is stated as Nontrivial ((R ⧸ 𝔪) ⊗[R] M) for every maximal 𝔪 rather than as Module.HasFullSupport (QuadraticForm/Representation.lean), for two reasons: it is exactly what the proof consumes — the LG axiom quantifies over residue fields — and it keeps this file below QuadraticForm/ in the import order. Module.HasFullSupport.nontrivial_quotient_tensor supplies it, and Module.exists_isUnimodular_of_hasFullSupport in QuadraticForm/Representation.lean packages the combination.

Following the implementation notes of LGRing/Defs.lean, the residue field is handled through the Prop-valued IsField (R ⧸ 𝔪) rather than the bundled Field instance from Ideal.Quotient.field, which avoids the instance diamond entirely.

GN proves 2.6(a) by scheme theory, applying its Proposition 2.4 to the punctured affine space W(M) ∖ Spec(R), a quasi-compact open subscheme; that is a stronger form of the LG axiom than the one taken as the definition here. The argument above is elementary and uses only the single- polynomial axiom, at the cost of choosing a presentation of M.

References #

source
noncomputable def MvPolynomial.bilinearPairing {R : Type u} [CommRing R] {n : ℕ} (E : Fin n → Fin n → R) :
MvPolynomial (Fin (n + n)) R

The pairing polynomial of a square array E, in n + n variables: reading the first block of variables as a column vector t and the second as a row vector c, this is cᵀ E t.

Equations
Instances For
    source
    theorem MvPolynomial.aeval_bilinearPairing {R : Type u} [CommRing R] {n : ℕ} {S : Type v} [CommRing S] [Algebra R S] (E : Fin n → Fin n → R) (s : Fin (n + n) → S) :
    (aeval s) (bilinearPairing E) = ∑ i : Fin n, ∑ j : Fin n, (algebraMap R S) (E i j) * s (Fin.castAdd n j) * s (Fin.natAdd n i)

    Evaluating bilinearPairing E over an R-algebra S gives the double sum ∑ᵢ ∑ⱼ Eᵢⱼ tⱼ cᵢ, where t and c are the two blocks of the evaluation point.

    source
    theorem IsLGRing.exists_isUnimodular {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (hLG : IsLGRing R) (hM : ∀ (𝔪 : Ideal R), 𝔪.IsMaximal → Nontrivial (TensorProduct R (R ⧸ 𝔪) M)) :
    ∃ (m : M), Module.IsUnimodular R m

    GN 2.6(a). Over an LG-ring, a finitely generated projective module that is nonzero at every residue field contains a unimodular element.

    See the module docstring for the construction; Module.HasFullSupport.nontrivial_quotient_tensor supplies the hypothesis from the more geometric formulation.