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 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
See also Monoid.toMulAction and MulZeroClass.toSMulWithZero.
Equations
- Mul.toSMul α = { smul := fun (x1 x2 : α) => x1 * x2 }
See also AddMonoid.toAddAction
Equations
- Add.toVAdd α = { vadd := fun (x1 x2 : α) => x1 + x2 }
Like Mul.toSMul, but multiplies on the right.
See also Monoid.toOppositeMulAction and MonoidWithZero.toOppositeMulActionWithZero.
Equations
- Mul.toSMulMulOpposite α = { smul := fun (a : αᵐᵒᵖ) (b : α) => b * MulOpposite.unop a }
Like Add.toVAdd, but adds on the right.
See also AddMonoid.toOppositeAddAction.
Equations
- Add.toVAddAddOpposite α = { vadd := fun (a : αᵃᵒᵖ) (b : α) => b + AddOpposite.unop a }
Type class for additive monoid actions on types, with notation g +ᵥ p.
The AddAction G P typeclass says that the additive monoid G acts additively on a type P.
More precisely this means that the action satisfies the two axioms 0 +ᵥ p = p and
(g₁ + g₂) +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p). A mathematician might simply say that the additive monoid G
acts on P.
For example, if A is an additive group and X is a type, if a mathematician says
say "let A act on the set X" they will usually mean [AddAction A X].
- vadd : G → P → P
Zero is a neutral element for
+ᵥAssociativity of
+and+ᵥ
Instances
Type class for monoid actions on types, with notation g • p.
The MulAction G P typeclass says that the monoid G acts multiplicatively on a type P.
More precisely this means that the action satisfies the two axioms 1 • p = p and
(g₁ * g₂) • p = g₁ • (g₂ • p). A mathematician might simply say that the monoid G
acts on P.
For example, if G is a group and X is a type, if a mathematician says
say "let G act on the set X" they will probably mean [AddAction G X].
- smul : α → β → β
One is the neutral element for
•Associativity of
•and*
Instances
Scalar tower and commuting actions #
Frequently, we find ourselves wanting to express a bilinear map M →ₗ[R] N →ₗ[R] P or an
equivalence between maps (M →ₗ[R] N) ≃ₗ[R] (M' →ₗ[R] N') where the maps have an associated ring
R. Unfortunately, using definitions like these requires that R satisfy CommSemiring R, and
not just Semiring R. Using M →ₗ[R] N →+ P and (M →ₗ[R] N) ≃+ (M' →ₗ[R] N') avoids this
problem, but throws away structure that is useful for when we do have a commutative (semi)ring.
To avoid making this compromise, we instead state these definitions as M →ₗ[R] N →ₗ[S] P or
(M →ₗ[R] N) ≃ₗ[S] (M' →ₗ[R] N') and require SMulCommClass S R on the appropriate modules. When
the caller has CommSemiring R, they can set S = R and smulCommClass_self will populate the
instance. If the caller only has Semiring R they can still set either R = ℕ or S = ℕ, and
AddCommMonoid.nat_smulCommClass or AddCommMonoid.nat_smulCommClass' will populate
the typeclass, which is still sufficient to recover a ≃+ or →+ structure.
An example of where this is used is LinearMap.prod_equiv.
Instances For
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.
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.
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
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 +ᵥ.
The right and left actions of
Monαare equal.
Instances
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 •.
The right and left actions of
Monαare equal.
Instances
Auxiliary definition for SMul.comp, MulAction.compHom,
DistribMulAction.compHom, Module.compHom, etc.
Equations
- SMul.comp.smul g n a = g n • a
Instances For
Auxiliary definition for VAdd.comp, AddAction.compHom, etc.
Equations
- VAdd.comp.vadd g n a = g n +ᵥ a
Instances For
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.
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.
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.
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 α β.
Note that the IsScalarTower α β β and SMulCommClass α β β typeclass arguments are usually
satisfied by Algebra α β.
Alias of smul_mul_smul_comm.
Note that the IsScalarTower α β β and SMulCommClass α β β typeclass arguments are usually
satisfied by Algebra α β.
Note that the IsScalarTower α β β and SMulCommClass α β β typeclass arguments are usually
satisfied by Algebra α β.
Pullback a multiplicative action along an injective map respecting •.
See note [reducible non-instances].
Equations
- Function.Injective.mulAction f hf smul = { smul := fun (x1 : M) (x2 : β) => x1 • x2, one_smul := ⋯, mul_smul := ⋯ }
Instances For
Pullback an additive action along an injective map respecting +ᵥ.
Equations
- Function.Injective.addAction f hf smul = { vadd := fun (x1 : M) (x2 : β) => x1 +ᵥ x2, zero_vadd := ⋯, add_vadd := ⋯ }
Instances For
Pushforward a multiplicative action along a surjective map respecting •.
See note [reducible non-instances].
Equations
- Function.Surjective.mulAction f hf smul = { smul := fun (x1 : M) (x2 : β) => x1 • x2, one_smul := ⋯, mul_smul := ⋯ }
Instances For
Pushforward an additive action along a surjective map respecting +ᵥ.
Equations
- Function.Surjective.addAction f hf smul = { vadd := fun (x1 : M) (x2 : β) => x1 +ᵥ x2, zero_vadd := ⋯, add_vadd := ⋯ }
Instances For
The regular action of a monoid on itself by left multiplication.
This is promoted to a module by Semiring.toModule.
Equations
- Monoid.toMulAction M = { smul := fun (x1 x2 : M) => x1 * x2, one_smul := ⋯, mul_smul := ⋯ }
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 = { vadd := fun (x1 x2 : M) => x1 + x2, zero_vadd := ⋯, add_vadd := ⋯ }
Let Q / P / N / M be a tower. If P / N / M, Q / P / M and Q / P / N are
scalar towers, then Q / N / M is also a scalar tower.
Let Q / P / N / M be a tower. If P / N / M, Q / N / M and Q / P / N are
scalar towers, then Q / P / M is also a scalar tower.
Let Q / P / N / M be a tower. If P / N / M, Q / N / M and Q / P / M are
scalar towers, then Q / P / N is also a scalar tower.
Typeclass for multiplicative actions on multiplicative structures.
The key axiom here is smul_mul : g • (x * y) = (g • x) * (g • y).
If G is a group (with group law multiplication) and Γ is its automorphism
group then there is a natural instance of MulDistribMulAction Γ G.
The axiom is also satisfied by a Galois group $Gal(L/K)$ acting on the field L,
but here you can use the even stronger class MulSemiringAction, which captures
how the action plays with both multiplication and addition.
- smul : M → N → N
Distributivity of
•across*Multiplying
1by a scalar gives1
Instances
A vector addition is cancellative if it is pointwise injective on the left and right.
Instances
A scalar multiplication is cancellative if it is pointwise injective on the left and right.