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 various degrees of monoid structure:

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.

Some lemmas about pointwise multiplication and submonoids. Ideally we put these in group_theory.submonoid.basic, but currently we cannot because that file is imported by this.

theorem submonoid.mul_subset {M : Type u_3} [monoid M] {s t : set M} {S : submonoid M} (hs : s S) (ht : t S) :
s * t S
theorem add_submonoid.add_subset {M : Type u_3} [add_monoid M] {s t : set M} {S : add_submonoid M} (hs : s S) (ht : t S) :
s + t S
theorem add_submonoid.add_subset_closure {M : Type u_3} [add_monoid M] {s t u : set M} (hs : s u) (ht : t u) :
theorem submonoid.mul_subset_closure {M : Type u_3} [monoid M] {s t u : set M} (hs : s u) (ht : t u) :
theorem submonoid.coe_mul_self_eq {M : Type u_3} [monoid M] (s : submonoid M) :
theorem submonoid.sup_eq_closure {M : Type u_3} [monoid M] (H K : submonoid M) :
theorem submonoid.pow_smul_mem_closure_smul {M : Type u_3} [monoid M] {N : Type u_1} [comm_monoid N] [mul_action M N] [is_scalar_tower M N N] (r : M) (s : set N) {x : N} (hx : x submonoid.closure s) :
(n : ), r ^ n x submonoid.closure (r s)
theorem add_submonoid.nsmul_vadd_mem_closure_vadd {M : Type u_3} [add_monoid M] {N : Type u_1} [add_comm_monoid N] [add_action M N] [vadd_assoc_class M N N] (r : M) (s : set N) {x : N} (hx : x add_submonoid.closure s) :
@[protected]

The additive submonoid with every element negated.

Equations
@[protected]
def submonoid.has_inv {G : Type u_2} [group G] :

The submonoid with every element inverted.

Equations
@[simp]
theorem add_submonoid.coe_neg {G : Type u_2} [add_group G] (S : add_submonoid G) :
@[simp]
theorem submonoid.coe_inv {G : Type u_2} [group G] (S : submonoid G) :
@[simp]
theorem submonoid.mem_inv {G : Type u_2} [group G] {g : G} {S : submonoid G} :
@[simp]
theorem add_submonoid.mem_neg {G : Type u_2} [add_group G] {g : G} {S : add_submonoid G} :
g -S -g S
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem submonoid.inv_le_inv {G : Type u_2} [group G] (S T : submonoid G) :
@[simp]
theorem add_submonoid.neg_le_neg {G : Type u_2} [add_group G] (S T : add_submonoid G) :
-S -T S T
theorem submonoid.inv_le {G : Type u_2} [group G] (S T : submonoid G) :
theorem add_submonoid.neg_le {G : Type u_2} [add_group G] (S T : add_submonoid G) :
-S T S -T
@[simp]
theorem add_submonoid.neg_inf {G : Type u_2} [add_group G] (S T : add_submonoid G) :
-(S T) = -S -T
@[simp]
theorem submonoid.inv_inf {G : Type u_2} [group G] (S T : submonoid G) :
@[simp]
theorem submonoid.inv_sup {G : Type u_2} [group G] (S T : submonoid G) :
@[simp]
theorem add_submonoid.neg_sup {G : Type u_2} [add_group G] (S T : add_submonoid G) :
-(S T) = -S -T
@[simp]
theorem submonoid.inv_bot {G : Type u_2} [group G] :
@[simp]
theorem add_submonoid.neg_bot {G : Type u_2} [add_group G] :
@[simp]
theorem add_submonoid.neg_top {G : Type u_2} [add_group G] :
@[simp]
theorem submonoid.inv_top {G : Type u_2} [group G] :
@[simp]
theorem submonoid.inv_infi {G : Type u_2} [group G] {ι : Sort u_1} (S : ι submonoid G) :
( (i : ι), S i)⁻¹ = (i : ι), (S i)⁻¹
@[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
@[simp]
theorem submonoid.inv_supr {G : Type u_2} [group G] {ι : Sort u_1} (S : ι submonoid G) :
( (i : ι), S i)⁻¹ = (i : ι), (S i)⁻¹
@[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
@[protected]

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

This is available as an instance in the pointwise locale.

Equations
@[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
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
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
@[simp]
theorem submonoid.smul_bot {α : Type u_1} {M : Type u_3} [monoid M] [monoid α] [mul_distrib_mul_action α M] (a : α) :
theorem submonoid.smul_sup {α : Type u_1} {M : Type u_3} [monoid M] [monoid α] [mul_distrib_mul_action α M] (a : α) (S T : submonoid M) :
a (S T) = a S a T
theorem submonoid.smul_closure {α : Type u_1} {M : Type u_3} [monoid M] [monoid α] [mul_distrib_mul_action α M] (a : α) (s : set M) :
@[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
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
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
@[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
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
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
@[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
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
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
@[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
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
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
@[protected]

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
@[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
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
theorem add_submonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] (m : A) (a : α) (S : add_submonoid A) :
m a S (s : A), s S a s = m
@[simp]
theorem add_submonoid.smul_bot {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] (a : α) :
theorem add_submonoid.smul_sup {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] (a : α) (S T : add_submonoid A) :
a (S T) = a S a T
@[simp]
theorem add_submonoid.smul_closure {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [distrib_mul_action α A] (a : α) (s : set A) :
@[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
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
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
@[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
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
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
@[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
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
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
@[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
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
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 monoid structure of additive submonoids #

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

@[simp]
theorem add_submonoid.mem_one {R : Type u_4} [add_monoid_with_one R] {x : R} :
x 1 (n : ), n = x
@[protected, instance]

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
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
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
@[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
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
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
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
@[protected]

add_submonoid.has_pointwise_neg distributes over multiplication.

This is available as an instance in the pointwise locale.

Equations
theorem add_submonoid.pow_subset_pow {R : Type u_4} [semiring R] {s : add_submonoid R} {n : } :
s ^ n (s ^ n)
theorem set.is_pwo.add_submonoid_closure {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : set α} (hpos : (x : α), x s 0 x) (h : s.is_pwo) :
theorem set.is_pwo.submonoid_closure {α : Type u_1} [ordered_cancel_comm_monoid α] {s : set α} (hpos : (x : α), x s 1 x) (h : s.is_pwo) :