HepLean Documentation

Mathlib.RingTheory.LocalRing.Basic

Local rings #

We prove basic properties of local rings.

source
theorem IsLocalRing.of_isUnit_or_isUnit_of_isUnit_add {R : Type u_1} [CommSemiring R] [Nontrivial R] (h : ∀ (a b : R), IsUnit (a + b) → IsUnit a ∨ IsUnit b) :
IsLocalRing R
source
theorem IsLocalRing.of_nonunits_add {R : Type u_1} [CommSemiring R] [Nontrivial R] (h : ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R) :
IsLocalRing R

A semiring is local if it is nontrivial and the set of nonunits is closed under the addition.

source
theorem IsLocalRing.of_unique_max_ideal {R : Type u_1} [CommSemiring R] (h : ∃! I : Ideal R, I.IsMaximal) :
IsLocalRing R

A semiring is local if it has a unique maximal ideal.

source
theorem IsLocalRing.of_unique_nonzero_prime {R : Type u_1} [CommSemiring R] (h : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime) :
IsLocalRing R
source
theorem IsLocalRing.isUnit_or_isUnit_of_isUnit_add {R : Type u_1} [CommSemiring R] [IsLocalRing R] {a b : R} (h : IsUnit (a + b)) :
IsUnit a ∨ IsUnit b
source
theorem IsLocalRing.nonunits_add {R : Type u_1} [CommSemiring R] [IsLocalRing R] {a b : R} (ha : a ∈ nonunits R) (hb : b ∈ nonunits R) :
a + b ∈ nonunits R
source
@[deprecated IsLocalRing.of_isUnit_or_isUnit_of_isUnit_add]
theorem LocalRing.of_isUnit_or_isUnit_of_isUnit_add {R : Type u_1} [CommSemiring R] [Nontrivial R] (h : ∀ (a b : R), IsUnit (a + b) → IsUnit a ∨ IsUnit b) :
IsLocalRing R

Alias of IsLocalRing.of_isUnit_or_isUnit_of_isUnit_add.

source
@[deprecated IsLocalRing.of_nonunits_add]
theorem LocalRing.of_nonunits_add {R : Type u_1} [CommSemiring R] [Nontrivial R] (h : ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R) :
IsLocalRing R

Alias of IsLocalRing.of_nonunits_add.

A semiring is local if it is nontrivial and the set of nonunits is closed under the addition.

source
@[deprecated IsLocalRing.of_unique_max_ideal]
theorem LocalRing.of_unique_max_ideal {R : Type u_1} [CommSemiring R] (h : ∃! I : Ideal R, I.IsMaximal) :
IsLocalRing R

Alias of IsLocalRing.of_unique_max_ideal.

A semiring is local if it has a unique maximal ideal.

source
@[deprecated IsLocalRing.of_unique_nonzero_prime]
theorem LocalRing.of_unique_nonzero_prime {R : Type u_1} [CommSemiring R] (h : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime) :
IsLocalRing R

Alias of IsLocalRing.of_unique_nonzero_prime.

source
@[deprecated IsLocalRing.isUnit_or_isUnit_of_isUnit_add]
theorem LocalRing.isUnit_or_isUnit_of_isUnit_add {R : Type u_1} [CommSemiring R] [IsLocalRing R] {a b : R} (h : IsUnit (a + b)) :
IsUnit a ∨ IsUnit b

Alias of IsLocalRing.isUnit_or_isUnit_of_isUnit_add.

source
@[deprecated IsLocalRing.nonunits_add]
theorem LocalRing.nonunits_add {R : Type u_1} [CommSemiring R] [IsLocalRing R] {a b : R} (ha : a ∈ nonunits R) (hb : b ∈ nonunits R) :
a + b ∈ nonunits R

Alias of IsLocalRing.nonunits_add.

source
theorem IsLocalRing.of_isUnit_or_isUnit_one_sub_self {R : Type u_1} [CommRing R] [Nontrivial R] (h : ∀ (a : R), IsUnit a ∨ IsUnit (1 - a)) :
IsLocalRing R
source
theorem IsLocalRing.isUnit_or_isUnit_one_sub_self {R : Type u_1} [CommRing R] [IsLocalRing R] (a : R) :
IsUnit a ∨ IsUnit (1 - a)
source
theorem IsLocalRing.isUnit_of_mem_nonunits_one_sub_self {R : Type u_1} [CommRing R] [IsLocalRing R] (a : R) (h : 1 - a ∈ nonunits R) :
IsUnit a
source
theorem IsLocalRing.isUnit_one_sub_self_of_mem_nonunits {R : Type u_1} [CommRing R] [IsLocalRing R] (a : R) (h : a ∈ nonunits R) :
IsUnit (1 - a)
source
theorem IsLocalRing.of_surjective' {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [Nontrivial S] (f : R →+* S) (hf : Function.Surjective ⇑f) :
IsLocalRing S
source
@[deprecated IsLocalRing.of_isUnit_or_isUnit_one_sub_self]
theorem IsLocalRing.LocalRing.of_isUnit_or_isUnit_one_sub_self {R : Type u_1} [CommRing R] [Nontrivial R] (h : ∀ (a : R), IsUnit a ∨ IsUnit (1 - a)) :
IsLocalRing R

Alias of IsLocalRing.of_isUnit_or_isUnit_one_sub_self.

source
@[deprecated IsLocalRing.isUnit_or_isUnit_one_sub_self]
theorem IsLocalRing.LocalRing.isUnit_or_isUnit_one_sub_self {R : Type u_1} [CommRing R] [IsLocalRing R] (a : R) :
IsUnit a ∨ IsUnit (1 - a)

Alias of IsLocalRing.isUnit_or_isUnit_one_sub_self.

source
@[deprecated IsLocalRing.isUnit_of_mem_nonunits_one_sub_self]
theorem IsLocalRing.LocalRing.isUnit_of_mem_nonunits_one_sub_self {R : Type u_1} [CommRing R] [IsLocalRing R] (a : R) (h : 1 - a ∈ nonunits R) :
IsUnit a

Alias of IsLocalRing.isUnit_of_mem_nonunits_one_sub_self.

source
@[deprecated IsLocalRing.isUnit_one_sub_self_of_mem_nonunits]
theorem IsLocalRing.LocalRing.isUnit_one_sub_self_of_mem_nonunits {R : Type u_1} [CommRing R] [IsLocalRing R] (a : R) (h : a ∈ nonunits R) :
IsUnit (1 - a)

Alias of IsLocalRing.isUnit_one_sub_self_of_mem_nonunits.

source
@[deprecated IsLocalRing.of_surjective']
theorem IsLocalRing.LocalRing.of_surjective' {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [Nontrivial S] (f : R →+* S) (hf : Function.Surjective ⇑f) :
IsLocalRing S

Alias of IsLocalRing.of_surjective'.

source
@[instance 100]
instance Field.instIsLocalRing (K : Type u_3) [Field K] :
IsLocalRing K
Equations
  • ⋯ = ⋯