Local rings, dimension and completion

Local rings and their residue fields, Krull dimension, adic completion, regular local rings and length of modules.

• Adic completion
• Krull dimension
• Local rings and residue fields
• Maximal ideals in integral extensions of local rings
• Reconstructing complete local rings from quotients
• Regular local rings

TheoremFlat local maps reflect integrally closed domains#✓fully proved

A flat local homomorphism from a local ring to a domain and integrally closed local ring forces the source to be a domain and integrally closed. The flatness is stated with the Flat class of Mathlib 4.35, where the FLT source used the older RingHom.Flat spelling.

theorem IsIntegrallyClosed.isDomain_and_isIntegrallyClosed_of_flat_of_isLocalHom
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
    [IsDomain S] [IsIntegrallyClosed S] [Algebra R S] [Module.Flat R S]
    [IsLocalHom (algebraMap R S)] :
    IsDomain R ∧ IsIntegrallyClosed R

TheoremLength bound for a quotient containing a kernel#✓fully proved

If ker f ≤ K, the length of M ⧸ K is at most the length of N.

theorem Module.length_quotient_le_of_ker_le {R : Type*} {M : Type*} {N : Type*} [Ring R]
    [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    (K : Submodule R M) (f : M →ₗ[R] N) (h : LinearMap.ker f ≤ K) :
    Module.length R (M ⧸ K) ≤ Module.length R N

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.