Lengths along extensions of local rings

This file proves results relating lengths along extensions of local rings.

Main results

• IsLocalRing.length_restrictScalars: If B/A is an extension of local rings, and if M is a B-module, then ℓ_A(M) = ℓ_B(M) * [κ(B) : κ(A)].
• IsLocalRing.length_baseChange: If B/A is a flat extension of local rings, and if M is an A-module, then ℓ_B(B ⊗[A] M) = ℓ_A(M) * ℓ_B(B ⧸ m_A).

theorem CovBy.length_restrictScalars (A : Type u_1) {B : Type u_2} {M : Type u_3} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M] {p q : Submodule B M} (h : p ⋖ q) : Module.length A ↥q = Module.length A ↥p + Module.length (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)

theorem IsLocalRing.length_restrictScalars (A : Type u_1) (B : Type u_2) (M : Type u_3) [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M] : Module.length A M = Module.length B M * Module.length (ResidueField A) (ResidueField B)

If B/A is an extension of local rings, and if M is a B-module, then ℓ_A(M) = ℓ_B(M) * [κ(B) : κ(A)].

theorem CovBy.length_baseChange {A : Type u_1} (B : Type u_2) {M : Type u_3} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [AddCommGroup M] [Module A M] [Module.Flat A B] {p q : Submodule A M} (h : p ⋖ q) : Module.length B ↥(Submodule.baseChange B q) = Module.length B ↥(Submodule.baseChange B p) + Module.length B (B ⧸ Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A))

theorem IsLocalRing.length_baseChange (A : Type u_1) (B : Type u_2) (M : Type u_3) [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [AddCommGroup M] [Module A M] [Module.Flat A B] : Module.length B (TensorProduct A B M) = Module.length A M * Module.length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

If B/A is a flat extension of local rings, and if M is an A-module, then ℓ_B(B ⊗[A] M) = ℓ_A(M) * ℓ_B(B ⧸ m_A).