## Stream: new members

### Topic: semilattice, dvd, associated

#### Damiano Testa (Apr 09 2021 at 10:17):

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 (Apr 09 2021 at 10:18):

anyone can change topics retroactively

#### Damiano Testa (Apr 09 2021 at 10:19):

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

#### Kevin Buzzard (Apr 09 2021 at 10:21):

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 (Apr 09 2021 at 10:22):

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 (Apr 09 2021 at 10:23):

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

#### Kevin Buzzard (Apr 09 2021 at 10:38):

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 (Apr 09 2021 at 10:46):

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

#### Mario Carneiro (Apr 09 2021 at 10:47):

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

#### Damiano Testa (Apr 09 2021 at 10:47):

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

#### Eric Wieser (Apr 09 2021 at 16:21):

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 (Apr 09 2021 at 16:33):

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 (Apr 09 2021 at 16:34):

That's a great way of thinking about it!

#### Damiano Testa (Apr 09 2021 at 18:43):

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

#### Damiano Testa (Apr 09 2021 at 18:44):

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

#### Eric Wieser (Apr 09 2021 at 19:47):

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 (Apr 11 2021 at 17:04):

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 (Apr 11 2021 at 17:15):

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 (Apr 11 2021 at 17:16):

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 (Apr 11 2021 at 17:21):

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

Last updated: May 08 2021 at 19:11 UTC