ring_mul_action

Stream: maths

[Kevin Buzzard]

A mul_action is G →* (X ≃ X), and a distrib_mul_action is G →* (X ≃+ X). For the study of decomposition and inertia groups @Michail Karatarakis needs G →* (X ≃+* X), e.g. a Galois group acting on the top field. Should there be a new typeclass for this? The extra axioms are g \bub 1 = 1 and g \bub (x * y) = g \bub x * g \bub y.

[Adam Topaz]

docs#mul_semiring_action

[Adam Topaz]

I learned this existed from @Eric Wieser !

[Eric Wieser]

I learnt it existed only because it being in mathlib interfered with a refactor at one point!

[Eric Wieser]

docs#mul_semiring_action.to_ring_equiv is almost what Kevin is asking for I think

[Eric Wieser]

I think we're missing the group structure on ring automorphisms? (docs#ring_aut.group)

[Eric Wieser]

docs#mul_semiring_action.to_ring_aut seems to be what's missing

[Yaël Dillies]

docs#ring_hom.End is a dead end

[Eric Wieser]

That's the one that I was thinking of as being missing, thanks

[Adam Topaz]

Is @Kevin Buzzard asking for the actual morphism G →* (X ≃+* X), or just for the class? Or both?

[Eric Wieser]

Well we have the class, just not the morphism

[Adam Topaz]

right

[Eric Wieser]

The latter would be easy to add!

[Kevin Buzzard]

Oh nice! Thanks!

[Eric Wieser]

We also seem to be missing the ring_equiv version of docs#alg_equiv.apply_mul_semiring_action

[Kevin Buzzard]

Do we have

example (G : Type) [group G] (X : Type) :
  mul_action G X ≃ (G →* (X ≃ X)) :=
{ to_fun := λ a, by exactI
  { to_fun := λ g,
    { to_fun := λ x, g • x,
      inv_fun := λ x, g⁻¹ • x,
      left_inv := inv_smul_smul g,
      right_inv := smul_inv_smul g },
    map_one' := equiv.ext (one_smul G),
    map_mul' := λ g h, equiv.ext (mul_smul g h) },
  inv_fun := λ f,
  { smul := λ g x, f g x,
    one_smul := λ x, begin
      have := f.map_one,
      rw equiv.ext_iff at this,
      exact this x,
    end,
    mul_smul := λ g h x, begin
      have := f.map_mul g h,
      rw equiv.ext_iff at this,
      exact this x,
    end  },
  left_inv := λ x, begin
    ext,
    refl,
  end,
  right_inv := λ f, begin
    ext g x,
    refl,
  end }

and the equivalent for distrib_mul_action and mul_semiring_action?

[Adam Topaz]

I doubt it.

[Kevin Buzzard]

IIRC

    { to_fun := λ x, g • x,
      inv_fun := λ x, g⁻¹ • x,
      left_inv := inv_smul_smul g,
      right_inv := smul_inv_smul g },

has a name

[Yaël Dillies]

docs#mul_action.to_perm

[Eric Wieser]

If you add the definitions I mention above then we essentially do have that

[Eric Wieser]

docs#mul_semiring_action.to_ring_aut would be the forward direction, and docs#mul_semiring_action.comp_hom would be the reverse (edit: also missing, c.f docs#mul_action.comp_hom)

[Kevin Buzzard]

@Michail Karatarakis can you put the pieces together?

[Michail Karatarakis]

Yes, thank you

[Eric Wieser]

If you end up PRing these, feel free to ping me in review

[Michail Karatarakis]

Hi, could someone give me permission to push (this is my first PR) please? My Github name is mkaratarakis

[Riccardo Brasca]

Invitation sent!

[Michail Karatarakis]

Great, thanks a lot!