doc-next-gen

Mathlib.Algebra.Group.Action.Units

Module docstring

{"# Group actions on and by Mˣ

This file provides the action of a unit on a type α, SMul Mˣ α, in the presence of SMul M α, with the obvious definition stated in Units.smul_def. This definition preserves MulAction and DistribMulAction structures too.

Additionally, a MulAction G M for some group G satisfying some additional properties admits a MulAction G Mˣ structure, again with the obvious definition stated in Units.coe_smul. These instances use a primed name.

The results are repeated for AddUnits and VAdd where relevant. ","### Action of a group G on units of M "}

Units.instSMul instance
[Monoid M] [SMul M α] : SMul Mˣ α
Full source 
@[to_additive] instance [Monoid M] [SMul M α] : SMul Mˣ α where smul m a := (m : M) • a
Scalar Multiplication Action by Units of a Monoid
Informal description
For any monoid $M$ and any type $\alpha$ with a scalar multiplication action by $M$, the group of units $M^\times$ of $M$ also acts on $\alpha$ via scalar multiplication, where the action of a unit $m \in M^\times$ on $a \in \alpha$ is given by the action of the underlying element $m \in M$ on $a$.
Units.smul_def theorem
[Monoid M] [SMul M α] (m : Mˣ) (a : α) : m • a = (m : M) • a
Full source 
@[to_additive] lemma smul_def [Monoid M] [SMul M α] (m : Mˣ) (a : α) : m • a = (m : M) • a := rfl
Scalar Multiplication by Unit Equals Underlying Action
Informal description
For a monoid $M$ and a type $\alpha$ with a scalar multiplication action by $M$, the action of a unit $m \in M^\times$ on an element $a \in \alpha$ is equal to the action of the underlying element $m \in M$ on $a$, i.e., $m \bullet a = m \bullet a$.
Units.smul_mk_apply theorem
{M α : Type*} [Monoid M] [SMul M α] (m n : M) (h₁) (h₂) (a : α) : (⟨m, n, h₁, h₂⟩ : Mˣ) • a = m • a
Full source 
@[to_additive, simp]
lemma smul_mk_apply {M α : Type*} [Monoid M] [SMul M α] (m n : M) (h₁) (h₂) (a : α) :
    (⟨m, n, h₁, h₂⟩ : Mˣ) • a = m • a := rfl
Action of Unit Constructor on Element Equals Underlying Action
Informal description
Let $M$ be a monoid and $\alpha$ a type with a scalar multiplication action by $M$. For any elements $m, n \in M$ and proofs $h_1, h_2$ that $m$ and $n$ are inverses, the action of the unit $\langle m, n, h_1, h_2 \rangle \in M^\times$ on an element $a \in \alpha$ is equal to the action of $m$ on $a$, i.e., $\langle m, n, h_1, h_2 \rangle \cdot a = m \cdot a$.
Units.smul_isUnit theorem
[Monoid M] [SMul M α] {m : M} (hm : IsUnit m) (a : α) : hm.unit • a = m • a
Full source 
@[simp]
lemma smul_isUnit [Monoid M] [SMul M α] {m : M} (hm : IsUnit m) (a : α) : hm.unit • a = m • a := rfl
Action of a Unit Element Equals Action of Its Underlying Element
Informal description
Let $M$ be a monoid with a scalar multiplication action on a type $\alpha$, and let $m \in M$ be a unit with witness $hm : \text{IsUnit}\, m$. Then the action of the unit $\text{hm.unit}$ on an element $a \in \alpha$ is equal to the action of $m$ on $a$, i.e., $\text{hm.unit} \cdot a = m \cdot a$.
IsUnit.inv_smul theorem
[Monoid α] {a : α} (h : IsUnit a) : h.unit⁻¹ • a = 1
Full source 
@[to_additive]
lemma _root_.IsUnit.inv_smul [Monoid α] {a : α} (h : IsUnit a) : h.unit⁻¹ • a = 1 := h.val_inv_mul
Inverse Unit Action Yields Identity: $h.\text{unit}^{-1} \cdot a = 1$
Informal description
For any monoid $\alpha$ and any element $a \in \alpha$ that is a unit (i.e., $h : \text{IsUnit } a$ holds), the action of the inverse of the unit $h.\text{unit}^{-1}$ on $a$ yields the multiplicative identity $1$.
Units.instFaithfulSMul instance
[Monoid M] [SMul M α] [FaithfulSMul M α] : FaithfulSMul Mˣ α
Full source 
@[to_additive]
instance [Monoid M] [SMul M α] [FaithfulSMul M α] : FaithfulSMul Mˣ α where
  eq_of_smul_eq_smul h := Units.ext <| eq_of_smul_eq_smul h
Faithful Scalar Multiplication Action by Units of a Monoid
Informal description
For any monoid $M$ with a faithful scalar multiplication action on a type $\alpha$, the group of units $M^\times$ of $M$ also has a faithful scalar multiplication action on $\alpha$.
Units.instMulAction instance
[Monoid M] [MulAction M α] : MulAction Mˣ α
Full source 
@[to_additive]
instance instMulAction [Monoid M] [MulAction M α] : MulAction Mˣ α where
  one_smul := one_smul M
  mul_smul m n := mul_smul (m : M) n
Multiplicative Action of Units on a Type
Informal description
For any monoid $M$ and any type $\alpha$ with a multiplicative action by $M$, the group of units $M^\times$ of $M$ also has a multiplicative action on $\alpha$, where the action of a unit $u \in M^\times$ on an element $a \in \alpha$ is given by the action of the underlying element $u \in M$ on $a$.
Units.smulCommClass_left instance
[Monoid M] [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass Mˣ N α
Full source 
@[to_additive]
instance smulCommClass_left [Monoid M] [SMul M α] [SMul N α] [SMulCommClass M N α] :
    SMulCommClass Mˣ N α where smul_comm m n := smul_comm (m : M) n
Commutation of Scalar Actions by Units and Another Type
Informal description
For any monoid $M$ and any type $\alpha$ with commuting scalar multiplication actions by $M$ and another type $N$, the group of units $M^\times$ of $M$ also commutes with $N$ in their actions on $\alpha$. That is, for any unit $m \in M^\times$, any $n \in N$, and any $a \in \alpha$, we have $m \cdot (n \cdot a) = n \cdot (m \cdot a)$.
Units.smulCommClass_right instance
[Monoid N] [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass M Nˣ α
Full source 
@[to_additive]
instance smulCommClass_right [Monoid N] [SMul M α] [SMul N α] [SMulCommClass M N α] :
    SMulCommClass M Nˣ α where smul_comm m n := smul_comm m (n : N)
Commutation of Scalar Actions by $M$ and Units of $N$
Informal description
For any monoid $N$, type $\alpha$ with scalar multiplication actions by $M$ and $N$, and given that the actions of $M$ and $N$ on $\alpha$ commute, then the actions of $M$ and the group of units $N^\times$ on $\alpha$ also commute.
Units.instIsScalarTower instance
[Monoid M] [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] : IsScalarTower Mˣ N α
Full source 
@[to_additive]
instance [Monoid M] [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] :
    IsScalarTower Mˣ N α where smul_assoc m n := smul_assoc (m : M) n
Scalar Tower Property for Units of a Monoid
Informal description
For any monoid $M$ and types $N$, $\alpha$ with scalar multiplication actions by $M$ and $N$ such that $M$ and $N$ form a scalar tower over $\alpha$, the group of units $M^\times$ of $M$ and $N$ also form a scalar tower over $\alpha$. This means that for any unit $m \in M^\times$, element $n \in N$, and $a \in \alpha$, the action satisfies $(m \cdot n) \cdot a = m \cdot (n \cdot a)$.
Units.mulAction' instance
[Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] : MulAction G Mˣ
Full source 
/-- If an action `G` associates and commutes with multiplication on `M`, then it lifts to an
action on `Mˣ`. Notably, this provides `MulAction Mˣ Nˣ` under suitable conditions. -/
@[to_additive]
instance mulAction' [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M]
    [IsScalarTower G M M] : MulAction G Mˣ where
  smul g m :=
    ⟨g • (m : M), (g⁻¹ • ((m⁻¹ : Mˣ) : M)),
      by rw [smul_mul_smul_comm, Units.mul_inv, mul_inv_cancel, one_smul],
      by rw [smul_mul_smul_comm, Units.inv_mul, inv_mul_cancel, one_smul]⟩
  one_smul _ := Units.ext <| one_smul _ _
  mul_smul _ _ _ := Units.ext <| mul_smul _ _ _
Lifting of Group Action to Units of a Monoid
Informal description
For any group $G$ acting on a monoid $M$ such that the action commutes with multiplication and is compatible with scalar multiplication (i.e., $G$ acts associatively and distributively over $M$), this action lifts canonically to the group of units $M^\times$ of $M$. More precisely, if $G$ acts on $M$ via a multiplicative action satisfying the conditions `SMulCommClass G M M` and `IsScalarTower G M M`, then $G$ also acts multiplicatively on the units $M^\times$ of $M$.
Units.val_smul theorem
[Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] (g : G) (m : Mˣ) : ↑(g • m) = g • (m : M)
Full source 
@[to_additive (attr := simp)]
lemma val_smul [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M]
    (g : G) (m : Mˣ) : ↑(g • m) = g • (m : M) := rfl
Compatibility of Group Action with Unit Map: $\overline{g \cdot m} = g \cdot \overline{m}$
Informal description
Let $G$ be a group acting multiplicatively on a monoid $M$, with the action satisfying the compatibility conditions `SMulCommClass G M M` and `IsScalarTower G M M`. Then for any element $g \in G$ and any unit $m \in M^\times$, the canonical map from $M^\times$ to $M$ satisfies $\overline{g \cdot m} = g \cdot \overline{m}$, where $\overline{m}$ denotes the image of $m$ in $M$.
Units.smul_inv theorem
[Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] (g : G) (m : Mˣ) : (g • m)⁻¹ = g⁻¹ • m⁻¹
Full source 
/-- Note that this lemma exists more generally as the global `smul_inv` -/
@[to_additive (attr := simp)]
lemma smul_inv [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M]
    (g : G) (m : Mˣ) : (g • m)⁻¹ = g⁻¹ • m⁻¹ := ext rfl
Inverse of Scalar Multiplication on Units: $(g \cdot m)^{-1} = g^{-1} \cdot m^{-1}$
Informal description
Let $G$ be a group acting multiplicatively on a monoid $M$, with the action satisfying the compatibility conditions `SMulCommClass G M M` and `IsScalarTower G M M`. Then for any element $g \in G$ and any unit $m \in M^\times$, the inverse of the scalar multiplication $g \cdot m$ is equal to the scalar multiplication of the inverse of $g$ with the inverse of $m$, i.e., $(g \cdot m)^{-1} = g^{-1} \cdot m^{-1}$.
Units.smulCommClass' instance
[Group G] [Group H] [Monoid M] [MulAction G M] [SMulCommClass G M M] [MulAction H M] [SMulCommClass H M M] [IsScalarTower G M M] [IsScalarTower H M M] [SMulCommClass G H M] : SMulCommClass G H Mˣ
Full source 
/-- Transfer `SMulCommClass G H M` to `SMulCommClass G H Mˣ`. -/
@[to_additive "Transfer `VAddCommClass G H M` to `VAddCommClass G H (AddUnits M)`."]
instance smulCommClass' [Group G] [Group H] [Monoid M] [MulAction G M] [SMulCommClass G M M]
    [MulAction H M] [SMulCommClass H M M] [IsScalarTower G M M] [IsScalarTower H M M]
    [SMulCommClass G H M] :
    SMulCommClass G H Mˣ where smul_comm g h m := Units.ext <| smul_comm g h (m : M)
Commutation of Group Actions on Units of a Monoid
Informal description
For any groups $G$ and $H$ acting on a monoid $M$ such that their actions commute with multiplication and are compatible with scalar multiplication (i.e., both $G$ and $H$ act associatively and distributively over $M$), and if the actions of $G$ and $H$ on $M$ commute with each other, then the actions of $G$ and $H$ also commute on the group of units $M^\times$ of $M$. More precisely, given: 1. Groups $G$ and $H$ acting multiplicatively on $M$, 2. The condition that $G$ and $M$ commute in their action on $M$ (`SMulCommClass G M M`), 3. The condition that $H$ and $M$ commute in their action on $M$ (`SMulCommClass H M M`), 4. The condition that $G$ and $M$ form a scalar tower when acting on $M$ (`IsScalarTower G M M`), 5. The condition that $H$ and $M$ form a scalar tower when acting on $M$ (`IsScalarTower H M M`), 6. The condition that the actions of $G$ and $H$ on $M$ commute (`SMulCommClass G H M`), then the actions of $G$ and $H$ on $M^\times$ also commute (`SMulCommClass G H Mˣ`).
Units.isScalarTower' instance
[SMul G H] [Group G] [Group H] [Monoid M] [MulAction G M] [SMulCommClass G M M] [MulAction H M] [SMulCommClass H M M] [IsScalarTower G M M] [IsScalarTower H M M] [IsScalarTower G H M] : IsScalarTower G H Mˣ
Full source 
/-- Transfer `IsScalarTower G H M` to `IsScalarTower G H Mˣ`. -/
@[to_additive "Transfer `VAddAssocClass G H M` to `VAddAssocClass G H (AddUnits M)`."]
instance isScalarTower' [SMul G H] [Group G] [Group H] [Monoid M] [MulAction G M]
    [SMulCommClass G M M] [MulAction H M] [SMulCommClass H M M] [IsScalarTower G M M]
    [IsScalarTower H M M] [IsScalarTower G H M] :
    IsScalarTower G H Mˣ where smul_assoc g h m := Units.ext <| smul_assoc g h (m : M)
Scalar Tower Property for Group Actions on Units of a Monoid
Informal description
For any groups $G$ and $H$ acting on a monoid $M$ such that their actions commute with multiplication and are compatible with scalar multiplication (i.e., both $G$ and $H$ act associatively and distributively over $M$), and if the actions of $G$ and $H$ on $M$ form a scalar tower, then the actions of $G$ and $H$ also form a scalar tower on the group of units $M^\times$ of $M$. More precisely, given: 1. Groups $G$ and $H$ acting multiplicatively on $M$, 2. The condition that $G$ and $M$ commute in their action on $M$ (`SMulCommClass G M M`), 3. The condition that $H$ and $M$ commute in their action on $M$ (`SMulCommClass H M M`), 4. The condition that $G$ and $M$ form a scalar tower when acting on $M$ (`IsScalarTower G M M`), 5. The condition that $H$ and $M$ form a scalar tower when acting on $M$ (`IsScalarTower H M M`), 6. The condition that the actions of $G$ and $H$ on $M$ form a scalar tower (`IsScalarTower G H M`), then the actions of $G$ and $H$ on $M^\times$ also form a scalar tower (`IsScalarTower G H Mˣ`).
Units.isScalarTower'_left instance
[Group G] [Monoid M] [MulAction G M] [SMul M α] [SMul G α] [SMulCommClass G M M] [IsScalarTower G M M] [IsScalarTower G M α] : IsScalarTower G Mˣ α
Full source 
/-- Transfer `IsScalarTower G M α` to `IsScalarTower G Mˣ α`. -/
@[to_additive "Transfer `VAddAssocClass G M α` to `VAddAssocClass G (AddUnits M) α`."]
instance isScalarTower'_left [Group G] [Monoid M] [MulAction G M] [SMul M α] [SMul G α]
    [SMulCommClass G M M] [IsScalarTower G M M] [IsScalarTower G M α] :
    IsScalarTower G Mˣ α where smul_assoc g m := smul_assoc g (m : M)
Scalar Tower Property for Group Action on Units
Informal description
For any group $G$, monoid $M$, and type $\alpha$ with compatible scalar multiplication actions by $G$ and $M$, if $G$ acts on $M$ in a way that commutes with multiplication and forms a scalar tower with $M$ acting on $\alpha$, then $G$ also forms a scalar tower with the group of units $M^\times$ acting on $\alpha$. More precisely, given: 1. A group $G$ acting on $M$ via a multiplicative action, 2. A scalar multiplication action of $M$ on $\alpha$, 3. A scalar multiplication action of $G$ on $\alpha$, 4. The condition that $G$ and $M$ commute in their action on $M$ (`SMulCommClass G M M`), 5. The condition that $G$ and $M$ form a scalar tower when acting on $M$ (`IsScalarTower G M M`), 6. The condition that $G$ and $M$ form a scalar tower when acting on $\alpha$ (`IsScalarTower G M α`), then $G$ and the group of units $M^\times$ also form a scalar tower when acting on $\alpha$ (`IsScalarTower G Mˣ α`).
IsUnit.smul theorem
[Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] {m : M} (g : G) (h : IsUnit m) : IsUnit (g • m)
Full source 
@[to_additive]
lemma IsUnit.smul [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M]
    {m : M} (g : G) (h : IsUnit m) : IsUnit (g • m) :=
  let ⟨u, hu⟩ := h
  hu ▸ ⟨g • u, Units.val_smul _ _⟩
Preservation of Units under Group Action
Informal description
Let $G$ be a group acting multiplicatively on a monoid $M$ such that the action commutes with multiplication and forms a scalar tower. For any element $g \in G$ and any unit $m \in M$, if $m$ is a unit in $M$, then the scalar multiple $g \cdot m$ is also a unit in $M$.