Mathlib.Algebra.Group.Subgroup.Actions

Subgroup.instMulAction instance

: MulAction S α

Full source

/-- The action by a subgroup is the action by the underlying group. -/
@[to_additive "The additive action by an add_subgroup is the action by the underlying `AddGroup`. "]
instance instMulAction : MulAction S α := inferInstanceAs (MulAction S.toSubmonoid α)

Multiplicative Action Inherited by Subgroup

Informal description

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

Subgroup.smul_def theorem

(g : S) (m : α) : g • m = (g : G) • m

Full source

@[to_additive] lemma smul_def (g : S) (m : α) : g • m = (g : G) • m := rfl

Subgroup Action Equals Group Action

Informal description

For a subgroup $S$ of a group $G$ acting on a type $\alpha$, the action of an element $g \in S$ on an element $m \in \alpha$ is equal to the action of $g$ considered as an element of $G$ on $m$, i.e., $g \bullet m = (g : G) \bullet m$.

Subgroup.mk_smul theorem

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

Full source

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

Subgroup Action Consistency: $\langle g, hg \rangle \bullet a = g \bullet a$

Informal description

For any group $G$ with a multiplicative action on a type $\alpha$, any subgroup $S$ of $G$, and any element $g \in G$ such that $g \in S$, the action of the subgroup element $\langle g, hg \rangle$ on $a \in \alpha$ equals the action of $g$ on $a$, i.e., $\langle g, hg \rangle \bullet a = g \bullet a$.

Subgroup.smulCommClass_left instance

[MulAction G β] [SMul α β] [SMulCommClass G α β] (S : Subgroup G) : SMulCommClass S α β

Full source

@[to_additive]
instance smulCommClass_left [MulAction G β] [SMul α β] [SMulCommClass G α β] (S : Subgroup G) :
    SMulCommClass S α β :=
  S.toSubmonoid.smulCommClass_left

Commutativity of Scalar Multiplication between Subgroup and Another Action

Informal description

For any group $G$ with a multiplicative action on a type $\beta$, and any scalar multiplication action of $\alpha$ on $\beta$ that commutes with the action of $G$ (i.e., $g \bullet (a \bullet b) = a \bullet (g \bullet b)$ for all $g \in G$, $a \in \alpha$, $b \in \beta$), the scalar multiplication actions of any subgroup $S$ of $G$ 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)$.

Subgroup.smulCommClass_right instance

[SMul α β] [MulAction G β] [SMulCommClass α G β] (S : Subgroup G) : SMulCommClass α S β

Full source

@[to_additive]
instance smulCommClass_right [SMul α β] [MulAction G β] [SMulCommClass α G β] (S : Subgroup G) :
    SMulCommClass α S β :=
  S.toSubmonoid.smulCommClass_right

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

Informal description

For any group $G$ with a multiplicative action on a type $\beta$, and any scalar multiplication action by a type $\alpha$ on $\beta$, if the actions of $\alpha$ and $G$ on $\beta$ commute (i.e., $a \cdot (g \cdot b) = g \cdot (a \cdot b)$ for all $a \in \alpha$, $g \in G$, $b \in \beta$), then for any subgroup $S$ of $G$, the actions of $\alpha$ and $S$ on $\beta$ also commute. That is, $a \cdot (s \cdot b) = s \cdot (a \cdot b)$ for all $a \in \alpha$, $s \in S$, $b \in \beta$.

Subgroup.instIsScalarTowerSubtypeMem instance

[SMul α β] [MulAction G α] [MulAction G β] [IsScalarTower G α β] (S : Subgroup G) : IsScalarTower S α β

Full source

/-- Note that this provides `IsScalarTower S G G` which is needed by `smul_mul_assoc`. -/
@[to_additive]
instance [SMul α β] [MulAction G α] [MulAction G β] [IsScalarTower G α β] (S : Subgroup G) :
    IsScalarTower S α β :=
  inferInstanceAs (IsScalarTower S.toSubmonoid α β)

Subgroups Inherit Scalar Tower Property

Informal description

For any group $G$ with multiplicative actions on types $\alpha$ and $\beta$ forming a scalar tower (i.e., $(g \cdot a) \cdot b = g \cdot (a \cdot b)$ for all $g \in G$, $a \in \alpha$, $b \in \beta$), and any subgroup $S$ of $G$, 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)$.

Subgroup.instFaithfulSMulSubtypeMem instance

[MulAction G α] [FaithfulSMul G α] (S : Subgroup G) : FaithfulSMul S α

Full source

@[to_additive]
instance [MulAction G α] [FaithfulSMul G α] (S : Subgroup G) : FaithfulSMul S α :=
  inferInstanceAs (FaithfulSMul S.toSubmonoid α)

Faithfulness of Subgroup Actions

Informal description

For any group $G$ with a faithful multiplicative action on a type $\alpha$, and any subgroup $S$ of $G$, the restricted action of $S$ on $\alpha$ is also faithful.

Subgroup.instDistribMulActionSubtypeMem instance

[AddMonoid α] [DistribMulAction G α] (S : Subgroup G) : DistribMulAction S α

Full source

/-- The action by a subgroup is the action by the underlying group. -/
instance [AddMonoid α] [DistribMulAction G α] (S : Subgroup G) : DistribMulAction S α :=
  inferInstanceAs (DistribMulAction S.toSubmonoid α)

Subgroups Inherit Distributive Multiplicative Actions

Informal description

For any additive monoid $\alpha$ and any group $G$ acting distributively on $\alpha$, a subgroup $S$ of $G$ inherits a distributive multiplicative action on $\alpha$. This means that the action of $S$ on $\alpha$ preserves addition and scalar multiplication, satisfying the distributive laws $(a + b) \cdot s = a \cdot s + b \cdot s$ and $a \cdot (s \cdot t) = (a \cdot s) \cdot t$ for all $a, b \in \alpha$ and $s, t \in S$.

Subgroup.instMulDistribMulActionSubtypeMem instance

[Monoid α] [MulDistribMulAction G α] (S : Subgroup G) : MulDistribMulAction S α

Full source

/-- The action by a subgroup is the action by the underlying group. -/
instance [Monoid α] [MulDistribMulAction G α] (S : Subgroup G) : MulDistribMulAction S α :=
  inferInstanceAs (MulDistribMulAction S.toSubmonoid α)

Subgroups Inherit Multiplicative Distributive Actions

Informal description

For any monoid $\alpha$ and any group $G$ acting multiplicatively and distributively on $\alpha$, a subgroup $S$ of $G$ inherits a multiplicative distributive action on $\alpha$. This means that the action of $S$ on $\alpha$ preserves multiplication and scalar multiplication, satisfying the distributive laws $(a \cdot b) \cdot s = (a \cdot s) \cdot (b \cdot s)$ for all $a, b \in \alpha$ and $s \in S$.

Subgroup.center.smulCommClass_left instance

: SMulCommClass (center G) G G

Full source

/-- The center of a group acts commutatively on that group. -/
instance center.smulCommClass_left : SMulCommClass (center G) G G :=
  Submonoid.center.smulCommClass_left

Commutative Action of the Center on a Group

Informal description

For any group $G$, the center of $G$ acts commutatively on $G$ itself. That is, for any element $z$ in the center of $G$ and any element $g \in G$, we have $z \cdot g = g \cdot z$.

Subgroup.center.smulCommClass_right instance

: SMulCommClass G (center G) G

Full source

/-- The center of a group acts commutatively on that group. -/
instance center.smulCommClass_right : SMulCommClass G (center G) G :=
  Submonoid.center.smulCommClass_right

Commutativity of Group Action with its Center

Informal description

For any group $G$, the scalar multiplication actions of $G$ and its center $\operatorname{center}(G)$ on $G$ commute with each other. That is, for any $g \in G$ and $z \in \operatorname{center}(G)$, we have $g \cdot (z \cdot h) = z \cdot (g \cdot h)$ for all $h \in G$.

Tags