mathlib documentation

group_theory.submonoid.pointwise

Pointwise instances on submonoids and add_submonoids #

This file provides:

and the actions

which matches the action of mul_action_set.

These are all available in the pointwise locale.

Implementation notes #

Most of the lemmas in this file are direct copies of lemmas from algebra/pointwise.lean. While the statements of these lemmas are defeq, we repeat them here due to them not being syntactically equal. Before adding new lemmas here, consider if they would also apply to the action on sets.

source
@[protected]
def add_submonoid.has_neg {G : Type u_3} [add_group G] :
has_neg (add_submonoid G)

The additive submonoid with every element negated.

Equations
source
@[protected, instance]
def submonoid.has_inv {G : Type u_3} [group G] :
has_inv (submonoid G)

The submonoid with every element inverted.

Equations
source
@[simp]
theorem add_submonoid.coe_neg {G : Type u_3} [add_group G] (S : add_submonoid G) :
↑-S = -↑S
source
@[simp]
theorem submonoid.coe_inv {G : Type u_3} [group G] (S : submonoid G) :
↑S⁻¹ = (↑S)⁻¹
source
@[simp]
theorem submonoid.mem_inv {G : Type u_3} [group G] {g : G} {S : submonoid G} :
g ∈ S⁻¹ ↔ g⁻¹ ∈ S
source
@[simp]
theorem add_submonoid.mem_neg {G : Type u_3} [add_group G] {g : G} {S : add_submonoid G} :
g ∈ -S ↔ -g ∈ S
source
@[protected, simp]
theorem add_submonoid.neg_neg {G : Type u_3} [add_group G] (S : add_submonoid G) :
--S = S
source
@[protected, simp]
theorem submonoid.inv_inv {G : Type u_3} [group G] (S : submonoid G) :
S⁻¹⁻¹ = S
source
@[simp]
theorem submonoid.inv_le_inv {G : Type u_3} [group G] (S T : submonoid G) :
S⁻¹ ≤ T⁻¹ ↔ S ≤ T
source
@[simp]
theorem add_submonoid.neg_le_neg {G : Type u_3} [add_group G] (S T : add_submonoid G) :
-S ≤ -T ↔ S ≤ T
source
theorem submonoid.inv_le {G : Type u_3} [group G] (S T : submonoid G) :
S⁻¹ ≤ T ↔ S ≤ T⁻¹
source
theorem add_submonoid.neg_le {G : Type u_3} [add_group G] (S T : add_submonoid G) :
-S ≤ T ↔ S ≤ -T
source
def add_submonoid.neg_order_iso {G : Type u_3} [add_group G] :
add_submonoid G ≃o add_submonoid G

add_submonoid.has_neg as an order isomorphism

Equations
source
@[simp]
theorem submonoid.inv_order_iso_apply {G : Type u_3} [group G] (ᾰ : submonoid G) :
⇑submonoid.inv_order_iso ᾰ = ᾰ⁻¹
source
@[simp]
theorem add_submonoid.neg_order_iso_symm_apply {G : Type u_3} [add_group G] (ᾰ : add_submonoid G) :
⇑(rel_iso.symm add_submonoid.neg_order_iso) ᾰ = -ᾰ
source
@[simp]
theorem add_submonoid.neg_order_iso_apply {G : Type u_3} [add_group G] (ᾰ : add_submonoid G) :
⇑add_submonoid.neg_order_iso ᾰ = -ᾰ
source
@[simp]
theorem submonoid.inv_order_iso_symm_apply {G : Type u_3} [group G] (ᾰ : submonoid G) :
⇑(rel_iso.symm submonoid.inv_order_iso) ᾰ = ᾰ⁻¹
source
def submonoid.inv_order_iso {G : Type u_3} [group G] :
submonoid G ≃o submonoid G

submonoid.has_inv as an order isomorphism.

Equations
source
theorem add_submonoid.closure_neg {G : Type u_3} [add_group G] (s : set G) :
add_submonoid.closure (-s) = -add_submonoid.closure s
source
theorem submonoid.closure_inv {G : Type u_3} [group G] (s : set G) :
submonoid.closure s⁻¹ = (submonoid.closure s)⁻¹
source
@[simp]
theorem add_submonoid.neg_inf {G : Type u_3} [add_group G] (S T : add_submonoid G) :
-(S ⊓ T) = -S ⊓ -T
source
@[simp]
theorem submonoid.inv_inf {G : Type u_3} [group G] (S T : submonoid G) :
(S ⊓ T)⁻¹ = S⁻¹ ⊓ T⁻¹
source
@[simp]
theorem submonoid.inv_sup {G : Type u_3} [group G] (S T : submonoid G) :
(S ⊔ T)⁻¹ = S⁻¹ ⊔ T⁻¹
source
@[simp]
theorem add_submonoid.neg_sup {G : Type u_3} [add_group G] (S T : add_submonoid G) :
-(S ⊔ T) = -S ⊔ -T
source
@[simp]
theorem submonoid.inv_bot {G : Type u_3} [group G] :
⊥⁻¹ = ⊥
source
@[simp]
theorem add_submonoid.neg_bot {G : Type u_3} [add_group G] :
-⊥ = ⊥
source
@[simp]
theorem add_submonoid.neg_top {G : Type u_3} [add_group G] :
-⊤ = ⊤
source
@[simp]
theorem submonoid.inv_top {G : Type u_3} [group G] :
⊤⁻¹ = ⊤
source
@[simp]
theorem submonoid.inv_infi {G : Type u_3} [group G] {ι : Sort u_1} (S : ι → submonoid G) :
(⨅ (i : ι), S i)⁻¹ = ⨅ (i : ι), (S i)⁻¹
source
@[simp]
theorem add_submonoid.neg_infi {G : Type u_3} [add_group G] {ι : Sort u_1} (S : ι → add_submonoid G) :
(-⨅ (i : ι), S i) = ⨅ (i : ι), -S i
source
@[simp]
theorem submonoid.inv_supr {G : Type u_3} [group G] {ι : Sort u_1} (S : ι → submonoid G) :
(⨆ (i : ι), S i)⁻¹ = ⨆ (i : ι), (S i)⁻¹
source
@[simp]
theorem add_submonoid.neg_supr {G : Type u_3} [add_group G] {ι : Sort u_1} (S : ι → add_submonoid G) :
(-⨆ (i : ι), S i) = ⨆ (i : ι), -S i
source
@[protected, instance]
def submonoid.pointwise_mul_action {α : Type u_1} {M : Type u_2} [monoid M] [monoid α] [mul_distrib_mul_action α M] :
mul_action α (submonoid M)

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

This is available as an instance in the pointwise locale.

Equations
source
@[simp]
theorem submonoid.coe_pointwise_smul {α : Type u_1} {M : Type u_2} [monoid M] [monoid α] [mul_distrib_mul_action α M] (a : α) (S : submonoid M) :
↑(a • S) = a • ↑S
source
theorem submonoid.smul_mem_pointwise_smul {α : Type u_1} {M : Type u_2} [monoid M] [monoid α] [mul_distrib_mul_action α M] (m : M) (a : α) (S : submonoid M) :
m ∈ S → a • m ∈ a • S
source
theorem submonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {M : Type u_2} [monoid M] [monoid α] [mul_distrib_mul_action α M] (m : M) (a : α) (S : submonoid M) :
m ∈ a • S ↔ ∃ (s : M), s ∈ S ∧ a • s = m
source
@[protected, instance]
def submonoid.pointwise_central_scalar {α : Type u_1} {M : Type u_2} [monoid M] [monoid α] [mul_distrib_mul_action α M] [mul_distrib_mul_action αᵐᵒᵖ M] [is_central_scalar α M] :
is_central_scalar α (submonoid M)
source
@[simp]
theorem submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S : submonoid M} {x : M} :
a • x ∈ a • S ↔ x ∈ S
source
theorem submonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S : submonoid M} {x : M} :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem submonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S : submonoid M} {x : M} :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem submonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S T : submonoid M} :
a • S ≤ a • T ↔ S ≤ T
source
theorem submonoid.pointwise_smul_subset_iff {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S T : submonoid M} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem submonoid.subset_pointwise_smul_iff {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S T : submonoid M} :
S ≤ a • T ↔ a⁻¹ • S ≤ T
source
@[simp]
theorem submonoid.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a ≠ 0) (S : submonoid M) (x : M) :
a • x ∈ a • S ↔ x ∈ S
source
theorem submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a ≠ 0) (S : submonoid M) (x : M) :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem submonoid.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a ≠ 0) (S : submonoid M) (x : M) :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem submonoid.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a ≠ 0) {S T : submonoid M} :
a • S ≤ a • T ↔ S ≤ T
source
theorem submonoid.pointwise_smul_le_iff₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a ≠ 0) {S T : submonoid M} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem submonoid.le_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a ≠ 0) {S T : submonoid M} :
S ≤ a • T ↔ a⁻¹ • S ≤ T
source
theorem add_submonoid.mem_closure_neg {G : Type u_1} [add_group G] (S : set G) (x : G) :
x ∈ add_submonoid.closure (-S) ↔ -x ∈ add_submonoid.closure S
source
theorem submonoid.mem_closure_inv {G : Type u_1} [group G] (S : set G) (x : G) :
x ∈ submonoid.closure S⁻¹ ↔ x⁻¹ ∈ submonoid.closure S
source
@[protected, instance]
def add_submonoid.pointwise_mul_action {α : Type u_1} {A : Type u_4} [add_monoid A] [monoid α] [distrib_mul_action α A] :
mul_action α (add_submonoid A)

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

This is available as an instance in the pointwise locale.

Equations
source
@[simp]
theorem add_submonoid.coe_pointwise_smul {α : Type u_1} {A : Type u_4} [add_monoid A] [monoid α] [distrib_mul_action α A] (a : α) (S : add_submonoid A) :
↑(a • S) = a • ↑S
source
theorem add_submonoid.smul_mem_pointwise_smul {α : Type u_1} {A : Type u_4} [add_monoid A] [monoid α] [distrib_mul_action α A] (m : A) (a : α) (S : add_submonoid A) :
m ∈ S → a • m ∈ a • S
source
@[protected, instance]
def add_submonoid.pointwise_central_scalar {α : Type u_1} {A : Type u_4} [add_monoid A] [monoid α] [distrib_mul_action α A] [distrib_mul_action αᵐᵒᵖ A] [is_central_scalar α A] :
is_central_scalar α (add_submonoid A)
source
@[simp]
theorem add_submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {A : Type u_4} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S : add_submonoid A} {x : A} :
a • x ∈ a • S ↔ x ∈ S
source
theorem add_submonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {A : Type u_4} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S : add_submonoid A} {x : A} :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem add_submonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {A : Type u_4} [add_monoid A] [group α] [distrib_mul_action α A] (m : A) (a : α) (S : add_submonoid A) :
m ∈ a • S ↔ ∃ (s : A), s ∈ S ∧ a • s = m
source
theorem add_submonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {A : Type u_4} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S : add_submonoid A} {x : A} :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem add_submonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {A : Type u_4} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S T : add_submonoid A} :
a • S ≤ a • T ↔ S ≤ T
source
theorem add_submonoid.pointwise_smul_le_iff {α : Type u_1} {A : Type u_4} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S T : add_submonoid A} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem add_submonoid.le_pointwise_smul_iff {α : Type u_1} {A : Type u_4} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S T : add_submonoid A} :
S ≤ a • T ↔ a⁻¹ • S ≤ T
source
@[simp]
theorem add_submonoid.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_4} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) (S : add_submonoid A) (x : A) :
a • x ∈ a • S ↔ x ∈ S
source
theorem add_submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {A : Type u_4} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) (S : add_submonoid A) (x : A) :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem add_submonoid.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_4} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) (S : add_submonoid A) (x : A) :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem add_submonoid.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_4} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) {S T : add_submonoid A} :
a • S ≤ a • T ↔ S ≤ T
source
theorem add_submonoid.pointwise_smul_le_iff₀ {α : Type u_1} {A : Type u_4} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) {S T : add_submonoid A} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem add_submonoid.le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_4} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) {S T : add_submonoid A} :
S ≤ a • T ↔ a⁻¹ • S ≤ T