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
- MulAction.toPerm a = { toFun := fun (x : β) => a • x, invFun := fun (x : β) => a⁻¹ • x, left_inv := ⋯, right_inv := ⋯ }
Given an action of an additive group α on β, each g : α defines a permutation of β.
Equations
- AddAction.toPerm a = { toFun := fun (x : β) => a +ᵥ x, invFun := fun (x : β) => -a +ᵥ x, left_inv := ⋯, right_inv := ⋯ }
theorem
MulAction.toPerm_injective
{α : Type u_5}
{β : Type u_6}
[Group α]
[MulAction α β]
[FaithfulSMul α β]
:
MulAction.toPerm is injective on faithful actions.
theorem
AddAction.toPerm_injective
{α : Type u_5}
{β : Type u_6}
[AddGroup α]
[AddAction α β]
[FaithfulVAdd α β]
:
AddAction.toPerm is injective on faithful actions.
theorem
MulAction.bijective
{α : Type u_5}
{β : Type u_6}
[Group α]
[MulAction α β]
(g : α)
:
Function.Bijective fun (x : β) => g • x
theorem
AddAction.bijective
{α : Type u_5}
{β : Type u_6}
[AddGroup α]
[AddAction α β]
(g : α)
:
Function.Bijective fun (x : β) => g +ᵥ x
theorem
MulAction.injective
{α : Type u_5}
{β : Type u_6}
[Group α]
[MulAction α β]
(g : α)
:
Function.Injective fun (x : β) => g • x
theorem
AddAction.injective
{α : Type u_5}
{β : Type u_6}
[AddGroup α]
[AddAction α β]
(g : α)
:
Function.Injective fun (x : β) => g +ᵥ x
theorem
MulAction.surjective
{α : Type u_5}
{β : Type u_6}
[Group α]
[MulAction α β]
(g : α)
:
Function.Surjective fun (x : β) => g • x
theorem
AddAction.surjective
{α : Type u_5}
{β : Type u_6}
[AddGroup α]
[AddAction α β]
(g : α)
:
Function.Surjective fun (x : β) => g +ᵥ x
def
arrowAction
{G : Type u_7}
{A : Type u_8}
{B : Type u_9}
[DivisionMonoid G]
[MulAction G A]
:
MulAction G (A → B)
If G acts on A, then it acts also on A → B, by (g • F) a = F (g⁻¹ • a).
Equations
- arrowAction = { smul := fun (g : G) (F : A → B) (a : A) => F (g⁻¹ • a), one_smul := ⋯, mul_smul := ⋯ }
def
arrowAddAction
{G : Type u_7}
{A : Type u_8}
{B : Type u_9}
[SubtractionMonoid G]
[AddAction G A]
:
AddAction G (A → B)
If G acts on A, then it acts also on A → B, by (g +ᵥ F) a = F (g⁻¹ +ᵥ a)
Equations
- arrowAddAction = { vadd := fun (g : G) (F : A → B) (a : A) => F (-g +ᵥ a), zero_vadd := ⋯, add_vadd := ⋯ }
def
arrowMulDistribMulAction
{M : Type u_2}
{G : Type u_7}
{A : Type u_8}
[DivisionMonoid G]
[MulAction G A]
[Monoid M]
:
MulDistribMulAction G (A → M)
When M is a monoid, ArrowAction is additionally a MulDistribMulAction.
Equations
- arrowMulDistribMulAction = { toMulAction := arrowAction, smul_mul := ⋯, smul_one := ⋯ }
theorem
IsUnit.smul_bijective
{α : Type u_5}
{β : Type u_6}
[Monoid α]
[MulAction α β]
{m : α}
(hm : IsUnit m)
:
Function.Bijective fun (a : β) => m • a
theorem
IsAddUnit.vadd_bijective
{α : Type u_5}
{β : Type u_6}
[AddMonoid α]
[AddAction α β]
{m : α}
(hm : IsAddUnit m)
:
Function.Bijective fun (a : β) => m +ᵥ a
@[deprecated IsAddUnit.vadd_bijective (since := "2025-03-03")]
theorem
AddAction.vadd_bijective_of_is_addUnit
{α : Type u_5}
{β : Type u_6}
[AddMonoid α]
[AddAction α β]
{m : α}
(hm : IsAddUnit m)
:
Function.Bijective fun (a : β) => m +ᵥ a
Alias of IsAddUnit.vadd_bijective.
@[deprecated IsUnit.smul_bijective (since := "2025-03-03")]
theorem
MulAction.smul_bijective_of_is_unit
{α : Type u_5}
{β : Type u_6}
[Monoid α]
[MulAction α β]
{m : α}
(hm : IsUnit m)
:
Function.Bijective fun (a : β) => m • a
Alias of IsUnit.smul_bijective.
@[simp]
theorem
isUnit_smul_iff
{α : Type u_5}
{β : Type u_6}
[Group α]
[Monoid β]
[MulAction α β]
[SMulCommClass α β β]
[IsScalarTower α β β]
(g : α)
(m : β)
:
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' := ⋯ }
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' := ⋯ }
@[reducible, inline]
abbrev
Function.Injective.mulDistribMulAction
{M : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Monoid M]
[Monoid A]
[MulDistribMulAction M A]
[Monoid B]
[SMul M B]
(f : B →* A)
(hf : Injective ⇑f)
(smul : ∀ (c : M) (x : B), f (c • x) = c • f x)
:
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 := ⋯ }
@[reducible, inline]
abbrev
Function.Surjective.mulDistribMulAction
{M : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Monoid M]
[Monoid A]
[MulDistribMulAction M A]
[Monoid B]
[SMul M B]
(f : A →* B)
(hf : Surjective ⇑f)
(smul : ∀ (c : M) (x : A), f (c • x) = c • f x)
:
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 := ⋯ }
def
MulDistribMulAction.toMonoidHom
{M : Type u_2}
(A : Type u_3)
[Monoid M]
[Monoid A]
[MulDistribMulAction M A]
(r : M)
:
Scalar multiplication by r as a MonoidHom.
Equations
- MulDistribMulAction.toMonoidHom A r = { toFun := fun (x : A) => r • x, map_one' := ⋯, map_mul' := ⋯ }
@[simp]
theorem
MulDistribMulAction.toMonoidHom_apply
{M : Type u_2}
(A : Type u_3)
[Monoid M]
[Monoid A]
[MulDistribMulAction M A]
(r : M)
(x✝ : A)
:
def
MulDistribMulAction.toMonoidEnd
(M : Type u_2)
(A : Type u_3)
[Monoid M]
[Monoid A]
[MulDistribMulAction M A]
:
Each element of the monoid defines a monoid homomorphism.
Equations
- MulDistribMulAction.toMonoidEnd M A = { toFun := MulDistribMulAction.toMonoidHom A, map_one' := ⋯, map_mul' := ⋯ }
@[simp]
theorem
MulDistribMulAction.toMonoidEnd_apply
(M : Type u_2)
(A : Type u_3)
[Monoid M]
[Monoid A]
[MulDistribMulAction M A]
(r : M)
: