# mathlibdocumentation

deprecated.submonoid

# Submonoids

This file defines unbundled multiplicative and additive submonoids (deprecated). For bundled form see group_theory/submonoid.

We some results about images and preimages of submonoids under monoid homomorphisms. These theorems use unbundled monoid homomorphisms (also deprecated).

There are also theorems about the submonoids generated by an element or a subset of a monoid, defined inductively.

## Implementation notes

Unbundled submonoids will slowly be removed from mathlib.

## Tags

submonoid, submonoids, is_submonoid

@[class]
set A → Prop
• zero_mem : 0 s
• add_mem : ∀ {a b : A}, a sb sa + b s

s is an additive submonoid: a set containing 0 and closed under addition.

Instances
@[class]
structure is_submonoid {M : Type u_1} [monoid M] :
set M → Prop
• one_mem : 1 s
• mul_mem : ∀ {a b : M}, a sb sa * b s

s is a submonoid: a set containing 1 and closed under multiplication.

Instances
theorem additive.is_add_submonoid {M : Type u_1} [monoid M] (s : set M) [is_submonoid s] :

theorem additive.is_add_submonoid_iff {M : Type u_1} [monoid M] {s : set M} :

theorem multiplicative.is_submonoid {A : Type u_2} [add_monoid A] (s : set A)  :

theorem multiplicative.is_submonoid_iff {A : Type u_2} [add_monoid A] {s : set A} :

@[instance]

The intersection of two add_submonoids of an add_monoid M is an add_submonoid of M.

@[instance]
def is_submonoid.inter {M : Type u_1} [monoid M] (s₁ s₂ : set M) [is_submonoid s₁] [is_submonoid s₂] :
is_submonoid (s₁ s₂)

The intersection of two submonoids of a monoid M is a submonoid of M.

@[instance]
def is_submonoid.Inter {M : Type u_1} [monoid M] {ι : Sort u_2} (s : ι → set M) [h : ∀ (y : ι), is_submonoid (s y)] :

The intersection of an indexed set of submonoids of a monoid M is a submonoid of M.

@[instance]
def is_add_submonoid.Inter {M : Type u_1} [add_monoid M] {ι : Sort u_2} (s : ι → set M) [h : ∀ (y : ι), is_add_submonoid (s y)] :

The intersection of an indexed set of add_submonoids of an add_monoid M is an add_submonoid of M.

theorem is_add_submonoid_Union_of_directed {M : Type u_1} [add_monoid M] {ι : Type u_2} [hι : nonempty ι] (s : ι → set M) [∀ (i : ι), is_add_submonoid (s i)] :
(∀ (i j : ι), ∃ (k : ι), s i s k s j s k)is_add_submonoid (⋃ (i : ι), s i)

The union of an indexed, directed, nonempty set of add_submonoids of an add_monoid M is an add_submonoid of M.

theorem is_submonoid_Union_of_directed {M : Type u_1} [monoid M] {ι : Type u_2} [hι : nonempty ι] (s : ι → set M) [∀ (i : ι), is_submonoid (s i)] :
(∀ (i j : ι), ∃ (k : ι), s i s k s j s k)is_submonoid (⋃ (i : ι), s i)

The union of an indexed, directed, nonempty set of submonoids of a monoid M is a submonoid of M.

def powers {M : Type u_1} [monoid M] :
M → set M

The set of natural number powers 1, x, x², ... of an element x of a monoid.

Equations
• = {y : M | ∃ (n : ), x ^ n = y}
def multiples {A : Type u_2} [add_monoid A] :
A → set A

The set of natural number multiples 0, x, 2x, ... of an element x of an add_monoid.

Equations
theorem powers.one_mem {M : Type u_1} [monoid M] {x : M} :
1

1 is in the set of natural number powers of an element of a monoid.

theorem multiples.zero_mem {A : Type u_2} [add_monoid A] {x : A} :
0

0 is in the set of natural number multiples of an element of an add_monoid.

theorem powers.self_mem {M : Type u_1} [monoid M] {x : M} :
x

An element of a monoid is in the set of that element's natural number powers.

theorem multiples.self_mem {A : Type u_2} [add_monoid A] {x : A} :
x

An element of an add_monoid is in the set of that element's natural number multiples.

theorem powers.mul_mem {M : Type u_1} [monoid M] {x y z : M} :
y z y * z

The set of natural number powers of an element of a monoid is closed under multiplication.

theorem multiples.add_mem {A : Type u_2} [add_monoid A] {x y z : A} :
y z y + z

The set of natural number multiples of an element of an add_monoid is closed under addition.

@[instance]
def multiples.is_add_submonoid {M : Type u_1} [add_monoid M] (x : M) :

The set of natural number multiples of an element of an add_monoid M is an add_submonoid of M.

@[instance]
def powers.is_submonoid {M : Type u_1} [monoid M] (x : M) :

The set of natural number powers of an element of a monoid M is a submonoid of M.

@[instance]
def univ.is_submonoid {M : Type u_1} [monoid M] :

A monoid is a submonoid of itself.

@[instance]

An add_monoid is an add_submonoid of itself.

@[instance]
def preimage.is_submonoid {M : Type u_1} [monoid M] {N : Type u_2} [monoid N] (f : M → N) (s : set N) [is_submonoid s] :

The preimage of a submonoid under a monoid hom is a submonoid of the domain.

@[instance]
def preimage.is_add_submonoid {M : Type u_1} [add_monoid M] {N : Type u_2} [add_monoid N] (f : M → N) (s : set N)  :

The preimage of an add_submonoid under an add_monoid hom is an add_submonoid of the domain.

@[instance]
theorem image.is_submonoid {M : Type u_1} [monoid M] {γ : Type u_2} [monoid γ] (f : M → γ) (s : set M) [is_submonoid s] :

The image of a submonoid under a monoid hom is a submonoid of the codomain.

@[instance]
theorem image.is_add_submonoid {M : Type u_1} [add_monoid M] {γ : Type u_2} [add_monoid γ] (f : M → γ) (s : set M)  :

The image of an add_submonoid under an add_monoid hom is an add_submonoid of the codomain.

@[instance]
def range.is_submonoid {M : Type u_1} [monoid M] {γ : Type u_2} [monoid γ] (f : M → γ)  :

The image of a monoid hom is a submonoid of the codomain.

@[instance]
def range.is_add_submonoid {M : Type u_1} [add_monoid M] {γ : Type u_2} [add_monoid γ] (f : M → γ)  :

The image of an add_monoid hom is an add_submonoid of the codomain.

theorem is_submonoid.pow_mem {M : Type u_1} [monoid M] {s : set M} {a : M} [is_submonoid s] (h : a s) {n : } :
a ^ n s

Submonoids are closed under natural powers.

theorem is_add_submonoid.smul_mem {A : Type u_2} [add_monoid A] {t : set A} {a : A} (h : a t) {n : } :
n •ℕ a t

An add_submonoid is closed under multiplication by naturals.

theorem is_submonoid.power_subset {M : Type u_1} [monoid M] {s : set M} {a : M} [is_submonoid s] :
a s s

The set of natural number powers of an element of a submonoid is a subset of the submonoid.

theorem is_add_submonoid.multiple_subset {A : Type u_2} [add_monoid A] {t : set A} {a : A}  :
a t t

The set of natural number multiples of an element of an add_submonoid is a subset of the add_submonoid.

theorem is_add_submonoid.list_sum_mem {M : Type u_1} [add_monoid M] {s : set M} {l : list M} :
(∀ (x : M), x lx s)l.sum s

The sum of a list of elements of an add_submonoid is an element of the add_submonoid.

theorem is_submonoid.list_prod_mem {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] {l : list M} :
(∀ (x : M), x lx s)l.prod s

The product of a list of elements of a submonoid is an element of the submonoid.

theorem is_submonoid.multiset_prod_mem {M : Type u_1} [comm_monoid M] (s : set M) [is_submonoid s] (m : multiset M) :
(∀ (a : M), a ma s)m.prod s

The product of a multiset of elements of a submonoid of a comm_monoid is an element of the submonoid.

theorem is_add_submonoid.multiset_sum_mem {M : Type u_1} (s : set M) (m : multiset M) :
(∀ (a : M), a ma s)m.sum s

The sum of a multiset of elements of an add_submonoid of an add_comm_monoid is an element of the add_submonoid.

theorem is_add_submonoid.finset_sum_mem {M : Type u_1} {A : Type u_2} (s : set M) (f : A → M) (t : finset A) :
(∀ (b : A), b tf b s)∑ (b : A) in t, f b s

The sum of elements of an add_submonoid of an add_comm_monoid indexed by a finset is an element of the add_submonoid.

theorem is_submonoid.finset_prod_mem {M : Type u_1} {A : Type u_2} [comm_monoid M] (s : set M) [is_submonoid s] (f : A → M) (t : finset A) :
(∀ (b : A), b tf b s)∏ (b : A) in t, f b s

The product of elements of a submonoid of a comm_monoid indexed by a finset is an element of the submonoid.

def subtype.monoid {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] :

Submonoids are themselves monoids.

Equations
def subtype.add_monoid {M : Type u_1} [add_monoid M] {s : set M}  :

An add_submonoid is itself an add_monoid.

def subtype.add_comm_monoid {M : Type u_1} {s : set M}  :

An add_submonoid of a commutative add_monoid is itself a commutative add_monoid.

def subtype.comm_monoid {M : Type u_1} [comm_monoid M] {s : set M} [is_submonoid s] :

Submonoids of commutative monoids are themselves commutative monoids.

Equations
@[simp]
theorem is_submonoid.coe_one {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] :
1 = 1

Submonoids inherit the 1 of the monoid.

@[simp]
theorem is_add_submonoid.coe_zero {M : Type u_1} [add_monoid M] {s : set M}  :
0 = 0

An add_submonoid inherits the 0 of the add_monoid.

@[simp]
theorem is_add_submonoid.coe_add {M : Type u_1} [add_monoid M] {s : set M} (a b : s) :
(a + b) = a + b

An add_submonoid inherits the addition of the add_monoid.

@[simp]
theorem is_submonoid.coe_mul {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] (a b : s) :
a * b = (a) * b

Submonoids inherit the multiplication of the monoid.

@[simp]
theorem is_submonoid.coe_pow {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] (a : s) (n : ) :
(a ^ n) = a ^ n

Submonoids inherit the exponentiation by naturals of the monoid.

@[simp]
theorem is_add_submonoid.smul_coe {A : Type u_1} [add_monoid A] {s : set A} (a : s) (n : ) :

An add_submonoid inherits the multiplication by naturals of the add_monoid.

@[instance]
def subtype_val.is_add_monoid_hom {M : Type u_1} [add_monoid M] {s : set M}  :

The natural injection from an add_submonoid into the add_monoid is an add_monoid hom.

@[instance]
def subtype_val.is_monoid_hom {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] :

The natural injection from a submonoid into the monoid is a monoid hom.

@[instance]
def coe.is_monoid_hom {M : Type u_1} [monoid M] {s : set M} [is_submonoid s] :

The natural injection from a submonoid into the monoid is a monoid hom.

@[instance]
def coe.is_add_monoid_hom {M : Type u_1} [add_monoid M] {s : set M}  :

The natural injection from an add_submonoid into the add_monoid is an add_monoid hom.

@[instance]
def subtype_mk.is_monoid_hom {M : Type u_1} [monoid M] {s : set M} {γ : Type u_2} [monoid γ] [is_submonoid s] (f : γ → M) (h : ∀ (x : γ), f x s) :
is_monoid_hom (λ (x : γ), f x, _⟩)

Given a monoid hom f : γ → M whose image is contained in a submonoid s, the induced map from γ to s is a monoid hom.

@[instance]
def subtype_mk.is_add_monoid_hom {M : Type u_1} [add_monoid M] {s : set M} {γ : Type u_2} [add_monoid γ] (f : γ → M) (h : ∀ (x : γ), f x s) :
is_add_monoid_hom (λ (x : γ), f x, _⟩)

Given an add_monoid hom f : γ → M whose image is contained in an add_submonoid s, the induced map from γ to s is an add_monoid hom.

@[instance]
def set_inclusion.is_monoid_hom {M : Type u_1} [monoid M] {s : set M} (t : set M) [is_submonoid s] [is_submonoid t] (h : s t) :

Given two submonoids s and t such that s ⊆ t, the natural injection from s into t is a monoid hom.

@[instance]
def set_inclusion.is_add_monoid_hom {M : Type u_1} [add_monoid M] {s : set M} (t : set M) (h : s t) :

Given two add_submonoids s and t such that s ⊆ t, the natural injection from s into t is an add_monoid hom.

set AA → Prop
• basic : ∀ {A : Type u_2} [_inst_2 : (s : set A) {a : A}, a s
• zero : ∀ {A : Type u_2} [_inst_2 : (s : set A),
• add : ∀ {A : Type u_2} [_inst_2 : (s : set A) {a b : A}, (a + b)

The inductively defined membership predicate for the submonoid generated by a subset of a monoid.

inductive monoid.in_closure {M : Type u_1} [monoid M] :
set MM → Prop
• basic : ∀ {M : Type u_1} [_inst_1 : monoid M] (s : set M) {a : M}, a s
• one : ∀ {M : Type u_1} [_inst_1 : monoid M] (s : set M),
• mul : ∀ {M : Type u_1} [_inst_1 : monoid M] (s : set M) {a b : M}, (a * b)

The inductively defined membership predicate for the add_submonoid generated by a subset of an add_monoid.

set Mset M

The inductively defined add_submonoid genrated by a subset of an add_monoid.

def monoid.closure {M : Type u_1} [monoid M] :
set Mset M

The inductively defined submonoid generated by a subset of a monoid.

Equations
• = {a : M |
@[instance]
def monoid.closure.is_submonoid {M : Type u_1} [monoid M] (s : set M) :

@[instance]

theorem add_monoid.subset_closure {M : Type u_1} [add_monoid M] {s : set M} :

A subset of an add_monoid is contained in the add_submonoid it generates.

theorem monoid.subset_closure {M : Type u_1} [monoid M] {s : set M} :

A subset of a monoid is contained in the submonoid it generates.

theorem monoid.closure_subset {M : Type u_1} [monoid M] {s t : set M} [is_submonoid t] :
s t

The submonoid generated by a set is contained in any submonoid that contains the set.

theorem add_monoid.closure_subset {M : Type u_1} [add_monoid M] {s t : set M}  :
s t

The add_submonoid generated by a set is contained in any add_submonoid that contains the set.

theorem monoid.closure_mono {M : Type u_1} [monoid M] {s t : set M} :
s t

Given subsets t and s of a monoid M, if s ⊆ t, the submonoid of M generated by s is contained in the submonoid generated by t.

theorem add_monoid.closure_mono {M : Type u_1} [add_monoid M] {s t : set M} :
s t

Given subsets t and s of an add_monoid M, if s ⊆ t, the add_submonoid of M generated by s is contained in the add_submonoid generated by t.

theorem monoid.closure_singleton {M : Type u_1} [monoid M] {x : M} :
=

The submonoid generated by an element of a monoid equals the set of natural number powers of the element.

theorem add_monoid.closure_singleton {M : Type u_1} [add_monoid M] {x : M} :

The add_submonoid generated by an element of an add_monoid equals the set of natural number multiples of the element.

theorem monoid.image_closure {M : Type u_1} [monoid M] {A : Type u_2} [monoid A] (f : M → A) (s : set M) :

The image under a monoid hom of the submonoid generated by a set equals the submonoid generated by the image of the set under the monoid hom.

theorem add_monoid.image_closure {M : Type u_1} [add_monoid M] {A : Type u_2} [add_monoid A] (f : M → A) (s : set M) :

The image under an add_monoid hom of the add_submonoid generated by a set equals the add_submonoid generated by the image of the set under the add_monoid hom.

theorem monoid.exists_list_of_mem_closure {M : Type u_1} [monoid M] {s : set M} {a : M} :
(∃ (l : list M), (∀ (x : M), x lx s) l.prod = a)

Given an element a of the submonoid of a monoid M generated by a set s, there exists a list of elements of s whose product is a.

theorem add_monoid.exists_list_of_mem_closure {M : Type u_1} [add_monoid M] {s : set M} {a : M} :
(∃ (l : list M), (∀ (x : M), x lx s) l.sum = a)

Given an element a of the add_submonoid of an add_monoid M generated by a set s, there exists a list of elements of s whose sum is a.

theorem monoid.mem_closure_union_iff {M : Type u_1} [comm_monoid M] {s t : set M} {x : M} :
x monoid.closure (s t) ∃ (y : M) (H : y (z : M) (H : z , y * z = x

Given sets s, t of a commutative monoid M, x ∈ M is in the submonoid of M generated by s ∪ t iff there exists an element of the submonoid generated by s and an element of the submonoid generated by t whose product is x.

theorem add_monoid.mem_closure_union_iff {M : Type u_1} {s t : set M} {x : M} :
x add_monoid.closure (s t) ∃ (y : M) (H : (z : M) (H : , y + z = x

Given sets s, t of a commutative add_monoid M, x ∈ M is in the add_submonoid of M generated by s ∪ t iff there exists an element of the add_submonoid generated by s and an element of the add_submonoid generated by t whose sum is x.

def add_submonoid.of {M : Type u_1} [add_monoid M] (s : set M) [h : is_add_submonoid s] :

Create a bundled additive submonoid from a set s and [is_add_submonoid s].

def submonoid.of {M : Type u_1} [monoid M] (s : set M) [h : is_submonoid s] :

Create a bundled submonoid from a set s and [is_submonoid s].

Equations
@[instance]