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
Multiplying 0
by a scalar gives 0
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 ⋯
Instances For
Pushforward a zero-preserving scalar multiplication along a zero-preserving map. See note [reducible non-instances].
Equations
- f.smulZeroClass smul = SMulZeroClass.mk ⋯
Instances For
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 ⋯
Instances For
Compose a SMulZeroClass
with a function, with scalar multiplication f r' • m
.
See note [reducible non-instances].
Equations
Instances For
Each element of the scalars defines a zero-preserving map.
Equations
- SMulZeroClass.toZeroHom A x = { toFun := fun (x_1 : A) => x • x_1, map_zero' := ⋯ }
Instances For
Typeclass for scalar multiplication that preserves 0
and +
on the right.
This is exactly DistribMulAction
without the MulAction
part.
- smul : M → A → A
Scalar multiplication distributes across addition
Instances
Scalar multiplication distributes across addition
Equations
- AddMonoidHom.smulZeroClass = SMulZeroClass.mk ⋯
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 ⋯
Instances For
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 := (↑f).smulZeroClass smul; DistribSMul.mk ⋯
Instances For
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 ⋯
Instances For
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 ⋯
Instances For
Each element of the scalars defines an additive monoid homomorphism.
Equations
- DistribSMul.toAddMonoidHom A x = let __src := SMulZeroClass.toZeroHom A x; { toFun := (fun (x : M) (x_1 : A) => x • x_1) x, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Typeclass for multiplicative actions on additive structures. This generalizes group modules.
- smul : M → A → A
Multiplying
0
by a scalar gives0
Scalar multiplication distributes across addition
Instances
Multiplying 0
by a scalar gives 0
Equations
- DistribMulAction.toDistribSMul = let __src := inst; DistribSMul.mk ⋯
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
- Function.Injective.distribMulAction f hf smul = let __src := Function.Injective.distribSMul f hf smul; let __src_1 := Function.Injective.mulAction (⇑f) hf smul; DistribMulAction.mk ⋯ ⋯
Instances For
Pushforward a distributive multiplicative action along a surjective additive monoid homomorphism. See note [reducible non-instances].
Equations
- Function.Surjective.distribMulAction f hf smul = let __src := Function.Surjective.distribSMul f hf smul; let __src_1 := Function.Surjective.mulAction (⇑f) hf smul; DistribMulAction.mk ⋯ ⋯
Instances For
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.
Instances For
Compose a DistribMulAction
with a MonoidHom
, with action f r' • m
.
See note [reducible non-instances].
Equations
- DistribMulAction.compHom A f = let __src := DistribSMul.compFun A ⇑f; let __src_1 := MulAction.compHom A f; DistribMulAction.mk ⋯ ⋯
Instances For
Each element of the monoid defines an additive monoid homomorphism.
Equations
Instances For
Each element of the monoid defines an additive monoid homomorphism.
Equations
- DistribMulAction.toAddMonoidEnd M A = { toFun := DistribMulAction.toAddMonoidHom A, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Typeclass for multiplicative actions on multiplicative structures. This generalizes conjugation actions.
- smul : M → A → A
Distributivity of
•
across*
Multiplying
1
by a scalar gives1
Instances
Multiplying 1
by a scalar gives 1
Pullback a multiplicative distributive multiplicative action along an injective monoid homomorphism. See note [reducible non-instances].
Equations
- Function.Injective.mulDistribMulAction f hf smul = let __src := Function.Injective.mulAction (⇑f) hf smul; MulDistribMulAction.mk ⋯ ⋯
Instances For
Pushforward a multiplicative distributive multiplicative action along a surjective monoid homomorphism. See note [reducible non-instances].
Equations
- Function.Surjective.mulDistribMulAction f hf smul = let __src := Function.Surjective.mulAction (⇑f) hf smul; MulDistribMulAction.mk ⋯ ⋯
Instances For
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 ⋯ ⋯
Instances For
Scalar multiplication by r
as a MonoidHom
.
Equations
- MulDistribMulAction.toMonoidHom A r = { toFun := fun (x : A) => r • x, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Each element of the monoid defines a monoid homomorphism.
Equations
- MulDistribMulAction.toMonoidEnd M A = { toFun := MulDistribMulAction.toMonoidHom A, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The tautological action by AddMonoid.End α
on α
.
This generalizes Function.End.applyMulAction
.
Equations
- AddMonoid.End.applyDistribMulAction = DistribMulAction.mk ⋯ ⋯
AddMonoid.End.applyDistribMulAction
is faithful.
Equations
- ⋯ = ⋯