# mathlibdocumentation

group_theory.submonoid.basic

# Submonoids: definition and complete_lattice structure

This file defines bundled multiplicative and additive submonoids. We also define a complete_lattice structure on submonoids, define the closure of a set as the minimal submonoid that includes this set, and prove a few results about extending properties from a dense set (i.e. a set with closure s = ⊤) to the whole monoid, see submonoid.dense_induction and monoid_hom.of_mdense.

## Main definitions

• submonoid M: the type of bundled submonoids of a monoid M; the underlying set is given in the carrier field of the structure, and should be accessed through coercion as in (S : set M).
• add_submonoid M : the type of bundled submonoids of an additive monoid M.

For each of the following definitions in the submonoid namespace, there is a corresponding definition in the add_submonoid namespace.

• submonoid.copy : copy of a submonoid with carrier replaced by a set that is equal but possibly not definitionally equal to the carrier of the original submonoid.
• submonoid.closure : monoid closure of a set, i.e., the least submonoid that includes the set.
• submonoid.gi : closure : set M → submonoid M and coercion coe : submonoid M → set M form a galois_insertion;
• monoid_hom.eq_mlocus: the submonoid of elements x : M such that f x = g x;
• monoid_hom.of_mdense: if a map f : M → N between two monoids satisfies f 1 = 1 and f (x * y) = f x * f y for y from some dense set s, then f is a monoid homomorphism. E.g., if f : ℕ → M satisfies f 0 = 0 and f (x + 1) = f x + f 1, then f is an additive monoid homomorphism.

## Implementation notes

Submonoid inclusion is denoted ≤ rather than ⊆, although ∈ is defined as membership of a submonoid's underlying set.

This file is designed to have very few dependencies. In particular, it should not use natural numbers.

## Tags

submonoid, submonoids

structure submonoid (M : Type u_3) [monoid M] :
Type u_3

A submonoid of a monoid M is a subset containing 1 and closed under multiplication.

Type u_3

An additive submonoid of an additive monoid M is a subset containing 0 and closed under addition.

@[instance]
(set M)

@[instance]
def submonoid.set.has_coe {M : Type u_1} [monoid M] :

Equations
@[instance]
def submonoid.has_coe_to_sort {M : Type u_1} [monoid M] :

Equations
@[instance]

@[instance]
def submonoid.has_mem {M : Type u_1} [monoid M] :

Equations
@[instance]

@[simp]
x s.carrier x s

@[simp]
theorem submonoid.mem_carrier {M : Type u_1} [monoid M] {s : submonoid M} {x : M} :
x s.carrier x s

@[simp]
m S m S

@[simp]
theorem submonoid.mem_coe {M : Type u_1} [monoid M] {S : submonoid M} {m : M} :
m S m S

@[simp]

@[simp]
theorem submonoid.coe_coe {M : Type u_1} [monoid M] (s : submonoid M) :

theorem add_submonoid.exists {M : Type u_1} [add_monoid M] {s : add_submonoid M} {p : s → Prop} :
(∃ (x : s), p x) ∃ (x : M) (H : x s), p x, H⟩

theorem submonoid.exists {M : Type u_1} [monoid M] {s : submonoid M} {p : s → Prop} :
(∃ (x : s), p x) ∃ (x : M) (H : x s), p x, H⟩

theorem add_submonoid.forall {M : Type u_1} [add_monoid M] {s : add_submonoid M} {p : s → Prop} :
(∀ (x : s), p x) ∀ (x : M) (H : x s), p x, H⟩

theorem submonoid.forall {M : Type u_1} [monoid M] {s : submonoid M} {p : s → Prop} :
(∀ (x : s), p x) ∀ (x : M) (H : x s), p x, H⟩

theorem submonoid.ext' {M : Type u_1} [monoid M] ⦃S T : submonoid M⦄ :
S = TS = T

Two submonoids are equal if the underlying subsets are equal.

S = TS = T

Two add_submonoids are equal if the underlying subsets are equal.

theorem submonoid.ext'_iff {M : Type u_1} [monoid M] {S T : submonoid M} :
S = T S = T

Two submonoids are equal if and only if the underlying subsets are equal.

S = T S = T

Two add_submonoids are equal if and only if the underlying subsets are equal.

@[ext]
(∀ (x : M), x S x T)S = T

Two add_submonoids are equal if they have the same elements.

@[ext]
theorem submonoid.ext {M : Type u_1} [monoid M] {S T : submonoid M} :
(∀ (x : M), x S x T)S = T

Two submonoids are equal if they have the same elements.

def submonoid.copy {M : Type u_1} [monoid M] (S : submonoid M) (s : set M) :
s = S

Copy a submonoid replacing carrier with a set that is equal to it.

Equations
def add_submonoid.copy {M : Type u_1} [add_monoid M] (S : add_submonoid M) (s : set M) :
s = S

Copy an additive submonoid replacing carrier with a set that is equal to it.

@[simp]
theorem add_submonoid.coe_copy {M : Type u_1} [add_monoid M] {S : add_submonoid M} {s : set M} (hs : s = S) :
(S.copy s hs) = s

@[simp]
theorem submonoid.coe_copy {M : Type u_1} [monoid M] {S : submonoid M} {s : set M} (hs : s = S) :
(S.copy s hs) = s

theorem submonoid.copy_eq {M : Type u_1} [monoid M] {S : submonoid M} {s : set M} (hs : s = S) :
S.copy s hs = S

theorem add_submonoid.copy_eq {M : Type u_1} [add_monoid M] {S : add_submonoid M} {s : set M} (hs : s = S) :
S.copy s hs = S

theorem submonoid.one_mem {M : Type u_1} [monoid M] (S : submonoid M) :
1 S

A submonoid contains the monoid's 1.

0 S

An add_submonoid contains the monoid's 0.

x Sy Sx + y S

An add_submonoid is closed under addition.

theorem submonoid.mul_mem {M : Type u_1} [monoid M] (S : submonoid M) {x y : M} :
x Sy Sx * y S

A submonoid is closed under multiplication.

theorem submonoid.coe_injective {M : Type u_1} [monoid M] (S : submonoid M) :

@[simp]
theorem submonoid.coe_eq_coe {M : Type u_1} [monoid M] (S : submonoid M) (x y : S) :
x = y x = y

@[simp]
theorem add_submonoid.coe_eq_coe {M : Type u_1} [add_monoid M] (S : add_submonoid M) (x y : S) :
x = y x = y

@[instance]

@[instance]
def submonoid.has_le {M : Type u_1} [monoid M] :

Equations
S T ∀ ⦃x : M⦄, x Sx T

theorem submonoid.le_def {M : Type u_1} [monoid M] {S T : submonoid M} :
S T ∀ ⦃x : M⦄, x Sx T

@[simp]
theorem submonoid.coe_subset_coe {M : Type u_1} [monoid M] {S T : submonoid M} :
S T S T

@[simp]
S T S T

@[instance]
def submonoid.partial_order {M : Type u_1} [monoid M] :

Equations
@[instance]

@[simp]
theorem submonoid.coe_ssubset_coe {M : Type u_1} [monoid M] {S T : submonoid M} :
S T S < T

@[simp]
S T S < T

@[instance]
def submonoid.has_top {M : Type u_1} [monoid M] :

The submonoid M of the monoid M.

Equations
@[instance]

The additive submonoid M of the add_monoid M.

@[instance]

The trivial add_submonoid {0} of an add_monoid M.

@[instance]
def submonoid.has_bot {M : Type u_1} [monoid M] :

The trivial submonoid {1} of an monoid M.

Equations
@[instance]

@[instance]
def submonoid.inhabited {M : Type u_1} [monoid M] :

Equations
@[simp]
theorem submonoid.mem_bot {M : Type u_1} [monoid M] {x : M} :
x x = 1

@[simp]
theorem add_submonoid.mem_bot {M : Type u_1} [add_monoid M] {x : M} :
x x = 0

@[simp]
theorem submonoid.mem_top {M : Type u_1} [monoid M] (x : M) :

@[simp]
theorem add_submonoid.mem_top {M : Type u_1} [add_monoid M] (x : M) :

@[simp]

@[simp]
theorem submonoid.coe_top {M : Type u_1} [monoid M] :

@[simp]
theorem submonoid.coe_bot {M : Type u_1} [monoid M] :
= {1}

@[simp]
= {0}

@[instance]

The inf of two add_submonoids is their intersection.

@[instance]
def submonoid.has_inf {M : Type u_1} [monoid M] :

The inf of two submonoids is their intersection.

Equations
@[simp]
(p p') = p p'

@[simp]
theorem submonoid.coe_inf {M : Type u_1} [monoid M] (p p' : submonoid M) :
(p p') = p p'

@[simp]
theorem add_submonoid.mem_inf {M : Type u_1} [add_monoid M] {p p' : add_submonoid M} {x : M} :
x p p' x p x p'

@[simp]
theorem submonoid.mem_inf {M : Type u_1} [monoid M] {p p' : submonoid M} {x : M} :
x p p' x p x p'

@[instance]
def submonoid.has_Inf {M : Type u_1} [monoid M] :

Equations
@[instance]

@[simp]
theorem submonoid.coe_Inf {M : Type u_1} [monoid M] (S : set (submonoid M)) :
(Inf S) = ⋂ (s : (H : s S), s

@[simp]
theorem add_submonoid.coe_Inf {M : Type u_1} [add_monoid M] (S : set ) :
(Inf S) = ⋂ (s : (H : s S), s

theorem add_submonoid.mem_Inf {M : Type u_1} [add_monoid M] {S : set } {x : M} :
x Inf S ∀ (p : , p Sx p

theorem submonoid.mem_Inf {M : Type u_1} [monoid M] {S : set (submonoid M)} {x : M} :
x Inf S ∀ (p : , p Sx p

theorem submonoid.mem_infi {M : Type u_1} [monoid M] {ι : Sort u_2} {S : ι → } {x : M} :
(x ⨅ (i : ι), S i) ∀ (i : ι), x S i

theorem add_submonoid.mem_infi {M : Type u_1} [add_monoid M] {ι : Sort u_2} {S : ι → } {x : M} :
(x ⨅ (i : ι), S i) ∀ (i : ι), x S i

@[simp]
theorem submonoid.coe_infi {M : Type u_1} [monoid M] {ι : Sort u_2} {S : ι → } :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)

@[simp]
theorem add_submonoid.coe_infi {M : Type u_1} [add_monoid M] {ι : Sort u_2} {S : ι → } :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)

@[instance]
def submonoid.complete_lattice {M : Type u_1} [monoid M] :

Submonoids of a monoid form a complete lattice.

Equations
@[instance]

The add_submonoids of an add_monoid form a complete lattice.

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

The submonoid generated by a set.

Equations
set M

The add_submonoid generated by a set

theorem add_submonoid.mem_closure {M : Type u_1} [add_monoid M] {s : set M} {x : M} :
∀ (S : , s Sx S

theorem submonoid.mem_closure {M : Type u_1} [monoid M] {s : set M} {x : M} :
∀ (S : , s Sx S

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

The submonoid generated by a set includes the set.

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

The add_submonoid generated by a set includes the set.

@[simp]
theorem submonoid.closure_le {M : Type u_1} [monoid M] {s : set M} {S : submonoid M} :
s S

A submonoid S includes closure s if and only if it includes s.

@[simp]
theorem add_submonoid.closure_le {M : Type u_1} [add_monoid M] {s : set M} {S : add_submonoid M} :
s S

An additive submonoid S includes closure s if and only if it includes s

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

Additive submonoid closure of a set is monotone in its argument: if s ⊆ t, then closure s ≤ closure t

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

Submonoid closure of a set is monotone in its argument: if s ⊆ t, then closure s ≤ closure t.

theorem add_submonoid.closure_eq_of_le {M : Type u_1} [add_monoid M] {s : set M} {S : add_submonoid M} :
s S

theorem submonoid.closure_eq_of_le {M : Type u_1} [monoid M] {s : set M} {S : submonoid M} :
s S

theorem submonoid.closure_induction {M : Type u_1} [monoid M] {s : set M} {p : M → Prop} {x : M} :
(∀ (x : M), x sp x)p 1(∀ (x y : M), p xp yp (x * y))p x

An induction principle for closure membership. If p holds for 1 and all elements of s, and is preserved under multiplication, then p holds for all elements of the closure of s.

theorem add_submonoid.closure_induction {M : Type u_1} [add_monoid M] {s : set M} {p : M → Prop} {x : M} :
(∀ (x : M), x sp x)p 0(∀ (x y : M), p xp yp (x + y))p x

An induction principle for additive closure membership. If p holds for 0 and all elements of s, and is preserved under addition, then p holds for all elements of the additive closure of s.

theorem add_submonoid.dense_induction {M : Type u_1} [add_monoid M] {p : M → Prop} (x : M) {s : set M} :
(∀ (x : M), x sp x)p 0(∀ (x y : M), p xp yp (x + y))p x

If s is a dense set in an additive monoid M, add_submonoid.closure s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, verify p 0, and verify that p x and p y imply p (x + y).

theorem submonoid.dense_induction {M : Type u_1} [monoid M] {p : M → Prop} (x : M) {s : set M} :
(∀ (x : M), x sp x)p 1(∀ (x y : M), p xp yp (x * y))p x

If s is a dense set in a monoid M, submonoid.closure s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, verify p 1, and verify that p x and p y imply p (x * y).

closure forms a Galois insertion with the coercion to set.

def submonoid.gi (M : Type u_1) [monoid M] :

closure forms a Galois insertion with the coercion to set.

Equations
@[simp]
theorem submonoid.closure_eq {M : Type u_1} [monoid M] (S : submonoid M) :

Closure of a submonoid S equals S.

@[simp]

Additive closure of an additive submonoid S equals S

@[simp]

@[simp]
theorem submonoid.closure_empty {M : Type u_1} [monoid M] :

@[simp]

@[simp]
theorem submonoid.closure_univ {M : Type u_1} [monoid M] :

theorem submonoid.closure_union {M : Type u_1} [monoid M] (s t : set M) :

theorem add_submonoid.closure_union {M : Type u_1} [add_monoid M] (s t : set M) :

theorem add_submonoid.closure_Union {M : Type u_1} [add_monoid M] {ι : Sort u_2} (s : ι → set M) :
add_submonoid.closure (⋃ (i : ι), s i) = ⨆ (i : ι),

theorem submonoid.closure_Union {M : Type u_1} [monoid M] {ι : Sort u_2} (s : ι → set M) :
submonoid.closure (⋃ (i : ι), s i) = ⨆ (i : ι), submonoid.closure (s i)

def is_unit.submonoid (M : Type u_1) [monoid M] :

The submonoid consisting of the units of a monoid

Equations
theorem is_unit.mem_submonoid_iff {M : Type u_1} [monoid M] (a : M) :

(M →+ N)(M →+ N)

The additive submonoid of elements x : M such that f x = g x

def monoid_hom.eq_mlocus {M : Type u_1} [monoid M] {N : Type u_3} [monoid N] :
(M →* N)(M →* N)

The submonoid of elements x : M such that f x = g x

Equations
theorem monoid_hom.eq_on_mclosure {M : Type u_1} [monoid M] {N : Type u_3} [monoid N] {f g : M →* N} {s : set M} :
g s g

If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.

theorem add_monoid_hom.eq_on_mclosure {M : Type u_1} [add_monoid M] {N : Type u_3} [add_monoid N] {f g : M →+ N} {s : set M} :
g s

theorem monoid_hom.eq_of_eq_on_mtop {M : Type u_1} [monoid M] {N : Type u_3} [monoid N] {f g : M →* N} :
g f = g

theorem add_monoid_hom.eq_of_eq_on_mtop {M : Type u_1} [add_monoid M] {N : Type u_3} [add_monoid N] {f g : M →+ N} :
g f = g

theorem add_monoid_hom.eq_of_eq_on_mdense {M : Type u_1} [add_monoid M] {N : Type u_3} [add_monoid N] {s : set M} (hs : = ) {f g : M →+ N} :
g sf = g

theorem monoid_hom.eq_of_eq_on_mdense {M : Type u_1} [monoid M] {N : Type u_3} [monoid N] {s : set M} (hs : = ) {f g : M →* N} :
g sf = g

def monoid_hom.of_mdense {M : Type u_1} [monoid M] {s : set M} {N : Type u_3} [monoid N] (f : M → N) :
f 1 = 1(∀ (x y : M), y sf (x * y) = (f x) * f y)M →* N

Let s be a subset of a monoid M such that the closure of s is the whole monoid. Then monoid_hom.of_mdense defines a monoid homomorphism from M asking for a proof of f (x * y) = f x * f y only for y ∈ s.

Equations
def add_monoid_hom.of_mdense {M : Type u_1} [add_monoid M] {s : set M} {N : Type u_3} [add_monoid N] (f : M → N) :
f 0 = 0(∀ (x y : M), y sf (x + y) = f x + f y)M →+ N

Let s be a subset of an additive monoid M such that the closure of s is the whole monoid. Then add_monoid_hom.of_mdense defines an additive monoid homomorphism from M asking for a proof of f (x + y) = f x + f y only for y ∈ s.

@[simp]
theorem add_monoid_hom.coe_of_mdense {M : Type u_1} [add_monoid M] {s : set M} {N : Type u_3} [add_monoid N] (f : M → N) (hs : = ) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) :
h1 hmul) = f

@[simp]
theorem monoid_hom.coe_of_mdense {M : Type u_1} [monoid M] {s : set M} {N : Type u_3} [monoid N] (f : M → N) (hs : = ) (h1 : f 1 = 1) (hmul : ∀ (x y : M), y sf (x * y) = (f x) * f y) :
hs h1 hmul) = f