group acting on algebra

Stream: Is there code for X?

[Johan Commelin]

How do I say that a group G acts on a K-algebra L via algebra automorphisms?

I have

import field_theory.galois

variables {K L G : Type*} [field K] [field L] [algebra K L] [group G] [distrib_mul_action G L]

but distrib_mul_action is certainly not strong enough for what I want. Do we have a class that does what I want?

[Eric Wieser]

Do you mean that each G is associated with a L ≃ₐ[K] L?

[Eric Wieser]

I think mul_semiring_action is close

[Eric Wieser]

Where docs#mul_semiring_action.to_semiring_equiv is the associated L ≃+* L

[Eric Wieser]

I guess to show it's an alg_equiv, you also need smul_comm_class K G L

[Eric Wieser]

So final answer,

variables {K L G : Type*} [field K] [field L] [algebra K L] [group G] [mul_semiring_action G L] [smul_comm_class K G L]

[Eric Wieser]

With these defs:

def mul_semiring_action.to_alg_hom
  (M R A : Type*) [monoid M] [comm_semiring R] [semiring A] [algebra R A] [mul_semiring_action M A]
  [smul_comm_class M R A] (x : M) :
  A →ₐ[R] A :=
{ commutes' := λ r, begin
    rw algebra.algebra_map_eq_smul_one r,
    refine (smul_comm _ _ _).trans _,
    rw smul_one,
  end,
  .. mul_semiring_action.to_ring_hom _ _ x}

def mul_semiring_action.to_alg_equiv
  (G R A : Type*) [group G] [comm_semiring R] [semiring A] [algebra R A] [mul_semiring_action G A]
  [smul_comm_class G R A] (x : G) :
  A ≃ₐ[R] A :=
{ .. mul_semiring_action.to_semiring_equiv _ _ x,
  .. mul_semiring_action.to_alg_hom _ _ _ x}

[Eric Wieser]

We should probably have distrib_mul_action.to_linear_map and distrib_mul_action.to_linear_equiv too (which I did in this thread)

[Johan Commelin]

@Eric Wieser awesome! and I can also make the action faithful, since a couple of days, right?

[Johan Commelin]

btw, I think the to_alg_equiv should be a monoid hom, or would that get another name?

[Eric Wieser]

It's a bit of a mess

[Eric Wieser]

We have docs#mul_action.to_perm and docs#mul_action.to_perm_hom

[Eric Wieser]

So in principle we should have mul_semiring_action.to_alg_hom and mul_semiring_action.to_alg_hom_hom

[Eric Wieser]

Alternatively, we should maybe eliminate the non-hom versions

[Eric Wieser]

We also have two spellings for docs#distrib_mul_action.to_add_monoid_hom, docs#const_smul_hom, which appear in entirely different files

[Eric Wieser]

The mess is further complicated by the fact that some auto-/endo- morphisms don't have instances for their monoid structures.

[Eric Wieser]

This would be a great cleanup project for someone looking to contribute!

[Eric Wieser]

I'll PR the above two defs, but leave the _hom variants to someone else

[Johan Commelin]

Thanks!

[Eric Wieser]

#8936

[Johan Commelin]

@Eric Wieser Are there any conventions on whether to use [smul_comm_class M R A] or [smul_comm_class R M A]?

[Eric Wieser]

Not yet. At any rate, if one instance is present the other one should always be too

[Eric Wieser]

Usually it ends up being the one that results in smul_comm rather than ←smul_comm being used in the proof. I guess the other rule is that you should never assume both typeclasses as that just slows down typeclass search for no good reason.