Zulip Chat Archive

Stream: Is there code for X?

Topic: Maximal ideals are pairwise coprime


view this post on Zulip Thomas Browning (Jan 03 2021 at 19:19):

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

view this post on Zulip Aaron Anderson (Jan 03 2021 at 19:25):

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

view this post on Zulip Aaron Anderson (Jan 03 2021 at 19:28):

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.

view this post on Zulip Thomas Browning (Jan 03 2021 at 19:32):

Sure, I can do it

view this post on Zulip Thomas Browning (Jan 03 2021 at 20:03):

#5596


Last updated: May 16 2021 at 05:21 UTC