ModEq

Stream: mathlib4

[Yury G. Kudryashov]

I suggest that we unify the 3 existing ModEq predicates (docs#Nat.ModEq, docs#Int.ModEq, and docs#AddCommGroup.ModEq) using this definition:

def MyModEq {G : Type*} [Add G] [SMul ℕ G] (p : G) (a b : G) : Prop :=
  ∃ m n : ℕ, m • p + a = n • p + b

Then we can provide Decidable instances for Nat and Int. WDYT?

[Yury G. Kudryashov]

If we're going to do this, what would be the migration path? Do I introduce a new definition or redefine AddCommGroup.ModEq?

[Snir Broshi]

I vote new definition + deprecations, it would be weird for something under the AddCommGroup namespace to not require [AddCommGroup G].
IIUC docs#SModEq could also be generalized to submonoids per this TODO to work on Nat

[Kyle Miller]

Here's some justification that this is the correct definition for commutative additive monoids:

The assumption is that we want a equivalence relation ~ such that (1) it's a congruence for + and (2) for all m : Nat then m • p ~ 0. The claim is that Yury's definition is the coarsest equivalence relation satisfying these assumptions. By (1) and (2) together we have that for all m : Nat and a : G that m • p + a ~ a. Since Nat has a zero, then a ~ b is equivalent to there existing m n : Nat such that m • p + a ~ n • p + b. Since equivalence relations contain Eq, for a ~ b it is sufficient if there exists m n : Nat such that m • p + a = n • p + b, which is Yury's definition. So, if Yury's definition is an equivalence relation that satisfies (1) and (2) then it's the coarsest one.

And also, for commutative additive groups, (1) and (2) together imply that for m : Int then m • p ~ 0, so the relation isn't coarser than it should be.

[Snir Broshi]

If we change docs#MulAction.orbitRel from a ∈ orbit G b to (orbit a b ∩ orbit G b).Nonempty it should:

• generalize it from Group to Monoid (or even Semiring?)
• which generalizes docs#QuotientGroup.leftRel from Subgroup to Submonoid
• which generalizes docs#Submodule.quotientRel / docs#Submodule.hasQuotient / docs#Submodule.Quotient.mk / docs#SModEq from AddCommGroup over Ring to AddCommMonoid over Semiring

Then SModEq is exactly Yury's MyModEq but but stated with quotients. Wdyt?
(I'm not suggesting merging it with the 3 ModEqs, just generalizing it the same way)

[Yury G. Kudryashov]

How should I call the new relation?

[Eric Wieser]

Claim ModEq in the root namespace?

[Ruben Van de Velde]

Crossing the streams: Mathlib.ModEq

[Yury G. Kudryashov]

I don't think that we should selectively namespace parts of the library.

[Yury G. Kudryashov]

@Eric Wieser Should it take over the ... [MOD _] notation while deprecating the ZMOD and PMOD versions?

[Yury G. Kudryashov]

One more question: should I care about AddMonoid, or assume at least AddCommMonoid everywhere? Some facts are true for an AddMonoid, but the proofs are more complicated. Unless someone objects, I'm going to assume AddCommMonoid and leave a comment saying that the definition and some lemmas can be generalized to an AddMonoid, but we won't do it until we need it for the first time.

[Joseph Myers]

I think that general version of orbitRel isn't an equivalence relation for a general monoid action (though it's one for any action of a commutative monoid, a group or a group with zero, at least).

This form of relation is certainly useful in various places; for example, the definition of docs#SameRay involves such a relation (for an action by the submonoid of positive elements of an ordered commutative semiring).

[Snir Broshi]

Joseph Myers said:

I think that general version of orbitRel isn't an equivalence relation for a general monoid action (though it's one for any action of a commutative monoid, a group or a group with zero, at least).

Yeah I also bumped into this while trying to prove transitivity, although I don't have a counterexample offhand

[Aaron Liu]

which relation

[Aaron Liu]

is it the relation fun a b => ∃ m n, m • a = n • b

[Aaron Liu]

In that case I have a counterexample

[Snir Broshi]

yes

[Aaron Liu]

counterexample

import Mathlib

def M := Bool
instance : Nontrivial M := inferInstanceAs (Nontrivial Bool)

instance : Semigroup M where
  mul a b := b
  mul_assoc _ _ _ := rfl

theorem M.mul_def (a b : M) : a * b = b := rfl

#synth Monoid (WithOne M)
#synth MulAction (WithOne M) (WithOne M)

theorem not_trans : ∃ (a b c : WithOne M),
    (∃ m n : WithOne M, m • a = n • b) ∧
    (∃ m n : WithOne M, m • b = n • c) ∧
    ¬(∃ m n : WithOne M, m • a = n • c) := by
  have h (m : WithOne M) (n : M) : m * WithOne.coe n = WithOne.coe n := by
    cases m with
    | one => rw [one_mul]
    | coe m => rw [← WithOne.coe_mul, M.mul_def]
  obtain ⟨a, c, hac⟩ := exists_pair_ne M
  refine ⟨a, 1, c, ⟨a, a, by simp [h]⟩, ⟨c, c, by simp [h]⟩, ?_⟩
  push_neg
  intro m n
  simpa [h] using hac

[Snir Broshi]

Aaron Liu said:

counterexample

Nice, perhaps I can save the situation by requiring a CancelMonoid, which still generalizes Group and applies to Multiplicative ℕ.
It avoids this counterexample, although there might still be one

[Aaron Liu]

counterexample the sequel

import Mathlib

abbrev M := FreeMonoid Bool

#synth CancelMonoid M
#synth MulAction M M

theorem not_trans : ∃ (a b c : M),
    (∃ m n : M, m • a = n • b) ∧
    (∃ m n : M, m • b = n • c) ∧
    ¬(∃ m n : M, m • a = n • c) := by
  let a : M := .of true
  let c : M := .of false
  refine ⟨a, 1, c, ⟨1, a, by simp⟩, ⟨c, 1, by simp⟩, ?_⟩
  push_neg
  intro m n
  apply ne_of_apply_ne FreeMonoid.toList
  apply ne_of_apply_ne List.getLast?
  simp [a, c]

[Edward van de Meent]

Afaict the relation that was suggested uses SMul Nat M, not SMul R M, so both of these aren't counterexamples nvm you were talking about an entirely different relation

[Snir Broshi]

It seems this relation is an equivalence in either Group or CommMonoid, but not in any common ancestor of them, so maybe the answer is adding a separate orbitRel/leftRel/quotientRel/SModEq for commutative monoids. Has no one needed to take a quotient in a commutative monoid that isn't a group so far? (other than Nat.ModEq, which is equivalent to using quotients but isn't defined using them)

[Edward van de Meent]

i think a good condition is IsDirected Mᵐᵒᵖ (· ∣ ·)? a solution to this being transitive is would be finding, given elements m n : M, some element z : M such that there exist x y : M with x * m = z and y * n = z. this is precisely m | z and n | z in MulOpposite M, which is precisely m <= z and n <= z in Associates (MulOpposite M).

[Edward van de Meent]

i.e. we have the following:

import Mathlib

instance directed_of_comm {M : Type*} [CommMonoid M] : IsDirected Mᵐᵒᵖ (· ∣ ·) := by
  constructor
  simp only [MulOpposite.exists, MulOpposite.forall]
  intro m n
  use m * n
  simp

instance directed_of_group {M : Type*} [Group M] : IsDirected Mᵐᵒᵖ (· ∣ ·) := by
  constructor
  simp only [dvd_def, MulOpposite.exists, MulOpposite.forall, ← MulOpposite.op_mul,
    MulOpposite.op_inj, ↓existsAndEq, and_true]
  intro m n
  use n⁻¹,m⁻¹
  simp

theorem rel_trans {M : Type*} {X : Type*} [Monoid M] [MulAction M X] [h : IsDirected Mᵐᵒᵖ (· ∣ ·)] (a b c : X)
    (hab : ∃ m n : M, m • a = n • b)
    (hbc : ∃ m n : M, m • b = n • c) :
    (∃ m n : M, m • a = n • c) := by
  obtain ⟨a',m,hab⟩ := hab
  obtain ⟨n,c',hbc⟩ := hbc
  obtain ⟨z,hzm,hzn⟩ := h.directed (.op m) (.op n)
  cases z with
  | h z =>
  simp [dvd_def,← MulOpposite.op_mul] at hzm hzn
  obtain ⟨m',rfl⟩ := hzm
  obtain ⟨n',hnm'⟩ := hzn
  use m' * a', n' * c'
  rw [mul_smul,hab,mul_smul,← hbc,← mul_smul,hnm',mul_smul]

[Kevin Buzzard]

Given that we currently have no ModEq in mathlib for any situation beyond cancellative additive commutative monoids, I would be cautious about over-engineering this.

[Eric Wieser]

Can I suggest we just refactor AddCommGroup.ModEq in place for now?

[Eric Wieser]

Ring.inverse is not about rings but monoids with zero, Module.rank is not about modules but semi modules, ...: so I don't think the namespace is a disaster

[Eric Wieser]

And it will be easier to review the generalization separately from a rename

[Yury G. Kudryashov]

I've already started a new file...

[Yury G. Kudryashov]

I'll try to split it into separate PRs for "generalize", "split", "review API".

[Yury G. Kudryashov]

@Eric Wieser #33849

[Eric Wieser]

I left some comments, that looks pretty clean to me

[Eric Wieser]

Should be good to go now, I guess eliminating Nat.ModEq is next?

[Yury G. Kudryashov]

I'm going to

• split the file into Group/, Ring/ and Field/
• review the API
• eliminate Nat.ModEq
• eliminate Int.ModEq