Mathlib.Algebra.Group.Action.End

Function.End.applyMulAction instance

: MulAction (Function.End α) α

Full source

/-- The tautological action by `Function.End α` on `α`.

This is generalized to bundled endomorphisms by:
* `Equiv.Perm.applyMulAction`
* `AddMonoid.End.applyDistribMulAction`
* `AddMonoid.End.applyModule`
* `AddAut.applyDistribMulAction`
* `MulAut.applyMulDistribMulAction`
* `LinearEquiv.applyDistribMulAction`
* `LinearMap.applyModule`
* `RingHom.applyMulSemiringAction`
* `RingAut.applyMulSemiringAction`
* `AlgEquiv.applyMulSemiringAction`
* `RelHom.applyMulAction`
* `RelEmbedding.applyMulAction`
* `RelIso.applyMulAction`
-/
instance applyMulAction : MulAction (Function.End α) α where
  smul := (· <| ·)
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Endomorphism Action by Function Application

Informal description

The set of endomorphisms $\text{End}(\alpha)$ (functions from $\alpha$ to itself) has a natural multiplicative action on $\alpha$, where the action of $f \in \text{End}(\alpha)$ on $a \in \alpha$ is given by function application $f \cdot a = f(a)$.

Function.End.applyAddAction instance

: AddAction (Additive (Function.End α)) α

Full source

/-- The tautological additive action by `Additive (Function.End α)` on `α`. -/
instance applyAddAction : AddAction (Additive (Function.End α)) α := inferInstance

Additive Action of Endomorphisms by Function Application

Informal description

The set of endomorphisms $\text{End}(\alpha)$ (functions from $\alpha$ to itself) has a natural additive action on $\alpha$, where the action of $f \in \text{End}(\alpha)$ on $a \in \alpha$ is given by function application $f \cdot a = f(a)$.

Function.End.smul_def theorem

(f : Function.End α) (a : α) : f • a = f a

Full source

@[simp] lemma smul_def (f : Function.End α) (a : α) : f • a = f a := rfl

Scalar Action of Endomorphism Equals Function Application

Informal description

For any endomorphism $f$ of a type $\alpha$ and any element $a \in \alpha$, the scalar action of $f$ on $a$ is equal to the function application $f(a)$, i.e., $f \cdot a = f(a)$.

Function.End.mul_def theorem

(f g : Function.End α) : (f * g) = f ∘ g

Full source

lemma mul_def (f g : Function.End α) : (f * g) = f ∘ g := rfl

Composition of Endomorphisms as Multiplication

Informal description

For any endomorphisms $f$ and $g$ of a type $\alpha$, the product $f * g$ is equal to the composition $f \circ g$.

Function.End.one_def theorem

: (1 : Function.End α) = id

Full source

lemma one_def : (1 : Function.End α) = id := rfl

Identity Endomorphism is the Multiplicative Identity

Informal description

The multiplicative identity element in the monoid of endomorphisms on a type $\alpha$ is equal to the identity function $\text{id}$ on $\alpha$.

Function.End.apply_FaithfulSMul instance

: FaithfulSMul (Function.End α) α

Full source

/-- `Function.End.applyMulAction` is faithful. -/
instance apply_FaithfulSMul : FaithfulSMul (Function.End α) α where eq_of_smul_eq_smul := funext

Faithfulness of Endomorphism Action by Function Application

Informal description

The multiplicative action of the monoid of endomorphisms $\text{End}(\alpha)$ on $\alpha$ given by function application is faithful. That is, distinct endomorphisms act differently on $\alpha$.

Equiv.Perm.applyMulAction instance

(α : Type*) : MulAction (Perm α) α

Full source

/-- The tautological action by `Equiv.Perm α` on `α`.

This generalizes `Function.End.applyMulAction`. -/
instance applyMulAction (α : Type*) : MulAction (Perm α) α where
  smul f a := f a
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Permutation Action on a Type by Function Application

Informal description

For any type $\alpha$, the group of permutations $\text{Perm}(\alpha)$ acts on $\alpha$ via function application. That is, for any permutation $f \in \text{Perm}(\alpha)$ and any element $a \in \alpha$, the action $f \cdot a$ is defined as $f(a)$.

Equiv.Perm.smul_def theorem

{α : Type*} (f : Perm α) (a : α) : f • a = f a

Full source

@[simp]
protected lemma smul_def {α : Type*} (f : Perm α) (a : α) : f • a = f a := rfl

Permutation Action Equals Function Application: $f \cdot a = f(a)$

Informal description

For any type $\alpha$, permutation $f \in \text{Perm}(\alpha)$, and element $a \in \alpha$, the action of $f$ on $a$ (denoted $f \cdot a$) is equal to the function application $f(a)$.

Equiv.Perm.applyFaithfulSMul instance

(α : Type*) : FaithfulSMul (Perm α) α

Full source

/-- `Equiv.Perm.applyMulAction` is faithful. -/
instance applyFaithfulSMul (α : Type*) : FaithfulSMul (Perm α) α := ⟨Equiv.ext⟩

Faithfulness of Permutation Action on a Type

Informal description

For any type $\alpha$, the action of the permutation group $\mathrm{Perm}(\alpha)$ on $\alpha$ via function application is faithful. That is, if two permutations $f, g \in \mathrm{Perm}(\alpha)$ satisfy $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

MulAut.applyMulAction instance

: MulAction (MulAut M) M

Full source

/-- The tautological action by `MulAut M` on `M`. -/
instance applyMulAction : MulAction (MulAut M) M where
  smul := (· <| ·)
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Tautological Action of Multiplicative Automorphisms on $M$

Informal description

The multiplicative automorphism group $\mathrm{MulAut}(M)$ acts on $M$ via function application. That is, for any $f \in \mathrm{MulAut}(M)$ and $a \in M$, the action is defined by $f \cdot a = f(a)$.

MulAut.applyMulDistribMulAction instance

: MulDistribMulAction (MulAut M) M

Full source

/-- The tautological action by `MulAut M` on `M`.

This generalizes `Function.End.applyMulAction`. -/
instance applyMulDistribMulAction : MulDistribMulAction (MulAut M) M where
  smul := (· <| ·)
  one_smul _ := rfl
  mul_smul _ _ _ := rfl
  smul_one := map_one
  smul_mul := map_mul

Multiplicative Automorphisms Act as Multiplicative Distributors on $M$

Informal description

The group of multiplicative automorphisms $\mathrm{MulAut}(M)$ acts on $M$ in a way that distributes over multiplication. Specifically, for any $f \in \mathrm{MulAut}(M)$ and $a, b \in M$, we have $f \cdot (a * b) = (f \cdot a) * (f \cdot b)$.

MulAut.smul_def theorem

(f : MulAut M) (a : M) : f • a = f a

Full source

@[simp] protected lemma smul_def (f : MulAut M) (a : M) : f • a = f a := rfl

Action of Multiplicative Automorphism via Function Application: $f \cdot a = f(a)$

Informal description

For any multiplicative automorphism $f \in \mathrm{MulAut}(M)$ and any element $a \in M$, the action of $f$ on $a$ is given by function application, i.e., $f \cdot a = f(a)$.

MulAut.apply_faithfulSMul instance

: FaithfulSMul (MulAut M) M

Full source

/-- `MulAut.applyDistribMulAction` is faithful. -/
instance apply_faithfulSMul : FaithfulSMul (MulAut M) M where eq_of_smul_eq_smul := MulEquiv.ext

Faithfulness of the Tautological Action of Multiplicative Automorphisms

Informal description

The action of the group of multiplicative automorphisms $\mathrm{MulAut}(M)$ on $M$ via function application is faithful. That is, distinct automorphisms in $\mathrm{MulAut}(M)$ act differently on $M$.

AddAut.applyMulAction instance

: MulAction (AddAut M) M

Full source

/-- The tautological action by `AddAut M` on `M`. -/
instance applyMulAction : MulAction (AddAut M) M where
  smul := (· <| ·)
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Action of Additive Automorphisms on Their Base Type

Informal description

The additive automorphism group $\text{AddAut}(M)$ acts on $M$ via function application, where for any $f \in \text{AddAut}(M)$ and $a \in M$, the action is defined by $f \cdot a = f(a)$.

AddAut.smul_def theorem

(f : AddAut M) (a : M) : f • a = f a

Full source

@[simp] protected lemma smul_def (f : AddAut M) (a : M) : f • a = f a := rfl

Action of Additive Automorphism Equals Function Application

Informal description

For any additive automorphism $f$ of a type $M$ and any element $a \in M$, the action of $f$ on $a$ is equal to the application of $f$ to $a$, i.e., $f \cdot a = f(a)$.

AddAut.apply_faithfulSMul instance

: FaithfulSMul (AddAut M) M

Full source

/-- `AddAut.applyDistribMulAction` is faithful. -/
instance apply_faithfulSMul : FaithfulSMul (AddAut M) M where eq_of_smul_eq_smul := AddEquiv.ext

Faithfulness of the Additive Automorphism Action on Its Base Type

Informal description

The scalar multiplication action of the group of additive automorphisms $\text{AddAut}(M)$ on $M$ via function application is faithful. That is, distinct additive automorphisms of $M$ act differently on $M$.

MulAction.toEndHom definition

[MulAction M α] : M →* Function.End α

Full source

/-- The monoid hom representing a monoid action.

When `M` is a group, see `MulAction.toPermHom`. -/
def MulAction.toEndHom [MulAction M α] : M →* Function.End α where
  toFun := (· • ·)
  map_one' := funext (one_smul M)
  map_mul' x y := funext (mul_smul x y)

Monoid action as homomorphism to endomorphisms

Informal description

Given a monoid action of $ M $ on $ \alpha $, this defines the monoid homomorphism from $ M $ to the monoid of endomorphisms of $ \alpha $, where each element $ m \in M $ is mapped to the endomorphism $ \alpha \to \alpha $ defined by left multiplication by $ m $. The homomorphism preserves the monoid structure, mapping the identity of $ M $ to the identity endomorphism and the product of two elements to the composition of their corresponding endomorphisms.

MulAction.ofEndHom abbrev

(f : M →* Function.End α) : MulAction M α

Full source

/-- The monoid action induced by a monoid hom to `Function.End α`

See note [reducible non-instances]. -/
abbrev MulAction.ofEndHom (f : M →* Function.End α) : MulAction M α := .compHom α f

Multiplicative Action Induced by Monoid Homomorphism to Endomorphisms

Informal description

Given a monoid homomorphism $f \colon M \to \text{End}(\alpha)$, where $\text{End}(\alpha)$ denotes the monoid of endomorphisms of $\alpha$, there is an induced multiplicative action of $M$ on $\alpha$ defined by $m \cdot a = f(m)(a)$ for $m \in M$ and $a \in \alpha$.

AddAction.toEndHom definition

[AddAction M α] : M →+ Additive (Function.End α)

Full source

/-- The additive monoid hom representing an additive monoid action.

When `M` is a group, see `AddAction.toPermHom`. -/
def AddAction.toEndHom [AddAction M α] : M →+ Additive (Function.End α) :=
  MonoidHom.toAdditive'' MulAction.toEndHom

Additive monoid action as homomorphism to endomorphisms

Informal description

Given an additive monoid action of $ M $ on $ \alpha $, this defines the additive monoid homomorphism from $ M $ to the additive monoid of endomorphisms of $ \alpha $, where each element $ m \in M $ is mapped to the endomorphism $ \alpha \to \alpha $ defined by left addition by $ m $. The homomorphism preserves the additive monoid structure, mapping the zero of $ M $ to the zero endomorphism and the sum of two elements to the sum of their corresponding endomorphisms.

AddAction.ofEndHom abbrev

(f : M →+ Additive (Function.End α)) : AddAction M α

Full source

/-- The additive action induced by a hom to `Additive (Function.End α)`

See note [reducible non-instances]. -/
abbrev AddAction.ofEndHom (f : M →+ Additive (Function.End α)) : AddAction M α := .compHom α f

Additive Action Induced by Homomorphism to Endomorphisms

Informal description

Given an additive monoid homomorphism $f \colon M \to \text{End}(\alpha)$, where $\text{End}(\alpha)$ denotes the monoid of endomorphisms of $\alpha$ with addition as the operation, there is an induced additive action of $M$ on $\alpha$ defined by $m \cdot a = f(m)(a)$ for $m \in M$ and $a \in \alpha$.

MulAction.toPermHom definition

: G →* Equiv.Perm α

Full source

/-- Given an action of a group `G` on a set `α`, each `g : G` defines a permutation of `α`. -/
@[simps]
def MulAction.toPermHom : G →* Equiv.Perm α where
  toFun := MulAction.toPerm
  map_one' := Equiv.ext <| one_smul G
  map_mul' u₁ u₂ := Equiv.ext <| mul_smul (u₁ : G) u₂

Group action as permutation homomorphism

Informal description

Given a group action of $ G $ on $ \alpha $, the function $ \text{MulAction.toPermHom} $ maps each element $ g \in G $ to the permutation of $ \alpha $ defined by $ x \mapsto g \cdot x $. This function is a group homomorphism from $ G $ to the group of permutations of $ \alpha $, where the group operation on permutations is composition. The homomorphism property ensures that $ \text{MulAction.toPermHom}(g_1 g_2) = \text{MulAction.toPermHom}(g_1) \circ \text{MulAction.toPermHom}(g_2) $ for all $ g_1, g_2 \in G $, and $ \text{MulAction.toPermHom}(1) $ is the identity permutation.

AddAction.toPermHom definition

: G →+ Additive (Equiv.Perm α)

Full source

/-- Given an action of an additive group `G` on a set `α`, each `g : G` defines a permutation of
`α`. -/
@[simps!]
def AddAction.toPermHom : G →+ Additive (Equiv.Perm α) :=
  MonoidHom.toAdditive'' <| MulAction.toPermHom ..

Additive group action as permutation homomorphism

Informal description

Given an additive group action of $G$ on a set $\alpha$, the function $\text{AddAction.toPermHom}$ maps each element $g \in G$ to the permutation of $\alpha$ defined by $x \mapsto g \cdot x$. This function is an additive group homomorphism from $G$ to the additive group of permutations of $\alpha$, where the group operation on permutations is composition. The homomorphism property ensures that $\text{AddAction.toPermHom}(g_1 + g_2) = \text{AddAction.toPermHom}(g_1) \circ \text{AddAction.toPermHom}(g_2)$ for all $g_1, g_2 \in G$, and $\text{AddAction.toPermHom}(0)$ is the identity permutation.

MulDistribMulAction.toMulEquiv definition

(x : G) : M ≃* M

Full source

/-- Each element of the group defines a multiplicative monoid isomorphism.

This is a stronger version of `MulAction.toPerm`. -/
@[simps +simpRhs]
def MulDistribMulAction.toMulEquiv (x : G) : M ≃* M :=
  { MulDistribMulAction.toMonoidHom M x, MulAction.toPermHom G M x with }

Multiplicative equivalence induced by a distributive multiplicative action

Informal description

For a group $ G $ acting distributively on a monoid $ M $, each element $ x \in G $ defines a multiplicative equivalence (isomorphism) $ M \simeq M $, which is both a monoid homomorphism and a permutation of $ M $ induced by the action of $ x $.

MulDistribMulAction.toMulAut definition

: G →* MulAut M

Full source

/-- Each element of the group defines a multiplicative monoid isomorphism.

This is a stronger version of `MulAction.toPermHom`. -/
@[simps]
def MulDistribMulAction.toMulAut : G →* MulAut M where
  toFun := MulDistribMulAction.toMulEquiv M
  map_one' := MulEquiv.ext (one_smul _)
  map_mul' _ _ := MulEquiv.ext (mul_smul _ _)

Group homomorphism to multiplicative automorphisms induced by a distributive multiplicative action

Informal description

The function that maps each element $ x $ of a group $ G $ to the multiplicative automorphism $ M \simeq M $ induced by the distributive multiplicative action of $ G $ on a monoid $ M $. This function is a group homomorphism from $ G $ to the group of multiplicative automorphisms of $ M $, where the group operation is composition of automorphisms. The homomorphism property ensures that the action of the product $ x_1 x_2 $ is the composition of the actions of $ x_1 $ and $ x_2 $, and the action of the identity element is the identity automorphism.

mulAutArrow definition

: G →* MulAut (A → M)

Full source

/-- Given groups `G H` with `G` acting on `A`, `G` acts by
multiplicative automorphisms on `A → H`. -/
@[simps!] def mulAutArrow : G →* MulAut (A → M) := MulDistribMulAction.toMulAut _ _

Multiplicative automorphism action on function space

Informal description

Given groups $G$ and $H$ with $G$ acting on a type $A$, the group $G$ acts by multiplicative automorphisms on the function space $A \to H$. This means each element $g \in G$ induces a multiplicative automorphism (i.e., a bijective homomorphism preserving multiplication) on the space of functions from $A$ to $H$.

Tags