Definitions of group actions #
This file defines a hierarchy of group action type-classes on top of the previously defined
notation classes SMul
and its additive version VAdd
:
MulAction M α
and its additive versionAddAction G P
are typeclasses used for actions of multiplicative and additive monoids and groups; they extend notation classesSMul
andVAdd
that are defined inAlgebra.Group.Defs
;DistribMulAction M A
is a typeclass for an action of a multiplicative monoid on an additive monoid such thata • (b + c) = a • b + a • c
anda • 0 = 0
.
The hierarchy is extended further by Module
, defined elsewhere.
Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the interaction of different group actions,
SMulCommClass M N α
and its additive versionVAddCommClass M N α
;IsScalarTower M N α
and its additive versionVAddAssocClass M N α
;IsCentralScalar M α
and its additive versionIsCentralVAdd M N α
.
Notation #
Implementation details #
This file should avoid depending on other parts of GroupTheory
, to avoid import cycles.
More sophisticated lemmas belong in GroupTheory.GroupAction
.
Tags #
group action
Faithful actions #
Two elements g₁
and g₂
are equal whenever they act in the same way on all points.
Two elements m₁
and m₂
are equal whenever they act in the same way on all points.
See also AddMonoid.toAddAction
Equations
- Add.toVAdd α = { vadd := fun (x x_1 : α) => x + x_1 }
See also Monoid.toMulAction
and MulZeroClass.toSMulWithZero
.
Equations
- Mul.toSMul α = { smul := fun (x x_1 : α) => x * x_1 }
AddMonoid.toAddAction
is faithful on additive cancellative monoids.
Equations
- ⋯ = ⋯
Monoid.toMulAction
is faithful on cancellative monoids.
Equations
- ⋯ = ⋯
Type class for additive monoid actions.
- vadd : G → P → P
Zero is a neutral element for
+ᵥ
Associativity of
+
and+ᵥ
Instances
Typeclass for multiplicative actions by monoids. This generalizes group actions.
- smul : α → β → β
One is the neutral element for
•
Associativity of
•
and*
Instances
(Pre)transitive action #
M
acts pretransitively on α
if for any x y
there is g
such that g • x = y
(or g +ᵥ x = y
for an additive action). A transitive action should furthermore have α
nonempty.
In this section we define typeclasses MulAction.IsPretransitive
and
AddAction.IsPretransitive
and provide MulAction.exists_smul_eq
/AddAction.exists_vadd_eq
,
MulAction.surjective_smul
/AddAction.surjective_vadd
as public interface to access this
property. We do not provide typeclasses *Action.IsTransitive
; users should assume
[MulAction.IsPretransitive M α] [Nonempty α]
instead.
M
acts pretransitively on α
if for any x y
there is g
such that g +ᵥ x = y
.
A transitive action should furthermore have α
nonempty.
There is
g
such thatg +ᵥ x = y
.
Instances
There is g
such that g +ᵥ x = y
.
M
acts pretransitively on α
if for any x y
there is g
such that g • x = y
.
A transitive action should furthermore have α
nonempty.
There is
g
such thatg • x = y
.
Instances
There is g
such that g • x = y
.
The regular action of a group on itself is transitive.
Equations
- ⋯ = ⋯
The regular action of a group on itself is transitive.
Equations
- ⋯ = ⋯
Scalar tower and commuting actions #
Commutativity of additive actions is a symmetric relation. This lemma can't be an instance because this would cause a loop in the instance search graph.
Commutativity of actions is a symmetric relation. This lemma can't be an instance because this would cause a loop in the instance search graph.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
An instance of VAddAssocClass M N α
states that the additive action of M
on α
is
determined by the additive actions of M
on N
and N
on α
.
Associativity of
+ᵥ
Instances
An instance of IsScalarTower M N α
states that the multiplicative
action of M
on α
is determined by the multiplicative actions of M
on N
and N
on α
.
Associativity of
•
Instances
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A typeclass indicating that the right (aka AddOpposite
) and left actions by M
on α
are
equal, that is that M
acts centrally on α
. This can be thought of as a version of commutativity
for +ᵥ
.
- op_vadd_eq_vadd : ∀ (m : M) (a : α), AddOpposite.op m +ᵥ a = m +ᵥ a
The right and left actions of
M
onα
are equal.
Instances
The right and left actions of M
on α
are equal.
A typeclass indicating that the right (aka MulOpposite
) and left actions by M
on α
are
equal, that is that M
acts centrally on α
. This can be thought of as a version of commutativity
for •
.
- op_smul_eq_smul : ∀ (m : M) (a : α), MulOpposite.op m • a = m • a
The right and left actions of
M
onα
are equal.
Instances
The right and left actions of M
on α
are equal.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Auxiliary definition for VAdd.comp
, AddAction.compHom
, etc.
Equations
- VAdd.comp.vadd g n a = g n +ᵥ a
Instances For
Auxiliary definition for SMul.comp
, MulAction.compHom
,
DistribMulAction.compHom
, Module.compHom
, etc.
Equations
- SMul.comp.smul g n a = g n • a
Instances For
Given a tower of additive actions M → α → β
, if we use SMul.comp
to pull back both of
M
's actions by a map g : N → M
, then we obtain a new tower of scalar actions N → α → β
.
This cannot be an instance because it can cause infinite loops whenever the SMul
arguments
are still metavariables.
Given a tower of scalar actions M → α → β
, if we use SMul.comp
to pull back both of M
's actions by a map g : N → M
, then we obtain a new
tower of scalar actions N → α → β
.
This cannot be an instance because it can cause infinite loops whenever the SMul
arguments
are still metavariables.
This cannot be an instance because it can cause infinite loops whenever the VAdd
arguments
are still metavariables.
This cannot be an instance because it can cause infinite loops whenever the SMul
arguments
are still metavariables.
This cannot be an instance because it can cause infinite loops whenever the VAdd
arguments
are still metavariables.
This cannot be an instance because it can cause infinite loops whenever the SMul
arguments
are still metavariables.
Note that the SMulCommClass α β β
typeclass argument is usually satisfied by Algebra α β
.
Note that the IsScalarTower α β β
typeclass argument is usually satisfied by Algebra α β
.
Note that the IsScalarTower α β β
typeclass argument is usually satisfied by Algebra α β
.
Pullback an additive action along an injective map respecting +ᵥ
.
Equations
- Function.Injective.addAction f hf smul = AddAction.mk ⋯ ⋯
Instances For
Pullback a multiplicative action along an injective map respecting •
.
See note [reducible non-instances].
Equations
- Function.Injective.mulAction f hf smul = MulAction.mk ⋯ ⋯
Instances For
Pushforward an additive action along a surjective map respecting +ᵥ
.
Equations
- Function.Surjective.addAction f hf smul = AddAction.mk ⋯ ⋯
Instances For
Pushforward a multiplicative action along a surjective map respecting •
.
See note [reducible non-instances].
Equations
- Function.Surjective.mulAction f hf smul = MulAction.mk ⋯ ⋯
Instances For
Push forward the action of R
on M
along a compatible surjective map f : R →+ S
.
Equations
- Function.Surjective.addActionLeft f hf hsmul = AddAction.mk ⋯ ⋯
Instances For
Push forward the action of R
on M
along a compatible surjective map f : R →* S
.
See also Function.Surjective.distribMulActionLeft
and Function.Surjective.moduleLeft
.
Equations
- Function.Surjective.mulActionLeft f hf hsmul = MulAction.mk ⋯ ⋯
Instances For
The regular action of a monoid on itself by left addition.
This is promoted to an AddTorsor
by addGroup_is_addTorsor
.
Equations
The regular action of a monoid on itself by left multiplication.
This is promoted to a module by Semiring.toModule
.
Equations
- Monoid.toMulAction M = MulAction.mk ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Note that the IsScalarTower M α α
and SMulCommClass M α α
typeclass arguments are
usually satisfied by Algebra M α
.
Embedding of α
into functions M → α
induced by an additive action of M
on α
.
Equations
- AddAction.toFun M α = { toFun := fun (y : α) (x : M) => x +ᵥ y, inj' := ⋯ }
Instances For
Embedding of α
into functions M → α
induced by a multiplicative action of M
on α
.
Equations
- MulAction.toFun M α = { toFun := fun (y : α) (x : M) => x • y, inj' := ⋯ }
Instances For
An additive action of M
on α
and an additive monoid homomorphism N → M
induce
an additive action of N
on α
.
See note [reducible non-instances].
Equations
- AddAction.compHom α g = AddAction.mk ⋯ ⋯
Instances For
A multiplicative action of M
on α
and a monoid homomorphism N → M
induce
a multiplicative action of N
on α
.
See note [reducible non-instances].
Equations
- MulAction.compHom α g = MulAction.mk ⋯ ⋯
Instances For
If an action is transitive, then composing this action with a surjective homomorphism gives again a transitive action.
If the additive action of M
on N
is compatible with addition on N
, then
fun x ↦ x +ᵥ 0
is an additive monoid homomorphism from M
to N
.
Equations
Instances For
If the multiplicative action of M
on N
is compatible with multiplication on N
, then
fun x ↦ x • 1
is a monoid homomorphism from M
to N
.
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- addMonoidHomEquivAddActionIsScalarTower.match_1 M N motive x h_1 = Subtype.casesOn x fun (val : AddAction M N) (property : VAddAssocClass M N N) => h_1 val property
Instances For
A monoid homomorphism between two additive monoids M and N can be equivalently specified by an additive action of M on N that is compatible with the addition on N.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A monoid homomorphism between two monoids M and N can be equivalently specified by a multiplicative action of M on N that is compatible with the multiplication on N.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The monoid of endomorphisms.
Note that this is generalized by CategoryTheory.End
to categories other than Type u
.
Equations
- Function.End α = (α → α)
Instances For
Equations
- instMonoidEnd α = Monoid.mk ⋯ ⋯ (fun (n : ℕ) (f : Function.End α) => f^[n]) ⋯ ⋯
Equations
- instInhabitedEnd α = { default := 1 }
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
Equations
- Function.End.applyMulAction = MulAction.mk ⋯ ⋯
Function.End.applyMulAction
is faithful.
Equations
- ⋯ = ⋯
The monoid hom representing a monoid action.
When M
is a group, see MulAction.toPermHom
.
Equations
Instances For
The monoid action induced by a monoid hom to Function.End α
See note [reducible non-instances].
Equations
Instances For
Equations
- Multiplicative.smul = { smul := fun (a : Multiplicative α) (x : β) => Multiplicative.toAdd a +ᵥ x }
Equations
- Additive.addAction = AddAction.mk ⋯ ⋯
Equations
- Multiplicative.mulAction = MulAction.mk ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The additive monoid hom representing an additive monoid action.
When M
is a group, see AddAction.toPermHom
.
Equations
- AddAction.toEndHom = MonoidHom.toAdditive'' MulAction.toEndHom
Instances For
The additive action induced by a hom to Additive (Function.End α)
See note [reducible non-instances].