Documentation

LeanPool.CompositionAlgebrasOverRings.Module.Unimodular

Unimodular elements of a module #

An element m of an R-module M is unimodular when some linear functional takes the value 1 at m. This is mathlib's Module.IsUnimodular R m, which the library uses throughout. GPR 9.13 defines unimodularity differently, by asking that R·m be free of rank 1 and a direct summand of M, and observes there that the two agree. This file proves that agreement and supplies the API the rest of the library needs beyond what mathlib provides.

This is not a norm-theoretic notion — no quadratic form is in sight here — but it is the piece QuadraticForm/Isotropic.lean needs to state GPR-sense isotropy correctly (GPR 11.17): a unimodular null vector, not merely a nonzero one. See overview §6(c).

Main definitions #

Main results #

Implementation notes #

GPR also states unimodularity geometrically: m is unimodular iff m ⊗ 1_{κ(𝔭)} ≠ 0 for every 𝔭 ∈ Spec R (i.e. m survives in every residue field). ⚠ That criterion needs M finitely generated projective (GPR 9.17): in the ℤ-module ℤ ⊕ ℤ/2 the element (2, 1) survives in every residue field, but no linear functional takes it to 1. Only the two algebraic formulations above are formalized here; the geometric one is not. Note that residue fields cannot detect whether an element is nonzero — ε in the free rank-one module over 𝔽₂[ε]/(ε²) dies in every residue field — so the geometric criterion genuinely uses unimodularity, not mere non-vanishing.

We use mathlib's general lattice notion IsComplemented (Mathlib.Order.Disjoint) for "direct summand" in the GPR 9.13 characterization rather than inventing a submodule-specific one, per overview §0.

References #

source
theorem Module.isUnimodular_iff_injective_toSpanSingleton_and_isComplemented_span {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {m : M} :
IsUnimodular R m ↔ Function.Injective ⇑(LinearMap.toSpanSingleton R M m) ∧ IsComplemented (R ∙ m)

GPR 9.13: m is unimodular — hit by a functional — exactly when the cyclic submodule R·m is free of rank 1 (equivalently, r • m = 0 → r = 0) and a direct summand of M, which is how GPR 9.13 defines unimodularity.

source
theorem Module.IsUnimodular.map {R : Type u} [CommRing R] {M : Type u_1} [AddCommGroup M] [Module R M] {M' : Type u_2} [AddCommGroup M'] [Module R M'] {m : M} (hm : IsUnimodular R m) (e : M ≃ₗ[R] M') :
IsUnimodular R (e m)

Unimodularity transports along a linear equivalence: m unimodular in M and e : M ≃ₗ N give e m unimodular in N.

source
theorem Module.IsUnimodular.units_smul {R : Type u} [CommRing R] {M : Type u_1} [AddCommGroup M] [Module R M] {m : M} (hm : IsUnimodular R m) (u : Rˣ) :
IsUnimodular R (u • m)

Unimodularity is unaffected by scaling by a unit: if m is unimodular then so is u • m for u : Rˣ, since R·(u • m) = R·m.

source
theorem Module.isUnimodular_of_ne_zero {K : Type u} [Field K] {M : Type v} [AddCommGroup M] [Module K M] {x : M} (hx : x ≠ 0) :
IsUnimodular K x

Over a field, unimodular is exactly nonzero: every nonzero vector of a vector space is hit by a functional.

Splitting off a unimodular element #

A unimodular element does not merely span a complemented line — it splits M as R ⊕ M' with the free factor identified, which is what an induction on the rank needs.

source
noncomputable def LinearMap.equivProdKerOfApplyEqOne {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (l : M →ₗ[R] R) (m : M) (hl : l m = 1) :
M ≃ₗ[R] R × ↥l.ker

The splitting determined by a functional l with l m = 1: M ≃ R × ker l, by x ↦ (l x, x - l x • m) with inverse (r, y) ↦ r • m + y.

Since such an l is exactly a witness for Module.IsUnimodular R m, this says a unimodular element splits off a free rank-one direct summand. The complement is presented concretely as ker l rather than as an abstract summand so that it stays a Submodule R M, hence lives in the same universe as M — which is what makes the induction on the rank in Module.free_of_rankAtStalk_eq (LGRing/ConstantRank.lean) go through.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem LinearMap.equivProdKerOfApplyEqOne_symm_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (l : M →ₗ[R] R) (m : M) (hl : l m = 1) (x : R × ↥l.ker) :
    (l.equivProdKerOfApplyEqOne m hl).symm x = x.1 • m + ↑x.2
    source
    theorem Module.IsUnimodular.exists_linearEquiv_prod {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {m : M} (hm : IsUnimodular R m) :
    ∃ (M' : Submodule R M), Nonempty (M ≃ₗ[R] R × ↥M')

    A unimodular element splits M as R ⊕ M' for a submodule M' of M.

    source
    theorem Module.Finite.of_linearEquiv_prod {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] [Module.Finite R M] (e : M ≃ₗ[R] R × N) :
    Module.Finite R N

    A module that splits off a free rank-one summand from a finitely generated module is itself finitely generated.

    source
    theorem Module.Projective.of_linearEquiv_prod {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] [Projective R M] (e : M ≃ₗ[R] R × N) :
    Projective R N

    A module that splits off a free rank-one summand from a projective module is itself projective.