Actions by Submonoids

These instances transfer the action by an element m : M of a monoid M written as m • a onto the action by an element s : S of a submonoid S : Submonoid M such that s • a = (s : M) • a.

These instances work particularly well in conjunction with Monoid.toMulAction, enabling s • m as an alias for ↑s * m.

instance Submonoid.smul {M' : Type u_1} {α : Type u_2} [MulOneClass M'] [SMul M' α] (S : Submonoid M') : SMul (↥S) α

Equations

• S.smul = SMul.comp α ⇑S.subtype

instance AddSubmonoid.vadd {M' : Type u_1} {α : Type u_2} [AddZeroClass M'] [VAdd M' α] (S : AddSubmonoid M') : VAdd (↥S) α

Equations

• S.vadd = VAdd.comp α ⇑S.subtype

instance Submonoid.smulCommClass_left {M' : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass M'] [SMul M' β] [SMul α β] [SMulCommClass M' α β] (S : Submonoid M') : SMulCommClass (↥S) α β

instance AddSubmonoid.vaddCommClass_left {M' : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass M'] [VAdd M' β] [VAdd α β] [VAddCommClass M' α β] (S : AddSubmonoid M') : VAddCommClass (↥S) α β

instance Submonoid.smulCommClass_right {M' : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass M'] [SMul α β] [SMul M' β] [SMulCommClass α M' β] (S : Submonoid M') : SMulCommClass α (↥S) β

instance AddSubmonoid.vaddCommClass_right {M' : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass M'] [VAdd α β] [VAdd M' β] [VAddCommClass α M' β] (S : AddSubmonoid M') : VAddCommClass α (↥S) β

instance Submonoid.isScalarTower {M' : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass M'] [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] (S : Submonoid M') : IsScalarTower (↥S) α β

Note that this provides IsScalarTower S M' M' which is needed by SMulMulAssoc.

theorem Submonoid.smul_def {M' : Type u_1} {α : Type u_2} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} (g : ↥S) (a : α) : g • a = ↑g • a

theorem AddSubmonoid.vadd_def {M' : Type u_1} {α : Type u_2} [AddZeroClass M'] [VAdd M' α] {S : AddSubmonoid M'} (g : ↥S) (a : α) : g +ᵥ a = ↑g +ᵥ a

@[simp]

theorem Submonoid.mk_smul {M' : Type u_1} {α : Type u_2} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} (g : M') (hg : g ∈ S) (a : α) : ⟨g, hg⟩ • a = g • a

@[simp]

theorem AddSubmonoid.mk_vadd {M' : Type u_1} {α : Type u_2} [AddZeroClass M'] [VAdd M' α] {S : AddSubmonoid M'} (g : M') (hg : g ∈ S) (a : α) : ⟨g, hg⟩ +ᵥ a = g +ᵥ a

instance Submonoid.mulAction {M' : Type u_1} {α : Type u_2} [Monoid M'] [MulAction M' α] (S : Submonoid M') : MulAction (↥S) α

The action by a submonoid is the action by the underlying monoid.

Equations

• S.mulAction = MulAction.mk ⋯ ⋯

instance AddSubmonoid.addAction {M' : Type u_1} {α : Type u_2} [AddMonoid M'] [AddAction M' α] (S : AddSubmonoid M') : AddAction (↥S) α

The additive action by an AddSubmonoid is the action by the underlying AddMonoid.

Equations

• S.addAction = AddAction.mk ⋯ ⋯