mathlib docs: group_theory.group

source

@[class]

structure has_scalar (α : Type u) (γ : Type v) :

Type (max u v)

smul : α → γ → γ

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

Instances

source

@[class]

structure mul_action (α : Type u) (β : Type v) [monoid α] :

Type (max u v)

to_has_scalar : 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

source

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

(a₁ * a₂) • b = a₁ • a₂ • b

source

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

a₁ • a₂ • b = (a₁ * a₂) • b

source

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

a₁ • a₂ • b = a₂ • a₁ • b

source

@[simp]

theorem one_smul (α : Type u) {β : Type v} [monoid α] [mul_action α β] (b : β) :

1 • b = b

source

@[simp]

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

↑u⁻¹ • ↑u • x = x

source

@[simp]

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

↑u • ↑u⁻¹ • x = x

source

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

mul_action α γ

Pullback a multiplicative action along an injective map respecting •.

Equations

function.injective.mul_action f hf smul = {to_has_scalar := {smul := has_scalar.smul _inst_3}, one_smul := _, mul_smul := _}

source

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

mul_action α γ

Pushforward a multiplicative action along a surjective map respecting •.

Equations

function.surjective.mul_action f hf smul = {to_has_scalar := {smul := has_scalar.smul _inst_3}, one_smul := _, mul_smul := _}

source

theorem inv_smul_smul' {β : Type v} {G : Type u_1} [group_with_zero G] [mul_action G β] {c : G} (hc : c ≠ 0) (x : β) :

c⁻¹ • c • x = x

source

theorem smul_inv_smul' {β : Type v} {G : Type u_1} [group_with_zero G] [mul_action G β] {c : G} (hc : c ≠ 0) (x : β) :

c • c⁻¹ • x = x

source

theorem inv_smul_eq_iff {β : Type v} {G : Type u_1} [group_with_zero G] [mul_action G β] {a : G} (ha : a ≠ 0) {x y : β} :

a⁻¹ • x = y ↔ x = a • y

source

theorem eq_inv_smul_iff {β : Type v} {G : Type u_1} [group_with_zero G] [mul_action G β] {a : G} (ha : a ≠ 0) {x y : β} :

x = a⁻¹ • y ↔ a • x = y

source

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

ite p a₁ a₂ • b = ite p (a₁ • b) (a₂ • b)

source

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

a • ite p b₁ b₂ = ite p (a • b₁) (a • b₂)

source

@[class]

structure is_scalar_tower (R : Type u_1) (M : Type u_2) (N : Type u_3) [has_scalar R M] [has_scalar M N] [has_scalar R 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

source

@[simp]

theorem smul_assoc {R : Type u_1} {M : Type u_2} {N : Type u_3} [has_scalar R M] [has_scalar M N] [has_scalar R N] [is_scalar_tower R M N] (x : R) (y : M) (z : N) :

(x • y) • z = x • y • z

source

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

mul_action α α

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

Equations

mul_action.regular α = {to_has_scalar := {smul := λ (a₁ a₂ : α), a₁ * a₂}, one_smul := _, mul_smul := _}

source

@[instance]

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

is_scalar_tower α α β

source

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

set β

The orbit of an element under an action.

Equations

mul_action.orbit α b = set.range (λ (x : α), x • b)

source

theorem mul_action.mem_orbit_iff {α : Type u} {β : Type v} [monoid α] [mul_action α β] {b₁ b₂ : β} :

b₂ ∈ mul_action.orbit α b₁ ↔ ∃ (x : α), x • b₁ = b₂

source

@[simp]

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

x • b ∈ mul_action.orbit α b

source

@[simp]

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

b ∈ mul_action.orbit α b

source

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

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

mul_action.stabilizer_carrier α b = {x : α | x • b = b}

source

@[simp]

theorem mul_action.mem_stabilizer_iff {α : Type u} {β : Type v} [monoid α] [mul_action α β] {b : β} {x : α} :

x ∈ mul_action.stabilizer_carrier α b ↔ x • b = b

source

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

set β

The set of elements fixed under the whole action.

Equations

mul_action.fixed_points α β = {b : β | ∀ (x : α), x • b = b}

source

def mul_action.fixed_by (α : Type u) (β : Type v) [monoid α] [mul_action α β] (g : α) :

set β

fixed_by g is the subfield of elements fixed by g.

Equations

mul_action.fixed_by α β g = {x : β | g • x = x}

source

theorem mul_action.fixed_eq_Inter_fixed_by (α : Type u) (β : Type v) [monoid α] [mul_action α β] :

mul_action.fixed_points α β = ⋂ (g : α), mul_action.fixed_by α β g

source

@[simp]

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

b ∈ mul_action.fixed_points α β ↔ ∀ (x : α), x • b = b

source

@[simp]

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

b ∈ mul_action.fixed_by α β g ↔ g • b = b

source

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

b ∈ mul_action.fixed_points α β ↔ ∀ (b' : β), b' ∈ mul_action.orbit α b → b' = b

source

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

mul_action γ β

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

Equations

mul_action.comp_hom β g = {to_has_scalar := {smul := λ (x : γ) (b : β), ⇑g x • b}, one_smul := _, mul_smul := _}

source

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

submonoid α

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

Equations

mul_action.stabilizer.submonoid α b = {carrier := mul_action.stabilizer_carrier α b, one_mem' := _, mul_mem' := _}

source

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

β ↪ α → β

Embedding induced by action.

Equations

mul_action.to_fun α β = {to_fun := λ (y : β) (x : α), x • y, inj' := _}

source

@[simp]

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

⇑(mul_action.to_fun α β) y x = x • y

source

@[simp]

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

c⁻¹ • c • x = x

source

@[simp]

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

c • c⁻¹ • x = x

source

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

a⁻¹ • x = y ↔ x = a • y

source

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

x = a⁻¹ • y ↔ a • x = y

source

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

subgroup α

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

Equations

mul_action.stabilizer α b = {carrier := (mul_action.stabilizer.submonoid α b).carrier, one_mem' := _, mul_mem' := _, inv_mem' := _}

source

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

equiv.perm β

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

Equations

mul_action.to_perm α β g = {to_fun := has_scalar.smul g, inv_fun := has_scalar.smul g⁻¹, left_inv := _, right_inv := _}

source

@[instance]

def mul_action.is_group_hom {α : Type u} {β : Type v} [group α] [mul_action α β] :

is_group_hom (mul_action.to_perm α β)

source

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

function.bijective (λ (b : β), g • b)

source

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

mul_action.orbit α a = mul_action.orbit α b ↔ a ∈ mul_action.orbit α b

source

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

subgroup α

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

Equations

mul_action.stabilizer.subgroup α b = {carrier := (mul_action.stabilizer.submonoid α b).carrier, one_mem' := _, mul_mem' := _, inv_mem' := _}

source

@[simp]

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

a ∈ mul_action.orbit α (g • a)

source

@[simp]

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

g • a ∈ mul_action.orbit α (h • a)

source

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

setoid β

The relation "in the same orbit".

Equations

mul_action.orbit_rel α β = {r := λ (a b : β), a ∈ mul_action.orbit α b, iseqv := _}

source

def mul_action.mul_left_cosets {α : Type u} [group α] (H : subgroup α) (x : α) (y : quotient_group.quotient H) :

quotient_group.quotient H

Action on left cosets.

Equations

mul_action.mul_left_cosets H x y = quotient.lift_on' y (λ (y : α), quotient_group.mk (x * y)) _

source

@[instance]

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

mul_action α (quotient_group.quotient H)

Equations

mul_action.mul_action H = {to_has_scalar := {smul := mul_action.mul_left_cosets H}, one_smul := _, mul_smul := _}

source

@[instance]

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

mul_action ↥I (quotient_group.quotient H)

Equations

mul_action.mul_left_cosets_comp_subtype_val H I = mul_action.comp_hom (quotient_group.quotient H) I.subtype

source

def mul_action.of_quotient_stabilizer (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : quotient_group.quotient (mul_action.stabilizer α x)) :

β

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

Equations

mul_action.of_quotient_stabilizer α x g = quotient.lift_on' g (λ (_x : α), _x • x) _

source

@[simp]

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

mul_action.of_quotient_stabilizer α x (quotient_group.mk g) = g • x

source

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

mul_action.of_quotient_stabilizer α x g ∈ mul_action.orbit α x

source

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

mul_action.of_quotient_stabilizer α x (g • g') = g • mul_action.of_quotient_stabilizer α x g'

source

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

function.injective (mul_action.of_quotient_stabilizer α x)

source

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

↥(mul_action.orbit α b) ≃ quotient_group.quotient (mul_action.stabilizer α b)

Orbit-stabilizer theorem.

Equations

mul_action.orbit_equiv_quotient_stabilizer α b = (equiv.of_bijective (λ (g : quotient_group.quotient (mul_action.stabilizer α b)), ⟨mul_action.of_quotient_stabilizer α b g, _⟩) _).symm

source

@[simp]

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

↑(⇑((mul_action.orbit_equiv_quotient_stabilizer α b).symm) ↑a) = a • b

source

@[class]

structure distrib_mul_action (α : Type u) (β : Type v) [monoid α] [add_monoid β] :

Type (max u v)

to_mul_action : 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

source

@[simp]

theorem smul_add {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] (a : α) (b₁ b₂ : β) :

a • (b₁ + b₂) = a • b₁ + a • b₂

source

@[simp]

theorem smul_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] (a : α) :

a • 0 = 0

source

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

distrib_mul_action α γ

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

Equations

function.injective.distrib_mul_action f hf smul = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul _inst_5}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}

source

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

distrib_mul_action α γ

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

Equations

function.surjective.distrib_mul_action f hf smul = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul _inst_5}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}

source

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

↑u • x = 0 ↔ x = 0

source

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

↑u • x ≠ 0 ↔ x ≠ 0

source

@[simp]

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

u • x = 0 ↔ x = 0

source

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

β →+ β

Scalar multiplication by r as an add_monoid_hom.

Equations

const_smul_hom β r = {to_fun := has_scalar.smul r, map_zero' := _, map_add' := _}

source

@[simp]

theorem const_smul_hom_apply {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] (r : α) (x : β) :

⇑(const_smul_hom β r) x = r • x

source

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

r • l.sum = (list.map (has_scalar.smul r) l).sum

source

theorem multiset.smul_sum {α : Type u} {β : Type v} [monoid α] [add_comm_monoid β] [distrib_mul_action α β] {r : α} {s : multiset β} :

r • s.sum = (multiset.map (has_scalar.smul r) s).sum

source

theorem finset.smul_sum {α : Type u} {β : Type v} {γ : Type w} [monoid α] [add_comm_monoid β] [distrib_mul_action α β] {r : α} {f : γ → β} {s : finset γ} :

r • ∑ (x : γ) in s, f x = ∑ (x : γ) in s, r • f x

source

@[simp]

theorem smul_neg {α : Type u} {β : Type v} [monoid α] [add_group β] [distrib_mul_action α β] (r : α) (x : β) :

r • -x = -(r • x)

source

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

r • (x - y) = r • x - r • y