Non-local rings #
This file gathers some results about non-local rings.
Main results #
not_isLocalRing_of_nontrivial_pi
: for an index typeι
with at least two elements and an indexed family of (semi)ringsR : ι → Type*
, the indexed product (semi)ringΠ i, R i
is not local.not_isLocalRing_of_prod_of_nontrivial
: the product of two nontrivial (semi)rings is not local.not_isLocalRing_tfae
: the following conditions are equivalent for a commutative (semi)ringR
:R
is not local,- the maximal spectrum of
R
is nontrivial, R
has two distinct maximal ideals.
exists_surjective_of_not_isLocalRing
: there exists a surjective ring homomorphism from a non-local commutative ring onto a product of two fields.
theorem
IsLocalRing.not_isLocalRing_of_nontrivial_pi
{ι : Type u_1}
[Nontrivial ι]
(R : ι → Type u_2)
[(i : ι) → Semiring (R i)]
[∀ (i : ι), Nontrivial (R i)]
:
¬IsLocalRing ((i : ι) → R i)
For an index type ι
with at least two elements and an indexed family of (semi)rings
R : ι → Type*
, the indexed product (semi)ring Π i, R i
is not local.
theorem
IsLocalRing.not_isLocalRing_of_prod_of_nontrivial
(R₁ : Type u_1)
(R₂ : Type u_2)
[Semiring R₁]
[Semiring R₂]
[Nontrivial R₁]
[Nontrivial R₂]
:
¬IsLocalRing (R₁ × R₂)
The product of two nontrivial (semi)rings is not local.
The following conditions are equivalent for a commutative (semi)ring R
:
R
is not local,- the maximal spectrum of
R
is nontrivial, R
has two distinct maximal ideals.
theorem
IsLocalRing.exists_surjective_of_not_isLocalRing
{R : Type u}
[CommRing R]
[Nontrivial R]
(h : ¬IsLocalRing R)
:
There exists a surjective ring homomorphism from a non-local commutative ring onto a product of two fields.