MulAction.QuotientAction variant for mulaction on module

Stream: Is there code for X?

[Edward van de Meent]

from as far as i can tell, docs#MulAction.QuotientAction only works for using smul on a set with a multiplicative structure, but i'd like to talk about the (multiplicative) action of a group on a quotient of modules, which has an additive structure. IsScalarTower does not hold, the semi-"toAdd"-ification of the field of MulAction.QuotientAction does...

[Johan Commelin]

Do we have quotients of group representations in Mathlib/RepresentationTheory/? They should give you the right action...

[Edward van de Meent]

not as far as i can tell...

[Johan Commelin]

And where does a quotient of modules get the smul of its ring of scalars? Because that ring is a multiplicative monoid... So hopefully that's done in the right abstraction

[Edward van de Meent]

that does exist, but that only works for the ring of scalars itself...
for the record, that is docs#Submodule.Quotient.mulAction

[Edward van de Meent]

for now, i've defined this:

section
variable {α : Type*} (β : Type*) (K : Type*) [Ring K]
  [AddCommGroup α]
  [Module K α]
  [Monoid β] [MulAction β α] (H : Submodule K α)


class MulAction.ModuleQuotientAction : Prop where
  neg_add_mem : ∀ (b : β), ∀ (a a' : α) , - a + a' ∈ H → - (b • a) + (b • a') ∈ H


variable [MulAction.ModuleQuotientAction β K H]

instance : MulAction β (α ⧸ H) where
  smul b := Quotient.map' (b • ·) fun a a' h => by
    apply QuotientAddGroup.leftRel_apply.mpr
    simp only [Submodule.mem_toAddSubgroup]
    apply MulAction.ModuleQuotientAction.neg_add_mem b
    apply QuotientAddGroup.leftRel_apply.mp h
  one_smul q := Quotient.inductionOn' q fun a => congr_arg Quotient.mk'' (one_smul β a)
  mul_smul b b' q := Quotient.inductionOn' q fun a => congr_arg Quotient.mk'' (mul_smul b b' a)

-- #synth SMul β (α ⧸ H)

end

this quite possibly might conflict due to some defEq issues in combination with addition being commutative, but this at least does give the instance i want

[Kevin Buzzard]

Shouldn't docs#SubMulAction be involved somehow?

Typically we don't do the golfy "closed under x - y" trick because even though it's one axiom not two, in practice you use add_mem and neg_mem and zero_mem so you have to prove them anyway.

[Edward van de Meent]

the thing is, i basically lifted this proof from the one at docs#MulAction.quotient

[Edward van de Meent]

(as well as the field for the structure)

[Edward van de Meent]

so although you might be right, i wouldn't know how to adress this...