class/lemmas for smul distributing over smul

Stream: Is there code for X?

[Edward van de Meent]

i have three instances of SMul, and i'd like to use the fact that these are related via one distributing over another:

variable {K I:Type*} [Field K]

#synth MulAction Kˣ (I -> K) -- u • v = fun i => ↑u * (v i)

#synth MulAction (RingAut K) (I -> K) -- f • v := fun i => f (v i)

#synth MulAction (RingAut K) Kˣ -- f • u := ↑(f ↑u)

lemma ringaut_smul_unit_distrib (f : RingAut K) (d:Kˣ) (v:ι → K) :
    f • (d • v) = (f • d) • (f • v) := by
  ext i
  simp only [Pi.smul_apply, RingAut.smul_def]
  calc
    f (d • v i)
      = f (d * v i) := by rfl
    _ = f d * f (v i) := by rw [f.map_mul]

i'd like to know if there is some class i can use to lift this fact to functions d: I -> Kˣ

[Edward van de Meent]

i can imagine some kind of SMulDistribSMulClass would be used:

class SMulDistribSMulClass (A B C:Type*) [SMul A B] [SMul A C] [SMul B C] : Prop where
  smul_distrib (a:A) (b:B) (c:C) : a • (b • c) = (a • b) • (a • c)


instance Pi.instSMulDistribSMulClass (I A B : Type*) (C:I → Type*) [SMul A B]
    [∀ i, SMul A (C i)] [∀ i, SMul B (C i)] [∀ i,SMulDistribSMulClass A B (C i)]:
    SMulDistribSMulClass A B ((i:I) → C i) where
  smul_distrib a b c := by
    ext i
    simp only [Pi.smul_apply]
    rw [SMulDistribSMulClass.smul_distrib]

instance Pi.instSMulDistribSMulClass' (I A : Type*) (B C: I → Type*)
    [∀ i, SMul A (B i)] [∀ i, SMul A (C i)] [∀ i, SMul (B i) (C i)]
    [∀ i, SMulDistribSMulClass A (B i) (C i)] :
    SMulDistribSMulClass A ((i:I) → B i) ((i:I) → C i) where
  smul_distrib a b c := by
    ext i
    simp only [Pi.smul_apply, Pi.smul_apply']
    rw [SMulDistribSMulClass.smul_distrib]

instance Pi.instSMulDistribSMulClass'' (I : Type*) (A B C: I → Type*)
    [∀ i, SMul (A i) (B i)] [∀ i, SMul (A i) (C i)] [∀ i, SMul (B i) (C i)]
    [∀ i, SMulDistribSMulClass (A i) (B i) (C i)] :
    SMulDistribSMulClass ((i:I) → A i) ((i:I) → B i) ((i:I) → C i) where
  smul_distrib a b c := by
    ext i
    simp only [Pi.smul_apply']
    rw [SMulDistribSMulClass.smul_distrib]

[Edward van de Meent]

can someone point out what's going on here?

section
variable {G M K:Type*} [Semiring K]

-- #synth IsScalarTower (RingAut K) K K
-- #synth SMulCommClass (RingAut K) K K

instance [Monoid G] [Monoid M] [MulDistribMulAction G M] : MulDistribMulAction G Mˣ where
  smul g u := ⟨g • u, g • u⁻¹,
    by rw [← smul_mul', Units.mul_inv, smul_one],
    by rw [← smul_mul', Units.inv_mul, smul_one]⟩
  one_smul u := Units.ext <| one_smul _ _
  mul_smul g₁ g₂ u := Units.ext <| mul_smul _ _ _
  smul_mul g u₁ u₂ := Units.ext <| smul_mul' _ _ _
  smul_one g := Units.ext <| smul_one _

end

section

class SMulDistribSMulClass (A B C:Type*) [SMul A B] [SMul A C] [SMul B C] : Prop where
  smul_distrib (a:A) (b:B) (c:C) : a • (b • c) = (a • b) • (a • c)

instance MulDistribMulAction.instSMulDistribSmulClass (A B : Type*)
    [Monoid A] [Monoid B] [MulDistribMulAction A B] :
    SMulDistribSMulClass A B B where
  smul_distrib a b₁ b₂ := by
    simp only [smul_eq_mul, smul_mul']

variable {K:Type*} [Field K]

#synth MulDistribMulAction (RingAut K) Kˣ

#synth SMulDistribSMulClass (RingAut K) Kˣ Kˣ -- fails

example : SMulDistribSMulClass (RingAut K) Kˣ Kˣ := by
  apply MulDistribMulAction.instSMulDistribSmulClass (RingAut K) Kˣ
    -- failed to unify
    --   SMulDistribSMulClass (RingAut K) Kˣ Kˣ
    -- with
    --   SMulDistribSMulClass (RingAut K) Kˣ Kˣ

def foo := by
  apply MulDistribMulAction.instSMulDistribSmulClass (RingAut K) Kˣ

#check foo -- foo.{u_1} {K : Type u_1} [inst✝ : Field K] : SMulDistribSMulClass (RingAut K) Kˣ Kˣ

#synth SMulDistribSMulClass (RingAut K) K K -- succeeds

[Eric Wieser]

I think there is a bug in the error message generation there; I thought it was supposed to automatically add @s to make the differing arguments visible

[Eric Wieser]

Either way, if you click on the terms in the infoview you should be able to track down the issue

[Edward van de Meent]

it seems to be having problems with the fact that K has commutative multiplication...
it fails with CommMonoid K, but succeeds with Monoid K...

[Kevin Buzzard]

Can you post a #mwe ?

[Eric Wieser]

I am happy to look at this further tomorrow morning if someone doesn't beat me to it, but am not at lean right now: this is very likely either a problem I've seen before, or one of my own creation

[Edward van de Meent]

import Mathlib.Algebra.Module.Equiv
-- import Mathlib
import Init.Tactics

section

instance Units.instMulDistribMulAction' {G M :Type*}
    [Monoid G] [Monoid M] [MulDistribMulAction G M] : MulDistribMulAction G Mˣ where
  smul g u := ⟨g • u, g • u⁻¹,
    by rw [← smul_mul', Units.mul_inv, smul_one],
    by rw [← smul_mul', Units.inv_mul, smul_one]⟩
  one_smul u := Units.ext <| one_smul _ _
  mul_smul g₁ g₂ u := Units.ext <| mul_smul _ _ _
  smul_mul g u₁ u₂ := Units.ext <| smul_mul' _ _ _
  smul_one g := Units.ext <| smul_one _
end

section
class SMulDistribSMulClass (A B C:Type*) [SMul A B] [SMul A C] [SMul B C] : Prop where
  smul_distrib (a:A) (b:B) (c:C) : a • (b • c) = (a • b) • (a • c)

instance MulDistribMulAction.instSMulDistribSmulClass (A B : Type*)
    [Monoid A] [Monoid B] [MulDistribMulAction A B] :
    SMulDistribSMulClass A B B where
  smul_distrib a b₁ b₂ := by
    simp only [smul_eq_mul, smul_mul']


end

variable {K:Type*}
section
variable [Monoid K]

#synth MulDistribMulAction (MulAut K) Kˣ -- succeeds
#synth SMulDistribSMulClass (MulAut K) Kˣ Kˣ -- succeeds
end

section
variable [CommMonoid K]

#synth MulDistribMulAction (MulAut K) Kˣ -- succeeds
#synth SMulDistribSMulClass (MulAut K) Kˣ Kˣ -- fails
end

[Eric Wieser]

This is the issue:

example {K} [CommMonoid K] : (Monoid.toMulAction _ : MulAction Kˣ Kˣ) = Units.mulAction' :=
  -- fails
  rfl

example {K} [CommMonoid K] : (Monoid.toMulAction _ : MulAction Kˣ Kˣ) = Units.mulAction' := by
  -- ok
  ext
  rfl

[Eric Wieser]

I think this is what was being discussed in the other thread I linked to before

[Edward van de Meent]

ah yes, that seems right...

[Edward van de Meent]

so, for posterity, the issue is with the following definitional difference:

example {K} [CommMonoid K] (u₁ u₂:Kˣ):
  u₁ • u₂ = ⟨(u₁:K) * u₂,((u₁⁻¹:Kˣ):K) * u₂⁻¹,by sorry,by sorry⟩ := by rfl

example {K} [Monoid K] (u₁ u₂:Kˣ):
  u₁ • u₂ = ⟨u₁ * u₂, u₂⁻¹ * u₁⁻¹,by sorry,by sorry⟩ := by rfl

[Eric Wieser]

Here's the old thread