More lemmas about group actions #
This file contains lemmas about group actions that require more imports than
Mathlib.Algebra.Group.Action.Defs
offers.
Given an action of a group α
on β
, each g : α
defines a permutation of β
.
Equations
Instances For
Given an action of an additive group α
on β
, each g : α
defines a permutation of β
.
Equations
Instances For
MulAction.toPerm
is injective on faithful actions.
AddAction.toPerm
is injective on faithful actions.
If G
acts on A
, then it acts also on A → B
, by (g • F) a = F (g⁻¹ • a)
.
Equations
Instances For
If G
acts on A
, then it acts also on A → B
, by (g +ᵥ F) a = F (g⁻¹ +ᵥ a)
Equations
Instances For
When M
is a monoid, ArrowAction
is additionally a MulDistribMulAction
.
Equations
- arrowMulDistribMulAction = { toMulAction := arrowAction, smul_mul := ⋯, smul_one := ⋯ }
Instances For
Alias of IsAddUnit.vadd_bijective
.
Alias of IsUnit.smul_bijective
.
Pullback a multiplicative distributive multiplicative action along an injective monoid homomorphism.
Equations
- Function.Injective.mulDistribMulAction f hf smul = { toMulAction := Function.Injective.mulAction (⇑f) hf smul, smul_mul := ⋯, smul_one := ⋯ }
Instances For
Pushforward a multiplicative distributive multiplicative action along a surjective monoid homomorphism.
Equations
- Function.Surjective.mulDistribMulAction f hf smul = { toMulAction := Function.Surjective.mulAction (⇑f) hf smul, smul_mul := ⋯, smul_one := ⋯ }
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' := ⋯ }