# mathlibdocumentation

group_theory.submonoid.pointwise

# Pointwise instances on submonoids and add_submonoids #

This file provides:

• submonoid.has_inv
• add_submonoid.has_neg

and the actions

• submonoid.pointwise_mul_action
• add_submonoid.pointwise_mul_action

which matches the action of mul_action_set.

These are all available in the pointwise locale.

Additionally, it provides various degrees of monoid structure:

• add_submonoid.has_one
• add_submonoid.has_mul
• add_submonoid.mul_one_class
• add_submonoid.semigroup
• add_submonoid.monoid which is available globally to match the monoid structure implied by submodule.semiring.

## 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.

@[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]
@[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]
g -S -g S
@[protected, instance]
def submonoid.has_involutive_inv {G : Type u_2} [group G] :
Equations
@[protected, instance]
Equations
@[simp]
theorem submonoid.inv_le_inv {G : Type u_2} [group G] (S T : submonoid G) :
@[simp]
-S -T S T
theorem submonoid.inv_le {G : Type u_2} [group G] (S T : submonoid G) :
-S T S -T

add_submonoid.has_neg as an order isomorphism

Equations
@[simp]
@[simp]
@[simp]
theorem submonoid.inv_order_iso_symm_apply_coe {G : Type u_2} [group G] (ᾰ : submonoid G) :
@[simp]
theorem submonoid.inv_order_iso_apply_coe {G : Type u_2} [group G] (ᾰ : submonoid G) :
def submonoid.inv_order_iso {G : Type u_2} [group G] :

submonoid.has_inv as an order isomorphism.

Equations
theorem add_submonoid.closure_neg {G : Type u_2} [add_group G] (s : set G) :
theorem submonoid.closure_inv {G : Type u_2} [group G] (s : set G) :
@[simp]
-(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]
-(S T) = -S -T
@[simp]
theorem submonoid.inv_bot {G : Type u_2} [group G] :
@[simp]
@[simp]
@[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 : ι → ) :
(⨅ (i : ι), S i)⁻¹ = ⨅ (i : ι), (S i)⁻¹
@[simp]
theorem add_submonoid.neg_infi {G : Type u_2} [add_group G] {ι : Sort u_1} (S : ι → ) :
(-⨅ (i : ι), S i) = ⨅ (i : ι), -S i
@[simp]
theorem submonoid.inv_supr {G : Type u_2} [group G] {ι : Sort u_1} (S : ι → ) :
(⨆ (i : ι), S i)⁻¹ = ⨆ (i : ι), (S i)⁻¹
@[simp]
theorem add_submonoid.neg_supr {G : Type u_2} [add_group G] {ι : Sort u_1} (S : ι → ) :
(-⨆ (i : ι), S i) = ⨆ (i : ι), -S i
@[protected]
def submonoid.pointwise_mul_action {α : Type u_1} {M : Type u_3} [monoid M] [monoid α]  :

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 α] (a : α) (S : submonoid M) :
(a S) = a S
theorem submonoid.smul_mem_pointwise_smul {α : Type u_1} {M : Type u_3} [monoid M] [monoid α] (m : M) (a : α) (S : submonoid M) :
m Sa m a S
theorem submonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {M : Type u_3} [monoid M] [monoid α] (m : M) (a : α) (S : submonoid M) :
m a S ∃ (s : M), s S a s = m
@[protected, instance]
def submonoid.pointwise_central_scalar {α : Type u_1} {M : Type u_3} [monoid M] [monoid α] [ M] :
@[simp]
theorem submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [monoid M] [group α] {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 α] {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 α] {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 α] {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 α] {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 α] {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] {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] {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] {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] {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] {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] {a : α} (ha : a 0) {S T : submonoid M} :
S a T a⁻¹ S T
theorem add_submonoid.mem_closure_neg {G : Type u_1} [add_group G] (S : set G) (x : G) :
theorem submonoid.mem_closure_inv {G : Type u_1} [group G] (S : set G) (x : G) :
@[protected]
def add_submonoid.pointwise_mul_action {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [ 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
@[simp]
theorem add_submonoid.coe_pointwise_smul {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [ 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 α] [ A] (m : A) (a : α) (S : add_submonoid A) :
m Sa m a S
@[protected, instance]
def add_submonoid.pointwise_central_scalar {α : Type u_1} {A : Type u_5} [add_monoid A] [monoid α] [ A] [ A] :
@[simp]
theorem add_submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [add_monoid A] [group α] [ 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 α] [ A] {a : α} {S : add_submonoid A} {x : A} :
x a S a⁻¹ x S
theorem add_submonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {A : Type u_5} [add_monoid A] [group α] [ A] (m : A) (a : α) (S : add_submonoid A) :
m a S ∃ (s : A), s S a s = m
theorem add_submonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [add_monoid A] [group α] [ 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 α] [ 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 α] [ 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 α] [ 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] [ 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] [ 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] [ 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] [ 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] [ 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] [ 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.

@[protected, instance]
def add_submonoid.has_one {R : Type u_4}  :
Equations
theorem add_submonoid.one_eq_mrange {R : Type u_4}  :
theorem add_submonoid.nat_cast_mem_one {R : Type u_4} (n : ) :
n 1
@[simp]
theorem add_submonoid.mem_one {R : Type u_4} {x : R} :
x 1 ∃ (n : ), n = x
theorem add_submonoid.one_eq_closure {R : Type u_4}  :
theorem add_submonoid.one_eq_closure_one_set {R : Type u_4}  :
@[protected, instance]
def add_submonoid.has_mul {R : Type u_4}  :

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} {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} {M N P : add_submonoid R} :
M * N P ∀ (m : R), m M∀ (n : R), n Nm * n P
@[protected]
theorem add_submonoid.mul_induction_on {R : Type u_4} {M N : add_submonoid R} {C : R → Prop} {r : R} (hr : r M * N) (hm : ∀ (m : R), m M∀ (n : R), n NC (m * n)) (ha : ∀ (x y : R), C xC yC (x + y)) :
C r
theorem add_submonoid.closure_mul_closure {R : Type u_4} (S T : set R) :
@[simp]
@[simp]
theorem add_submonoid.mul_le_mul {R : Type u_4} {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} {M N P : add_submonoid R} (h : M N) :
M * P N * P
theorem add_submonoid.mul_le_mul_right {R : Type u_4} {M N P : add_submonoid R} (h : N P) :
M * N M * P
theorem add_submonoid.mul_subset_mul {R : Type u_4} {M N : add_submonoid R} :
M * N (M * N)
@[protected]
def add_submonoid.has_distrib_neg {R : Type u_4}  :

add_submonoid.has_pointwise_neg distributes over multiplication.

This is available as an instance in the pointwise locale.

Equations
@[protected, instance]
def add_submonoid.mul_one_class {R : Type u_4}  :
Equations
@[protected, instance]
def add_submonoid.semigroup {R : Type u_4}  :
Equations
@[protected, instance]
def add_submonoid.monoid {R : Type u_4} [semiring R] :
Equations
theorem add_submonoid.closure_pow {R : Type u_4} [semiring R] (s : set R) (n : ) :
theorem add_submonoid.pow_eq_closure_pow_set {R : Type u_4} [semiring R] (s : add_submonoid R) (n : ) :
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} {s : set α} (hpos : ∀ (x : α), x s0 x) (h : s.is_pwo) :
theorem set.is_pwo.submonoid_closure {α : Type u_1} {s : set α} (hpos : ∀ (x : α), x s1 x) (h : s.is_pwo) :