RingAutomorphisms act on units via application

Stream: Is there code for X?

[Edward van de Meent]

i tried looking for an applicable instance, but i have yet to find it...

in particular, i'd like to know if there already exists something along the lines of this:

import Mathlib.FieldTheory.Finite.GaloisField
import Mathlib.GroupTheory.GroupAction.DomAct.Basic -- unoptimised imports

section
instance {K:Type*} [Semiring K]: MulDistribMulAction (RingAut K) Kˣ where
  smul := fun σ x => ⟨σ x, σ x.inv,
    by
      rw [← σ.map_mul]
      simp only [Units.inv_eq_val_inv, Units.mul_inv, map_one],
    by
      rw [← σ.map_mul]
      simp only [Units.inv_eq_val_inv, Units.inv_mul, map_one]⟩
  one_smul := fun b => rfl
  mul_smul := fun x y b => rfl
  smul_mul := fun r x y => by
    simp_rw [HSMul.hSMul]
    simp only [Units.val_mul, map_mul, Units.inv_eq_val_inv, mul_inv_rev]
    rfl
  smul_one := fun r => by
    simp_rw [HSMul.hSMul]
    simp only [Units.val_one, map_one, Units.inv_eq_val_inv, inv_one]
    rfl

end
section

variable {K:Type*} [Field K] -- this is my specific use case
#synth MulDistribMulAction (RingAut K) Kˣ
end

[Edward van de Meent]

in comparison it does find the action MulDistribMulAction (RingAut K) K when not just looking at units

[Eric Wieser]

We have the MulAction version:

[Eric Wieser]

@loogle MulAction _ (Units _)

[loogle]

:search: Units.mulAction'

[Eric Wieser]

In theory, docs#Units.mulDistribMulAction' should apply here, but maybe it is stated with the wrong assumptions

[Edward van de Meent]

both of these seem to require IsScalarTower (RingAut K) K K, which doesn't hold...

[Edward van de Meent]

because that would mean that f x * y = f (x * y)

[Edward van de Meent]

similarly, SMulCommClass (RingAut K) K K is equivalent to x * f y = f (x * y)

[Edward van de Meent]

btw, is there a reason IsScalarTower isn't called SMulAssocClass?

[Eric Wieser]

Edward van de Meent said:

both of these seem to require IsScalarTower (RingAut K) K K, which doesn't hold...

I think it's likely this is a mistake; maybe try looking through the history to see if there were any comments when it was written? (Prediction: I wrote it...)

[Eric Wieser]

The fix will be to replace that instance with your proof, which will hold just fine in the general case after notation modifications. The question is whether we still need the old instance as well for something, or if it's completely useless

[Edward van de Meent]

it looks like the multiplication in those instances is also different from the one i'm looking for...
those instances use (f x).inv = f.inv x.inv, but i believe i need (f x).inv = f x.inv

[Eric Wieser]

Well, in any situation where both your instance and that instance apply, they must be propositionally equal

[Eric Wieser]

My point was more "you should generalize your result away from RingAut"

[Edward van de Meent]

ah yes, that makes sense

[Edward van de Meent]

how about this:

instance [Monoid G] [Monoid M] [MulDistribMulAction G M] : MulDistribMulAction G Mˣ where
  smul := fun f x => ⟨f • x, f • x.inv,
    by
      rw [← MulDistribMulAction.smul_mul]
      simp only [Units.inv_eq_val_inv, Units.mul_inv, smul_one],
    by
      rw [← MulDistribMulAction.smul_mul]
      simp only [Units.inv_eq_val_inv, Units.inv_mul, smul_one]⟩
  one_smul := fun b => by
    ext
    exact (@MulAction.one_smul G M) b
  mul_smul := fun x y b => by
    ext
    exact (@MulAction.mul_smul G M) x y b
  smul_mul := fun r x y => by
    ext
    exact (@MulDistribMulAction.smul_mul G M) r x y
  smul_one := fun r => by
    ext
    exact (@MulDistribMulAction.smul_one G M) r

[Eric Wieser]

I think you can avoid the long theorems names there by using docs#smul_mul' etc

[Eric Wieser]

Here's the golfed version:

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 _

[Eric Wieser]

Eric Wieser said:

I think it's likely this is a mistake; maybe try looking through the history to see if there were any comments when it was written? (Prediction: I wrote it...)

Yep, this was me in #10480

[Eric Wieser]

It looks like I somehow lost track of Reid's comments in response to that PR:

@Reid Barton said:

But those are the wrong conditions!

It should be simply [group G] [monoid M] [mul_distrib_mul_action G M]

[Edward van de Meent]

I mean... It does compile, so I'm not sure it's "wrong" per se, maybe not as applicable as expected.