Span rank under operations

In this file we show how operations on submodules interact with Submodule.spanRank.

Main results

• Submodule.spanRank_baseChange_le: Base change doesn't increase the span rank.

• TensorProduct.spanFinrank_top_eq_of_residueField: For a finitely generated module over a local ring, the dimension of the base change to the residue field is equal to its span rank.

• IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace: The minimal number of generators of the unique maximal ideal is equal to the dimension of the cotangent space.

theorem Submodule.spanRank_baseChange_le {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module R M] (N : Submodule R M) : (baseChange A N).spanRank ≤ Cardinal.lift.{u_2, u_3} N.spanRank

theorem Submodule.FG.spanFinrank_baseChange_le {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module R M] (N : Submodule R M) (fg : N.FG) : (baseChange A N).spanFinrank ≤ N.spanFinrank

theorem TensorProduct.spanRank_top_le {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module R M] (N : Submodule R M) : ⊤.spanRank ≤ Cardinal.lift.{u_2, u_3} N.spanRank

theorem TensorProduct.spanFinrank_top_le_of_fg {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module R M] (N : Submodule R M) (fg : N.FG) : ⊤.spanFinrank ≤ N.spanFinrank

theorem TensorProduct.spanFinrank_top_eq_of_residueField {R : Type u_1} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] (N : Submodule R M) [IsLocalRing R] (fg : N.FG) : ⊤.spanFinrank = N.spanFinrank

theorem IsLocalRing.spanFinrank_eq_finrank_quotient {R : Type u_1} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsLocalRing R] (N : Submodule R M) (fg : N.FG) : N.spanFinrank = Module.finrank (R ⧸ maximalIdeal R) (↥N ⧸ maximalIdeal R • ⊤)

theorem IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg {R : Type u_1} [CommRing R] [IsLocalRing R] (fg : (maximalIdeal R).FG) : Submodule.spanFinrank (maximalIdeal R) = Module.finrank (ResidueField R) (CotangentSpace R)

theorem IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : Submodule.spanFinrank (maximalIdeal R) = Module.finrank (ResidueField R) (CotangentSpace R)

theorem IsLocalRing.spanFinrank_maximalIdeal_add_finrank_eq_of_surjective {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {S : Type u_4} [CommRing S] [IsLocalRing S] [Algebra R S] (surj : Function.Surjective ⇑(algebraMap R S)) [IsLocalHom (algebraMap R S)] : Submodule.spanFinrank (maximalIdeal S) + Module.finrank (ResidueField R) ↥(Submodule.map (toCotangentSpace R) (Submodule.comap (Submodule.subtype (maximalIdeal R)) (RingHom.ker (algebraMap R S)))) = Submodule.spanFinrank (maximalIdeal R)