Bad Diamonds in Lean Tutorial

Stream: new members

[Nick Attkiss]

Section 7.1 of the Mathematics in Lean tutorial discusses the "bad diamond" formed when we define two different instances of Module₁ ℤ ℤ. The rest of the section discusses how to solve the issue, but it's pretty unclear to me what changing the definition of AddMonoid has to do with modules or bad diamonds; in fact, we don't find the term "module" or "bad diamond" anywhere in S7.1 after the paragraph beginning "In our concrete case." May I have some clarification on what the problem and solution in this section actually are?

[Eric Wieser]

I wrote a little more about this specific example in my thesis, section 4.5 or more specifically 4.5.2.

[Nick Attkiss]

I took a look through that section but I'm still stuck on a few points. I think the problem being solved is that a \bu b has an ambiguous meaning when a b : Int, and defining the scalar multiplication in addGroup instances rather than in Module instances allows us to reconcile the two definitions and provide a proof that they're equivalent. But then how do we implement the rest of the module axioms for scalar multiplication of Int on itself? And do we abandon the module instances selfModule and addCommGroup, even though they make elementary and important mathematical observations?

[Ruben Van de Velde]

So, the thing is: an AddGroup, or more pedantically, a SubNegMonoid gives rise to a scalar multiplication by Int ( docs#SubNegMonoid.SMulInt ), namely z \bu x = x + ... + x (z times). The trick is that we don't literally define the scalar multiplication as x + ... + x, but instead any time you define an instance of SubNegMonoid, you have to define a zsmul function that just happens to behave as (be propositionally equal to) x + ... + x. In the case of Int ( docs#Int.instAddCommGroup ), this zsmul is defined to be z * x instead.

This happens to match docs#Semiring.toModule (actually docs#Monoid.toMulAction ), which also defines a \bu b as a * b

That is, the problem we had is that the two scalar multiplications int \bu int are mathematically the same (z * x vs x + ... + x), but defined differently, and we've solved it by making the definition of SubNegMonoid.SMulInt more flexible

Does that help?