coprime ideal

Stream: mathlib4

[Patrick Massot]

Is there any reason why Mathlib uses I ⊔ J = ⊤ to say that ideals I and J are coprime instead of I + K = 1?

[Kevin Buzzard]

Are they defeq? :-)

[Patrick Massot]

No.

[Patrick Massot]

theorem one_eq_top : (1 : Ideal R) = ⊤ := by erw [Submodule.one_eq_range, LinearMap.range_id]

[Patrick Massot]

The sup equal add is rfl.

[Kevin Buzzard]

Oh didn't we have some huuge debate about the meaning of coprime in some arbitrary (abstract thing) at some point? Maybe that was the conclusion?

[Patrick Massot]

The trouble comes from docs#LinearMap.range_id which is not rfl.

[Pedro Sánchez Terraf]

Kevin Buzzard said:

Oh didn't we have some huuge debate about the meaning of coprime in some arbitrary (abstract thing) at some point? Maybe that was the conclusion?

One such (naming) debate was around this message, but it seems nothing executive came out of that.

[Patrick Massot]

I don't think that discussion is really relevant. I'm not talking about having a coprime definition, I'm talking about statements such as docs#Ideal.quotientInfRingEquivPiQuotient

[Eric Wieser]

docs#Codisjoint would also work here I think (c.f docs#codisjoint_iff)

[Patrick Massot]

Eric, this is precisely my point. The current writing is natural from an abstract lattice theory point of view, but not from an arithmetic point of view.

[Antoine Chambert-Loir]

Patrick, why do you say this?
There are many places where such pairs of ideals are called “comaximal”. If that doesn't mean sup(I,J)=top, what else could it mean?
In practice, it is often as easy to use comaximality this way than using the + definition and decompositions of 1 as a sum.

[Patrick Massot]

If you want to use the semi-ring structure on ideals this is clearly the wrong formulation, but I can use it if you prefer it. It is only one rewrite away from the arithmetic formulation.

[Eric Wieser]

I'm confused, aren't the semiring and arithmetic structure one and the same? Or did you intend one of them to mean lattice?

[Patrick Massot]

Yes, but I don't see where I wrote something else.

[Eric Wieser]

I read your message as saying "the semiring structure is clearly the wrong formulation" and "the semiring structure is only one rewrite away from the arithmetic one".

[Eric Wieser]

I assume I must have read both parts incorrectly

[Timo Carlin-Burns]

I believe Patrick was saying "If you want to use the semi-ring structure, I ⊔ J = ⊤ is clearly the wrong formulation" and "I ⊔ J = ⊤ is only one rewrite away from the arithmetic formulation"

[Riccardo Brasca]

Without entering the discussion about the correct definition, in #7466, we add Ideal.isCoprime_iff_add.

[Patrick Massot]

Let me tag people that I know have worked on algebraic number theory in mathlib @Riccardo Brasca, @Anne Baanen, @Filippo A. E. Nuccio, @Alex J. Best. Do you mind if we settle this discussion by using IsCoprime I J everywhere and have lemmas:

theorem isCoprime_iff_codisjoint : IsCoprime I J ↔ Codisjoint I J := by
  rw [IsCoprime, codisjoint_iff]
  constructor
  · rintro ⟨x, y, hxy⟩
    rw [eq_top_iff_one]
    apply (show x * I + y * J ≤ I ⊔ J from
      sup_le (mul_le_left.trans le_sup_left) (mul_le_left.trans le_sup_right))
    rw [hxy]
    simp only [one_eq_top, Submodule.mem_top]
  · intro h
    refine' ⟨1, 1, _⟩
    simpa only [one_eq_top, top_mul, Submodule.add_eq_sup]

theorem isCoprime_iff_add : IsCoprime I J ↔ I + J = 1 := by
  rw [isCoprime_iff_codisjoint, codisjoint_iff, add_eq_sup, one_eq_top]

theorem isCoprime_iff_exists : IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1 := by
  rw [← add_eq_one_iff, isCoprime_iff_add]

theorem isCoprime_iff_sup_eq : IsCoprime I J ↔ I ⊔ J = ⊤ := by
  rw [isCoprime_iff_codisjoint, codisjoint_iff]

maybe even with aliases in the IsCoprime namespace for all the forward direction? This means changing quite a few statements in RingTheorey.DedekindDomain.Ideal for instance but of course these are tiny changes.

[Riccardo Brasca]

LGTM.

[Anne Baanen]

I agree. Consistently using IsCoprime everywhere should end the discussion which formulation is best.

[Riccardo Brasca]

Exactly, I think this is mathlib general philosophy: we don't worry about the actual definition, we just want a good API

[Filippo A. E. Nuccio]

Certainly LGTM.

[Yaël Dillies]

That sounds like you want a TFAE statement

[Patrick Massot]

TFAE look nice but they are a bit harder to use.

[Patrick Massot]

I opened #7523. It needs to wait for CI since I didn't build locally

[Yaël Dillies]

Patrick Massot said:

TFAE look nice but they are a bit harder to use.

Oh I mean on top of your statements, not instead.

[Patrick Massot]

Given P : Prop, how do you prove TFAE [P, P, P, P, P]? I was hoping simp would do it...

[Adam Topaz]

Do we not have the fact that TFAE L is equivalent to TFAE L.dedup? We probably should.

[Adam Topaz]

although maybe that's not useful because Prop doesn't have decidable equality.

[Adam Topaz]

wait, maybe it does?

[Adam Topaz]

Well, at least simp does reduce [P, P, P].dedup to [P].

[Patrick Massot]

I mean P literally appear five times, syntactically.

[Patrick Massot]

How do you manage to call dedup on a list of Prop?

[Adam Topaz]

yeah I understand, that's why I think adding a lemma foo : L.TFAE \iff L.dedup.TFAE would let you prove your statement with simp [foo].

[Joachim Breitner]

Should tfae_finish maybe just handle syntactic equivalent statements?

[Adam Topaz]

oh yeah, that's probably a better approach!

[Eric Rodriguez]

simp [List.tfae_cons_cons, List.tfae_singleton] works around it for now if you just want something fast

[Adam Topaz]

although that would be a significant refactor of tfae_finish, I think!

[Patrick Massot]

I ended up with tagging List.tfae_singleton with simp and adding

@[simp]
theorem tfae_cons_self {a} {l : List Prop} : TFAE (a :: a :: l) ↔ TFAE (a :: l) := by
  simp [tfae_cons_cons]

[Joachim Breitner]

Really? Wouldn’t just

partial def dfs (i j : ℕ) (P P' : Q(Prop)) (hP : Q($P)) : StateT (HashSet ℕ) MetaM Q($P') := do
  if i == j then
    return hP

have to add a case for i not equal to j, but the atoms being defEq?

[Patrick Massot]

I don't want to mix meta-code with an otherwise trivial algebra PR, put feel free to fix this in a later PR.

[Joachim Breitner]

Actually, reading through the code, it’s using AtomM to collect and number the propositions, shouldn’t that deduplicate the atoms in the list?

      let is ← tfaeList.mapM AtomM.addAtom

[Joachim Breitner]

Indeed, this works:

import Mathlib.Tactic.TFAE
set_option autoImplicit false
open List
example (P : Prop) : TFAE [P, P, P] := by
  tfae_finish

[Joachim Breitner]

@Patrick Massot , did you try tfae_finish? :-)

[Patrick Massot]

It looks like I didn't...

[Joachim Breitner]

(Completely unrelated, how can anyone write any code with autoImplicit true? So many typos or unopened namespaces not leading to errors, but weird sorryAx in the goal state… Not expecting a response, just ranting :-))

[Patrick Massot]

I have a much more serious mystery to solve. The indentation style linter says:

Error: Mathlib/RingTheory/Ideal/Operations.lean#L855: ERR_IND: If the theorem/def statement requires multiple lines, indent it correctly (4 spaces or 2 for `|`)
Error: Process completed with exit code 123.

[Patrick Massot]

about https://github.com/leanprover-community/mathlib4/pull/7523/files#diff-cd0998115e627d03a50bc6846968ec95f9f85d137e3e89c92eb09a7a95aed7b9R853-R857

[Mauricio Collares]

The reviewbot comment suggests the linter was complaining about a previous version (0f38c80)

[Patrick Massot]

Oh, GitHub has been very confusing then.

[Patrick Massot]

Sorry about the noise.

[Patrick Massot]

CI is indeed happy now. This is ready for an easy review.

[Patrick Massot]

Thanks Johan. I can now proceed with the actual motivation for this discussion which was to refactor our Chinese remainder theorem proof. Recall I was looking for nice challenges for GlimpseOfLean during the spring and thought proving the Chinese remainder theorem would make a nice exercice about rings, but I was a bit shocked to discover our proof in Mathlib. In particular surjectivity used the following single-use ad-hoc lemmas:

theorem exists_sub_one_mem_and_mem (s : Finset ι) {f : ι → Ideal R}
    (hf : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ⊔ f j = ⊤) (i : ι) (his : i ∈ s) :
    ∃ r : R, r - 1 ∈ f i ∧ ∀ j ∈ s, j ≠ i → r ∈ f j := by
  have : ∀ j ∈ s, j ≠ i → ∃ r : R, ∃ _ : r - 1 ∈ f i, r ∈ f j := by
    intro j hjs hji
    specialize hf i his j hjs hji.symm
    rw [eq_top_iff_one, Submodule.mem_sup] at hf
    rcases hf with ⟨r, hri, s, hsj, hrs⟩
    refine' ⟨1 - r, _, _⟩
    · rw [sub_right_comm, sub_self, zero_sub]
      exact (f i).neg_mem hri
    · rw [← hrs, add_sub_cancel']
      exact hsj
  classical
    have : ∃ g : ι → R, (∀ j, g j - 1 ∈ f i) ∧ ∀ j ∈ s, j ≠ i → g j ∈ f j := by
      choose g hg1 hg2 using this
      refine' ⟨fun j => if H : j ∈ s ∧ j ≠ i then g j H.1 H.2 else 1, fun j => _, fun j => _⟩
      · dsimp only
        split_ifs with h
        · apply hg1
        rw [sub_self]
        exact (f i).zero_mem
      · intro hjs hji
        dsimp only
        rw [dif_pos]
        · apply hg2
        exact ⟨hjs, hji⟩
    rcases this with ⟨g, hgi, hgj⟩
    use ∏ x in s.erase i, g x
    constructor
    · rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem, map_one, map_prod]
      apply Finset.prod_eq_one
      intros
      rw [← RingHom.map_one, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
      apply hgi
    · intro j hjs hji
      rw [← Quotient.eq_zero_iff_mem, map_prod]
      refine' Finset.prod_eq_zero (Finset.mem_erase_of_ne_of_mem hji hjs) _
      rw [Quotient.eq_zero_iff_mem]
      exact hgj j hjs hji
#align ideal.exists_sub_one_mem_and_mem Ideal.exists_sub_one_mem_and_mem

theorem exists_sub_mem [Finite ι] {f : ι → Ideal R} (hf : ∀ i j, i ≠ j → f i ⊔ f j = ⊤)
    (g : ι → R) : ∃ r : R, ∀ i, r - g i ∈ f i := by
  cases nonempty_fintype ι
  have : ∃ φ : ι → R, (∀ i, φ i - 1 ∈ f i) ∧ ∀ i j, i ≠ j → φ i ∈ f j := by
    have := exists_sub_one_mem_and_mem (Finset.univ : Finset ι) fun i _ j _ hij => hf i j hij
    choose φ hφ using this
    exists fun i => φ i (Finset.mem_univ i)
    exact ⟨fun i => (hφ i _).1, fun i j hij => (hφ i _).2 j (Finset.mem_univ j) hij.symm⟩
  rcases this with ⟨φ, hφ1, hφ2⟩
  use ∑ i, g i * φ i
  intro i
  rw [← Quotient.mk_eq_mk_iff_sub_mem, map_sum]
  refine' Eq.trans (Finset.sum_eq_single i _ _) _
  · intro j _ hji
    rw [Quotient.eq_zero_iff_mem]
    exact (f i).mul_mem_left _ (hφ2 j i hji)
  · intro hi
    exact (hi <| Finset.mem_univ i).elim
  specialize hφ1 i
  rw [← Quotient.mk_eq_mk_iff_sub_mem, RingHom.map_one] at hφ1
  rw [RingHom.map_mul, hφ1, mul_one]
#align ideal.exists_sub_mem Ideal.exists_sub_mem

that I propose to replace with

theorem coprime_iInf_of_coprime {J : ι → Ideal R} {s : Finset ι}
    (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
  classical
  simp_rw [isCoprime_iff_add] at *
  revert hf
  induction s using Finset.induction with
  | empty =>
      simp
  | @insert i s _ hs =>
      intro h
      rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
      set K := ⨅ j ∈ s, J j
      calc
        1 = I + K            := (hs fun j hj ↦ h j (Finset.mem_insert_of_mem hj)).symm
        _ = I + K*(I + J i)  := by rw [h i (Finset.mem_insert_self i s), mul_one]
        _ = (1+K)*I + K*J i  := by ring
        _ ≤ I + K ⊓ J i      := add_le_add mul_le_left mul_le_inf

[Patrick Massot]

The only "downside" is that it requires moving this theorem one file later, in the file importing both quotients and ideal operations.

[Patrick Massot]

This is #7532.

[Patrick Massot]

The injectivity proof is also modified, following the paper proof saying the kernel is obviously what it is.

[Patrick Massot]

using the previously missing lemma

lemma _root_.Pi.ker_ringHom {ι : Type*} {R : ι → Type*} [∀ i, Semiring (R i)]
    (φ : ∀ i, S →+* R i) : ker (Pi.ringHom φ) = ⨅ i, ker (φ i) := by
  ext x
  simp [mem_ker, Ideal.mem_iInf, Function.funext_iff]

[Antoine Chambert-Loir]

I believe that IsCoprime should be named IsComaximal.

[Ruben Van de Velde]

Even for integers?

[Antoine Chambert-Loir]

That's a general definition for ideals in a ring.

[Ruben Van de Velde]

What is?

[Eric Wieser]

I think IsComaximal (in the lattice interpretation) is precisely what docs#Codisjoint is intended to mean?

[Eric Wieser]

Maybe Codisjoint should be renamed to Comaximal? I think the Is prefix is fine, but we shouldn't add it unless we also add it to docs#Disjoint.

[Antoine Chambert-Loir]

Ruben Van de Velde said:

What is?

That their sum (or their sup, it's the same) is the unit ideal.

[Riccardo Brasca]

Antoine Chambert-Loir said:

I believe that IsCoprime should be named IsComaximal.

docs#IsCoprime is a statement about two elements in a CommSemiring, so it is the one we use two say that (2 : ℤ) and (3 : ℤ) are coprime. It would be quite weird to say that they are comaximal... but we can add an alias for ideals.

[Kevin Buzzard]

There's another interpretation of coprime in a UFD which is weaker (and makes $X$ and $Y$ coprime in $\R[X,Y]$), but IIRC we have already had a lengthy discussion on this.