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 Pare typeclasses used for actions of multiplicative and additive monoids and groups; they extend notation classesSMulandVAddthat are defined inAlgebra.Group.Defs;DistribMulAction M Ais a typeclass for an action of a multiplicative monoid on an additive monoid such thata • (b + c) = a • b + a • canda • 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 #
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 }
Zero is a neutral element for
+ᵥAssociativity of
+and+ᵥ
Type class for additive monoid actions.
Instances
One is the neutral element for
•Associativity of
•and*
Typeclass for multiplicative actions by monoids. This generalizes group actions.
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.
There is
gsuch thatg +ᵥ 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.
Instances
There is
gsuch thatg • 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.
Instances
Equations
- (_ : AddAction.IsPretransitive G G) = (_ : AddAction.IsPretransitive G G)
The regular action of a group on itself is transitive.
The regular action of a group on itself is transitive.
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
- (_ : VAddCommClass M M α) = (_ : VAddCommClass M M α)
Associativity of
+ᵥ
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 α.
Instances
Associativity of
•
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 α.
Instances
Equations
- (_ : VAddAssocClass α α α) = (_ : VAddAssocClass α α α)
The right and left actions of
Monαare equal.
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 +ᵥ.
Instances
The right and left actions of
Monα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 •.
Instances
Equations
- (_ : VAddCommClass Mᵃᵒᵖ N α) = (_ : VAddCommClass Mᵃᵒᵖ N α)
Equations
- (_ : VAddCommClass M Nᵃᵒᵖ α) = (_ : VAddCommClass M Nᵃᵒᵖ α)
Equations
- (_ : VAddAssocClass Mᵃᵒᵖ N α) = (_ : VAddAssocClass Mᵃᵒᵖ N α)
Equations
- (_ : VAddAssocClass M Nᵃᵒᵖ α) = (_ : VAddAssocClass M Nᵃᵒᵖ α)
Auxiliary definition for VAdd.comp, AddAction.compHom, etc.
Equations
- VAdd.comp.vadd g n a = g n +ᵥ a
Auxiliary definition for SMul.comp, MulAction.compHom,
DistribMulAction.compHom, Module.compHom, etc.
Equations
- SMul.comp.smul g n a = g n • a
An action of M on α and a function N → M induces an action of N on α.
See note [reducible non-instances]. Since this is reducible, we make sure to go via
SMul.comp.smul to prevent typeclass inference unfolding too far.
Equations
- SMul.comp α g = { smul := SMul.comp.smul g }
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 wheneverthe 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 α β.
Pullback an additive action along an injective map respecting +ᵥ.
Equations
- Function.Injective.addAction f hf smul = AddAction.mk (_ : ∀ (x : β), 0 +ᵥ x = x) (_ : ∀ (c₁ c₂ : M) (x : β), c₁ + c₂ +ᵥ x = c₁ +ᵥ (c₂ +ᵥ x))
Pullback a multiplicative action along an injective map respecting •.
See note [reducible non-instances].
Equations
- Function.Injective.mulAction f hf smul = MulAction.mk (_ : ∀ (x : β), 1 • x = x) (_ : ∀ (c₁ c₂ : M) (x : β), (c₁ * c₂) • x = c₁ • c₂ • x)
Pushforward an additive action along a surjective map respecting +ᵥ.
Equations
- Function.Surjective.addAction f hf smul = AddAction.mk (_ : ∀ (y : β), 0 +ᵥ y = y) (_ : ∀ (c₁ c₂ : M) (y : β), c₁ + c₂ +ᵥ y = c₁ +ᵥ (c₂ +ᵥ y))
Pushforward a multiplicative action along a surjective map respecting •.
See note [reducible non-instances].
Equations
- Function.Surjective.mulAction f hf smul = MulAction.mk (_ : ∀ (y : β), 1 • y = y) (_ : ∀ (c₁ c₂ : M) (y : β), (c₁ * c₂) • y = c₁ • c₂ • y)
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 (_ : ∀ (b : M), 0 +ᵥ b = b) (_ : ∀ (y₁ y₂ : S) (b : M), y₁ + y₂ +ᵥ b = y₁ +ᵥ (y₂ +ᵥ b))
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 (_ : ∀ (b : M), 1 • b = b) (_ : ∀ (y₁ y₂ : S) (b : M), (y₁ * y₂) • b = y₁ • y₂ • b)
The regular action of a monoid on itself by left addition.
This is promoted to an AddTorsor by addGroup_is_addTorsor.
Equations
- AddMonoid.toAddAction M = AddAction.mk (_ : ∀ (a : M), 0 + a = a) (_ : ∀ (a b c : M), a + b + c = a + (b + c))
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 (_ : ∀ (a : M), 1 * a = a) (_ : ∀ (a b c : M), a * b * c = a * (b * c))
Equations
- (_ : VAddAssocClass M M α) = (_ : VAddAssocClass M M α)
Note that the IsScalarTower M α α and SMulCommClass M α α typeclass arguments are
usually satisfied by Algebra M α.
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 (_ : ∀ (x : α), 0 +ᵥ x = x) (_ : ∀ (x x_1 : N) (x_2 : α), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2))
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 (_ : ∀ (x : α), 1 • x = x) (_ : ∀ (x x_1 : N) (x_2 : α), (x * x_1) • x_2 = x • x_1 • x_2)
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
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
Pullback a zero-preserving scalar multiplication along an injective zero-preserving map. See note [reducible non-instances].
Equations
- Function.Injective.smulZeroClass f hf smul = SMulZeroClass.mk (_ : ∀ (c : M), c • 0 = 0)
Pushforward a zero-preserving scalar multiplication along a zero-preserving map. See note [reducible non-instances].
Equations
- ZeroHom.smulZeroClass f smul = SMulZeroClass.mk (_ : ∀ (c : M), c • 0 = 0)
Push forward the multiplication of R on M along a compatible surjective map f : R → S.
See also Function.Surjective.distribMulActionLeft.
Equations
- Function.Surjective.smulZeroClassLeft f hf hsmul = SMulZeroClass.mk (_ : ∀ (y : S), y • 0 = 0)
Compose a SMulZeroClass with a function, with scalar multiplication f r' • m.
See note [reducible non-instances].
Equations
- SMulZeroClass.compFun A f = SMulZeroClass.mk (_ : ∀ (x : N), f x • 0 = 0)
Each element of the scalars defines a zero-preserving map.
Equations
- SMulZeroClass.toZeroHom A x = { toFun := (fun x x_1 => x • x_1) x, map_zero' := (_ : x • 0 = 0) }
Scalar multiplication distributes across addition
Typeclass for scalar multiplication that preserves 0 and + on the right.
This is exactly DistribMulAction without the MulAction part.
Instances
Pullback a distributive scalar multiplication along an injective additive monoid homomorphism. See note [reducible non-instances].
Equations
- Function.Injective.distribSMul f hf smul = let src := Function.Injective.smulZeroClass (↑f) hf smul; DistribSMul.mk (_ : ∀ (c : M) (x y : B), c • (x + y) = c • x + c • y)
Pushforward a distributive scalar multiplication along a surjective additive monoid homomorphism. See note [reducible non-instances].
Equations
- Function.Surjective.distribSMul f hf smul = let src := ZeroHom.smulZeroClass (↑f) smul; DistribSMul.mk (_ : ∀ (c : M) (x y : B), c • (x + y) = c • x + c • y)
Push forward the multiplication of R on M along a compatible surjective map f : R → S.
See also Function.Surjective.distribMulActionLeft.
Equations
- Function.Surjective.distribSMulLeft f hf hsmul = let src := Function.Surjective.smulZeroClassLeft f hf hsmul; DistribSMul.mk (_ : ∀ (y : S) (x y_1 : M), y • (x + y_1) = y • x + y • y_1)
Compose a DistribSMul with a function, with scalar multiplication f r' • m.
See note [reducible non-instances].
Equations
- DistribSMul.compFun A f = let src := SMulZeroClass.compFun A f; DistribSMul.mk (_ : ∀ (x : N) (x_1 y : A), f x • (x_1 + y) = f x • x_1 + f x • y)
Each element of the scalars defines a additive monoid homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Multiplying
0by a scalar gives0Scalar multiplication distributes across addition
Typeclass for multiplicative actions on additive structures. This generalizes group modules.
Instances
Since Lean 3 does not have definitional eta for structures, we have to make sure
that the definition of DistribMulAction.toDistribSMul was done correctly,
and the two paths from DistribMulAction to SMul are indeed definitionally equal.
Pullback a distributive multiplicative action along an injective additive monoid homomorphism. See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pushforward a distributive multiplicative action along a surjective additive monoid homomorphism. See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Push forward the action of R on M along a compatible surjective map f : R →* S.
See also Function.Surjective.mulActionLeft and Function.Surjective.moduleLeft.
Equations
- One or more equations did not get rendered due to their size.
Compose a DistribMulAction with a MonoidHom, with action f r' • m.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Each element of the monoid defines a additive monoid homomorphism.
Equations
Each element of the monoid defines an additive monoid homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Distributivity of
•across*Multiplying
1by a scalar gives1
Typeclass for multiplicative actions on multiplicative structures. This generalizes conjugation actions.
Instances
Pullback a multiplicative distributive multiplicative action along an injective monoid homomorphism. See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pushforward a multiplicative distributive multiplicative action along a surjective monoid homomorphism. See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Compose a MulDistribMulAction with a MonoidHom, with action f r' • m.
See note [reducible non-instances].
Equations
- MulDistribMulAction.compHom A f = let src := MulAction.compHom A f; MulDistribMulAction.mk (_ : ∀ (x : N) (b₁ b₂ : A), ↑f x • (b₁ * b₂) = ↑f x • b₁ * ↑f x • b₂) (_ : ∀ (x : N), ↑f x • 1 = 1)
Scalar multiplication by r as a MonoidHom.
Each element of the monoid defines a monoid homomorphism.
Equations
- One or more equations did not get rendered due to their size.
The monoid of endomorphisms.
Note that this is generalized by CategoryTheory.End to categories other than Type u.
Equations
- Function.End α = (α → α)
Equations
- instMonoidEnd α = Monoid.mk (_ : ∀ (f : Function.End α), 1 * f = 1 * f) (_ : ∀ (f : Function.End α), f * 1 = f * 1) npowRec
Equations
- instInhabitedEnd α = { default := 1 }
The tautological action by Function.End α on α.
This is generalized to bundled endomorphisms by:
Equiv.Perm.applyMulActionAddMonoid.End.applyDistribMulActionAddAut.applyDistribMulActionMulAut.applyMulDistribMulActionRingHom.applyDistribMulActionLinearEquiv.applyDistribMulActionLinearMap.applyModuleRingHom.applyMulSemiringActionAlgEquiv.applyMulSemiringAction
Function.End.applyMulAction is faithful.
The tautological action by AddMonoid.End α on α.
This generalizes Function.End.applyMulAction.
AddMonoid.End.applyDistribMulAction is faithful.
The monoid hom representing a monoid action.
When M is a group, see MulAction.toPermHom.
Equations
- One or more equations did not get rendered due to their size.
The monoid action induced by a monoid hom to Function.End α
See note [reducible non-instances].
Equations
additive, multiplicative #
The additive monoid hom representing an additive monoid action.
When M is a group, see AddAction.toPermHom.
Equations
- AddAction.toEndHom = ↑MonoidHom.toAdditive'' MulAction.toEndHom
The additive action induced by a hom to Additive (Function.End α)
See note [reducible non-instances].