Maximal ideal of local rings #

We prove basic properties of the maximal ideal of a local ring.

source

@[simp]

theorem IsLocalRing.mem_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] (x : R) :

x ∈ maximalIdeal R ↔ x ∈ nonunits R

source

instance IsLocalRing.maximalIdeal.isMaximal (R : Type u_1) [CommSemiring R] [IsLocalRing R] :

(maximalIdeal R).IsMaximal

source

theorem IsLocalRing.isMaximal_iff (R : Type u_1) [CommSemiring R] [IsLocalRing R] {I : Ideal R} :

I.IsMaximal ↔ I = maximalIdeal R

source

theorem IsLocalRing.maximal_ideal_unique (R : Type u_1) [CommSemiring R] [IsLocalRing R] :

∃! I : Ideal R, I.IsMaximal

source

theorem IsLocalRing.eq_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {I : Ideal R} (hI : I.IsMaximal) :

I = maximalIdeal R

source

instance IsLocalRing.instUniqueMaximalSpectrum {R : Type u_1} [CommSemiring R] [IsLocalRing R] :

Unique (MaximalSpectrum R)

The maximal spectrum of a local ring is a singleton.

Equations

IsLocalRing.instUniqueMaximalSpectrum = { default := { asIdeal := IsLocalRing.maximalIdeal R, isMaximal := ⋯ }, uniq := ⋯ }

source

theorem IsLocalRing.of_singleton_maximalSpectrum {R : Type u_1} [CommSemiring R] [Subsingleton (MaximalSpectrum R)] [Nonempty (MaximalSpectrum R)] :

IsLocalRing R

If the maximal spectrum of a ring is a singleton, then the ring is local.

source

theorem IsLocalRing.le_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {J : Ideal R} (hJ : J ≠ ⊤) :

J ≤ maximalIdeal R

source

theorem IsLocalRing.le_maximalIdeal_of_isPrime {R : Type u_1} [CommSemiring R] [IsLocalRing R] (p : Ideal R) [hp : p.IsPrime] :

p ≤ maximalIdeal R

source

theorem IsLocalRing.notMem_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {x : R} :

x ∉ maximalIdeal R ↔ IsUnit x

An element x of a commutative local semiring is not contained in the maximal ideal iff it is a unit.

source

@[deprecated IsLocalRing.notMem_maximalIdeal (since := "2025-05-23")]

theorem IsLocalRing.not_mem_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {x : R} :

x ∉ maximalIdeal R ↔ IsUnit x

Alias of IsLocalRing.notMem_maximalIdeal.

An element x of a commutative local semiring is not contained in the maximal ideal iff it is a unit.

source

theorem IsLocalRing.isField_iff_maximalIdeal_eq {R : Type u_1} [CommSemiring R] [IsLocalRing R] :

IsField R ↔ maximalIdeal R = ⊥

source

@[deprecated IsLocalRing.maximal_ideal_unique (since := "2024-11-11")]

theorem LocalRing.maximal_ideal_unique (R : Type u_1) [CommSemiring R] [IsLocalRing R] :

∃! I : Ideal R, I.IsMaximal

Alias of IsLocalRing.maximal_ideal_unique.

source

@[deprecated IsLocalRing.eq_maximalIdeal (since := "2024-11-11")]

theorem LocalRing.eq_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {I : Ideal R} (hI : I.IsMaximal) :

I = IsLocalRing.maximalIdeal R

Alias of IsLocalRing.eq_maximalIdeal.

source

@[deprecated IsLocalRing.le_maximalIdeal (since := "2024-11-11")]

theorem LocalRing.le_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {J : Ideal R} (hJ : J ≠ ⊤) :

J ≤ IsLocalRing.maximalIdeal R

Alias of IsLocalRing.le_maximalIdeal.

source

@[deprecated IsLocalRing.mem_maximalIdeal (since := "2024-11-11")]

theorem LocalRing.mem_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] (x : R) :

x ∈ IsLocalRing.maximalIdeal R ↔ x ∈ nonunits R

Alias of IsLocalRing.mem_maximalIdeal.

source

@[deprecated IsLocalRing.not_mem_maximalIdeal (since := "2024-11-11")]

theorem LocalRing.not_mem_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {x : R} :

x ∉ IsLocalRing.maximalIdeal R ↔ IsUnit x

Alias of IsLocalRing.notMem_maximalIdeal.

An element x of a commutative local semiring is not contained in the maximal ideal iff it is a unit.

source

@[deprecated IsLocalRing.isField_iff_maximalIdeal_eq (since := "2024-11-11")]

theorem LocalRing.isField_iff_maximalIdeal_eq {R : Type u_1} [CommSemiring R] [IsLocalRing R] :

IsField R ↔ IsLocalRing.maximalIdeal R = ⊥

Alias of IsLocalRing.isField_iff_maximalIdeal_eq.

source

theorem IsLocalRing.maximalIdeal_le_jacobson {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) :

maximalIdeal R ≤ I.jacobson

source

theorem IsLocalRing.jacobson_eq_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) (h : I ≠ ⊤) :

I.jacobson = maximalIdeal R

source

@[deprecated IsLocalRing.maximalIdeal_le_jacobson (since := "2024-11-11")]

theorem LocalRing.maximalIdeal_le_jacobson {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) :

IsLocalRing.maximalIdeal R ≤ I.jacobson

Alias of IsLocalRing.maximalIdeal_le_jacobson.

source

@[deprecated IsLocalRing.jacobson_eq_maximalIdeal (since := "2024-11-11")]

theorem LocalRing.jacobson_eq_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) (h : I ≠ ⊤) :

I.jacobson = IsLocalRing.maximalIdeal R

Alias of IsLocalRing.jacobson_eq_maximalIdeal.

source

theorem IsLocalRing.ker_eq_maximalIdeal {R : Type u_1} {K : Type u_3} [CommRing R] [IsLocalRing R] [DivisionRing K] (φ : R →+* K) (hφ : Function.Surjective ⇑φ) :

RingHom.ker φ = maximalIdeal R

source

theorem IsLocalRing.maximalIdeal_eq_bot {R : Type u_4} [Field R] :

maximalIdeal R = ⊥

source

@[deprecated IsLocalRing.ker_eq_maximalIdeal (since := "2024-11-09")]

theorem LocalRing.ker_eq_maximalIdeal {R : Type u_1} {K : Type u_3} [CommRing R] [IsLocalRing R] [DivisionRing K] (φ : R →+* K) (hφ : Function.Surjective ⇑φ) :

RingHom.ker φ = IsLocalRing.maximalIdeal R

Alias of IsLocalRing.ker_eq_maximalIdeal.

source

@[deprecated IsLocalRing.maximalIdeal_eq_bot (since := "2024-11-09")]

theorem LocalRing.maximalIdeal_eq_bot {R : Type u_4} [Field R] :

IsLocalRing.maximalIdeal R = ⊥

Alias of IsLocalRing.maximalIdeal_eq_bot.

Documentation

Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Maximal ideal of local rings #