Mathlib.Algebra.Group.Submonoid.MulAction

Submonoid.instSMulSubtypeMem instance

[SMul M' α] : SMul s α

Full source

@[to_additive]
instance (priority := low) [SMul M' α]  : SMul s α where
  smul m a := (m : M') • a

Scalar Multiplication Action Inherited by Submonoid

Informal description

For any submonoid $S$ of a monoid $M$ with a scalar multiplication action on a type $\alpha$, the submonoid $S$ inherits a scalar multiplication action on $\alpha$ defined by $s \bullet a = (s : M) \bullet a$ for $s \in S$ and $a \in \alpha$.

Submonoid.instSMulCommClassSubtypeMem instance

[SMul M' β] [SMul α β] [SMulCommClass M' α β] : SMulCommClass s α β

Full source

@[to_additive]
instance (priority := low) [SMul M' β] [SMul α β] [SMulCommClass M' α β] : SMulCommClass s α β :=
  ⟨fun a _ _ => smul_comm (a : M') _ _⟩

Commutativity of Scalar Multiplication between Submonoid and Another Action

Informal description

For any submonoid $S$ of a monoid $M$ with a scalar multiplication action on a type $\beta$, and given a scalar multiplication action of $\alpha$ on $\beta$ that commutes with the action of $M$ (i.e., $m \bullet (a \bullet b) = a \bullet (m \bullet b)$ for all $m \in M$, $a \in \alpha$, $b \in \beta$), the scalar multiplication actions of $S$ and $\alpha$ on $\beta$ also commute. That is, for any $s \in S$, $a \in \alpha$, and $b \in \beta$, we have $s \bullet (a \bullet b) = a \bullet (s \bullet b)$.

Submonoid.instSMulCommClassSubtypeMem_1 instance

[SMul α β] [SMul M' β] [SMulCommClass α M' β] : SMulCommClass α s β

Full source

@[to_additive]
instance (priority := low) [SMul α β] [SMul M' β] [SMulCommClass α M' β] : SMulCommClass α s β :=
  ⟨fun a s => smul_comm a (s : M')⟩

Commutativity of Scalar Multiplication between Submonoid and Another Action (Variant)

Informal description

For any type $\beta$ with a scalar multiplication action by a monoid $M'$ and another scalar multiplication action by a type $\alpha$, if these actions commute (i.e., $a \bullet (m \bullet b) = m \bullet (a \bullet b)$ for all $a \in \alpha$, $m \in M'$, $b \in \beta$), then for any submonoid $S$ of $M'$, the actions of $\alpha$ and $S$ on $\beta$ also commute. That is, $a \bullet (s \bullet b) = s \bullet (a \bullet b)$ for all $a \in \alpha$, $s \in S$, $b \in \beta$.

Submonoid.instIsScalarTowerSubtypeMem instance

[SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] : IsScalarTower s α β

Full source

@[to_additive]
instance (priority := low) [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] :
    IsScalarTower s α β :=
  ⟨fun a => smul_assoc (a : M')⟩

Scalar Tower Property for Submonoid Actions

Informal description

For any submonoid $S$ of a monoid $M$ with scalar multiplication actions on types $\alpha$ and $\beta$, if the actions of $M$ on $\alpha$ and $\beta$ form a scalar tower (i.e., $(m \cdot a) \cdot b = m \cdot (a \cdot b)$ for all $m \in M$, $a \in \alpha$, $b \in \beta$), then the actions of $S$ on $\alpha$ and $\beta$ also form a scalar tower. That is, for any $s \in S$, $a \in \alpha$, and $b \in \beta$, we have $(s \cdot a) \cdot b = s \cdot (a \cdot b)$.

Submonoid.instMulActionSubtypeMem instance

[MulAction M' α] : MulAction s α

Full source

@[to_additive]
instance (priority := low) [MulAction M' α] : MulAction s α where
  one_smul := one_smul M'
  mul_smul m₁ m₂ := mul_smul (m₁ : M') m₂

Multiplicative Action Inherited by Submonoid

Informal description

For any monoid $M'$ with a multiplicative action on a type $\alpha$, and any submonoid $s$ of $M'$, the submonoid $s$ inherits a multiplicative action on $\alpha$ defined by $s \bullet a = (s : M') \bullet a$ for $s \in s$ and $a \in \alpha$.

Submonoid.smul instance

[SMul M' α] (S : Submonoid M') : SMul S α

Full source

@[to_additive]
instance smul [SMul M' α] (S : Submonoid M') : SMul S α :=
  inferInstance

Scalar Multiplication Action Inherited by Submonoid

Informal description

For any monoid $M'$ with a scalar multiplication action on a type $\alpha$, and any submonoid $S$ of $M'$, the submonoid $S$ inherits a scalar multiplication action on $\alpha$ defined by $s \bullet a = (s : M') \bullet a$ for $s \in S$ and $a \in \alpha$.

Submonoid.smulCommClass_left instance

[SMul M' β] [SMul α β] [SMulCommClass M' α β] (S : Submonoid M') : SMulCommClass S α β

Full source

@[to_additive]
instance smulCommClass_left [SMul M' β] [SMul α β] [SMulCommClass M' α β]
    (S : Submonoid M') : SMulCommClass S α β :=
  inferInstance

Commutativity of Scalar Multiplication between Submonoid and Another Action

Informal description

For any monoid $M'$ with a scalar multiplication action on a type $\beta$, and any scalar multiplication action of $\alpha$ on $\beta$ that commutes with the action of $M'$ (i.e., $m \bullet (a \bullet b) = a \bullet (m \bullet b)$ for all $m \in M'$, $a \in \alpha$, $b \in \beta$), the scalar multiplication actions of any submonoid $S$ of $M'$ and $\alpha$ on $\beta$ also commute. That is, for any $s \in S$, $a \in \alpha$, and $b \in \beta$, we have $s \bullet (a \bullet b) = a \bullet (s \bullet b)$.

Submonoid.smulCommClass_right instance

[SMul α β] [SMul M' β] [SMulCommClass α M' β] (S : Submonoid M') : SMulCommClass α S β

Full source

@[to_additive]
instance smulCommClass_right [SMul α β] [SMul M' β] [SMulCommClass α M' β]
    (S : Submonoid M') : SMulCommClass α S β :=
  inferInstance

Commutativity of Scalar Multiplication between Submonoid and Another Action (Right Variant)

Informal description

For any type $\beta$ with a scalar multiplication action by a monoid $M'$ and another scalar multiplication action by a type $\alpha$, if these actions commute (i.e., $a \bullet (m \bullet b) = m \bullet (a \bullet b)$ for all $a \in \alpha$, $m \in M'$, $b \in \beta$), then for any submonoid $S$ of $M'$, the actions of $\alpha$ and $S$ on $\beta$ also commute. That is, $a \bullet (s \bullet b) = s \bullet (a \bullet b)$ for all $a \in \alpha$, $s \in S$, $b \in \beta$.

Submonoid.isScalarTower instance

[SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] (S : Submonoid M') : IsScalarTower S α β

Full source

/-- Note that this provides `IsScalarTower S M' M'` which is needed by `SMulMulAssoc`. -/
@[to_additive]
instance isScalarTower [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β]
      (S : Submonoid M') :
    IsScalarTower S α β :=
  inferInstance

Submonoid Actions Form a Scalar Tower

Informal description

For any monoid $M'$ with scalar multiplication actions on types $\alpha$ and $\beta$ forming a scalar tower (i.e., $(m \cdot a) \cdot b = m \cdot (a \cdot b)$ for all $m \in M'$, $a \in \alpha$, $b \in \beta$), and any submonoid $S$ of $M'$, the actions of $S$ on $\alpha$ and $\beta$ also form a scalar tower. That is, for any $s \in S$, $a \in \alpha$, and $b \in \beta$, we have $(s \cdot a) \cdot b = s \cdot (a \cdot b)$.

Submonoid.smul_def theorem

(g : S) (a : α) : g • a = (g : M') • a

Full source

@[to_additive] lemma smul_def (g : S) (a : α) : g • a = (g : M') • a := rfl

Submonoid Scalar Multiplication Definition

Informal description

For any submonoid $S$ of a monoid $M'$ with a scalar multiplication action on a type $\alpha$, and for any element $g \in S$ and $a \in \alpha$, the scalar multiplication $g \bullet a$ is equal to the scalar multiplication of $g$ (viewed as an element of $M'$) with $a$.

Submonoid.mk_smul theorem

(g : M') (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a

Full source

@[to_additive (attr := simp)]
lemma mk_smul (g : M') (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a := rfl

Submonoid Element Scalar Multiplication Equals Parent Monoid Action

Informal description

For any element $g$ of a monoid $M'$ that belongs to a submonoid $S$ (with proof $hg : g \in S$), and any element $a$ of a type $\alpha$ with a scalar multiplication action by $M'$, the scalar multiplication of the submonoid element $\langle g, hg \rangle$ on $a$ equals the scalar multiplication of $g$ on $a$. That is, $\langle g, hg \rangle \bullet a = g \bullet a$.

Submonoid.mulAction instance

[MulAction M' α] (S : Submonoid M') : MulAction S α

Full source

/-- The action by a submonoid is the action by the underlying monoid. -/
@[to_additive
      "The additive action by an `AddSubmonoid` is the action by the underlying `AddMonoid`. "]
instance mulAction [MulAction M' α] (S : Submonoid M') : MulAction S α :=
  inferInstance

Multiplicative Action Inherited by Submonoid

Informal description

For any monoid $M'$ with a multiplicative action on a type $\alpha$, and any submonoid $S$ of $M'$, the submonoid $S$ inherits a multiplicative action on $\alpha$ defined by $s \bullet a = (s : M') \bullet a$ for $s \in S$ and $a \in \alpha$.