Results for non-local rings

Stream: mathlib4

[Michał Staromiejski]

I have the following results about rings that are non-local:

import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
import Mathlib.RingTheory.Spectrum.Maximal.Basic

theorem IsLocalRing.of_unique_maxiamlSpectrum {R : Type*} [CommSemiring R] [h : Unique (MaximalSpectrum R)] : IsLocalRing R :=
  .of_unique_max_ideal ⟨h.default.asIdeal, ⟨h.default.isMaximal,
    fun I hI ↦ MaximalSpectrum.mk.inj <| h.eq_default ⟨I, hI⟩⟩⟩

/-- For a non-local ring, `MaximalSpectrum R` is non-trivial. -/
theorem nontrivial_maximalSpectrum_of_not_isLocalRing {R : Type*} [CommSemiring R] [Nontrivial R] (h : ¬IsLocalRing R) :
    Nontrivial (MaximalSpectrum R) := by
  rw [← not_subsingleton_iff_nontrivial]; by_contra; apply h
  have : Unique (MaximalSpectrum R) := uniqueOfSubsingleton Classical.ofNonempty
  exact .of_unique_maxiamlSpectrum

/-- In a non-local ring, there are two distinct maximal ideals. -/
theorem exist_maximal_ne_of_not_isLocalRing {R : Type*} [CommSemiring R] [Nontrivial R] (h : ¬IsLocalRing R) :
    ∃ m₁ m₂ : Ideal R, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂ :=
  let ⟨⟨m₁, hm₁⟩, ⟨m₂, hm₂⟩, hm₁m₂⟩ := nontrivial_maximalSpectrum_of_not_isLocalRing h
  ⟨m₁, m₂, ⟨hm₁, hm₂, by by_contra; apply hm₁m₂; congr⟩⟩

/-- There exists a surjective ring homomorphism from a non-local ring onto product of two fields. -/
lemma exists_surjective_of_not_isLocalRing.{u} {R : Type u} [CommRing R] [Nontrivial R] (h : ¬IsLocalRing R) :
    ∃ (K₁ K₂ : Type u) (_ : Field K₁) (_ : Field K₂) (f : R →+* K₁ × K₂), Function.Surjective f := by
  /- get two different maximal ideals and project on the product of quotients -/
  obtain ⟨m₁, m₂, _, _, hm₁m₂⟩ := exist_maximal_ne_of_not_isLocalRing h
  let e := Ideal.quotientInfEquivQuotientProd m₁ m₂ <| Ideal.isCoprime_of_isMaximal hm₁m₂
  let f := e.toRingHom.comp <| Ideal.Quotient.mk (m₁ ⊓ m₂)
  use R ⧸ m₁, R ⧸ m₂, Ideal.Quotient.field m₁, Ideal.Quotient.field m₂, f
  apply Function.Surjective.comp e.surjective Ideal.Quotient.mk_surjective

Is there interest in having those in Mathlib as well?
For the first, positive result there is already a PR #23994.

[Kevin Buzzard]

These are all iffs, aren't they? I mean in the presence of everything else, not IsLocalRing is equivalent to the conclusion.

[Michał Staromiejski]

That's true, there are already contrapositions like docs#IsLocalRing.maximal_ideal_unique but I could also add iff versions.

[Michał Staromiejski]

I actually use the last one in my work, but I think there will be rarely situation to have an assumption like

∃ (K₁ K₂ : Type u) (_ : Field K₁) (_ : Field K₂) (f : R →+* K₁ × K₂), Function.Surjective f

but maybe...

[Michał Staromiejski]

Also, for IsLocalRing.of_unique_maxiamlSpectrum above, there is other direction: docs#IsLocalRing.instUniqueMaximalSpectrum but Unique is not a Prop so to form iff version, I would have to "wrap" it in Nonempty I guess? Like so:

theorem IsLocalRing.iff_unique_maxiamlSpectrum {R : Type*} [CommSemiring R] :
    IsLocalRing R ↔ Nonempty (Unique (MaximalSpectrum R)) := sorry

[Michał Staromiejski]

Created PR #24043, the results are in a separate file Mathlib.RingTheory.LocalRing.NonLocalRing. All comments highly appreciated!