Module

LocalAlgebra.lean

Nyll.SchemeTheory.RingTheory.LocalAlgebra

4 declarations indexed from sourceView source ↗

Module documentation

Adic local algebras and module depth

A local ring is adic when its maximal ideal defines its topology. Topological finite generation means that finitely many algebra generators form a dense subalgebra. Module depth is the supremum of the lengths of weakly regular sequences in the maximal ideal.

Imports6

Mathlib.Data.ENat.Lattice
Mathlib.RingTheory.FiniteType
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Regular.RegularSequence
Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Mathlib.Topology.Algebra.Ring.Basic

Imported by13

class

IsAdicTopology

L34 ↗

IsLocalRing.IsAdicTopology

Documentation

The topology of the local ring is the adic topology defined by its maximal ideal.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing
namespace IsLocalRing

Lean source · full declaration

class IsAdicTopology (R : Type*) [CommRing R] [IsLocalRing R]
    [TopologicalSpace R] [IsTopologicalRing R] : Prop where
  /-- The maximal ideal defines the given adic topology. -/
  isAdic : IsAdic (maximalIdeal R)

class

TopologicallyFG

L43 ↗

Algebra.TopologicallyFG

Documentation

The algebra contains a dense subalgebra generated by finitely many elements over the base ring.

Source context 1 command

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing

Lean source · full declaration

class Algebra.TopologicallyFG (R S : Type*) [CommRing R] [Ring S] [Algebra R S]
    [TopologicalSpace S] [IsTopologicalRing S] : Prop where
  /-- A finite set of elements generates a dense subalgebra. -/
  out : ∃ s : Finset S, Dense (Algebra.adjoin R (s : Set S) : Set S)

instance

(anonymous instance)

L48 ↗

Source context 1 command

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing

Lean source · full declaration

instance (priority := 100) {R S : Type*} [CommRing R] [Ring S] [Algebra R S]
    [TopologicalSpace S] [IsTopologicalRing S] [Algebra.FiniteType R S] :
    Algebra.TopologicallyFG R S where
  out := have ⟨s, hs⟩ := Algebra.FiniteType.out (R := R) (A := S); ⟨s, by simp [hs]⟩

def

depth

L56 ↗

Module.depth

Documentation

The supremum of the lengths of weakly regular sequences in the maximal ideal acting on the module.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing
open RingTheory in

Lean source · statement

def Module.depth (R M : Type*) [CommRing R] [IsLocalRing R]
    [AddCommGroup M] [Module R M] : ℕ∞

Module documentation

Adic local algebras and module depth

Declarations

IsAdicTopology

TopologicallyFG

(anonymous instance)

depth