Instance diamond in Equiv.TransferInstance

Stream: mathlib4

[Christian Merten]

Currently docs#Equiv.algebra is defined using docs#RingHom.toAlgebra'. This leads to a conflict with docs#Equiv.module. Namely the induced module instance by toAlgebra from the algebra instance coming from docs#Equiv.algebra is not defeq to the module instance coming from docs#Equiv.module.

import Mathlib.Logic.Equiv.TransferInstance

variable {R α β : Type} [CommRing R] (e : α ≃ β)
  [Semiring β] [Algebra R β]

def mod1 : let _ := e.addCommMonoid; Module R α :=
  e.module R

def mod2 : let _ := e.addCommMonoid; Module R α :=
  let _ := e.semiring
  (e.algebra R).toModule

-- this fails
example (x : α) (r : R) :
  let _ := e.addCommMonoid
  (mod1 e).smul r x = (mod2 e).smul r x := rfl

I suggest to redefine docs#Equiv.algebra using docs#Algebra.ofModule like so:

open Equiv

def Equiv.algebra' (e : α ≃ β) [Semiring β] :
    let semiring := Equiv.semiring e
    ∀ [Algebra R β], Algebra R α := by
  intros
  letI : Module R α := e.module R
  fapply Algebra.ofModule
  · intro r x y
    show e.symm (e (e.symm (r • e x)) * e y) = e.symm (r • e.ringEquiv (x * y))
    simp only [apply_symm_apply, Algebra.smul_mul_assoc, map_mul, ringEquiv_apply]
  · intro r x y
    show e.symm (e x * e (e.symm (r • e y))) = e.symm (r • e (e.symm (e x * e y)))
    simp only [apply_symm_apply, Algebra.mul_smul_comm]

def mod3 : let _ := e.addCommMonoid; Module R α :=
  let _ := e.semiring
  (e.algebra').toModule

-- this works
example (x : α) (r : R) :
  let _ := e.addCommMonoid
  (mod1 e).smul r x = (mod3 e).smul r x := rfl

Any objections?

[Christian Merten]

Since no one objected: #11419

[Matthew Ballard]

I asked bors to merge this. It would be nice to record your example as a issue. @Christian Merten can you do this?

[Antoine Chambert-Loir]

I take this thread as an opportunity to ask about how one should understand the comments to docs#AddMonoid.nsmulRec (“Multiplication by a natural number. Set this to nsmulRec unless Module diamonds are possible.”) and docs#AddGroup.zsmulRec (“Use instead n • a, which has better definitional behavior.”) when one wishes to define a module structure on a type, in my case, with respect to a CommRing. (It seems that something changed in a recent modification of mathlib. )

• One first has to define an AddCommMonoid or an AddCommGroup structure on it. Which one is preferable?
• Should one set the field nsmul and zsmul to nsmulRec and zsmulRec or is it better to first define the smulfield, and define nsmul n a as n • x? and similarly for zsmul n a?

[Eric Wieser]

It's better to define smul first and use that if possible; zsmulRec and nsmulRec are for the case where you don't expect to work with modules on your type at all, or at least don't want to think about them yet

[Eric Wieser]

I don't really understand your first question

[Eric Wieser]

Matthew Ballard said:

I asked bors to merge this. It would be nice to record your example as a issue. Christian Merten can you do this?

A test in instance_diamonds.lean might be more natural than an issue? Or did you have something more general in mind?

[Matthew Ballard]

A test is ok also but I didn't think about fixing the diamond completely itself only enough to note that the PR was the preferred way to transfer given how everything else transferred (eg SMul)

[Christian Merten]

Matthew Ballard said:

I asked bors to merge this. It would be nice to record your example as a issue. Christian Merten can you do this?

I am confused, are you suggesting to record this as a closed issue?

[Matthew Ballard]

The diamond still exists (in the aether). We are just taking the non-diamond path for this particular instance. It would be good to not forget the diamond still exists and even better if it gets fixed itself.

[Eric Wieser]

Are you suggesting that we stick a warning on docs#RingHom.toAlgebra that says "do not use this if you can avoid it, it creates instance diamonds"?

[Matthew Ballard]

I am suggesting recording the example above for now as an issue. I didn’t have time to pinpoint the exact issue of why there is a diamond.

[Antoine Chambert-Loir]

Eric Wieser said:

I don't really understand your first question

To get a module, an add comm monoid with an smul is enough, and one may get the add comm group afterwards. Is it safe to do so, or should one define them all, in a specific order?

[Eric Wieser]

Matthew Ballard said:

I am suggesting recording the example above for now as an issue. I didn’t have time to pinpoint the exact issue of why there is a diamond.

The diamond is from RingHom.toAlgebra, which creates a diamond by design

[Eric Wieser]

@Antoine Chambert-Loir , can you give a bit more context about what instance you're constructing? Do you have an example in a branch somewhere that is what you're referring to?

[Antoine Chambert-Loir]

It's the definition of polynomial maps, in the project @María Inés de Frutos Fernández and are doing.

[Antoine Chambert-Loir]

https://github.com/AntoineChambert-Loir/DividedPowers4/blob/0275b395b29d66f679c1c6ba84dd0d206eb38bfd/DividedPowers/PolynomialMap/Basic.lean#L236

[Eric Wieser]

Do you care about polynomial maps over additive monoids?

[Eric Wieser]

If not, you can skip the AddCommMonoid instance and just define the AddCommGroup instance

[Eric Wieser]

The sequence I recommend is:

• Provide a Zero and Add instance
• Provide a SMul instance
• Provide an AddCommGroup instance that uses the earlier smul for nsmul and zsmul
• Provide a Module instance

[Eric Wieser]

I think your question maybe stems from trying to merge step 1 with 3 and 2 with 4, and ending up with a dependency chain you can't untangle

[Antoine Chambert-Loir]

Eric Wieser said:

Do you care about polynomial maps over additive monoids?

Ultimately I will, just because the theory works, but for the moment it doesn't because a lot of stuff is incompletely done in mathlib (direct limits, eg).

[Eric Wieser]

I think in your example you can do steps 3 and 4 by pulling back the structure from functions

[Eric Wieser]

(docs#Function.injective.addCommGroup etc)

[Antoine Chambert-Loir]

No I don't, polynomial maps don't have such a natural injective map to functions (or they have, but one has to take a very large ring, such as MvPolynomial M R, which does not make a very natural proof).

[Eric Wieser]

Isn't toFun that map?

[Antoine Chambert-Loir]

It is indexed by all rings in the universe u.

[Eric Wieser]

Sure, it's not a function with the domain you're thinking of, but all the matters for lifting the structure is the codomain

[Antoine Chambert-Loir]

Yes, I understand. No, I don't. For docs#Function.Injective.addCommGroup to work, the domain has to look like a kind of additive group, with a zero, an addition, a subtraction. Maybe I do.

[Matthew Ballard]

Eric Wieser said:

Matthew Ballard said:

I am suggesting recording the example above for now as an issue. I didn’t have time to pinpoint the exact issue of why there is a diamond.

The diamond is from RingHom.toAlgebra, which creates a diamond by design

I understand the tension between the two pieces of data in Algebra but

1. I don't see any clear preference for one over the other in the library. (Maybe I am not looking hard enough.)
2. Any structure constructor that creates diamonds by design should probably be minimized or eliminated.

[Antoine Chambert-Loir]

Ad 2. Probably not, because 1) if you don't provide it, users will implement one, and diamonds will appear that were not predicted. 2) it will be possible to work on the design so that diamonds disappear.

[Matthew Ballard]

Not sure I agree but also

3. Algebra should unbundle the function and still extend SMul

[Eric Wieser]

I think RingHom.toAlgebra is a hack in the same way that Module.semiringToRing is; in rare cases there are no diamonds that could exist, so it's convenient.

[Kevin Buzzard]

So what am I supposed to do if in the middle of a proof I construct a ring hom from R to A and from this point on in the proof I want A to be an R-algebra?

[Christian Merten]

In my understanding, as long as there is no Module R A floating around, you are safe to use RingHom.toAlgebra. And if there already is a Module R A there should be no need to construct a ring hom (as long as that module instance is compatible with the multiplication of course).

[Kevin Buzzard]

I'm a bit confused. What if I did just construct the ring hom and I already have a module instance?

[Yaël Dillies]

Kevin Buzzard said:

So what am I supposed to do if in the middle of a proof I construct a ring hom from R to A and from this point on in the proof I want A to be an R-algebra?

You build the Algebra instance by hand, without using RingHom.toAlgebra

[Christian Merten]

So you alredy have an existing Module R A and then construct a new ring hom R to A? I think in this case you throw away your ring hom, use docs#Algebra.ofModule.

[Riccardo Brasca]

In a proof at worst you can always prove by hand that there is no diamond, can't you? I mean, the two structures are maybe not definitionally equal, but they're surely propositionally equal (otherwise you have another problem)

[Yaël Dillies]

Riccardo is right, but you can get the correct defeqs in the situation Kevin is talking about

[Matthew Ballard]

NB: right now there are issues with not-reducibly defeq instances all around Algebra Be sure to specify the function by hand

[Notification Bot]

28 messages were moved from this topic to #mathlib4 > Performance issues with Function.Injective.$typeclass by Eric Wieser.

[Junyan Xu]

Notice that there's currently a diamond between Ideal.Quotient.algebraOfLiesOver and Ideal.quotientAlgebra because Ideal.Quotient.algebraQuotientOfLEComap uses docs#RingHom.toAlgebra. This is causing an error in my PR.
cc authors and reviewer of #17415: @Yongle Hu @Jiang Jiedong @Andrew Yang
The proper fix is probably to change Ideal.Quotient.algebraQuotientOfLEComap (inherited from mathlib3) to take an Algebra argument instead of RingHom, and move it to the same file as Ideal.quotientAlgebra to golf it.

[Andrew Yang]

import Mathlib.RingTheory.Ideal.Over

variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B)

example : Ideal.Quotient.algebraOfLiesOver (P := P) (p := P.comap (algebraMap A B)) = Ideal.quotientAlgebra := rfl

Looks fine to me?

[Junyan Xu]

Indeed, thanks for checking! Sorry, the diamond was actually due to my change to Ideal.quotientAlgebra in the PR; it was using RingHom.toAlgebra too. But I think both Ideal.quotientAlgebra and Ideal.Quotient.algebraOfLiesOver because using RingHom.toAlgebra just forgets the SMul field. I should submit a PR to change both at once ...

[Junyan Xu]

Another issue is that since Ideal.Quotient.algebraQuotientOfLEComap is used to define an instance, it should be an abbrev rather than def.

[Junyan Xu]

I opened #19847 and it builds. Currently, it changes a large part of RamificationInertia to use Algebra instead of RingHom, and removes a lemma. If we do want to keep using RingHom, I'd change Ideal.Quotient.algebraQuotientPowRamificationIdx to a local instance because it has to use RingHom.toAlgebra. What do you think?