Subrings of local rings #
We prove basic properties of subrings of local rings.
theorem
IsLocalRing.of_injective
{R : Type u_2}
{S : Type u_1}
[Semiring R]
[Semiring S]
[IsLocalRing S]
{f : R →+* S}
(hf : Function.Injective ⇑f)
(h : ∀ a ∈ nonZeroDivisors R, IsUnit a)
:
If a (semi)ring R in which every element is either invertible or a zero divisor
embeds in a local (semi)ring S, then R is local.
theorem
IsLocalRing.of_subring
{S : Type u_1}
[Semiring S]
[IsLocalRing S]
{R : Subsemiring S}
(h : ∀ a ∈ nonZeroDivisors ↥R, IsUnit a)
:
IsLocalRing ↥R
If in a sub(semi)ring R of a local (semi)ring S every element is either
invertible or a zero divisor, then R is local.
theorem
IsLocalRing.of_subring'
{S : Type u_1}
[Semiring S]
{R R' : Subsemiring S}
[IsLocalRing ↥R']
(inc : R ≤ R')
(h : ∀ a ∈ nonZeroDivisors ↥R, IsUnit a)
:
IsLocalRing ↥R
If in a sub(semi)ring R of a local (semi)ring R' every element is either
invertible or a zero divisor, then R is local.
This version is for R and R' that are both sub(semi)rings of a (semi)ring S.