Can there be two instances of `Algebra R A`?

Stream: mathlib4

[The-Anh Vu-Le]

I am not well-versed in abstract algebra, so I want to ask if there can be two R-algebras with different structure maps?

I am asking to see if there are multiple instances, how does mathlib4 know which one to use?

[Kevin Buzzard]

It uses the last one that it saw. You can have two maps f g : R →+* S but you cannot use the [Algebra R S] typeclass for both of them; the typeclass inference system works under the assumption that there's at most one term of a typeclass type, and if there is more than one then code is likely to break in obscure ways -- this is called a "diamond" by the community here.

[Kevin Buzzard]

The notation R →+* S is notation for RingHom R S and this is a structure, not a class, so it's fine to have more than one term of that type.

[Kevin Buzzard]

Of course you can have [Algebra R A] and [Algebra R B], that's fine.

[Kyle Miller]

Correct me if I'm wrong, I think "diamonds" refer to the issue where depending on which way you go through the class hierarchy you might get different equal-but-not-defeq definitions.

I think the word "canonicity" is used for the assumption that there's at most one instance.

[Kevin Buzzard]

Oh I see, a diamond is more general than "two instances of one class", it's "two unequal paths through the typeclass system" (possibly of larger length than one)

[Eric Wieser]

I think "diamond" is also used for not-equal-at-all, such as the conflict caused by Algebra R A[X] and Algebra R[X] A[X] (both assuming Algebra R A) for Algebra R[X] R[X][X]

[Johan Commelin]

Kyle Miller said:

I think the word "canonicity" is used for the assumption that there's at most one instance.

Wait, are you claiming there is a definition of "canonical"? :rofl:

[Johan Commelin]

alias canonical := inferInstance

[Kevin Buzzard]

That's my working definition of canonical in lean!

[Jon Eugster]

a bit late, but just to note: If you do have a statement about two algebra structures, you could still formulate it as theorem xyz (h1 : Algebra R S) (h2 : Algebra R S) ... : ... := ... instead of using []. Then the user has to provide the algebras manually when using the theorem, but could still use inferInstance to canonically fill in one of the two arguments.

[Eric Wieser]

This is still going to be a nightmare because Lean will automatically pick between the two in the theorem statement in a probably-surprising way.