MulDistribMulAction instances

Stream: mathlib4

[Kevin Buzzard]

Are these instances suitable for inclusion in mathlib?

import Mathlib.Analysis.Normed.Lp.WithLp -- thanks #min_imports

-- Is this a bad instance?
instance (G M : Type*) [Monoid G] [Monoid M] [MulDistribMulAction G M] :
    MulDistribMulAction G Mˣ where
  smul g mx := ⟨g • mx, g • mx⁻¹, by simp [← smul_mul'], by simp [← smul_mul']⟩
  one_smul mx := by ext; exact one_smul G mx.1
  mul_smul g h mx := by ext; exact mul_smul g h mx.1
  smul_mul g mx nx := by ext; exact smul_mul' g mx.1 nx.1
  smul_one g := by ext; exact smul_one g

-- is this a bad instance?
instance (G M : Type*) [Monoid G] [Monoid M] [MulDistribMulAction G M] :
    DistribMulAction G (Additive M) where
  smul g am := .ofMul (g • am.toMul)
  one_smul _ := by simp only [one_smul]
  mul_smul _ _ _ := by simp only [mul_smul]
  smul_zero g := by simpa [HSMul.hSMul] using smul_one g
  smul_add g x y :=  by simpa [HSMul.hSMul] using smul_mul' g x.toMul _

The back story is that if $L/K$ is a Galois extension of fields with Galois group $G$ then I want to make $L^\times$ into a term of type Rep ℤ G and with both these instances in place it's as simple as Rep.ofDistribMulAction ℤ G (Additive Lˣ).

[Kevin Buzzard]

(I'm expecting an answer of the form "these instances are not allowed in mathlib because what if G=M^*" or "G = Unit" or some such thing, but I can't see any problems myself yet)

[Andrew Yang]

This fails:

-- Is this a bad instance?
def foo (G M : Type*) [Monoid G] [Monoid M] [MulDistribMulAction G M] :
    MulDistribMulAction G Mˣ where
  smul g mx := ⟨g • mx, g • mx⁻¹, by simp [← smul_mul'], by simp [← smul_mul']⟩
  one_smul mx := by ext; exact one_smul G mx.1
  mul_smul g h mx := by ext; exact mul_smul g h mx.1
  smul_mul g mx nx := by ext; exact smul_mul' g mx.1 nx.1
  smul_one g := by ext; exact smul_one g

variable (G : Type*) [Monoid G] in
example : foo (ConjAct Gˣ) G = (by infer_instance) := rfl --fails

I am not entirely sure if we care or not. I am guessing me might care.

[Eric Wieser]

What's the diamond expand to there?

[Eric Wieser]

Kevin's instances look sensible enough to me

[Andrew Yang]

The RHS is MulDistribMulAction (ConjAct Gˣ) Gˣ which comes from the generic MulDistribMulAction (ConjAct G) G instance.

[Andrew Yang]

The LHS goes through docs#ConjAct.unitsMulDistribMulAction and Kevin's instance.

[Yaël Dillies]

Investigating this further, @Kenny Lau noticed this instance was conflicting with docs#Units.mulDistribMulAction'. I was very confused at first since foo above sets g • u := ⟨g • u, g • u⁻¹, _, _⟩ while Units.mulDistribMulAction' sets g • u := ⟨g • u, g⁻¹ • u⁻¹, _, _⟩ and these are a priori not even propeq!

[Yaël Dillies]

By uniqueness of inverses, the above means that, whenever both instances are available, g⁻¹ • u⁻¹ = g • u⁻¹, which is certainly quite odd.

[Yaël Dillies]

And now I have figured out what's going on: The typeclass assumptions of Units.mulDistribMulAction' include MulDistribMulAction G M and SMulCommClass G M M. The first one reads g • (m₁ * m₂) = m₁ * g • m₂ while the second one reads g • (m₁ * m₂) = g • m₁ * g • m₂. If M is cancellative, this implies g • m₁ = m₁ for all g : G and m₁ : M. In other words, the action is trivial!

[Kenny Lau]

I see, so we should remove Units.mulDistribMulAction'!

[Yaël Dillies]

Yes, exactly. This unfortunately doesn't remove Andrew's diamond above, but at least we will have only one diamond to care about, rather than two.

[Kenny Lau]

Is Units.mulAction' also bad then?

[Yaël Dillies]

No, because it doesn't have this MulDistribMulAction G M assumption

[Yaël Dillies]

But my argument above also shows that it doesn't cause a diamond in non-degenerate cases: The only action on a (cancellative) monoid that satisfies both Units.mulAction' and foo is the trivial one.

[Yaël Dillies]

The instance was added in !3#10480 by no else than @Eric Wieser. Eric, did you have an application in mind?

[Yaël Dillies]

#32430

[Eric Wieser]

I think there's a previous thread about this somewhere

[Eric Wieser]

I claim the instance is harmless because it adds only proofs not data

[Yaël Dillies]

Lean-wise it is harmless. Mathematically, it is extremely confusing.

[Eric Wieser]

I think a docstring is a good solution then

[Eric Wieser]

But also I think there is an underlying issue here about right actions

[Yaël Dillies]

Sure, although I do wonder if we should have "theoretically harmless but mathematically useless" instances

[Yaël Dillies]

#32432

[Kenny Lau]

I don't understand this point, this wrong instance is blocking us from having the correct instance that we need

[Eric Wieser]

Kenny Lau said:

Is Units.mulAction' also bad then?

The situation is different if the answer to this is yes

[Eric Wieser]

Kenny, I claim what we mostly care about is diamonds in the notation classes, not diamonds in the derived classes (though obviously the latter implies the former)

[Eric Wieser]

Fixing the derived instances but not the underlying notation instance is just looking away from the problem

[Yaël Dillies]

Kenny Lau said:

I don't understand this point, this wrong instance is blocking us from having the correct instance that we need

It was mentally blocking, but not actually blocking. My argument for why Units.mulAction' is okay to have also applies to Units.mulDistribMulAction'