mathlib3 documentation

deprecated.submonoid

Unbundled submonoids (deprecated) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

This file defines unbundled multiplicative and additive submonoids. Instead of using this file, please use submonoid G and add_submonoid A, defined in group_theory.submonoid.basic.

Main definitions #

is_add_submonoid (S : set M) : the predicate that S is the underlying subset of an additive submonoid of M. The bundled variant add_submonoid M should be used in preference to this.

is_submonoid (S : set M) : the predicate that S is the underlying subset of a submonoid of M. The bundled variant submonoid M should be used in preference to this.

Tags #

submonoid, submonoids, is_submonoid

structure is_add_submonoid {A : Type u_2} [add_monoid A] (s : set A) :

Prop

zero_mem : 0 ∈ s
add_mem : ∀ {a b : A}, a ∈ s → b ∈ s → a + b ∈ s

s is an additive submonoid: a set containing 0 and closed under addition. Note that this structure is deprecated, and the bundled variant add_submonoid A should be preferred.

structure is_submonoid {M : Type u_1} [monoid M] (s : set M) :

Prop

one_mem : 1 ∈ s
mul_mem : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s

s is a submonoid: a set containing 1 and closed under multiplication. Note that this structure is deprecated, and the bundled variant submonoid M should be preferred.

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

is_add_submonoid s

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

is_add_submonoid s ↔ is_submonoid s

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

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

is_submonoid s ↔ is_add_submonoid s

theorem is_add_submonoid.inter {M : Type u_1} [add_monoid M] {s₁ s₂ : set M} (is₁ : is_add_submonoid s₁) (is₂ : is_add_submonoid s₂) :

is_add_submonoid (s₁ ∩ s₂)

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

theorem is_submonoid.inter {M : Type u_1} [monoid M] {s₁ s₂ : set M} (is₁ : is_submonoid s₁) (is₂ : is_submonoid s₂) :

is_submonoid (s₁ ∩ s₂)

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

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

is_submonoid (set.Inter s)

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

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

is_add_submonoid (set.Inter s)

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} (hs : ∀ (i : ι), is_add_submonoid (s i)) (directed : ∀ (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} (hs : ∀ (i : ι), is_submonoid (s i)) (directed : ∀ (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 multiples {M : Type u_1} [add_monoid M] (x : M) :

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

Equations

multiples x = {y : M | ∃ (n : ℕ), n • x = y}

def powers {M : Type u_1} [monoid M] (x : M) :

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

Equations

powers x = {y : M | ∃ (n : ℕ), x ^ n = y}

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

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

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

0 ∈ multiples x

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

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

x ∈ multiples x

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

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

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

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

y ∈ powers x → z ∈ powers x → y * z ∈ powers x

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

theorem multiples.add_mem {M : Type u_1} [add_monoid M] {x y z : M} :

y ∈ multiples x → z ∈ multiples x → y + z ∈ multiples x

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

theorem multiples.is_add_submonoid {M : Type u_1} [add_monoid M] (x : M) :

is_add_submonoid (multiples x)

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

theorem powers.is_submonoid {M : Type u_1} [monoid M] (x : M) :

is_submonoid (powers x)

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

theorem univ.is_submonoid {M : Type u_1} [monoid M] :

is_submonoid set.univ

A monoid is a submonoid of itself.

theorem univ.is_add_submonoid {M : Type u_1} [add_monoid M] :

is_add_submonoid set.univ

An add_monoid is an add_submonoid of itself.

theorem is_add_submonoid.preimage {M : Type u_1} [add_monoid M] {N : Type u_2} [add_monoid N] {f : M → N} (hf : is_add_monoid_hom f) {s : set N} (hs : is_add_submonoid s) :

is_add_submonoid (f ⁻¹' s)

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

theorem is_submonoid.preimage {M : Type u_1} [monoid M] {N : Type u_2} [monoid N] {f : M → N} (hf : is_monoid_hom f) {s : set N} (hs : is_submonoid s) :

is_submonoid (f ⁻¹' s)

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

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

is_submonoid (f '' s)

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

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

is_add_submonoid (f '' s)

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

theorem range.is_submonoid {M : Type u_1} [monoid M] {γ : Type u_2} [monoid γ] {f : M → γ} (hf : is_monoid_hom f) :

is_submonoid (set.range f)

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

theorem range.is_add_submonoid {M : Type u_1} [add_monoid M] {γ : Type u_2} [add_monoid γ] {f : M → γ} (hf : is_add_monoid_hom f) :

is_add_submonoid (set.range f)

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

theorem is_add_submonoid.smul_mem {M : Type u_1} [add_monoid M] {s : set M} {a : M} (hs : is_add_submonoid s) (h : a ∈ s) {n : ℕ} :

n • a ∈ s

An add_submonoid is closed under multiplication by naturals.

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

a ^ n ∈ s

Submonoids are closed under natural powers.

theorem is_submonoid.power_subset {M : Type u_1} [monoid M] {s : set M} {a : M} (hs : is_submonoid s) (h : a ∈ s) :

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

theorem is_add_submonoid.multiples_subset {M : Type u_1} [add_monoid M] {s : set M} {a : M} (hs : is_add_submonoid s) (h : a ∈ s) :

multiples a ⊆ s

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} (hs : is_add_submonoid s) {l : list M} :

(∀ (x : M), x ∈ l → x ∈ 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} (hs : is_submonoid s) {l : list M} :

(∀ (x : M), x ∈ l → x ∈ 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} (hs : is_submonoid s) (m : multiset M) :

(∀ (a : M), a ∈ m → a ∈ 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} [add_comm_monoid M] {s : set M} (hs : is_add_submonoid s) (m : multiset M) :

(∀ (a : M), a ∈ m → a ∈ 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} [add_comm_monoid M] {s : set M} (hs : is_add_submonoid s) (f : A → M) (t : finset A) :

(∀ (b : A), b ∈ t → f b ∈ s) → t.sum (λ (b : A), 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} (hs : is_submonoid s) (f : A → M) (t : finset A) :

(∀ (b : A), b ∈ t → f b ∈ s) → t.prod (λ (b : A), f b) ∈ s

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

inductive add_monoid.in_closure {A : Type u_2} [add_monoid A] (s : set A) :

A → Prop

basic : ∀ {A : Type u_2} [_inst_2 : add_monoid A] {s : set A} {a : A}, a ∈ s → add_monoid.in_closure s a
zero : ∀ {A : Type u_2} [_inst_2 : add_monoid A] {s : set A}, add_monoid.in_closure s 0
add : ∀ {A : Type u_2} [_inst_2 : add_monoid A] {s : set A} {a b : A}, add_monoid.in_closure s a → add_monoid.in_closure s b → add_monoid.in_closure s (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] (s : set M) :

M → Prop

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

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

def add_monoid.closure {M : Type u_1} [add_monoid M] (s : set M) :

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

Equations

add_monoid.closure s = {a : M | add_monoid.in_closure s a}

def monoid.closure {M : Type u_1} [monoid M] (s : set M) :

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

Equations

monoid.closure s = {a : M | monoid.in_closure s a}

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

is_submonoid (monoid.closure s)

theorem add_monoid.closure.is_add_submonoid {M : Type u_1} [add_monoid M] (s : set M) :

is_add_submonoid (add_monoid.closure s)

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

s ⊆ add_monoid.closure s

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} :

s ⊆ monoid.closure s

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} (ht : is_submonoid t) (h : s ⊆ t) :

monoid.closure 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} (ht : is_add_submonoid t) (h : s ⊆ t) :

add_monoid.closure 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} (h : s ⊆ t) :

monoid.closure s ⊆ monoid.closure 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} (h : s ⊆ t) :

add_monoid.closure s ⊆ add_monoid.closure 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} :

monoid.closure {x} = powers x

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} :

add_monoid.closure {x} = multiples x

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} (hf : is_monoid_hom f) (s : set M) :

f '' monoid.closure s = monoid.closure (f '' s)

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} (hf : is_add_monoid_hom f) (s : set M) :

f '' add_monoid.closure s = add_monoid.closure (f '' s)

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} (h : a ∈ monoid.closure s) :

∃ (l : list M), (∀ (x : M), x ∈ l → x ∈ 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} (h : a ∈ add_monoid.closure s) :

∃ (l : list M), (∀ (x : M), x ∈ l → x ∈ 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 ∈ monoid.closure s) (z : M) (H : z ∈ monoid.closure t), 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} [add_comm_monoid M] {s t : set M} {x : M} :

x ∈ add_monoid.closure (s ∪ t) ↔ ∃ (y : M) (H : y ∈ add_monoid.closure s) (z : M) (H : z ∈ add_monoid.closure t), 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) :

add_submonoid M

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

Equations

add_submonoid.of h = {carrier := s, add_mem' := _, zero_mem' := _}

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

submonoid.of h = {carrier := s, mul_mem' := _, one_mem' := _}

theorem add_submonoid.is_add_submonoid {M : Type u_1} [add_monoid M] (S : add_submonoid M) :

is_add_submonoid ↑S

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

is_submonoid ↑S