mathlib documentation

group_theory.subgroup.pointwise

Pointwise instances on subgroup and add_subgroups #

This file provides the actions

which matches the action of mul_action_set.

These actions are available in the pointwise locale.

Implementation notes #

The pointwise section of this file is almost identical to group_theory/submonoid/pointwise.lean. Where possible, try to keep them in sync.

@[simp]
theorem inv_coe_set {G : Type u_2} {S : Type u_4} [group G] [set_like S G] [subgroup_class S G] {H : S} :
@[simp]
theorem neg_coe_set {G : Type u_2} {S : Type u_4} [add_group G] [set_like S G] [add_subgroup_class S G] {H : S} :
@[simp]
theorem subgroup.inv_subset_closure {G : Type u_2} [group G] (S : set G) :
@[simp]
theorem add_subgroup.closure_induction_left {G : Type u_2} [add_group G] {s : set G} {p : G Prop} {x : G} (h : x add_subgroup.closure s) (H1 : p 0) (Hmul : (x : G), x s (y : G), p y p (x + y)) (Hinv : (x : G), x s (y : G), p y p (-x + y)) :
p x
theorem subgroup.closure_induction_left {G : Type u_2} [group G] {s : set G} {p : G Prop} {x : G} (h : x subgroup.closure s) (H1 : p 1) (Hmul : (x : G), x s (y : G), p y p (x * y)) (Hinv : (x : G), x s (y : G), p y p (x⁻¹ * y)) :
p x
theorem add_subgroup.closure_induction_right {G : Type u_2} [add_group G] {s : set G} {p : G Prop} {x : G} (h : x add_subgroup.closure s) (H1 : p 0) (Hmul : (x y : G), y s p x p (x + y)) (Hinv : (x y : G), y s p x p (x + -y)) :
p x
theorem subgroup.closure_induction_right {G : Type u_2} [group G] {s : set G} {p : G Prop} {x : G} (h : x subgroup.closure s) (H1 : p 1) (Hmul : (x y : G), y s p x p (x * y)) (Hinv : (x y : G), y s p x p (x * y⁻¹)) :
p x
@[simp]
theorem subgroup.closure_induction'' {G : Type u_2} [group G] {s : set G} {p : G Prop} {x : G} (h : x subgroup.closure s) (Hk : (x : G), x s p x) (Hk_inv : (x : G), x s p x⁻¹) (H1 : p 1) (Hmul : (x y : G), p x p y p (x * y)) :
p x

An induction principle for closure membership. If p holds for 1 and all elements of k and their inverse, and is preserved under multiplication, then p holds for all elements of the closure of k.

theorem add_subgroup.closure_induction'' {G : Type u_2} [add_group G] {s : set G} {p : G Prop} {x : G} (h : x add_subgroup.closure s) (Hk : (x : G), x s p x) (Hk_inv : (x : G), x s p (-x)) (H1 : p 0) (Hmul : (x y : G), p x p y p (x + y)) :
p x

An induction principle for additive closure membership. If p holds for 0 and all elements of k and their negation, and is preserved under addition, then p holds for all elements of the additive closure of k.

theorem add_subgroup.supr_induction {G : Type u_2} [add_group G] {ι : Sort u_1} (S : ι add_subgroup G) {C : G Prop} {x : G} (hx : x (i : ι), S i) (hp : (i : ι) (x : G), x S i C x) (h1 : C 0) (hmul : (x y : G), C x C y C (x + y)) :
C x

An induction principle for elements of ⨆ i, S i. If C holds for 0 and all elements of S i for all i, and is preserved under addition, then it holds for all elements of the supremum of S.

theorem subgroup.supr_induction {G : Type u_2} [group G] {ι : Sort u_1} (S : ι subgroup G) {C : G Prop} {x : G} (hx : x (i : ι), S i) (hp : (i : ι) (x : G), x S i C x) (h1 : C 1) (hmul : (x y : G), C x C y C (x * y)) :
C x

An induction principle for elements of ⨆ i, S i. If C holds for 1 and all elements of S i for all i, and is preserved under multiplication, then it holds for all elements of the supremum of S.

theorem subgroup.supr_induction' {G : Type u_2} [group G] {ι : Sort u_1} (S : ι subgroup G) {C : Π (x : G), (x (i : ι), S i) Prop} (hp : (i : ι) (x : G) (H : x S i), C x _) (h1 : C 1 _) (hmul : (x y : G) (hx : x (i : ι), S i) (hy : y (i : ι), S i), C x hx C y hy C (x * y) _) {x : G} (hx : x (i : ι), S i) :
C x hx

A dependent version of subgroup.supr_induction.

theorem add_subgroup.supr_induction' {G : Type u_2} [add_group G] {ι : Sort u_1} (S : ι add_subgroup G) {C : Π (x : G), (x (i : ι), S i) Prop} (hp : (i : ι) (x : G) (H : x S i), C x _) (h1 : C 0 _) (hmul : (x y : G) (hx : x (i : ι), S i) (hy : y (i : ι), S i), C x hx C y hy C (x + y) _) {x : G} (hx : x (i : ι), S i) :
C x hx

A dependent version of add_subgroup.supr_induction.

theorem subgroup.sup_eq_closure {G : Type u_2} [group G] (H K : subgroup G) :
theorem add_subgroup.add_normal {G : Type u_2} [add_group G] (H N : add_subgroup G) [N.normal] :
(H N) = H + N

The carrier of H ⊔ N is just ↑H + ↑N (pointwise set addition) when N is normal.

theorem subgroup.mul_normal {G : Type u_2} [group G] (H N : subgroup G) [N.normal] :
(H N) = H * N

The carrier of H ⊔ N is just ↑H * ↑N (pointwise set product) when N is normal.

theorem add_subgroup.normal_add {G : Type u_2} [add_group G] (N H : add_subgroup G) [N.normal] :
(N H) = N + H

The carrier of N ⊔ H is just ↑N + ↑H (pointwise set addition) when N is normal.

theorem subgroup.normal_mul {G : Type u_2} [group G] (N H : subgroup G) [N.normal] :
(N H) = N * H

The carrier of N ⊔ H is just ↑N * ↑H (pointwise set product) when N is normal.

theorem subgroup.mul_inf_assoc {G : Type u_2} [group G] (A B C : subgroup G) (h : A C) :
A * (B C) = A * B C
theorem add_subgroup.add_inf_assoc {G : Type u_2} [add_group G] (A B C : add_subgroup G) (h : A C) :
A + (B C) = (A + B) C
theorem subgroup.inf_mul_assoc {G : Type u_2} [group G] (A B C : subgroup G) (h : C A) :
(A B) * C = A B * C
theorem add_subgroup.inf_add_assoc {G : Type u_2} [add_group G] (A B C : add_subgroup G) (h : C A) :
(A B) + C = A (B + C)
@[protected, instance]
def subgroup.sup_normal {G : Type u_2} [group G] (H K : subgroup G) [hH : H.normal] [hK : K.normal] :
(H K).normal
theorem subgroup.smul_opposite_image_mul_preimage {G : Type u_2} [group G] {H : subgroup G} (g : G) (h : (subgroup.opposite H)) (s : set G) :
(λ (y : G), h y) '' (has_mul.mul g ⁻¹' s) = has_mul.mul g ⁻¹' ((λ (y : G), h y) '' s)
theorem add_subgroup.vadd_opposite_image_add_preimage {G : Type u_2} [add_group G] {H : add_subgroup G} (g : G) (h : (add_subgroup.opposite H)) (s : set G) :
(λ (y : G), h +ᵥ y) '' (has_add.add g ⁻¹' s) = has_add.add g ⁻¹' ((λ (y : G), h +ᵥ y) '' s)

Pointwise action #

@[protected]
def subgroup.pointwise_mul_action {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] :

The action on a subgroup corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

Equations
theorem subgroup.pointwise_smul_def {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] {a : α} (S : subgroup G) :
@[simp]
theorem subgroup.coe_pointwise_smul {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (a : α) (S : subgroup G) :
(a S) = a S
@[simp]
theorem subgroup.pointwise_smul_to_submonoid {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (a : α) (S : subgroup G) :
theorem subgroup.smul_mem_pointwise_smul {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (m : G) (a : α) (S : subgroup G) :
m S a m a S
theorem subgroup.mem_smul_pointwise_iff_exists {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (m : G) (a : α) (S : subgroup G) :
m a S (s : G), s S a s = m
@[simp]
theorem subgroup.smul_bot {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (a : α) :
theorem subgroup.smul_sup {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (a : α) (S T : subgroup G) :
a (S T) = a S a T
theorem subgroup.smul_closure {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (a : α) (s : set G) :
theorem subgroup.conj_smul_le_of_le {G : Type u_2} [group G] {P H : subgroup G} (hP : P H) (h : H) :
theorem subgroup.conj_smul_subgroup_of {G : Type u_2} [group G] {P H : subgroup G} (hP : P H) (h : H) :
@[simp]
theorem subgroup.smul_mem_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] {a : α} {S : subgroup G} {x : G} :
a x a S x S
theorem subgroup.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] {a : α} {S : subgroup G} {x : G} :
x a S a⁻¹ x S
theorem subgroup.mem_inv_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] {a : α} {S : subgroup G} {x : G} :
x a⁻¹ S a x S
@[simp]
theorem subgroup.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] {a : α} {S T : subgroup G} :
a S a T S T
theorem subgroup.pointwise_smul_subset_iff {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] {a : α} {S T : subgroup G} :
a S T S a⁻¹ T
theorem subgroup.subset_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] {a : α} {S T : subgroup G} :
S a T a⁻¹ S T
@[simp]
theorem subgroup.smul_inf {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] (a : α) (S T : subgroup G) :
a (S T) = a S a T
@[simp]
theorem subgroup.equiv_smul_apply_coe {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] (a : α) (H : subgroup G) (x : (H.to_submonoid)) :
def subgroup.equiv_smul {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] (a : α) (H : subgroup G) :
H ≃* (a H)

Applying a mul_distrib_mul_action results in an isomorphic subgroup

Equations
theorem subgroup.subgroup_mul_singleton {G : Type u_2} [group G] {H : subgroup G} {h : G} (hh : h H) :
H * {h} = H
theorem subgroup.singleton_mul_subgroup {G : Type u_2} [group G] {H : subgroup G} {h : G} (hh : h H) :
{h} * H = H
theorem subgroup.normal.conj_act {G : Type u_1} [group G] {H : subgroup G} (hH : H.normal) (g : conj_act G) :
g H = H
@[simp]
theorem subgroup.smul_normal {G : Type u_2} [group G] (g : G) (H : subgroup G) [h : H.normal] :
@[simp]
theorem subgroup.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [group G] [group_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a 0) (S : subgroup G) (x : G) :
a x a S x S
theorem subgroup.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {G : Type u_2} [group G] [group_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a 0) (S : subgroup G) (x : G) :
x a S a⁻¹ x S
theorem subgroup.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [group G] [group_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a 0) (S : subgroup G) (x : G) :
x a⁻¹ S a x S
@[simp]
theorem subgroup.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [group G] [group_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a 0) {S T : subgroup G} :
a S a T S T
theorem subgroup.pointwise_smul_le_iff₀ {α : Type u_1} {G : Type u_2} [group G] [group_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a 0) {S T : subgroup G} :
a S T S a⁻¹ T
theorem subgroup.le_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [group G] [group_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a 0) {S T : subgroup G} :
S a T a⁻¹ S T
@[protected]

The action on an additive subgroup corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

Equations
@[simp]
theorem add_subgroup.coe_pointwise_smul {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] (a : α) (S : add_subgroup A) :
(a S) = a S
@[simp]
theorem add_subgroup.smul_mem_pointwise_smul {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] (m : A) (a : α) (S : add_subgroup A) :
m S a m a S
theorem add_subgroup.mem_smul_pointwise_iff_exists {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] (m : A) (a : α) (S : add_subgroup A) :
m a S (s : A), s S a s = m
@[simp]
theorem add_subgroup.smul_mem_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S : add_subgroup A} {x : A} :
a x a S x S
theorem add_subgroup.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S : add_subgroup A} {x : A} :
x a S a⁻¹ x S
theorem add_subgroup.mem_inv_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S : add_subgroup A} {x : A} :
x a⁻¹ S a x S
@[simp]
theorem add_subgroup.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S T : add_subgroup A} :
a S a T S T
theorem add_subgroup.pointwise_smul_le_iff {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S T : add_subgroup A} :
a S T S a⁻¹ T
theorem add_subgroup.le_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S T : add_subgroup A} :
S a T a⁻¹ S T
@[simp]
theorem add_subgroup.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) (S : add_subgroup A) (x : A) :
a x a S x S
theorem add_subgroup.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) (S : add_subgroup A) (x : A) :
x a S a⁻¹ x S
theorem add_subgroup.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) (S : add_subgroup A) (x : A) :
x a⁻¹ S a x S
@[simp]
theorem add_subgroup.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) {S T : add_subgroup A} :
a S a T S T
theorem add_subgroup.pointwise_smul_le_iff₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) {S T : add_subgroup A} :
a S T S a⁻¹ T
theorem add_subgroup.le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) {S T : add_subgroup A} :
S a T a⁻¹ S T