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.

Additionally, it provides add_submonoid.has_mul, which is available globally to match submodule.has_mul.

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_2} [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_2} [group G] :
has_inv (submonoid G)

The submonoid with every element inverted.

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

add_submonoid.has_neg as an order isomorphism

Equations
source
@[simp]
theorem add_submonoid.neg_order_iso_apply_coe {G : Type u_2} [add_group G] (ᾰ : add_submonoid G) :
↑(⇑add_submonoid.neg_order_iso ᾰ) = -↑ᾰ
source
@[simp]
theorem add_submonoid.neg_order_iso_symm_apply_coe {G : Type u_2} [add_group G] (ᾰ : add_submonoid G) :
↑(⇑(rel_iso.symm add_submonoid.neg_order_iso) ᾰ) = -↑ᾰ
source
@[simp]
theorem submonoid.inv_order_iso_symm_apply_coe {G : Type u_2} [group G] (ᾰ : submonoid G) :
↑(⇑(rel_iso.symm submonoid.inv_order_iso) ᾰ) = (↑ᾰ)⁻¹
source
@[simp]
theorem submonoid.inv_order_iso_apply_coe {G : Type u_2} [group G] (ᾰ : submonoid G) :
↑(⇑submonoid.inv_order_iso ᾰ) = (↑ᾰ)⁻¹
source
def submonoid.inv_order_iso {G : Type u_2} [group G] :
submonoid G ≃o submonoid G

submonoid.has_inv as an order isomorphism.

Equations
source
theorem add_submonoid.closure_neg {G : Type u_2} [add_group G] (s : set G) :
add_submonoid.closure (-s) = -add_submonoid.closure s
source
theorem submonoid.closure_inv {G : Type u_2} [group G] (s : set G) :
submonoid.closure s⁻¹ = (submonoid.closure s)⁻¹
source
@[simp]
theorem add_submonoid.neg_inf {G : Type u_2} [add_group G] (S T : add_submonoid G) :
-(S ⊓ T) = -S ⊓ -T
source
@[simp]
theorem submonoid.inv_inf {G : Type u_2} [group G] (S T : submonoid G) :
(S ⊓ T)⁻¹ = S⁻¹ ⊓ T⁻¹
source
@[simp]
theorem submonoid.inv_sup {G : Type u_2} [group G] (S T : submonoid G) :
(S ⊔ T)⁻¹ = S⁻¹ ⊔ T⁻¹
source
@[simp]
theorem add_submonoid.neg_sup {G : Type u_2} [add_group G] (S T : add_submonoid G) :
-(S ⊔ T) = -S ⊔ -T
source
@[simp]
theorem submonoid.inv_bot {G : Type u_2} [group G] :
⊥⁻¹ = ⊥
source
@[simp]
theorem add_submonoid.neg_bot {G : Type u_2} [add_group G] :
-⊥ = ⊥
source
@[simp]
theorem add_submonoid.neg_top {G : Type u_2} [add_group G] :
-⊤ = ⊤
source
@[simp]
theorem submonoid.inv_top {G : Type u_2} [group G] :
⊤⁻¹ = ⊤
source
@[simp]
theorem submonoid.inv_infi {G : Type u_2} [group G] {ι : Sort u_1} (S : ι → submonoid G) :
(⨅ (i : ι), S i)⁻¹ = ⨅ (i : ι), (S i)⁻¹
source
@[simp]
theorem add_submonoid.neg_infi {G : Type u_2} [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_2} [group G] {ι : Sort u_1} (S : ι → submonoid G) :
(⨆ (i : ι), S i)⁻¹ = ⨆ (i : ι), (S i)⁻¹
source
@[simp]
theorem add_submonoid.neg_supr {G : Type u_2} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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

Elementwise multiplication of two additive submonoids #

These definitions are a cut-down versions of the ones around submodule.has_mul, as that API is usually more useful.

source
@[protected, instance]
def add_submonoid.has_mul {R : Type u_4} [non_unital_non_assoc_semiring R] :
has_mul (add_submonoid R)

Multiplication of additive submonoids of a semiring R. The additive submonoid S * T is the smallest R-submodule of R containing the elements s * t for s ∈ S and t ∈ T.

Equations
source
theorem add_submonoid.mul_mem_mul {R : Type u_4} [non_unital_non_assoc_semiring R] {M N : add_submonoid R} {m n : R} (hm : m ∈ M) (hn : n ∈ N) :
m * n ∈ M * N
source
theorem add_submonoid.mul_le {R : Type u_4} [non_unital_non_assoc_semiring R] {M N P : add_submonoid R} :
M * N ≤ P ↔ ∀ (m : R), m ∈ M → ∀ (n : R), n ∈ N → m * n ∈ P
source
@[protected]
theorem add_submonoid.mul_induction_on {R : Type u_4} [non_unital_non_assoc_semiring R] {M N : add_submonoid R} {C : R → Prop} {r : R} (hr : r ∈ M * N) (hm : ∀ (m : R), m ∈ M → ∀ (n : R), n ∈ N → C (m * n)) (ha : ∀ (x y : R), C x → C y → C (x + y)) :
C r
source
theorem add_submonoid.closure_mul_closure (R : Type u_4) [non_unital_non_assoc_semiring R] (S T : set R) :
(add_submonoid.closure S) * add_submonoid.closure T = add_submonoid.closure (S * T)
source
@[simp]
theorem add_submonoid.mul_bot {R : Type u_4} [non_unital_non_assoc_semiring R] (S : add_submonoid R) :
S * ⊥ = ⊥
source
@[simp]
theorem add_submonoid.bot_mul {R : Type u_4} [non_unital_non_assoc_semiring R] (S : add_submonoid R) :
⊥ * S = ⊥
source
theorem add_submonoid.mul_le_mul {R : Type u_4} [non_unital_non_assoc_semiring R] {M N P Q : add_submonoid R} (hmp : M ≤ P) (hnq : N ≤ Q) :
M * N ≤ P * Q
source
theorem add_submonoid.mul_le_mul_left {R : Type u_4} [non_unital_non_assoc_semiring R] {M N P : add_submonoid R} (h : M ≤ N) :
M * P ≤ N * P
source
theorem add_submonoid.mul_le_mul_right {R : Type u_4} [non_unital_non_assoc_semiring R] {M N P : add_submonoid R} (h : N ≤ P) :
M * N ≤ M * P
source
theorem add_submonoid.mul_subset_mul {R : Type u_4} [non_unital_non_assoc_semiring R] {M N : add_submonoid R} :
(↑M) * ↑N ⊆ ↑M * N