Modules over commutative rings

Projective, free and finitely generated modules over commutative rings and module-finite extensions: Kaplansky's theorem, the Quillen–Suslin theorem, descent of Noetherianness (Eakin–Nagata) and the direct summand theorem.

• Direct summand theorem

TheoremEakin–Nagata theorem#✓fully proved

Let \(A\) and \(B\) be commutative rings and let \(B\) be an \(A\)-algebra that is finitely generated as an \(A\)-module. If the structure map \(A \to B\) is injective and \(B\) is Noetherian, then \(A\) is Noetherian.

theorem eakin_nagata
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
    [Module.Finite A B] (hAB : Function.Injective (algebraMap A B))
    [IsNoetherianRing B] : IsNoetherianRing A

Sources

• P. M. Eakin Jr., 'The converse to a well known theorem on Noetherian rings', Mathematische Annalen 177 (1968), 278-282, DOI 10.1007/BF01350720.

TheoremFaithfully flat algebras inside a localization equal the base ring#✓fully proved

A faithfully flat R-algebra S which embeds compatibly in a localization K of R has bijective structure map. No restriction on the denominators or domain assumptions on the rings are required.

theorem IsLocalization.bijective_algebraMap_of_faithfullyFlat
    (R S K : Type*) [CommRing R] [CommRing S] [CommRing K]
    [Algebra R S] [Algebra S K] [Algebra R K] [IsScalarTower R S K]
    (M : Submonoid R) [IsLocalization M K]
    [FaithfulSMul S K] [Module.FaithfullyFlat R S] :
    Function.Bijective (algebraMap R S)

TheoremFinite projective modules of fiberwise rank one are invertible#✓fully proved

A finite projective module whose base change to every field has rank one is invertible.

This is the standard criterion for a module to define a line bundle: it is used to show that projective modules of constant rank one are invertible, to construct Picard group elements, and to recognize invertible sheaves from their fibers.

theorem Invertible.of_projective_of_forall_finrank_eq_one {A : Type u} [CommRing A]
    (P : Type v) [AddCommGroup P] [Module A P] [Module.Finite A P]
    [Module.Projective A P]
    (h : ∀ (K : Type u) [Field K] [Algebra A K],
      Module.finrank K (TensorProduct A K P) = 1) :
    Module.Invertible A P

TheoremKaplansky's theorem on projective modules over local rings#✓fully proved

Every projective module over a commutative local ring is free.

theorem kaplansky_projective_local_free
    {R : Type*} {M : Type*} [CommRing R] [IsLocalRing R]
    [AddCommGroup M] [Module R M] [Module.Projective R M] :
    Module.Free R M

Sources

• I. Kaplansky, Projective Modules, Ann. Math. 68 (1958), 372-377, DOI 10.2307/1970252.

TheoremQuillen–Suslin theorem#✓fully proved

Let \(k\) be a field and let \(n\) be a natural number. Every finitely generated projective module over the polynomial ring \(k[x_1, \dots, x_n]\) in \(n\) variables is free.

Proof: The argument follows Quillen's induction and patching route, using Roberts' idempotent-matrix proof of local Horrocks; see Quillen (1976), Lam, Lang, and Dicks.

theorem quillen_suslin
    {k : Type*} [Field k]
    {n : ℕ}
    {M : Type*} [AddCommGroup M] [Module (MvPolynomial (Fin n) k) M]
    [Module.Finite (MvPolynomial (Fin n) k) M]
    [Module.Projective (MvPolynomial (Fin n) k) M] :
    Module.Free (MvPolynomial (Fin n) k) M

Sources

• Serre's conjecture proved by D. Quillen, Invent. Math. 36 (1976) and A. A. Suslin, Dokl. Akad. Nauk SSSR 229 (1976); Lam, Serre's Problem; Lean states field case over MvPolynomial (Fin n) k with PID generalization existing.

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.