semilattice, dvd, associated

Stream: new members

[Damiano Testa]

Is it possible to move all that is here starting from Johan's comment directed a me to the new topic? Or should I simply start a new topic?

[Mario Carneiro]

anyone can change topics retroactively

[Damiano Testa]

Ok, topic name changed! Now, let's continue, since I found it quite interesting!

[Kevin Buzzard]

Yeah, if (∀ a : M, m ∣ a ↔ n ∣ a) ↔ associated m n is missing then that's one thing, and then for nat you need associated iff equal.

[Damiano Testa]

So, I would define a relation on a monoid to simply be that r a b if b is divisible by a. To "remove" loops, I would need to quotient by them.

How do you form quotients by relations?

[Damiano Testa]

Once that is done, I would prove that the relation is induces a partial order on the quotient.

[Kevin Buzzard]

I think you need commutativity to make this sensible. To form a quotient by a relation check out the section on quotients in #tpil or my notes on quotients from my course https://xenaproject.wordpress.com/2021/03/04/formalising-mathematics-workshop-7-quotients/

[Mario Carneiro]

Also, I'm suggesting here that the construction of a partial order quotienting a preorder is independent of anything about divisibility

[Mario Carneiro]

although it has some relations to associated and other things when you instantiate the construction in this setting

[Damiano Testa]

Yes, I was going to take a "general" approach, where each step "resets the bar".

[Eric Wieser]

How bad an idea is this statement

/-- `dvd` is injective in the left argument -/
lemma dvd_left_injective : function.injective ((∣) : ℕ → ℕ → Prop) :=
λ m n h, let h := congr_fun h in dvd_antisymm ((h n).mpr (dvd_refl _)) ((h m).mp (dvd_refl _))

[Eric Wieser]

From which the original statement recovers as

lemma dvd_right_iff_eq {m n : ℕ} : (∀ a : ℕ, m ∣ a ↔ n ∣ a) ↔ m = n :=
iff.trans (forall_congr $ λ _, eq_iff_iff.symm) $
  function.funext_iff.symm.trans dvd_left_injective.eq_iff

[Kevin Buzzard]

That's a great way of thinking about it!

[Damiano Testa]

That is a very funny way of expressing the result! I had never thought about it like this!

[Damiano Testa]

Eric, if you want, I can add it to PR #7132, unless you want to PR it on its own.

[Eric Wieser]

I think your original version is better, but perhaps proving mine in terms of yours is fine to have too, if only to leave in as a puzzle for the reader to teach them more about equality in lean

[Damiano Testa]

I have been playing with the circle of ideas that was discussed here: I now have a (very easy) proof that divisibility in a monoid is a preorder.

I also proved that two elements that divide each other in a cancel_comm_monoid are "associated": they differ by a unit.

The next step would be to form the quotient of a preorder to obtain a partial_order.

Finally, in the case of the partial_order obtained as above from a cancel_comm_monoid, I will want to establish that the "fibres" of this quotient are torsors under the group of units (this is essentially already available).

My next main obstacle is that I do not know how to form quotients. I found quotient, but there is very little guidance on how to use it. Also, it is in the folder of files that I have been warned to not touch, so I feel a little worried about even browsing it!

Should I simply pull up my sleeves and learn how to use quotient, or is there some easier file that I can look at?

[Yakov Pechersky]

You can read Kevin's post on https://xenaproject.wordpress.com/2021/03/04/formalising-mathematics-workshop-7-quotients/, and look at the exercises in https://github.com/ImperialCollegeLondon/formalising-mathematics/tree/master/src/week_7

[Yakov Pechersky]

The basic aspect of it, if you have a setoid X, which you get from some equivalence on X, which is just a relation r : X -> X -> Prop such that reflexive r, symmetric r, transitive r, you can form a quotient.

[Damiano Testa]

Yakov, thanks for the pointer: I will take a look!