HepLean Documentation

Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Maximal ideal of local rings #

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

source
instance IsLocalRing.maximalIdeal.isMaximal (R : Type u_1) [CommSemiring R] [IsLocalRing R] :
(IsLocalRing.maximalIdeal R).IsMaximal
Equations
  • ⋯ = ⋯
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 = IsLocalRing.maximalIdeal R
source
theorem IsLocalRing.le_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {J : Ideal R} (hJ : J ≠ ⊤) :
J ≤ IsLocalRing.maximalIdeal R
source
@[simp]
theorem IsLocalRing.mem_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] (x : R) :
x ∈ IsLocalRing.maximalIdeal R ↔ x ∈ nonunits R
source
theorem IsLocalRing.not_mem_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {x : R} :
x ∉ IsLocalRing.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
theorem IsLocalRing.isField_iff_maximalIdeal_eq {R : Type u_1} [CommSemiring R] [IsLocalRing R] :
IsField R ↔ IsLocalRing.maximalIdeal R = ⊥
source
@[deprecated IsLocalRing.maximal_ideal_unique]
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]
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]
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]
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]
theorem LocalRing.not_mem_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {x : R} :
x ∉ IsLocalRing.maximalIdeal R ↔ IsUnit x

Alias of IsLocalRing.not_mem_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]
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) :
IsLocalRing.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 = IsLocalRing.maximalIdeal R
source
@[deprecated IsLocalRing.maximalIdeal_le_jacobson]
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]
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] [Field K] (φ : R →+* K) (hφ : Function.Surjective ⇑φ) :
RingHom.ker φ = IsLocalRing.maximalIdeal R
source
theorem IsLocalRing.maximalIdeal_eq_bot {R : Type u_4} [Field R] :
IsLocalRing.maximalIdeal R = ⊥
source
@[deprecated IsLocalRing.ker_eq_maximalIdeal]
theorem LocalRing.ker_eq_maximalIdeal {R : Type u_1} {K : Type u_3} [CommRing R] [IsLocalRing R] [Field K] (φ : R →+* K) (hφ : Function.Surjective ⇑φ) :
RingHom.ker φ = IsLocalRing.maximalIdeal R

Alias of IsLocalRing.ker_eq_maximalIdeal.

source
@[deprecated IsLocalRing.maximalIdeal_eq_bot]
theorem LocalRing.maximalIdeal_eq_bot {R : Type u_4} [Field R] :
IsLocalRing.maximalIdeal R = ⊥

Alias of IsLocalRing.maximalIdeal_eq_bot.

source
theorem IsLocalRing.of_nilradical_isMaximal {R : Type u_4} [CommSemiring R] [h : (nilradical R).IsMaximal] :
IsLocalRing R
source
@[deprecated IsLocalRing.of_nilradical_isMaximal]
theorem LocalRing.of_nilradical_isMaximal {R : Type u_4} [CommSemiring R] [h : (nilradical R).IsMaximal] :
IsLocalRing R

Alias of IsLocalRing.of_nilradical_isMaximal.

source
noncomputable def localizationEquivSelfOfNilradicalIsMaximal {R : Type u_4} [CommSemiring R] {S : Type u_5} [CommSemiring S] [Algebra R S] {M : Submonoid R} [h : (nilradical R).IsMaximal] (h' : 0 ∉ M) [IsLocalization M S] :
R ≃ₐ[R] S

Let S be the localization of a commutative semiring R at a submonoid M that does not contain 0. If the nilradical of R is maximal then there is a R-algebra isomorphism between R and S.

Equations
Instances For