Decomposition monoids, coprimality and square-freeness.

decomposition_monoid.lean

import Mathlib.Algebra.Squarefree

-- For definition of decomposition monoid and relative primeness, cf. https://link.springer.com/article/10.1007/s00233-019-10022-3
-- Discussion about the correct general definition of coprimality: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/IsCoprime.20is.20.40.5Bsimp.5D.3F
-- GCD monoids are decomposition monoids: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/GCDMonoid/Basic.html#exists_dvd_and_dvd_of_dvd_mul

class DecompositionMonoid (R) [Semigroup R] : Prop where
  exists_dvd_and_dvd_of_dvd_mul : ∀ m n k : R, k ∣ m * n → ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂

theorem exists_dvd_and_dvd_of_dvd_mul' {R} [Semigroup R] [DecompositionMonoid R] {m n k : R}
    (h : k ∣ m * n) : ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂ :=
  DecompositionMonoid.exists_dvd_and_dvd_of_dvd_mul m n k h

instance [CancelCommMonoidWithZero R] [GCDMonoid R] : DecompositionMonoid R :=
  ⟨@exists_dvd_and_dvd_of_dvd_mul _ _ _⟩

def RelPrime [Monoid R] (a b : R) : Prop := ∀ c, c ∣ a → c ∣ b → IsUnit c

theorem relPrime_of_squarefree_mul [CommMonoid R] {m n : R}
    (h : Squarefree (m * n)) : RelPrime m n := fun c hca hcb => h c (mul_dvd_mul hca hcb)

theorem relPrime_iff_isUnit_gcd [CancelCommMonoidWithZero R] [GCDMonoid R] {a b : R} :
    RelPrime a b ↔ IsUnit (gcd a b) :=
  ⟨fun h => h _ (gcd_dvd_left a b) (gcd_dvd_right a b),
    fun h _ ha hb => isUnit_of_dvd_unit (dvd_gcd ha hb) h⟩

namespace RelPrime

section
variable [Monoid R] {a b c : R}

theorem symm (h : RelPrime a b) : RelPrime b a := fun c hb ha => h c ha hb

theorem of_mul_right_left (h : RelPrime (a * b) c) : RelPrime a c :=
  fun d hb hc => h d (hb.mul_right b) hc

theorem of_mul_right_right (h : RelPrime a (b * c)) : RelPrime a b :=
  fun d hb hc => h d hb (hc.mul_right c)

theorem isUnit (h : RelPrime a a) : IsUnit a := h a dvd_rfl dvd_rfl
end

theorem dvd_of_mul_left [CommMonoid R] [DecompositionMonoid R] {a b c : R}
    (hp : RelPrime a c) (hd : a ∣ b * c) : a ∣ b := by
  obtain ⟨d₁, d₂, ⟨e₁, rfl⟩, ⟨e₂, rfl⟩, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul' hd
  rw [mul_comm] at hp
  apply mul_dvd_mul_left
  exact hp.of_mul_right_left.of_mul_right_right.isUnit.dvd

end RelPrime

lemma mul_dvd_mul_iff_left' [Semigroup R] [IsLeftCancelMul R]
    {a b c : R} : a * b ∣ a * c ↔ b ∣ c :=
  exists_congr fun d => by rw [mul_assoc, mul_right_inj]

lemma mul_dvd_mul_iff_right' [CommSemigroup R] [IsLeftCancelMul R] -- or equivalently, IsRightCancelMul
    {a b c : R} : a * c ∣ b * c ↔ a ∣ b := by
  rw [mul_comm a, mul_comm b, mul_dvd_mul_iff_left']

/-
lemma mul_dvd_mul_iff_left₀ [Semigroup R] [Zero R] [IsLeftCancelMulZero R]
    {a b c : R} (ha : a ≠ 0) : a * b ∣ a * c ↔ b ∣ c :=
  exists_congr fun d => by rw [mul_assoc, mul_right_inj' ha] -- mul_right_inj' needs to be generalized

lemma mul_dvd_mul_iff_right₀ [CommSemigroup R] [Zero R] [IsLeftCancelMulZero R]
    {a b c : R} (ha : a ≠ 0) : a * b ∣ a * c ↔ b ∣ c := by
  rw [mul_comm a, mul_comm b, mul_dvd_mul_iff_left₀ ha]
-/

theorem squarefree_mul_iff [CancelCommMonoid R] [DecompositionMonoid R] {m n : R} :
    Squarefree (m * n) ↔ RelPrime m n ∧ Squarefree m ∧ Squarefree n :=
  ⟨fun h => ⟨relPrime_of_squarefree_mul h, h.of_mul_left, h.of_mul_right⟩,
    fun ⟨hp, hm, hn⟩ c hc => by
      obtain ⟨d₁, d₂, ⟨e₁, rfl⟩, ⟨e₂, rfl⟩, hd⟩ := exists_dvd_and_dvd_of_dvd_mul' ((dvd_mul_right c c).trans hc)
      rw [mul_mul_mul_comm, hd, mul_dvd_mul_iff_left', ← hd] at hc
      obtain ⟨d₃, d₄, ⟨e₃, rfl⟩, ⟨e₄, rfl⟩, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul' hc
      rw [← mul_assoc] at hm hn
      apply IsUnit.mul
      · rw [mul_left_comm] at hp
        exact hm.of_mul_left d₃ (mul_dvd_mul_right
          (hp.of_mul_right_right.of_mul_right_left.dvd_of_mul_left (hd ▸ dvd_mul_right d₃ d₄)) d₃)
      · rw [mul_left_comm d₂] at hp
        rw [mul_comm, eq_comm, mul_comm] at hd
        exact hn.of_mul_left d₄ (mul_dvd_mul_right
          (hp.of_mul_right_right.of_mul_right_left.symm.dvd_of_mul_left ⟨d₃, hd⟩) d₄)⟩

-- Generalizes https://github.com/leanprover-community/mathlib4/pull/5669/files
theorem squarefree_mul_iff₀ [CancelCommMonoidWithZero R] [DecompositionMonoid R] {m n : R} :
    Squarefree (m * n) ↔ RelPrime m n ∧ Squarefree m ∧ Squarefree n :=
  ⟨fun h => ⟨relPrime_of_squarefree_mul h, h.of_mul_left, h.of_mul_right⟩,
    fun ⟨hp, hm, hn⟩ => by
      obtain rfl | hm0 := eq_or_ne m 0
      · simpa using hm
      obtain rfl | hn0 := eq_or_ne n 0
      · simpa using hn
      intros c hc
      obtain ⟨d₁, d₂, ⟨e₁, rfl⟩, ⟨e₂, rfl⟩, hd⟩ := exists_dvd_and_dvd_of_dvd_mul' ((dvd_mul_right c c).trans hc)
      have := mul_ne_zero (left_ne_zero_of_mul hm0) (left_ne_zero_of_mul hn0)
      rw [mul_mul_mul_comm, hd, mul_dvd_mul_iff_left this, ← hd] at hc
      obtain ⟨d₃, d₄, ⟨e₃, rfl⟩, ⟨e₄, rfl⟩, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul' hc
      rw [← mul_assoc] at hm hn
      apply IsUnit.mul
      · rw [mul_left_comm] at hp
        exact hm.of_mul_left d₃ (mul_dvd_mul_right
          (hp.of_mul_right_right.of_mul_right_left.dvd_of_mul_left (hd ▸ dvd_mul_right d₃ d₄)) d₃)
      · rw [mul_left_comm d₂] at hp
        rw [mul_comm, eq_comm, mul_comm] at hd
        exact hn.of_mul_left d₄ (mul_dvd_mul_right
          (hp.of_mul_right_right.of_mul_right_left.symm.dvd_of_mul_left ⟨d₃, hd⟩) d₄)⟩

theorem squarefree_mul_iff_gcd [CancelCommMonoidWithZero R] [GCDMonoid R] {m n : R} :
    Squarefree (m * n) ↔ IsUnit (gcd m n) ∧ Squarefree m ∧ Squarefree n := by
  rw [squarefree_mul_iff₀, relPrime_iff_isUnit_gcd]