Module

LocalRingEquiv.lean

Nyll.ValuedFieldTheory.Valuation.LocalRingEquiv

4 declarations indexed from sourceView source ↗

Module documentation

Local-ring equivalences and maximal ideals

Equivalences of local rings preserve the maximal ideal and all of its powers. The resulting membership criterion is useful when transporting principal-unit filtrations between equivalent valuation rings.

Imports3

Mathlib.NumberTheory.RamificationInertia.Ramification
Mathlib.RingTheory.LocalRing.Basic
Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Imported by15

theorem

ringEquiv_map_maximalIdeal

L22 ↗

ValuationTheory.ringEquiv_map_maximalIdeal

Documentation

A local-ring equivalence maps the maximal ideal onto the maximal ideal.

Source context 1 command

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

namespace ValuationTheory

Lean source · statement

theorem ringEquiv_map_maximalIdeal
    {R S : Type*} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (e : R ≃+* S) :
    Ideal.map e.toRingHom (IsLocalRing.maximalIdeal R) =
      IsLocalRing.maximalIdeal S

theorem

ringEquiv_map_maximalIdeal_pow

L44 ↗

ValuationTheory.ringEquiv_map_maximalIdeal_pow

Documentation

A local-ring equivalence maps every power of the maximal ideal onto the corresponding power.

Source context 1 command

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

namespace ValuationTheory

Lean source · statement

theorem ringEquiv_map_maximalIdeal_pow
    {R S : Type*} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (e : R ≃+* S) (n : ℕ) :
    Ideal.map e.toRingHom (IsLocalRing.maximalIdeal R ^ n) =
      IsLocalRing.maximalIdeal S ^ n

theorem

ringEquiv_mem_maximalIdeal_pow_iff

L53 ↗

ValuationTheory.ringEquiv_mem_maximalIdeal_pow_iff

Documentation

Membership in a maximal-ideal power is preserved by a local-ring equivalence.

Source context 1 command

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

namespace ValuationTheory

Lean source · statement

theorem ringEquiv_mem_maximalIdeal_pow_iff
    {R S : Type*} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (e : R ≃+* S) (n : ℕ) (x : R) :
    e x ∈ IsLocalRing.maximalIdeal S ^ n ↔
      x ∈ IsLocalRing.maximalIdeal R ^ n

theorem

map_maximalIdeal_eq_pow_ramificationIdx

L68 ↗

ValuationTheory.map_maximalIdeal_eq_pow_ramificationIdx

Documentation

For an injective local map of discrete valuation rings, the image of the maximal ideal is the power prescribed by the ramification index.

Source context 1 command

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

namespace ValuationTheory

Lean source · statement

theorem map_maximalIdeal_eq_pow_ramificationIdx
    {R S : Type*} [CommRing R] [IsDomain R]
    [CommRing S] [IsDomain S]
    [IsDiscreteValuationRing R] [IsDiscreteValuationRing S]
    [Algebra R S] [IsLocalHom (algebraMap R S)]
    (hi : Function.Injective (algebraMap R S)) :
    Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) =
      IsLocalRing.maximalIdeal S ^
        Ideal.ramificationIdx'
          (IsLocalRing.maximalIdeal R) (IsLocalRing.maximalIdeal S)

Module documentation

Local-ring equivalences and maximal ideals

Declarations

ringEquiv_map_maximalIdeal

ringEquiv_map_maximalIdeal_pow

ringEquiv_mem_maximalIdeal_pow_iff

map_maximalIdeal_eq_pow_ramificationIdx