Local rings #
We prove basic properties of local rings.
theorem
IsLocalRing.of_isUnit_or_isUnit_of_isUnit_add
{R : Type u_1}
[Semiring R]
[Nontrivial R]
(h : ∀ (a b : R), IsUnit (a + b) → IsUnit a ∨ IsUnit b)
:
theorem
IsLocalRing.of_unique_max_ideal
{R : Type u_1}
[CommSemiring R]
(h : ∃! I : Ideal R, I.IsMaximal)
:
A semiring is local if it has a unique maximal ideal.
theorem
IsLocalRing.of_unique_nonzero_prime
{R : Type u_1}
[CommSemiring R]
(h : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime)
:
theorem
IsLocalRing.isUnit_or_isUnit_of_isUnit_add
{R : Type u_1}
[CommSemiring R]
[IsLocalRing R]
{a b : R}
(h : IsUnit (a + b))
:
theorem
IsLocalRing.nonunits_add
{R : Type u_1}
[CommSemiring R]
[IsLocalRing R]
{a b : R}
(ha : a ∈ nonunits R)
(hb : b ∈ nonunits R)
:
@[deprecated IsLocalRing.of_isUnit_or_isUnit_of_isUnit_add]
theorem
IsLocalRing.LocalRing.of_isUnit_or_isUnit_of_isUnit_add
{R : Type u_1}
[Semiring R]
[Nontrivial R]
(h : ∀ (a b : R), IsUnit (a + b) → IsUnit a ∨ IsUnit b)
:
@[deprecated IsLocalRing.of_nonunits_add]
theorem
IsLocalRing.LocalRing.of_nonunits_add
{R : Type u_1}
[Semiring R]
[Nontrivial R]
(h : ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits 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.
@[deprecated IsLocalRing.of_unique_max_ideal]
theorem
IsLocalRing.LocalRing.of_unique_max_ideal
{R : Type u_1}
[CommSemiring R]
(h : ∃! I : Ideal R, I.IsMaximal)
:
Alias of IsLocalRing.of_unique_max_ideal.
A semiring is local if it has a unique maximal ideal.
@[deprecated IsLocalRing.of_unique_nonzero_prime]
theorem
IsLocalRing.LocalRing.of_unique_nonzero_prime
{R : Type u_1}
[CommSemiring R]
(h : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime)
:
Alias of IsLocalRing.of_unique_nonzero_prime.
@[deprecated IsLocalRing.isUnit_or_isUnit_of_isUnit_add]
theorem
IsLocalRing.LocalRing.isUnit_or_isUnit_of_isUnit_add
{R : Type u_1}
[CommSemiring R]
[IsLocalRing R]
{a b : R}
(h : IsUnit (a + b))
:
@[deprecated IsLocalRing.nonunits_add]
theorem
IsLocalRing.LocalRing.nonunits_add
{R : Type u_1}
[CommSemiring R]
[IsLocalRing R]
{a b : R}
(ha : a ∈ nonunits R)
(hb : b ∈ nonunits R)
:
Alias of IsLocalRing.nonunits_add.
theorem
IsLocalRing.of_isUnit_or_isUnit_one_sub_self
{R : Type u_1}
[Ring R]
[Nontrivial R]
(h : ∀ (a : R), IsUnit a ∨ IsUnit (1 - a))
:
theorem
IsLocalRing.isUnit_or_isUnit_one_sub_self
{R : Type u_1}
[CommRing R]
[IsLocalRing R]
(a : R)
:
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
theorem
IsLocalRing.isUnit_one_sub_self_of_mem_nonunits
{R : Type u_1}
[CommRing R]
[IsLocalRing R]
(a : R)
(h : a ∈ nonunits R)
:
theorem
IsLocalRing.of_surjective'
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[IsLocalRing R]
[Ring S]
[Nontrivial S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
:
@[deprecated IsLocalRing.of_isUnit_or_isUnit_one_sub_self]
theorem
IsLocalRing.LocalRing.of_isUnit_or_isUnit_one_sub_self
{R : Type u_1}
[Ring R]
[Nontrivial R]
(h : ∀ (a : R), IsUnit a ∨ IsUnit (1 - a))
:
@[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)
:
@[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
@[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)
:
@[deprecated IsLocalRing.of_surjective']
theorem
IsLocalRing.LocalRing.of_surjective'
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[IsLocalRing R]
[Ring S]
[Nontrivial S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
:
Alias of IsLocalRing.of_surjective'.