# mathlibdocumentation

group_theory.group_action

@[class]
structure has_scalar  :
Type uType vType (max u v)
• smul : α → γ → γ

Typeclass for types with a scalar multiplication operation, denoted • (\bu)

Instances
@[class]
structure mul_action (α : Type u) (β : Type v) [monoid α] :
Type (max u v)
• to_has_scalar : β
• one_smul : ∀ (b : β), 1 b = b
• mul_smul : ∀ (x y : α) (b : β), (x * y) b = x y b

Typeclass for multiplicative actions by monoids. This generalizes group actions.

Instances
theorem mul_smul {α : Type u} {β : Type v} [monoid α] [ β] (a₁ a₂ : α) (b : β) :
(a₁ * a₂) b = a₁ a₂ b

theorem smul_smul {α : Type u} {β : Type v} [monoid α] [ β] (a₁ a₂ : α) (b : β) :
a₁ a₂ b = (a₁ * a₂) b

theorem smul_comm {α : Type u} {β : Type v} [comm_monoid α] [ β] (a₁ a₂ : α) (b : β) :
a₁ a₂ b = a₂ a₁ b

@[simp]
theorem one_smul (α : Type u) {β : Type v} [monoid α] [ β] (b : β) :
1 b = b

@[simp]
theorem units.inv_smul_smul {α : Type u} {β : Type v} [monoid α] [ β] (u : units α) (x : β) :

@[simp]
theorem units.smul_inv_smul {α : Type u} {β : Type v} [monoid α] [ β] (u : units α) (x : β) :

def units.smul_perm_hom {α : Type u} {β : Type v} [monoid α] [ β] :

If a monoid α acts on β, then each u : units α defines a permutation of β.

Equations
@[simp]
theorem units.smul_left_cancel {α : Type u} {β : Type v} [monoid α] [ β] (u : units α) {x y : β} :
u x = u y x = y

theorem units.smul_eq_iff_eq_inv_smul {α : Type u} {β : Type v} [monoid α] [ β] (u : units α) {x y : β} :
u x = y x = u⁻¹ y

theorem is_unit.smul_left_cancel {α : Type u} {β : Type v} [monoid α] [ β] {a : α} (ha : is_unit a) {x y : β} :
a x = a y x = y

def function.injective.mul_action {α : Type u} {β : Type v} {γ : Type w} [monoid α] [ β] [ γ] (f : γ → β) :
(∀ (c : α) (x : γ), f (c x) = c f x) γ

Pullback a multiplicative action along an injective map respecting •.

Equations
def function.surjective.mul_action {α : Type u} {β : Type v} {γ : Type w} [monoid α] [ β] [ γ] (f : β → γ) :
(∀ (c : α) (x : β), f (c x) = c f x) γ

Pushforward a multiplicative action along a surjective map respecting •.

Equations
@[simp]
theorem inv_smul_smul' {β : Type v} {G : Type u_1} [ β] {c : G} (hc : c 0) (x : β) :
c⁻¹ c x = x

@[simp]
theorem smul_inv_smul' {β : Type v} {G : Type u_1} [ β] {c : G} (hc : c 0) (x : β) :
c c⁻¹ x = x

theorem inv_smul_eq_iff {β : Type v} {G : Type u_1} [ β] {a : G} (ha : a 0) {x y : β} :
a⁻¹ x = y x = a y

theorem eq_inv_smul_iff {β : Type v} {G : Type u_1} [ β] {a : G} (ha : a 0) {x y : β} :
x = a⁻¹ y a x = y

theorem ite_smul {α : Type u} {β : Type v} [monoid α] [ β] (p : Prop) [decidable p] (a₁ a₂ : α) (b : β) :
ite p a₁ a₂ b = ite p (a₁ b) (a₂ b)

theorem smul_ite {α : Type u} {β : Type v} [monoid α] [ β] (p : Prop) [decidable p] (a : α) (b₁ b₂ : β) :
a ite p b₁ b₂ = ite p (a b₁) (a b₂)

@[class]
structure is_scalar_tower (R : Type u_1) (M : Type u_2) (N : Type u_3) [ M] [ N] [ N] :
Prop
• smul_assoc : ∀ (x : R) (y : M) (z : N), (x y) z = x y z

An instance of is_scalar_tower R M N states that the multiplicative action of R on N is determined by the multiplicative actions of R on M and M on N.

Instances
@[simp]
theorem smul_assoc {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] [ N] [ N] (x : R) (y : M) (z : N) :
(x y) z = x y z

def mul_action.regular (α : Type u) [monoid α] :
α

The regular action of a monoid on itself by left multiplication.

Equations
@[instance]
def mul_action.is_scalar_tower.left (α : Type u) {β : Type v} [monoid α] [ β] :
β

def mul_action.orbit (α : Type u) {β : Type v} [monoid α] [ β] :
β → set β

The orbit of an element under an action.

Equations
theorem mul_action.mem_orbit_iff {α : Type u} {β : Type v} [monoid α] [ β] {b₁ b₂ : β} :
b₂ b₁ ∃ (x : α), x b₁ = b₂

@[simp]
theorem mul_action.mem_orbit {α : Type u} {β : Type v} [monoid α] [ β] (b : β) (x : α) :
x b

@[simp]
theorem mul_action.mem_orbit_self {α : Type u} {β : Type v} [monoid α] [ β] (b : β) :
b

def mul_action.stabilizer_carrier (α : Type u) {β : Type v} [monoid α] [ β] :
β → set α

The stabilizer of an element under an action, i.e. what sends the element to itself. Note that this is a set: for the group stabilizer see stabilizer.

Equations
• = {x : α | x b = b}
@[simp]
theorem mul_action.mem_stabilizer_iff {α : Type u} {β : Type v} [monoid α] [ β] {b : β} {x : α} :
x b = b

def mul_action.fixed_points (α : Type u) (β : Type v) [monoid α] [ β] :
set β

The set of elements fixed under the whole action.

Equations
• = {b : β | ∀ (x : α), x b = b}
def mul_action.fixed_by (α : Type u) (β : Type v) [monoid α] [ β] :
α → set β

fixed_by g is the subfield of elements fixed by g.

Equations
• g = {x : β | g x = x}
theorem mul_action.fixed_eq_Inter_fixed_by (α : Type u) (β : Type v) [monoid α] [ β] :
= ⋂ (g : α), g

@[simp]
theorem mul_action.mem_fixed_points {α : Type u} (β : Type v) [monoid α] [ β] {b : β} :
∀ (x : α), x b = b

@[simp]
theorem mul_action.mem_fixed_by {α : Type u} (β : Type v) [monoid α] [ β] {g : α} {b : β} :
b g g b = b

theorem mul_action.mem_fixed_points' {α : Type u} (β : Type v) [monoid α] [ β] {b : β} :
∀ (b' : β), b' b' = b

def mul_action.comp_hom {α : Type u} (β : Type v) {γ : Type w} [monoid α] [ β] [monoid γ] :
→* α) β

An action of α on β and a monoid homomorphism γ → α induce an action of γ on β.

Equations
def mul_action.stabilizer.submonoid (α : Type u) {β : Type v} [monoid α] [ β] :
β →

The stabilizer of a point b as a submonoid of α.

Equations
def mul_action.to_fun (α : Type u) (β : Type v) [monoid α] [ β] :
β α → β

Embedding induced by action.

Equations
@[simp]
theorem mul_action.to_fun_apply {α : Type u} {β : Type v} [monoid α] [ β] (x : α) (y : β) :
β) y x = x y

@[simp]
theorem mul_action.inv_smul_smul {α : Type u} {β : Type v} [group α] [ β] (c : α) (x : β) :
c⁻¹ c x = x

@[simp]
theorem mul_action.smul_inv_smul {α : Type u} {β : Type v} [group α] [ β] (c : α) (x : β) :
c c⁻¹ x = x

theorem mul_action.inv_smul_eq_iff {α : Type u} {β : Type v} [group α] [ β] {a : α} {x y : β} :
a⁻¹ x = y x = a y

theorem mul_action.eq_inv_smul_iff {α : Type u} {β : Type v} [group α] [ β] {a : α} {x y : β} :
x = a⁻¹ y a x = y

def mul_action.stabilizer (α : Type u) {β : Type v} [group α] [ β] :
β →

The stabilizer of an element under an action, i.e. what sends the element to itself. A subgroup.

Equations
def mul_action.to_perm (α : Type u) (β : Type v) [group α] [ β] :
α →*

Given an action of a group α on a set β, each g : α defines a permutation of β.

Equations
theorem mul_action.bijective {α : Type u} {β : Type v} [group α] [ β] (g : α) :
function.bijective (λ (b : β), g b)

theorem mul_action.orbit_eq_iff {α : Type u} {β : Type v} [group α] [ β] {a b : β} :
a

def mul_action.stabilizer.subgroup (α : Type u) {β : Type v} [group α] [ β] :
β →

The stabilizer of a point b as a subgroup of α.

Equations
@[simp]
theorem mul_action.mem_orbit_smul (α : Type u) {β : Type v} [group α] [ β] (g : α) (a : β) :
a (g a)

@[simp]
theorem mul_action.smul_mem_orbit_smul (α : Type u) {β : Type v} [group α] [ β] (g h : α) (a : β) :
g a (h a)

def mul_action.orbit_rel (α : Type u) (β : Type v) [group α] [ β] :

The relation "in the same orbit".

Equations
def mul_action.mul_left_cosets {α : Type u} [group α] (H : subgroup α) :

Action on left cosets.

Equations
@[instance]
def mul_action.mul_action {α : Type u} [group α] (H : subgroup α) :

Equations
@[instance]
def mul_action.mul_left_cosets_comp_subtype_val {α : Type u} [group α] (H I : subgroup α) :

Equations
def mul_action.of_quotient_stabilizer (α : Type u) {β : Type v} [group α] [ β] (x : β) :

The canonical map from the quotient of the stabilizer to the set.

Equations
• = (λ (_x : α), _x x) _
@[simp]
theorem mul_action.of_quotient_stabilizer_mk (α : Type u) {β : Type v} [group α] [ β] (x : β) (g : α) :
= g x

theorem mul_action.of_quotient_stabilizer_mem_orbit (α : Type u) {β : Type v} [group α] [ β] (x : β) (g : quotient_group.quotient ) :

theorem mul_action.of_quotient_stabilizer_smul (α : Type u) {β : Type v} [group α] [ β] (x : β) (g : α) (g' : quotient_group.quotient ) :
(g g') =

theorem mul_action.injective_of_quotient_stabilizer (α : Type u) {β : Type v} [group α] [ β] (x : β) :

def mul_action.orbit_equiv_quotient_stabilizer (α : Type u) {β : Type v} [group α] [ β] (b : β) :

Orbit-stabilizer theorem.

Equations
@[simp]
theorem mul_action.orbit_equiv_quotient_stabilizer_symm_apply (α : Type u) {β : Type v} [group α] [ β] (b : β) (a : α) :
a) = a b

@[class]
structure distrib_mul_action (α : Type u) (β : Type v) [monoid α] [add_monoid β] :
Type (max u v)
• to_mul_action : β
• smul_add : ∀ (r : α) (x y : β), r (x + y) = r x + r y
• smul_zero : ∀ (r : α), r 0 = 0

Typeclass for multiplicative actions on additive structures. This generalizes group modules.

Instances
@[simp]
theorem smul_add {α : Type u} {β : Type v} [monoid α] [add_monoid β] [ β] (a : α) (b₁ b₂ : β) :
a (b₁ + b₂) = a b₁ + a b₂

@[simp]
theorem smul_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [ β] (a : α) :
a 0 = 0

def function.injective.distrib_mul_action {α : Type u} {β : Type v} {γ : Type w} [monoid α] [add_monoid β] [ β] [add_monoid γ] [ γ] (f : γ →+ β) :
(∀ (c : α) (x : γ), f (c x) = c f x)

Pullback a distributive multiplicative action along an injective additive monoid homomorphism.

Equations
def function.surjective.distrib_mul_action {α : Type u} {β : Type v} {γ : Type w} [monoid α] [add_monoid β] [ β] [add_monoid γ] [ γ] (f : β →+ γ) :
(∀ (c : α) (x : β), f (c x) = c f x)

Pushforward a distributive multiplicative action along a surjective additive monoid homomorphism.

Equations
theorem units.smul_eq_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [ β] (u : units α) {x : β} :
u x = 0 x = 0

theorem units.smul_ne_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [ β] (u : units α) {x : β} :
u x 0 x 0

@[simp]
theorem is_unit.smul_eq_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [ β] {u : α} (hu : is_unit u) {x : β} :
u x = 0 x = 0

def const_smul_hom {α : Type u} (β : Type v) [monoid α] [add_monoid β] [ β] :
α → β →+ β

Scalar multiplication by r as an add_monoid_hom.

Equations
@[simp]
theorem const_smul_hom_apply {α : Type u} {β : Type v} [monoid α] [add_monoid β] [ β] (r : α) (x : β) :
r) x = r x

theorem list.smul_sum {α : Type u} {β : Type v} [monoid α] [add_monoid β] [ β] {r : α} {l : list β} :
r l.sum = l).sum

theorem multiset.smul_sum {α : Type u} {β : Type v} [monoid α] [ β] {r : α} {s : multiset β} :
r s.sum = s).sum

theorem finset.smul_sum {α : Type u} {β : Type v} {γ : Type w} [monoid α] [ β] {r : α} {f : γ → β} {s : finset γ} :
r ∑ (x : γ) in s, f x = ∑ (x : γ) in s, r f x

@[simp]
theorem smul_neg {α : Type u} {β : Type v} [monoid α] [add_group β] [ β] (r : α) (x : β) :
r -x = -(r x)

theorem smul_sub {α : Type u} {β : Type v} [monoid α] [add_group β] [ β] (r : α) (x y : β) :
r (x - y) = r x - r y