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 #

This file is almost identical to group_theory/submonoid/pointwise.lean. Where possible, try to keep them in sync.

source
@[protected, instance]
def subgroup.pointwise_mul_action {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] :
mul_action α (subgroup 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
source
theorem subgroup.pointwise_smul_def {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] {a : α} (S : subgroup G) :
a • S = subgroup.map (⇑(mul_distrib_mul_action.to_monoid_End α G) a) S
source
@[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
source
@[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) :
(a • S).to_submonoid = a • S.to_submonoid
source
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
source
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
source
@[protected, instance]
def subgroup.pointwise_central_scalar {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] [mul_distrib_mul_action αᵐᵒᵖ G] [is_central_scalar α G] :
is_central_scalar α (subgroup G)
source
@[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
source
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
source
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
source
@[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
source
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
source
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
source
@[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)) :
↑(⇑(subgroup.equiv_smul a H) x) = a • ↑x
source
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
source
@[simp]
theorem subgroup.equiv_smul_symm_apply_coe {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] (a : α) (H : subgroup G) (x : ↥(submonoid.map (mul_distrib_mul_action.to_mul_equiv G a).to_monoid_hom H.to_submonoid)) :
↑(⇑((subgroup.equiv_smul a H).symm) x) = a⁻¹ • ↑x
source
theorem subgroup.subgroup_mul_singleton {G : Type u_2} [group G] {H : subgroup G} {h : G} (hh : h ∈ H) :
(↑H) * {h} = ↑H
source
theorem subgroup.singleton_mul_subgroup {G : Type u_2} [group G] {H : subgroup G} {h : G} (hh : h ∈ H) :
{h} * ↑H = ↑H
source
@[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
source
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
source
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
source
@[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
source
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
source
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
source
@[protected, instance]
def add_subgroup.pointwise_mul_action {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] :
mul_action α (add_subgroup A)

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
source
@[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
source
@[simp]
theorem add_subgroup.pointwise_smul_to_add_submonoid {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] (a : α) (S : add_subgroup A) :
(a • S).to_add_submonoid = a • S.to_add_submonoid
source
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
source
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
source
@[protected, instance]
def add_subgroup.pointwise_central_scalar {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] [distrib_mul_action αᵐᵒᵖ A] [is_central_scalar α A] :
is_central_scalar α (add_subgroup A)
source
@[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
source
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
source
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
source
@[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
source
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
source
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
source
@[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
source
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
source
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
source
@[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
source
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
source
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