# Documentation

Mathlib.GroupTheory.Submonoid.Pointwise

# Pointwise instances on Submonoids and AddSubmonoids #

This file provides:

• Submonoid.inv
• AddSubmonoid.neg

and the actions

• Submonoid.pointwiseMulAction
• AddSubmonoid.pointwiseMulAction

which matches the action of Set.mulActionSet.

These are all available in the Pointwise locale.

Additionally, it provides various degrees of monoid structure:

• AddSubmonoid.one
• AddSubmonoid.mul
• AddSubmonoid.mulOneClass
• AddSubmonoid.semigroup
• AddSubmonoid.monoid which is available globally to match the monoid structure implied by Submodule.idemSemiring.

## 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 GroupTheory.Submonoid.Basic, but currently we cannot because that file is imported by this.

theorem AddSubmonoid.add_subset {M : Type u_3} [] {s : Set M} {t : Set M} {S : } (hs : s S) (ht : t S) :
s + t S
theorem Submonoid.mul_subset {M : Type u_3} [] {s : Set M} {t : Set M} {S : } (hs : s S) (ht : t S) :
s * t S
theorem AddSubmonoid.add_subset_closure {M : Type u_3} [] {s : Set M} {t : Set M} {u : Set M} (hs : s u) (ht : t u) :
s + t ↑()
theorem Submonoid.mul_subset_closure {M : Type u_3} [] {s : Set M} {t : Set M} {u : Set M} (hs : s u) (ht : t u) :
s * t ↑()
s + s = s
theorem Submonoid.coe_mul_self_eq {M : Type u_3} [] (s : ) :
s * s = s
theorem AddSubmonoid.closure_add_le {M : Type u_3} [] (S : Set M) (T : Set M) :
abbrev AddSubmonoid.closure_add_le.match_1 {M : Type u_1} [] (S : Set M) (T : Set M) (_x : M) (motive : _x S + TProp) :
(x : _x S + T) → ((_s _t : M) → (hs : _s S) → (ht : _t T) → (hx : (fun x x_1 => x + x_1) _s _t = _x) → motive (_ : a b, a S b T (fun x x_1 => x + x_1) a b = _x)) → motive x
Instances For
theorem Submonoid.closure_mul_le {M : Type u_3} [] (S : Set M) (T : Set M) :
theorem AddSubmonoid.sup_eq_closure {M : Type u_3} [] (H : ) (K : ) :
H K = AddSubmonoid.closure (H + K)
theorem Submonoid.sup_eq_closure {M : Type u_3} [] (H : ) (K : ) :
H K = Submonoid.closure (H * K)
theorem AddSubmonoid.nsmul_vadd_mem_closure_vadd {M : Type u_3} [] {N : Type u_6} [] [] [] (r : M) (s : Set N) {x : N} (hx : ) :
n, n r +ᵥ x AddSubmonoid.closure (r +ᵥ s)
theorem Submonoid.pow_smul_mem_closure_smul {M : Type u_3} [] {N : Type u_6} [] [] [] (r : M) (s : Set N) {x : N} (hx : ) :
n, r ^ n x Submonoid.closure (r s)
def AddSubmonoid.neg {G : Type u_2} [] :
Neg ()

The additive submonoid with every element negated.

Instances For
theorem AddSubmonoid.neg.proof_2 {G : Type u_1} [] (S : ) :
0 -S
theorem AddSubmonoid.neg.proof_1 {G : Type u_1} [] (S : ) :
∀ {a b : G}, a -Sb -Sa + b -S
def Submonoid.inv {G : Type u_2} [] :
Inv ()

The submonoid with every element inverted.

Instances For
@[simp]
theorem AddSubmonoid.coe_neg {G : Type u_2} [] (S : ) :
↑(-S) = -S
@[simp]
theorem Submonoid.coe_inv {G : Type u_2} [] (S : ) :
S⁻¹ = (S)⁻¹
@[simp]
theorem AddSubmonoid.mem_neg {G : Type u_2} [] {g : G} {S : } :
g -S -g S
@[simp]
theorem Submonoid.mem_inv {G : Type u_2} [] {g : G} {S : } :
def AddSubmonoid.involutiveNeg {G : Type u_2} [] :

Inversion is involutive on additive submonoids.

Instances For
theorem AddSubmonoid.involutiveNeg.proof_2 {G : Type u_1} [] :
∀ (x : ), ↑(-x) = ↑(-x)
def Submonoid.involutiveInv {G : Type u_2} [] :

Inversion is involutive on submonoids.

Instances For
@[simp]
theorem AddSubmonoid.neg_le_neg {G : Type u_2} [] (S : ) (T : ) :
-S -T S T
@[simp]
theorem Submonoid.inv_le_inv {G : Type u_2} [] (S : ) (T : ) :
theorem AddSubmonoid.neg_le {G : Type u_2} [] (S : ) (T : ) :
-S T S -T
theorem Submonoid.inv_le {G : Type u_2} [] (S : ) (T : ) :
def AddSubmonoid.negOrderIso {G : Type u_2} [] :

Pointwise negation of additive submonoids as an order isomorphism

Instances For
@[simp]
theorem Submonoid.invOrderIso_symm_apply_coe {G : Type u_2} [] :
∀ (a : ), ↑(↑(RelIso.symm Submonoid.invOrderIso) a) = (a)⁻¹
@[simp]
theorem Submonoid.invOrderIso_apply_coe {G : Type u_2} [] :
∀ (a : ), ↑(Submonoid.invOrderIso a) = (a)⁻¹
@[simp]
theorem AddSubmonoid.negOrderIso_apply_coe {G : Type u_2} [] :
∀ (a : ), ↑(AddSubmonoid.negOrderIso a) = -a
@[simp]
theorem AddSubmonoid.negOrderIso_symm_apply_coe {G : Type u_2} [] :
∀ (a : ), ↑(↑(RelIso.symm AddSubmonoid.negOrderIso) a) = -a
def Submonoid.invOrderIso {G : Type u_2} [] :

Pointwise inversion of submonoids as an order isomorphism.

Instances For
theorem AddSubmonoid.closure_neg {G : Type u_2} [] (s : Set G) :
theorem Submonoid.closure_inv {G : Type u_2} [] (s : Set G) :
@[simp]
theorem AddSubmonoid.neg_inf {G : Type u_2} [] (S : ) (T : ) :
-(S T) = -S -T
@[simp]
theorem Submonoid.inv_inf {G : Type u_2} [] (S : ) (T : ) :
@[simp]
theorem AddSubmonoid.neg_sup {G : Type u_2} [] (S : ) (T : ) :
-(S T) = -S -T
@[simp]
theorem Submonoid.inv_sup {G : Type u_2} [] (S : ) (T : ) :
@[simp]
theorem AddSubmonoid.neg_bot {G : Type u_2} [] :
@[simp]
theorem Submonoid.inv_bot {G : Type u_2} [] :
@[simp]
theorem AddSubmonoid.neg_top {G : Type u_2} [] :
@[simp]
theorem Submonoid.inv_top {G : Type u_2} [] :
@[simp]
theorem AddSubmonoid.neg_iInf {G : Type u_2} [] {ι : Sort u_6} (S : ι) :
-⨅ (i : ι), S i = ⨅ (i : ι), -S i
@[simp]
theorem Submonoid.inv_iInf {G : Type u_2} [] {ι : Sort u_6} (S : ι) :
(⨅ (i : ι), S i)⁻¹ = ⨅ (i : ι), (S i)⁻¹
@[simp]
theorem AddSubmonoid.neg_iSup {G : Type u_2} [] {ι : Sort u_6} (S : ι) :
-⨆ (i : ι), S i = ⨆ (i : ι), -S i
@[simp]
theorem Submonoid.inv_iSup {G : Type u_2} [] {ι : Sort u_6} (S : ι) :
(⨆ (i : ι), S i)⁻¹ = ⨆ (i : ι), (S i)⁻¹
def Submonoid.pointwiseMulAction {α : Type u_1} {M : Type u_3} [] [] [] :
MulAction α ()

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

This is available as an instance in the Pointwise locale.

Instances For
@[simp]
theorem Submonoid.coe_pointwise_smul {α : Type u_1} {M : Type u_3} [] [] [] (a : α) (S : ) :
↑(a S) = a S
theorem Submonoid.smul_mem_pointwise_smul {α : Type u_1} {M : Type u_3} [] [] [] (m : M) (a : α) (S : ) :
m Sa m a S
theorem Submonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {M : Type u_3} [] [] [] (m : M) (a : α) (S : ) :
m a S s, s S a s = m
@[simp]
theorem Submonoid.smul_bot {α : Type u_1} {M : Type u_3} [] [] [] (a : α) :
theorem Submonoid.smul_sup {α : Type u_1} {M : Type u_3} [] [] [] (a : α) (S : ) (T : ) :
a (S T) = a S a T
theorem Submonoid.smul_closure {α : Type u_1} {M : Type u_3} [] [] [] (a : α) (s : Set M) :
theorem Submonoid.pointwise_isCentralScalar {α : Type u_1} {M : Type u_3} [] [] [] [] [] :
@[simp]
theorem Submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [] [] [] {a : α} {S : } {x : M} :
a x a S x S
theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {M : Type u_3} [] [] [] {a : α} {S : } {x : M} :
x a S a⁻¹ x S
theorem Submonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [] [] [] {a : α} {S : } {x : M} :
x a⁻¹ S a x S
@[simp]
theorem Submonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [] [] [] {a : α} {S : } {T : } :
a S a T S T
theorem Submonoid.pointwise_smul_subset_iff {α : Type u_1} {M : Type u_3} [] [] [] {a : α} {S : } {T : } :
a S T S a⁻¹ T
theorem Submonoid.subset_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [] [] [] {a : α} {S : } {T : } :
S a T a⁻¹ S T
@[simp]
theorem Submonoid.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [] [] [] {a : α} (ha : a 0) (S : ) (x : M) :
a x a S x S
theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {M : Type u_3} [] [] [] {a : α} (ha : a 0) (S : ) (x : M) :
x a S a⁻¹ x S
theorem Submonoid.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [] [] [] {a : α} (ha : a 0) (S : ) (x : M) :
x a⁻¹ S a x S
@[simp]
theorem Submonoid.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
a S a T S T
theorem Submonoid.pointwise_smul_le_iff₀ {α : Type u_1} {M : Type u_3} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
a S T S a⁻¹ T
theorem Submonoid.le_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
S a T a⁻¹ S T
theorem AddSubmonoid.mem_closure_neg {G : Type u_6} [] (S : Set G) (x : G) :
theorem Submonoid.mem_closure_inv {G : Type u_6} [] (S : Set G) (x : G) :
def AddSubmonoid.pointwiseMulAction {α : Type u_1} {A : Type u_5} [] [] [] :

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

This is available as an instance in the Pointwise locale.

Instances For
@[simp]
theorem AddSubmonoid.coe_pointwise_smul {α : Type u_1} {A : Type u_5} [] [] [] (a : α) (S : ) :
↑(a S) = a S
theorem AddSubmonoid.smul_mem_pointwise_smul {α : Type u_1} {A : Type u_5} [] [] [] (m : A) (a : α) (S : ) :
m Sa m a S
theorem AddSubmonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {A : Type u_5} [] [] [] (m : A) (a : α) (S : ) :
m a S s, s S a s = m
@[simp]
theorem AddSubmonoid.smul_bot {α : Type u_1} {A : Type u_5} [] [] [] (a : α) :
theorem AddSubmonoid.smul_sup {α : Type u_1} {A : Type u_5} [] [] [] (a : α) (S : ) (T : ) :
a (S T) = a S a T
@[simp]
theorem AddSubmonoid.smul_closure {α : Type u_1} {A : Type u_5} [] [] [] (a : α) (s : Set A) :
theorem AddSubmonoid.pointwise_isCentralScalar {α : Type u_1} {A : Type u_5} [] [] [] [] [] :
@[simp]
theorem AddSubmonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [] [] [] {a : α} {S : } {x : A} :
a x a S x S
theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {A : Type u_5} [] [] [] {a : α} {S : } {x : A} :
x a S a⁻¹ x S
theorem AddSubmonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [] [] [] {a : α} {S : } {x : A} :
x a⁻¹ S a x S
@[simp]
theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [] [] [] {a : α} {S : } {T : } :
a S a T S T
theorem AddSubmonoid.pointwise_smul_le_iff {α : Type u_1} {A : Type u_5} [] [] [] {a : α} {S : } {T : } :
a S T S a⁻¹ T
theorem AddSubmonoid.le_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [] [] [] {a : α} {S : } {T : } :
S a T a⁻¹ S T
@[simp]
theorem AddSubmonoid.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [] [] [] {a : α} (ha : a 0) (S : ) (x : A) :
a x a S x S
theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {A : Type u_5} [] [] [] {a : α} (ha : a 0) (S : ) (x : A) :
x a S a⁻¹ x S
theorem AddSubmonoid.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [] [] [] {a : α} (ha : a 0) (S : ) (x : A) :
x a⁻¹ S a x S
@[simp]
theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
a S a T S T
theorem AddSubmonoid.pointwise_smul_le_iff₀ {α : Type u_1} {A : Type u_5} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
a S T S a⁻¹ T
theorem AddSubmonoid.le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [] [] [] {a : α} (ha : a 0) {S : } {T : } :
S a T a⁻¹ S T

### Elementwise monoid structure of additive submonoids #

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

def AddSubmonoid.one {R : Type u_4} [] :
One ()

If R is an additive monoid with one (e.g., a semiring), then 1 : AddSubmonoid R is the range of Nat.cast : ℕ → R.

Instances For
theorem AddSubmonoid.one_eq_mrange {R : Type u_4} [] :
theorem AddSubmonoid.natCast_mem_one {R : Type u_4} [] (n : ) :
n 1
@[simp]
theorem AddSubmonoid.mem_one {R : Type u_4} [] {x : R} :
x 1 n, n = x
def AddSubmonoid.mul {R : Type u_4} :
Mul ()

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.

Instances For
theorem AddSubmonoid.mul_mem_mul {R : Type u_4} {M : } {N : } {m : R} {n : R} (hm : m M) (hn : n N) :
m * n M * N
theorem AddSubmonoid.mul_le {R : Type u_4} {M : } {N : } {P : } :
M * N P ∀ (m : R), m M∀ (n : R), n Nm * n P
theorem AddSubmonoid.mul_induction_on {R : Type u_4} {M : } {N : } {C : RProp} {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 AddSubmonoid.closure_mul_closure {R : Type u_4} (S : Set R) (T : Set R) :
theorem AddSubmonoid.mul_eq_closure_mul_set {R : Type u_4} (M : ) (N : ) :
M * N = AddSubmonoid.closure (M * N)
@[simp]
theorem AddSubmonoid.mul_bot {R : Type u_4} (S : ) :
@[simp]
theorem AddSubmonoid.bot_mul {R : Type u_4} (S : ) :
theorem AddSubmonoid.mul_le_mul {R : Type u_4} {M : } {N : } {P : } {Q : } (hmp : M P) (hnq : N Q) :
M * N P * Q
theorem AddSubmonoid.mul_le_mul_left {R : Type u_4} {M : } {N : } {P : } (h : M N) :
M * P N * P
theorem AddSubmonoid.mul_le_mul_right {R : Type u_4} {M : } {N : } {P : } (h : N P) :
M * N M * P
theorem AddSubmonoid.mul_subset_mul {R : Type u_4} {M : } {N : } :
M * N ↑(M * N)

AddSubmonoid.neg distributes over multiplication.

This is available as an instance in the Pointwise locale.

Instances For
def AddSubmonoid.mulOneClass {R : Type u_4} [] :

A MulOneClass structure on additive submonoids of a (possibly, non-associative) semiring.

Instances For

Semigroup structure on additive submonoids of a (possibly, non-unital) semiring.

Instances For
def AddSubmonoid.monoid {R : Type u_4} [] :

Monoid structure on additive submonoids of a semiring.

Instances For
theorem AddSubmonoid.closure_pow {R : Type u_4} [] (s : Set R) (n : ) :
theorem AddSubmonoid.pow_eq_closure_pow_set {R : Type u_4} [] (s : ) (n : ) :
s ^ n = AddSubmonoid.closure (s ^ n)
theorem AddSubmonoid.pow_subset_pow {R : Type u_4} [] {s : } {n : } :
s ^ n ↑(s ^ n)
theorem Set.IsPwo.addSubmonoid_closure {α : Type u_1} {s : Set α} (hpos : ∀ (x : α), x s0 x) (h : ) :
theorem Set.IsPwo.submonoid_closure {α : Type u_1} {s : Set α} (hpos : ∀ (x : α), x s1 x) (h : ) :