Maximal ideals are pairwise coprime

Stream: Is there code for X?

[Thomas Browning]

Does mathlib know that maximal ideals (ideal.is_maximal) are pairwise coprime? Context: I want to apply the Chinese Remainder Theorem (ideal.quotient_inf_ring_equiv_pi_quotient) to some maximal ideals. It would follow from this generalized lemma about coatoms:

lemma lem1 {α : Type*} [complete_lattice α] {a b : α} (ha : is_coatom a) (hb : is_coatom b) (h : a ≠ b) : a ⊔ b = ⊤ :=
begin
  have h1 := eq_top_or_eq_of_coatom_le ha le_sup_left,
  cases h1,
  { exact h1 },
  have h2 := eq_top_or_eq_of_coatom_le hb le_sup_right,
  cases h2,
  { exact h2 },
  exact false.rec _ (h (le_antisymm (sup_eq_right.mp h2) (sup_eq_left.mp h1))),
end

[Aaron Anderson]

I don't know the answer yet to whether we have the right version for the CRT, but I do know that the coatom lemma should totally be PR'd. I just added atoms and coatoms, so the API's not all there

[Aaron Anderson]

I could write that PR if you'd like, but if you do it, I think it only needs [semilattice_sup_top], and there should also be a version for is_atom.

[Thomas Browning]

Sure, I can do it

[Thomas Browning]

#5596