# Documentation

Mathlib.GroupTheory.Subgroup.Pointwise

# Pointwise instances on Subgroup and AddSubgroups #

This file provides the actions

which matches the action of Set.mulActionSet.

These actions are available in the Pointwise locale.

## Implementation notes #

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

@[simp]
theorem neg_coe_set {G : Type u_2} {S : Type u_4} [] [SetLike S G] [] {H : S} :
-H = H
@[simp]
theorem inv_coe_set {G : Type u_2} {S : Type u_4} [] [SetLike S G] [] {H : S} :
(H)⁻¹ = H
@[simp]
theorem AddSubgroup.neg_subset_closure {G : Type u_2} [] (S : Set G) :
-S ↑()
@[simp]
theorem Subgroup.inv_subset_closure {G : Type u_2} [] (S : Set G) :
S⁻¹ ↑()
theorem AddSubgroup.closure_toAddSubmonoid {G : Type u_2} [] (S : Set G) :
theorem Subgroup.closure_toSubmonoid {G : Type u_2} [] (S : Set G) :
().toSubmonoid = Submonoid.closure (S S⁻¹)
theorem AddSubgroup.closure_induction_left {G : Type u_2} [] {s : Set G} {p : GProp} {x : G} (h : ) (H1 : p 0) (Hmul : (x : G) → x s(y : G) → p yp (x + y)) (Hinv : (x : G) → x s(y : G) → p yp (-x + y)) :
p x

For additive subgroups generated by a single element, see the simpler zsmul_induction_left.

theorem Subgroup.closure_induction_left {G : Type u_2} [] {s : Set G} {p : GProp} {x : G} (h : ) (H1 : p 1) (Hmul : (x : G) → x s(y : G) → p yp (x * y)) (Hinv : (x : G) → x s(y : G) → p yp (x⁻¹ * y)) :
p x

For subgroups generated by a single element, see the simpler zpow_induction_left.

theorem AddSubgroup.closure_induction_right {G : Type u_2} [] {s : Set G} {p : GProp} {x : G} (h : ) (H1 : p 0) (Hmul : (x y : G) → y sp xp (x + y)) (Hinv : (x y : G) → y sp xp (x + -y)) :
p x

For additive subgroups generated by a single element, see the simpler zsmul_induction_right.

theorem Subgroup.closure_induction_right {G : Type u_2} [] {s : Set G} {p : GProp} {x : G} (h : ) (H1 : p 1) (Hmul : (x y : G) → y sp xp (x * y)) (Hinv : (x y : G) → y sp xp (x * y⁻¹)) :
p x

For subgroups generated by a single element, see the simpler zpow_induction_right.

@[simp]
theorem AddSubgroup.closure_neg {G : Type u_2} [] (s : Set G) :
@[simp]
theorem Subgroup.closure_inv {G : Type u_2} [] (s : Set G) :
theorem AddSubgroup.closure_induction'' {G : Type u_2} [] {s : Set G} {p : GProp} {x : G} (h : ) (Hk : (x : G) → x sp x) (Hk_inv : (x : G) → x sp (-x)) (H1 : p 0) (Hmul : (x y : G) → p xp yp (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 Subgroup.closure_induction'' {G : Type u_2} [] {s : Set G} {p : GProp} {x : G} (h : ) (Hk : (x : G) → x sp x) (Hk_inv : (x : G) → x sp x⁻¹) (H1 : p 1) (Hmul : (x y : G) → p xp yp (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 AddSubgroup.iSup_induction {G : Type u_2} [] {ι : Sort u_5} (S : ι) {C : GProp} {x : G} (hx : x ⨆ (i : ι), S i) (hp : (i : ι) → (x : G) → x S iC x) (h1 : C 0) (hmul : (x y : G) → C xC yC (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.iSup_induction {G : Type u_2} [] {ι : Sort u_5} (S : ι) {C : GProp} {x : G} (hx : x ⨆ (i : ι), S i) (hp : (i : ι) → (x : G) → x S iC x) (h1 : C 1) (hmul : (x y : G) → C xC yC (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 AddSubgroup.iSup_induction' {G : Type u_2} [] {ι : Sort u_5} (S : ι) {C : (x : G) → x ⨆ (i : ι), S iProp} (hp : (i : ι) → (x : G) → (hx : x S i) → C x (_ : x ⨆ (i : ι), S i)) (h1 : C 0 (_ : 0 ⨆ (i : ι), S i)) (hmul : (x y : G) → (hx : x ⨆ (i : ι), S i) → (hy : y ⨆ (i : ι), S i) → C x hxC y hyC (x + y) (_ : x + y ⨆ (i : ι), S i)) {x : G} (hx : x ⨆ (i : ι), S i) :
C x hx

theorem Subgroup.iSup_induction' {G : Type u_2} [] {ι : Sort u_5} (S : ι) {C : (x : G) → x ⨆ (i : ι), S iProp} (hp : (i : ι) → (x : G) → (hx : x S i) → C x (_ : x ⨆ (i : ι), S i)) (h1 : C 1 (_ : 1 ⨆ (i : ι), S i)) (hmul : (x y : G) → (hx : x ⨆ (i : ι), S i) → (hy : y ⨆ (i : ι), S i) → C x hxC y hyC (x * y) (_ : x * y ⨆ (i : ι), S i)) {x : G} (hx : x ⨆ (i : ι), S i) :
C x hx

A dependent version of Subgroup.iSup_induction.

abbrev AddSubgroup.closure_add_le.match_1 {G : Type u_1} [] (S : Set G) (T : Set G) (_x : G) (motive : _x S + TProp) :
(x : _x S + T) → ((_s _t : G) → (hs : _s S) → (ht : _t T) → (hx : (fun x x_1 => x + x_1) _s _t = _x) → motive (_ : a b, a S b T (fun x x_1 => x + x_1) a b = _x)) → motive x
Instances For
theorem AddSubgroup.closure_add_le {G : Type u_2} [] (S : Set G) (T : Set G) :
theorem Subgroup.closure_mul_le {G : Type u_2} [] (S : Set G) (T : Set G) :
theorem AddSubgroup.sup_eq_closure {G : Type u_2} [] (H : ) (K : ) :
H K = AddSubgroup.closure (H + K)
theorem Subgroup.sup_eq_closure {G : Type u_2} [] (H : ) (K : ) :
H K = Subgroup.closure (H * K)
theorem AddSubgroup.set_add_normal_comm {G : Type u_2} [] (s : Set G) (N : ) [hN : ] :
s + N = N + s
theorem Subgroup.set_mul_normal_comm {G : Type u_2} [] (s : Set G) (N : ) [hN : ] :
s * N = N * s
theorem AddSubgroup.add_normal {G : Type u_2} [] (H : ) (N : ) [hN : ] :
↑(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} [] (H : ) (N : ) [hN : ] :
↑(H N) = H * N

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

theorem AddSubgroup.normal_add {G : Type u_2} [] (N : ) (H : ) :
↑(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} [] (N : ) (H : ) [] :
↑(N H) = N * H

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

theorem AddSubgroup.add_inf_assoc {G : Type u_2} [] (A : ) (B : ) (C : ) (h : A C) :
A + ↑(B C) = (A + B) C
theorem Subgroup.mul_inf_assoc {G : Type u_2} [] (A : ) (B : ) (C : ) (h : A C) :
A * ↑(B C) = A * B C
theorem AddSubgroup.inf_add_assoc {G : Type u_2} [] (A : ) (B : ) (C : ) (h : C A) :
↑(A B) + C = A (B + C)
theorem Subgroup.inf_mul_assoc {G : Type u_2} [] (A : ) (B : ) (C : ) (h : C A) :
↑(A B) * C = A B * C
theorem AddSubgroup.sup_normal.proof_1 {G : Type u_1} [] (H : ) (K : ) [hH : ] [hK : ] :
instance AddSubgroup.sup_normal {G : Type u_2} [] (H : ) (K : ) [hH : ] [hK : ] :
instance Subgroup.sup_normal {G : Type u_2} [] (H : ) (K : ) [hH : ] [hK : ] :
theorem AddSubgroup.vadd_opposite_image_add_preimage' {G : Type u_2} [] (g : G) (h : Gᵃᵒᵖ) (s : Set G) :
(fun y => h +ᵥ y) '' ((fun x => g + x) ⁻¹' s) = (fun x => g + x) ⁻¹' ((fun y => h +ᵥ y) '' s)
theorem Subgroup.smul_opposite_image_mul_preimage' {G : Type u_2} [] (g : G) (h : Gᵐᵒᵖ) (s : Set G) :
(fun y => h y) '' ((fun x => g * x) ⁻¹' s) = (fun x => g * x) ⁻¹' ((fun y => h y) '' s)
theorem AddSubgroup.vadd_opposite_image_add_preimage {G : Type u_2} [] {H : } (g : G) (h : { x // }) (s : Set G) :
(fun y => h +ᵥ y) '' ((fun x => g + x) ⁻¹' s) = (fun x => g + x) ⁻¹' ((fun y => h +ᵥ y) '' s)
theorem Subgroup.smul_opposite_image_mul_preimage {G : Type u_2} [] {H : } (g : G) (h : { x // x }) (s : Set G) :
(fun y => h y) '' ((fun x => g * x) ⁻¹' s) = (fun x => g * x) ⁻¹' ((fun y => h y) '' s)

### Pointwise action #

def Subgroup.pointwiseMulAction {α : Type u_1} {G : Type u_2} [] [] [] :
MulAction α ()

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

This is available as an instance in the Pointwise locale.

Instances For
theorem Subgroup.pointwise_smul_def {α : Type u_1} {G : Type u_2} [] [] [] {a : α} (S : ) :
a S = Subgroup.map (↑() a) S
@[simp]
theorem Subgroup.coe_pointwise_smul {α : Type u_1} {G : Type u_2} [] [] [] (a : α) (S : ) :
↑(a S) = a S
@[simp]
theorem Subgroup.pointwise_smul_toSubmonoid {α : Type u_1} {G : Type u_2} [] [] [] (a : α) (S : ) :
(a S).toSubmonoid = a S.toSubmonoid
theorem Subgroup.smul_mem_pointwise_smul {α : Type u_1} {G : Type u_2} [] [] [] (m : G) (a : α) (S : ) :
m Sa m a S
theorem Subgroup.mem_smul_pointwise_iff_exists {α : Type u_1} {G : Type u_2} [] [] [] (m : G) (a : α) (S : ) :
m a S s, s S a s = m
@[simp]
theorem Subgroup.smul_bot {α : Type u_1} {G : Type u_2} [] [] [] (a : α) :
theorem Subgroup.smul_sup {α : Type u_1} {G : Type u_2} [] [] [] (a : α) (S : ) (T : ) :
a (S T) = a S a T
theorem Subgroup.smul_closure {α : Type u_1} {G : Type u_2} [] [] [] (a : α) (s : Set G) :
instance Subgroup.pointwise_isCentralScalar {α : Type u_1} {G : Type u_2} [] [] [] [] [] :
theorem Subgroup.conj_smul_le_of_le {G : Type u_2} [] {P : } {H : } (hP : P H) (h : { x // x H }) :
MulAut.conj h P H
theorem Subgroup.conj_smul_subgroupOf {G : Type u_2} [] {P : } {H : } (hP : P H) (h : { x // x H }) :
MulAut.conj h = Subgroup.subgroupOf (MulAut.conj h P) H
@[simp]
theorem Subgroup.smul_mem_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [] [] [] {a : α} {S : } {x : G} :
a x a S x S
theorem Subgroup.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {G : Type u_2} [] [] [] {a : α} {S : } {x : G} :
x a S a⁻¹ x S
theorem Subgroup.mem_inv_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [] [] [] {a : α} {S : } {x : G} :
x a⁻¹ S a x S
@[simp]
theorem Subgroup.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [] [] [] {a : α} {S : } {T : } :
a S a T S T
theorem Subgroup.pointwise_smul_subset_iff {α : Type u_1} {G : Type u_2} [] [] [] {a : α} {S : } {T : } :
a S T S a⁻¹ T
theorem Subgroup.subset_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [] [] [] {a : α} {S : } {T : } :
S a T a⁻¹ S T
@[simp]
theorem Subgroup.smul_inf {α : Type u_1} {G : Type u_2} [] [] [] (a : α) (S : ) (T : ) :
a (S T) = a S a T
@[simp]
theorem Subgroup.equivSMul_symm_apply_coe {α : Type u_1} {G : Type u_2} [] [] [] (a : α) (H : ) :
∀ (a : ↑( '' H.toSubmonoid)), ↑(↑() a) = a⁻¹ a
@[simp]
theorem Subgroup.equivSMul_apply_coe {α : Type u_1} {G : Type u_2} [] [] [] (a : α) (H : ) :
∀ (a : H.toSubmonoid), ↑(↑() a) = a a
def Subgroup.equivSMul {α : Type u_1} {G : Type u_2} [] [] [] (a : α) (H : ) :
{ x // x H } ≃* { x // x a H }

Applying a MulDistribMulAction results in an isomorphic subgroup

Instances For
theorem Subgroup.subgroup_mul_singleton {G : Type u_2} [] {H : } {h : G} (hh : h H) :
H * {h} = H
theorem Subgroup.singleton_mul_subgroup {G : Type u_2} [] {H : } {h : G} (hh : h H) :
{h} * H = H
theorem Subgroup.Normal.conjAct {G : Type u_5} [] {H : } (hH : ) (g : ) :
g H = H
@[simp]
theorem Subgroup.smul_normal {G : Type u_2} [] (g : G) (H : ) [h : ] :
MulAut.conj g H = H
@[simp]
theorem Subgroup.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [] [] [] {a : α} (ha : a 0) (S : ) (x : G) :
a x a S x S
theorem Subgroup.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {G : Type u_2} [] [] [] {a : α} (ha : a 0) (S : ) (x : G) :
x a S a⁻¹ x S
theorem Subgroup.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [] [] [] {a : α} (ha : a 0) (S : ) (x : G) :
x a⁻¹ S a x S
@[simp]
theorem Subgroup.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
a S a T S T
theorem Subgroup.pointwise_smul_le_iff₀ {α : Type u_1} {G : Type u_2} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
a S T S a⁻¹ T
theorem Subgroup.le_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
S a T a⁻¹ S T
def AddSubgroup.pointwiseMulAction {α : Type u_1} {A : Type u_3} [] [] [] :
MulAction α ()

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

This is available as an instance in the Pointwise locale.

Instances For
@[simp]
theorem AddSubgroup.coe_pointwise_smul {α : Type u_1} {A : Type u_3} [] [] [] (a : α) (S : ) :
↑(a S) = a S
@[simp]
theorem AddSubgroup.pointwise_smul_toAddSubmonoid {α : Type u_1} {A : Type u_3} [] [] [] (a : α) (S : ) :
theorem AddSubgroup.smul_mem_pointwise_smul {α : Type u_1} {A : Type u_3} [] [] [] (m : A) (a : α) (S : ) :
m Sa m a S
theorem AddSubgroup.mem_smul_pointwise_iff_exists {α : Type u_1} {A : Type u_3} [] [] [] (m : A) (a : α) (S : ) :
m a S s, s S a s = m
instance AddSubgroup.pointwise_isCentralScalar {α : Type u_1} {A : Type u_3} [] [] [] [] [] :
@[simp]
theorem AddSubgroup.smul_mem_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [] [] [] {a : α} {S : } {x : A} :
a x a S x S
theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {A : Type u_3} [] [] [] {a : α} {S : } {x : A} :
x a S a⁻¹ x S
theorem AddSubgroup.mem_inv_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [] [] [] {a : α} {S : } {x : A} :
x a⁻¹ S a x S
@[simp]
theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [] [] [] {a : α} {S : } {T : } :
a S a T S T
theorem AddSubgroup.pointwise_smul_le_iff {α : Type u_1} {A : Type u_3} [] [] [] {a : α} {S : } {T : } :
a S T S a⁻¹ T
theorem AddSubgroup.le_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [] [] [] {a : α} {S : } {T : } :
S a T a⁻¹ S T
@[simp]
theorem AddSubgroup.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [] [] [] {a : α} (ha : a 0) (S : ) (x : A) :
a x a S x S
theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {A : Type u_3} [] [] [] {a : α} (ha : a 0) (S : ) (x : A) :
x a S a⁻¹ x S
theorem AddSubgroup.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [] [] [] {a : α} (ha : a 0) (S : ) (x : A) :
x a⁻¹ S a x S
@[simp]
theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
a S a T S T
theorem AddSubgroup.pointwise_smul_le_iff₀ {α : Type u_1} {A : Type u_3} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
a S T S a⁻¹ T
theorem AddSubgroup.le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
S a T a⁻¹ S T