Mathlib.Algebra.Group.Action.Basic

MulAction.toPerm definition

(a : α) : Equiv.Perm β

Full source

/-- Given an action of a group `α` on `β`, each `g : α` defines a permutation of `β`. -/
@[to_additive (attr := simps)]
def MulAction.toPerm (a : α) : Equiv.Perm β :=
  ⟨fun x => a • x, fun x => a⁻¹ • x, inv_smul_smul a, smul_inv_smul a⟩

Permutation induced by group action

Informal description

Given a group action of $\alpha$ on $\beta$, for each element $a \in \alpha$, the function $\text{MulAction.toPerm}(a)$ is a permutation of $\beta$ defined by $x \mapsto a \cdot x$, with its inverse given by $x \mapsto a^{-1} \cdot x$.

MulAction.toPerm_injective theorem

[FaithfulSMul α β] : Function.Injective (MulAction.toPerm : α → Equiv.Perm β)

Full source

/-- `MulAction.toPerm` is injective on faithful actions. -/
@[to_additive "`AddAction.toPerm` is injective on faithful actions."]
lemma MulAction.toPerm_injective [FaithfulSMul α β] :
    Function.Injective (MulAction.toPerm : α → Equiv.Perm β) :=
  (show Function.Injective (Equiv.toFunEquiv.toFun ∘ MulAction.toPerm) from smul_left_injective').of_comp

Injectivity of Group Action Permutation Map on Faithful Actions

Informal description

For a faithful scalar multiplication action of a type $\alpha$ on a type $\beta$, the map sending each element $a \in \alpha$ to the permutation $\text{toPerm}(a) \in \text{Perm}(\beta)$ (defined by $x \mapsto a \cdot x$) is injective. In other words, distinct elements of $\alpha$ induce distinct permutations of $\beta$.

MulAction.bijective theorem

(g : α) : Function.Bijective (g • · : β → β)

Full source

@[to_additive]
protected lemma MulAction.bijective (g : α) : Function.Bijective (g • · : β → β) :=
  (MulAction.toPerm g).bijective

Bijectivity of Group Action Elements

Informal description

For any element $g$ of a group $\alpha$ acting on a set $\beta$, the function $x \mapsto g \cdot x$ from $\beta$ to $\beta$ is bijective.

MulAction.injective theorem

(g : α) : Function.Injective (g • · : β → β)

Full source

@[to_additive]
protected lemma MulAction.injective (g : α) : Function.Injective (g • · : β → β) :=
  (MulAction.bijective g).injective

Injectivity of Group Action Elements

Informal description

For any element $g$ of a group $\alpha$ acting on a set $\beta$, the function $x \mapsto g \cdot x$ from $\beta$ to $\beta$ is injective.

MulAction.surjective theorem

(g : α) : Function.Surjective (g • · : β → β)

Full source

@[to_additive]
protected lemma MulAction.surjective (g : α) : Function.Surjective (g • · : β → β) :=
  (MulAction.bijective g).surjective

Surjectivity of Group Action Elements

Informal description

For any element $g$ of a group $\alpha$ acting on a set $\beta$, the function $x \mapsto g \cdot x$ from $\beta$ to $\beta$ is surjective.

smul_left_cancel theorem

(g : α) {x y : β} (h : g • x = g • y) : x = y

Full source

@[to_additive]
lemma smul_left_cancel (g : α) {x y : β} (h : g • x = g • y) : x = y := MulAction.injective g h

Left Cancellation Property for Group Actions

Informal description

For any element $g$ of a group $\alpha$ acting on a set $\beta$, and for any elements $x, y \in \beta$, if $g \cdot x = g \cdot y$, then $x = y$.

smul_left_cancel_iff theorem

(g : α) {x y : β} : g • x = g • y ↔ x = y

Full source

@[to_additive (attr := simp)]
lemma smul_left_cancel_iff (g : α) {x y : β} : g • x = g • y ↔ x = y :=
  (MulAction.injective g).eq_iff

Group Action Left Cancellation: $g \cdot x = g \cdot y \leftrightarrow x = y$

Informal description

For any element $g$ in a group $\alpha$ acting on a set $\beta$, and for any elements $x, y \in \beta$, the equality $g \cdot x = g \cdot y$ holds if and only if $x = y$.

smul_eq_iff_eq_inv_smul theorem

(g : α) {x y : β} : g • x = y ↔ x = g⁻¹ • y

Full source

@[to_additive]
lemma smul_eq_iff_eq_inv_smul (g : α) {x y : β} : g • x = y ↔ x = g⁻¹ • y :=
  (MulAction.toPerm g).apply_eq_iff_eq_symm_apply

Group Action Equivalence: $g \cdot x = y \leftrightarrow x = g^{-1} \cdot y$

Informal description

For any element $g$ in a group $\alpha$ acting on a type $\beta$, and for any elements $x, y \in \beta$, the equality $g \cdot x = y$ holds if and only if $x = g^{-1} \cdot y$.

invOf_smul_smul theorem

: ⅟ c • c • x = x

Full source

@[simp] lemma invOf_smul_smul : ⅟c • c • x = x := inv_smul_smul (unitOfInvertible c) _

Inverse Action Cancellation: $⅟ c \cdot (c \cdot x) = x$

Informal description

For any invertible element $c$ in a monoid acting on a type, and for any element $x$ in that type, the action of the inverse of $c$ followed by the action of $c$ on $x$ returns $x$, i.e., $⅟ c \cdot (c \cdot x) = x$.

smul_invOf_smul theorem

: c • (⅟ c • x) = x

Full source

@[simp] lemma smul_invOf_smul : c • (⅟ c • x) = x := smul_inv_smul (unitOfInvertible c) _

Action-Inverse Action Cancellation: $c \cdot (⅟ c \cdot x) = x$

Informal description

For any invertible element $c$ in a monoid acting on a type, and for any element $x$ in that type, the action of $c$ followed by the action of the inverse of $c$ on $x$ returns $x$, i.e., $c \cdot (⅟ c \cdot x) = x$.

invOf_smul_eq_iff theorem

: ⅟ c • x = y ↔ x = c • y

Full source

lemma invOf_smul_eq_iff : ⅟c⅟c • x = y ↔ x = c • y := inv_smul_eq_iff (g := unitOfInvertible c)

Equivalence of Inverse Action: $\text{⅟}c \cdot x = y \leftrightarrow x = c \cdot y$

Informal description

For an invertible element $c$ in a monoid acting on a type $\alpha$, the action of the inverse of $c$ on an element $x$ equals $y$ if and only if $x$ equals the action of $c$ on $y$. In symbols, $\text{⅟}c \cdot x = y \leftrightarrow x = c \cdot y$.

smul_eq_iff_eq_invOf_smul theorem

: c • x = y ↔ x = ⅟ c • y

Full source

lemma smul_eq_iff_eq_invOf_smul : c • x = y ↔ x = ⅟c • y :=
  smul_eq_iff_eq_inv_smul (g := unitOfInvertible c)

Equivalence of Action and Inverse Action: $c \cdot x = y \leftrightarrow x = \text{⅟}c \cdot y$

Informal description

For an invertible element $c$ in a monoid acting on a type $\alpha$, and for any elements $x, y \in \alpha$, the equality $c \cdot x = y$ holds if and only if $x = \text{⅟}c \cdot y$.

arrowAction definition

: MulAction G (A → B)

Full source

/-- If `G` acts on `A`, then it acts also on `A → B`, by `(g • F) a = F (g⁻¹ • a)`. -/
@[to_additive (attr := simps) arrowAddAction
"If `G` acts on `A`, then it acts also on `A → B`, by `(g +ᵥ F) a = F (g⁻¹ +ᵥ a)`"]
def arrowAction : MulAction G (A → B) where
  smul g F a := F (g⁻¹ • a)
  one_smul f := by
    show (fun x => f ((1 : G)⁻¹ • x)) = f
    simp only [inv_one, one_smul]
  mul_smul x y f := by
    show (fun a => f ((x*y)⁻¹ • a)) = (fun a => f (y⁻¹ • x⁻¹ • a))
    simp only [mul_smul, mul_inv_rev]

Group action on function space via precomposition with inverse action

Informal description

Given a group $G$ acting on a type $A$, there is an induced action of $G$ on the function space $A \to B$, defined by $(g \cdot F)(a) = F(g^{-1} \cdot a)$ for any $g \in G$, $F \colon A \to B$, and $a \in A$.

arrowMulDistribMulAction definition

: MulDistribMulAction G (A → M)

Full source

/-- When `M` is a monoid, `ArrowAction` is additionally a `MulDistribMulAction`. -/
def arrowMulDistribMulAction : MulDistribMulAction G (A → M) where
  smul_one _ := rfl
  smul_mul _ _ _ := rfl

Multiplicative distributive action on function space

Informal description

Given a monoid $M$ acting on a type $A$, the induced action of $M$ on the function space $A \to M$ is a multiplicative distributive action, meaning it preserves the multiplicative structure of $M$ when acting on functions. Specifically, for any $g \in M$ and functions $f_1, f_2 \colon A \to M$, the action satisfies $(g \cdot (f_1 \cdot f_2))(a) = (g \cdot f_1)(a) \cdot (g \cdot f_2)(a)$ for all $a \in A$, and $(g \cdot 1)(a) = 1$ where $1$ is the constant function returning the multiplicative identity of $M$.

IsUnit.smul_bijective theorem

{m : α} (hm : IsUnit m) : Function.Bijective (fun (a : β) ↦ m • a)

Full source

@[to_additive]
theorem smul_bijective {m : α} (hm : IsUnit m) :
    Function.Bijective (fun (a : β) ↦ m • a) := by
  lift m to αˣ using hm
  exact MulAction.bijective m

Bijectivity of Scalar Multiplication by a Unit Element

Informal description

For any element $m$ of a monoid $\alpha$ that is a unit (i.e., invertible), the function $a \mapsto m \cdot a$ from $\beta$ to $\beta$ is bijective, where $\beta$ is a type with a multiplicative action by $\alpha$.

IsUnit.smul_left_cancel theorem

{a : α} (ha : IsUnit a) {x y : β} : a • x = a • y ↔ x = y

Full source

@[to_additive]
lemma smul_left_cancel {a : α} (ha : IsUnit a) {x y : β} : a • x = a • y ↔ x = y :=
  let ⟨u, hu⟩ := ha
  hu ▸ smul_left_cancel_iff u

Left Cancellation Property for Scalar Multiplication by a Unit: $a \cdot x = a \cdot y \leftrightarrow x = y$

Informal description

For any element $a$ in a monoid $\alpha$ that is a unit (i.e., invertible), and for any elements $x, y$ in a type $\beta$ with a multiplicative action by $\alpha$, the equality $a \cdot x = a \cdot y$ holds if and only if $x = y$.

isUnit_smul_iff theorem

(g : α) (m : β) : IsUnit (g • m) ↔ IsUnit m

Full source

@[simp] lemma isUnit_smul_iff (g : α) (m : β) : IsUnitIsUnit (g • m) ↔ IsUnit m :=
  ⟨fun h => inv_smul_smul g m ▸ h.smul g⁻¹, IsUnit.smul g⟩

Equivalence of Unit Properties under Group Action: $g \cdot m$ is a unit $\leftrightarrow$ $m$ is a unit

Informal description

For any element $g$ in a group $\alpha$ and any element $m$ in a monoid $\beta$ with a multiplicative action of $\alpha$, the scalar multiple $g \cdot m$ is a unit in $\beta$ if and only if $m$ is a unit in $\beta$.

MulAction.toFun definition

: α ↪ M → α

Full source

/-- Embedding of `α` into functions `M → α` induced by a multiplicative action of `M` on `α`. -/
@[to_additive
"Embedding of `α` into functions `M → α` induced by an additive action of `M` on `α`."]
def toFun : α ↪ M → α :=
  ⟨fun y x ↦ x • y, fun y₁ y₂ H ↦ one_smul M y₁ ▸ one_smul M y₂ ▸ by convert congr_fun H 1⟩

Embedding induced by a multiplicative action

Informal description

Given a multiplicative action of a monoid $ M $ on a type $ \alpha $, the function maps an element $ y \in \alpha $ to the function $ x \mapsto x \bullet y $ from $ M $ to $ \alpha $. This mapping is injective.

MulAction.toFun_apply theorem

(x : M) (y : α) : MulAction.toFun M α y x = x • y

Full source

@[to_additive (attr := simp)]
lemma toFun_apply (x : M) (y : α) : MulAction.toFun M α y x = x • y := rfl

Action Function Evaluation: $\text{toFun}(y)(x) = x \bullet y$

Informal description

For any element $x$ in a monoid $M$ and any element $y$ in a type $\alpha$ with a multiplicative action of $M$, the function `MulAction.toFun` satisfies $\text{toFun}(y)(x) = x \bullet y$.

Function.Injective.mulDistribMulAction abbrev

 [Monoid B] [SMul M B] (f : B →* A) (hf : Injective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
  MulDistribMulAction M B

Full source

/-- Pullback a multiplicative distributive multiplicative action along an injective monoid
homomorphism. -/
-- See note [reducible non-instances]
protected abbrev Function.Injective.mulDistribMulAction [Monoid B] [SMul M B] (f : B →* A)
    (hf : Injective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulDistribMulAction M B where
  __ := hf.mulAction f smul
  smul_mul c x y := hf <| by simp only [smul, f.map_mul, smul_mul']
  smul_one c := hf <| by simp only [smul, f.map_one, smul_one]

Pullback of Distributive Multiplicative Action Along an Injective Homomorphism

Informal description

Let $M$ be a monoid acting distributively on a monoid $A$ via a multiplicative action, and let $B$ be another monoid with a multiplicative action of $M$. Given an injective monoid homomorphism $f \colon B \to A$ such that for all $c \in M$ and $x \in B$, $f(c \cdot x) = c \cdot f(x)$, then $M$ acts distributively on $B$ via the induced action.

Function.Surjective.mulDistribMulAction abbrev

 [Monoid B] [SMul M B] (f : A →* B) (hf : Surjective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
  MulDistribMulAction M B

Full source

/-- Pushforward a multiplicative distributive multiplicative action along a surjective monoid
homomorphism. -/
-- See note [reducible non-instances]
protected abbrev Function.Surjective.mulDistribMulAction [Monoid B] [SMul M B] (f : A →* B)
    (hf : Surjective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulDistribMulAction M B where
  __ := hf.mulAction f smul
  smul_mul c := by simp only [hf.forall, smul_mul', ← smul, ← f.map_mul, implies_true]
  smul_one c := by rw [← f.map_one, ← smul, smul_one]

Pushforward of Distributive Multiplicative Action Along a Surjective Homomorphism

Informal description

Let $M$ be a monoid acting distributively on a monoid $A$ via a multiplicative action, and let $B$ be another monoid with a multiplicative action of $M$. Given a surjective monoid homomorphism $f \colon A \to B$ such that for all $c \in M$ and $x \in A$, $f(c \cdot x) = c \cdot f(x)$, then $M$ acts distributively on $B$ via the induced action.

MulDistribMulAction.toMonoidHom definition

(r : M) : A →* A

Full source

/-- Scalar multiplication by `r` as a `MonoidHom`. -/
@[simps] def MulDistribMulAction.toMonoidHom (r : M) : A →* A where
  toFun := (r • ·)
  map_one' := smul_one r
  map_mul' := smul_mul' r

Monoid homomorphism induced by scalar multiplication

Informal description

For a monoid $M$ acting distributively on a monoid $A$, the scalar multiplication by an element $r \in M$ defines a monoid homomorphism from $A$ to itself. This homomorphism maps the identity element of $A$ to itself and preserves the multiplication operation in $A$.

smul_pow' theorem

(r : M) (x : A) (n : ℕ) : r • x ^ n = (r • x) ^ n

Full source

@[simp] lemma smul_pow' (r : M) (x : A) (n : ℕ) : r • x ^ n = (r • x) ^ n :=
  (MulDistribMulAction.toMonoidHom _ _).map_pow _ _

Distributive Action Preserves Powers: $r \cdot (x^n) = (r \cdot x)^n$

Informal description

Let $M$ be a monoid acting distributively on a monoid $A$. For any element $r \in M$, any element $x \in A$, and any natural number $n$, the action of $r$ on $x^n$ equals the $n$-th power of the action of $r$ on $x$, i.e., $r \cdot (x^n) = (r \cdot x)^n$.

MulDistribMulAction.toMonoidEnd definition

: M →* Monoid.End A

Full source

/-- Each element of the monoid defines a monoid homomorphism. -/
@[simps]
def MulDistribMulAction.toMonoidEnd : M →* Monoid.End A where
  toFun := MulDistribMulAction.toMonoidHom A
  map_one' := MonoidHom.ext <| one_smul M
  map_mul' x y := MonoidHom.ext <| mul_smul x y

Monoid homomorphism from $M$ to endomorphisms of $A$ induced by distributive multiplicative action

Informal description

Given a monoid $M$ acting distributively on a monoid $A$, the map sending each element $r \in M$ to the corresponding monoid endomorphism of $A$ (induced by scalar multiplication) is itself a monoid homomorphism from $M$ to the monoid of endomorphisms of $A$.

smul_inv' theorem

(r : M) (x : A) : r • x⁻¹ = (r • x)⁻¹

Full source

@[simp] lemma smul_inv' (r : M) (x : A) : r • x⁻¹ = (r • x)⁻¹ :=
  (MulDistribMulAction.toMonoidHom A r).map_inv x

Distributive Action Preserves Inverses: $r \cdot x^{-1} = (r \cdot x)^{-1}$

Informal description

Let $M$ be a monoid acting distributively on a group $A$. For any element $r \in M$ and any element $x \in A$, the action of $r$ on the inverse $x^{-1}$ equals the inverse of the action of $r$ on $x$, i.e., $r \cdot x^{-1} = (r \cdot x)^{-1}$.

smul_div' theorem

(r : M) (x y : A) : r • (x / y) = r • x / r • y

Full source

lemma smul_div' (r : M) (x y : A) : r • (x / y) = r • x / r • y :=
  map_div (MulDistribMulAction.toMonoidHom A r) x y

Distributive action preserves division: $r \cdot (x / y) = (r \cdot x) / (r \cdot y)$

Informal description

Let $M$ be a monoid acting distributively on a monoid $A$. For any $r \in M$ and any $x, y \in A$, the action of $r$ on the quotient $x / y$ is equal to the quotient of the actions of $r$ on $x$ and $y$, i.e., $r \cdot (x / y) = (r \cdot x) / (r \cdot y)$.