Submonoids: membership criteria #

In this file we prove various facts about membership in a submonoid:

list_prod_mem, multiset_prod_mem, prod_mem: if each element of a collection belongs to a multiplicative submonoid, then so does their product;
list_sum_mem, multiset_sum_mem, sum_mem: if each element of a collection belongs to an additive submonoid, then so does their sum;
pow_mem, nsmul_mem: if x ∈ S where S is a multiplicative (resp., additive) submonoid and n is a natural number, then x^n (resp., n • x) belongs to S;
mem_supr_of_directed, coe_supr_of_directed, mem_Sup_of_directed_on, coe_Sup_of_directed_on: the supremum of a directed collection of submonoid is their union.
sup_eq_range, mem_sup: supremum of two submonoids S, T of a commutative monoid is the set of products;
closure_singleton_eq, mem_closure_singleton: the multiplicative (resp., additive) closure of {x} consists of powers (resp., natural multiples) of x.

Tags #

submonoid, submonoids

source

@[simp, norm_cast]

theorem add_submonoid.coe_nsmul {M : Type u_1} [add_monoid M] (S : add_submonoid M) (x : ↥S) (n : ℕ) :

↑(n • x) = n • ↑x

source

@[simp, norm_cast]

theorem submonoid.coe_pow {M : Type u_1} [monoid M] (S : submonoid M) (x : ↥S) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

@[simp, norm_cast]

theorem add_submonoid.coe_list_sum {M : Type u_1} [add_monoid M] (S : add_submonoid M) (l : list ↥S) :

↑(l.sum) = (list.map coe l).sum

source

@[simp, norm_cast]

theorem submonoid.coe_list_prod {M : Type u_1} [monoid M] (S : submonoid M) (l : list ↥S) :

↑(l.prod) = (list.map coe l).prod

source

@[simp, norm_cast]

theorem add_submonoid.coe_multiset_sum {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (m : multiset ↥S) :

↑(m.sum) = (multiset.map coe m).sum

source

@[simp, norm_cast]

theorem submonoid.coe_multiset_prod {M : Type u_1} [comm_monoid M] (S : submonoid M) (m : multiset ↥S) :

↑(m.prod) = (multiset.map coe m).prod

source

@[simp, norm_cast]

theorem add_submonoid.coe_finset_sum {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] (S : add_submonoid M) (f : ι → ↥S) (s : finset ι) :

↑∑ (i : ι) in s, f i = ∑ (i : ι) in s, ↑(f i)

source

@[simp, norm_cast]

theorem submonoid.coe_finset_prod {ι : Type u_1} {M : Type u_2} [comm_monoid M] (S : submonoid M) (f : ι → ↥S) (s : finset ι) :

↑∏ (i : ι) in s, f i = ∏ (i : ι) in s, ↑(f i)

source

theorem submonoid.list_prod_mem {M : Type u_1} [monoid M] (S : submonoid M) {l : list M} (hl : ∀ (x : M), x ∈ l → x ∈ S) :

l.prod ∈ S

Product of a list of elements in a submonoid is in the submonoid.

source

theorem add_submonoid.list_sum_mem {M : Type u_1} [add_monoid M] (S : add_submonoid M) {l : list M} (hl : ∀ (x : M), x ∈ l → x ∈ S) :

l.sum ∈ S

Sum of a list of elements in an add_submonoid is in the add_submonoid.

source

theorem submonoid.multiset_prod_mem {M : Type u_1} [comm_monoid M] (S : submonoid M) (m : multiset M) (hm : ∀ (a : M), a ∈ m → a ∈ S) :

m.prod ∈ S

Product of a multiset of elements in a submonoid of a comm_monoid is in the submonoid.

source

theorem add_submonoid.multiset_sum_mem {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (m : multiset M) (hm : ∀ (a : M), a ∈ m → a ∈ S) :

m.sum ∈ S

Sum of a multiset of elements in an add_submonoid of an add_comm_monoid is in the add_submonoid.

source

theorem add_submonoid.sum_mem {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) {ι : Type u_2} {t : finset ι} {f : ι → M} (h : ∀ (c : ι), c ∈ t → f c ∈ S) :

∑ (c : ι) in t, f c ∈ S

Sum of elements in an add_submonoid of an add_comm_monoid indexed by a finset is in the add_submonoid.

source

theorem submonoid.prod_mem {M : Type u_1} [comm_monoid M] (S : submonoid M) {ι : Type u_2} {t : finset ι} {f : ι → M} (h : ∀ (c : ι), c ∈ t → f c ∈ S) :

∏ (c : ι) in t, f c ∈ S

Product of elements of a submonoid of a comm_monoid indexed by a finset is in the submonoid.

source

theorem submonoid.pow_mem {M : Type u_1} [monoid M] (S : submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) :

x ^ n ∈ S

source

theorem add_submonoid.nsmul_mem {M : Type u_1} [add_monoid M] (S : add_submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) :

n • x ∈ S

source

theorem add_submonoid.mem_supr_of_directed {M : Type u_1} [add_zero_class M] {ι : Sort u_2} [hι : nonempty ι] {S : ι → add_submonoid M} (hS : directed has_le.le S) {x : M} :

(x ∈ ⨆ (i : ι), S i) ↔ ∃ (i : ι), x ∈ S i

source

theorem submonoid.mem_supr_of_directed {M : Type u_1} [mul_one_class M] {ι : Sort u_2} [hι : nonempty ι] {S : ι → submonoid M} (hS : directed has_le.le S) {x : M} :

(x ∈ ⨆ (i : ι), S i) ↔ ∃ (i : ι), x ∈ S i

source

theorem add_submonoid.coe_supr_of_directed {M : Type u_1} [add_zero_class M] {ι : Sort u_2} [nonempty ι] {S : ι → add_submonoid M} (hS : directed has_le.le S) :

(↑⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

source

theorem submonoid.coe_supr_of_directed {M : Type u_1} [mul_one_class M] {ι : Sort u_2} [nonempty ι] {S : ι → submonoid M} (hS : directed has_le.le S) :

(↑⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

source

theorem submonoid.mem_Sup_of_directed_on {M : Type u_1} [mul_one_class M] {S : set (submonoid M)} (Sne : S.nonempty) (hS : directed_on has_le.le S) {x : M} :

x ∈ Sup S ↔ ∃ (s : submonoid M) (H : s ∈ S), x ∈ s

source

theorem add_submonoid.mem_Sup_of_directed_on {M : Type u_1} [add_zero_class M] {S : set (add_submonoid M)} (Sne : S.nonempty) (hS : directed_on has_le.le S) {x : M} :

x ∈ Sup S ↔ ∃ (s : add_submonoid M) (H : s ∈ S), x ∈ s

source

theorem add_submonoid.coe_Sup_of_directed_on {M : Type u_1} [add_zero_class M] {S : set (add_submonoid M)} (Sne : S.nonempty) (hS : directed_on has_le.le S) :

↑(Sup S) = ⋃ (s : add_submonoid M) (H : s ∈ S), ↑s

source

theorem submonoid.coe_Sup_of_directed_on {M : Type u_1} [mul_one_class M] {S : set (submonoid M)} (Sne : S.nonempty) (hS : directed_on has_le.le S) :

↑(Sup S) = ⋃ (s : submonoid M) (H : s ∈ S), ↑s

source

theorem submonoid.mem_sup_left {M : Type u_1} [mul_one_class M] {S T : submonoid M} {x : M} :

x ∈ S → x ∈ S ⊔ T

source

theorem add_submonoid.mem_sup_left {M : Type u_1} [add_zero_class M] {S T : add_submonoid M} {x : M} :

x ∈ S → x ∈ S ⊔ T

source

theorem submonoid.mem_sup_right {M : Type u_1} [mul_one_class M] {S T : submonoid M} {x : M} :

x ∈ T → x ∈ S ⊔ T

source

theorem add_submonoid.mem_sup_right {M : Type u_1} [add_zero_class M] {S T : add_submonoid M} {x : M} :

x ∈ T → x ∈ S ⊔ T

source

theorem add_submonoid.add_mem_sup {M : Type u_1} [add_zero_class M] {S T : add_submonoid M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) :

x + y ∈ S ⊔ T

source

theorem submonoid.mul_mem_sup {M : Type u_1} [mul_one_class M] {S T : submonoid M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) :

x * y ∈ S ⊔ T

source

theorem submonoid.mem_supr_of_mem {M : Type u_1} [mul_one_class M] {ι : Type u_2} {S : ι → submonoid M} (i : ι) {x : M} :

x ∈ S i → x ∈ supr S

source

theorem add_submonoid.mem_supr_of_mem {M : Type u_1} [add_zero_class M] {ι : Type u_2} {S : ι → add_submonoid M} (i : ι) {x : M} :

x ∈ S i → x ∈ supr S

source

theorem add_submonoid.mem_Sup_of_mem {M : Type u_1} [add_zero_class M] {S : set (add_submonoid M)} {s : add_submonoid M} (hs : s ∈ S) {x : M} :

x ∈ s → x ∈ Sup S

source

theorem submonoid.mem_Sup_of_mem {M : Type u_1} [mul_one_class M] {S : set (submonoid M)} {s : submonoid M} (hs : s ∈ S) {x : M} :

x ∈ s → x ∈ Sup S

source

theorem free_monoid.closure_range_of {α : Type u_3} :

submonoid.closure (set.range free_monoid.of) = ⊤

source

theorem free_add_monoid.closure_range_of {α : Type u_3} :

add_submonoid.closure (set.range free_add_monoid.of) = ⊤

source

theorem submonoid.closure_singleton_eq {M : Type u_1} [monoid M] (x : M) :

submonoid.closure {x} = (⇑(powers_hom M) x).mrange

source

theorem submonoid.mem_closure_singleton {M : Type u_1} [monoid M] {x y : M} :

y ∈ submonoid.closure {x} ↔ ∃ (n : ℕ), x ^ n = y

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

source

theorem submonoid.mem_closure_singleton_self {M : Type u_1} [monoid M] {y : M} :

y ∈ submonoid.closure {y}

source

theorem submonoid.closure_singleton_one {M : Type u_1} [monoid M] :

submonoid.closure {1} = ⊥

source

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

submonoid.closure s = (⇑free_monoid.lift coe).mrange

source

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

add_submonoid.closure s = (⇑free_add_monoid.lift coe).mrange

source

theorem submonoid.exists_list_of_mem_closure {M : Type u_1} [monoid M] {s : set M} {x : M} (hx : x ∈ submonoid.closure s) :

∃ (l : list M) (hl : ∀ (y : M), y ∈ l → y ∈ s), l.prod = x

source

theorem add_submonoid.exists_list_of_mem_closure {M : Type u_1} [add_monoid M] {s : set M} {x : M} (hx : x ∈ add_submonoid.closure s) :

∃ (l : list M) (hl : ∀ (y : M), y ∈ l → y ∈ s), l.sum = x

source

theorem add_submonoid.exists_multiset_of_mem_closure {M : Type u_1} [add_comm_monoid M] {s : set M} {x : M} (hx : x ∈ add_submonoid.closure s) :

∃ (l : multiset M) (hl : ∀ (y : M), y ∈ l → y ∈ s), l.sum = x

source

theorem submonoid.exists_multiset_of_mem_closure {M : Type u_1} [comm_monoid M] {s : set M} {x : M} (hx : x ∈ submonoid.closure s) :

∃ (l : multiset M) (hl : ∀ (y : M), y ∈ l → y ∈ s), l.prod = x

source

def submonoid.powers {M : Type u_1} [monoid M] (n : M) :

submonoid M

The submonoid generated by an element.

Equations

submonoid.powers n = (⇑(powers_hom M) n).mrange.copy (set.range (pow n)) _

source

@[simp]

theorem submonoid.mem_powers {M : Type u_1} [monoid M] (n : M) :

n ∈ submonoid.powers n

source

theorem submonoid.mem_powers_iff {M : Type u_1} [monoid M] (x z : M) :

x ∈ submonoid.powers z ↔ ∃ (n : ℕ), z ^ n = x

source

theorem submonoid.powers_eq_closure {M : Type u_1} [monoid M] (n : M) :

submonoid.powers n = submonoid.closure {n}

source

theorem submonoid.powers_subset {M : Type u_1} [monoid M] {n : M} {P : submonoid M} (h : n ∈ P) :

submonoid.powers n ≤ P

source

def submonoid.pow {M : Type u_1} [monoid M] (n : M) (m : ℕ) :

↥(submonoid.powers n)

Exponentiation map from natural numbers to powers.

Equations

submonoid.pow n m = ⟨n ^ m, _⟩

source

def submonoid.log {M : Type u_1} [monoid M] [decidable_eq M] {n : M} (p : ↥(submonoid.powers n)) :

ℕ

Logarithms from powers to natural numbers.

Equations

submonoid.log p = nat.find _

source

@[simp]

theorem submonoid.pow_log_eq_self {M : Type u_1} [monoid M] [decidable_eq M] {n : M} (p : ↥(submonoid.powers n)) :

submonoid.pow n (submonoid.log p) = p

source

theorem submonoid.pow_right_injective_iff_pow_injective {M : Type u_1} [monoid M] {n : M} :

function.injective (λ (m : ℕ), n ^ m) ↔ function.injective (submonoid.pow n)

source

theorem submonoid.log_pow_eq_self {M : Type u_1} [monoid M] [decidable_eq M] {n : M} (h : function.injective (λ (m : ℕ), n ^ m)) (m : ℕ) :

submonoid.log (submonoid.pow n m) = m

source

theorem submonoid.log_pow_int_eq_self {x : ℤ} (h : 1 < x.nat_abs) (m : ℕ) :

submonoid.log (submonoid.pow x m) = m

source

@[simp]

theorem submonoid.map_powers {M : Type u_1} [monoid M] {N : Type u_2} [monoid N] (f : M →* N) (m : M) :

submonoid.map f (submonoid.powers m) = submonoid.powers (⇑f m)

source

theorem add_submonoid.sup_eq_range {N : Type u_3} [add_comm_monoid N] (s t : add_submonoid N) :

s ⊔ t = (s.subtype.coprod t.subtype).mrange

source

theorem submonoid.sup_eq_range {N : Type u_3} [comm_monoid N] (s t : submonoid N) :

s ⊔ t = (s.subtype.coprod t.subtype).mrange

source

theorem submonoid.mem_sup {N : Type u_3} [comm_monoid N] {s t : submonoid N} {x : N} :

x ∈ s ⊔ t ↔ ∃ (y : N) (H : y ∈ s) (z : N) (H : z ∈ t), y * z = x

source

theorem add_submonoid.mem_sup {N : Type u_3} [add_comm_monoid N] {s t : add_submonoid N} {x : N} :

x ∈ s ⊔ t ↔ ∃ (y : N) (H : y ∈ s) (z : N) (H : z ∈ t), y + z = x

source

theorem add_submonoid.closure_singleton_eq {A : Type u_2} [add_monoid A] (x : A) :

add_submonoid.closure {x} = (⇑(multiples_hom A) x).mrange

source

theorem add_submonoid.mem_closure_singleton {A : Type u_2} [add_monoid A] {x y : A} :

y ∈ add_submonoid.closure {x} ↔ ∃ (n : ℕ), n • x = y

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

source

theorem add_submonoid.closure_singleton_zero {A : Type u_2} [add_monoid A] :

add_submonoid.closure {0} = ⊥

source

def add_submonoid.multiples {A : Type u_2} [add_monoid A] (x : A) :

add_submonoid A

The additive submonoid generated by an element.

Equations

add_submonoid.multiples x = (⇑(multiples_hom A) x).mrange.copy (set.range (λ (i : ℕ), i • x)) _

source

@[simp]

theorem add_submonoid.mem_multiples {A : Type u_2} [add_monoid A] (x : A) :

x ∈ add_submonoid.multiples x

source

theorem add_submonoid.mem_multiples_iff {A : Type u_2} [add_monoid A] (x z : A) :

x ∈ add_submonoid.multiples z ↔ ∃ (n : ℕ), n • z = x

source

theorem add_submonoid.multiples_eq_closure {A : Type u_2} [add_monoid A] (x : A) :

add_submonoid.multiples x = add_submonoid.closure {x}

source

theorem add_submonoid.multiples_subset {A : Type u_2} [add_monoid A] {x : A} {P : add_submonoid A} (h : x ∈ P) :

add_submonoid.multiples x ≤ P

Lemmas about additive closures of submonoid.

source

theorem submonoid.mul_right_mem_add_closure {R : Type u_3} [non_assoc_semiring R] (S : submonoid R) {a b : R} (ha : a ∈ add_submonoid.closure ↑S) (hb : b ∈ S) :

a * b ∈ add_submonoid.closure ↑S

The product of an element of the additive closure of a multiplicative submonoid M and an element of M is contained in the additive closure of M.

source

theorem submonoid.mul_mem_add_closure {R : Type u_3} [non_assoc_semiring R] (S : submonoid R) {a b : R} (ha : a ∈ add_submonoid.closure ↑S) (hb : b ∈ add_submonoid.closure ↑S) :

a * b ∈ add_submonoid.closure ↑S

The product of two elements of the additive closure of a submonoid M is an element of the additive closure of M.

source

theorem submonoid.mul_left_mem_add_closure {R : Type u_3} [non_assoc_semiring R] (S : submonoid R) {a b : R} (ha : a ∈ S) (hb : b ∈ add_submonoid.closure ↑S) :

a * b ∈ add_submonoid.closure ↑S

The product of an element of S and an element of the additive closure of a multiplicative submonoid S is contained in the additive closure of S.

source

theorem of_mul_image_powers_eq_multiples_of_mul {M : Type u_1} [monoid M] {x : M} :

⇑additive.of_mul '' ↑(submonoid.powers x) = ↑(add_submonoid.multiples (⇑additive.of_mul x))

source

theorem of_add_image_multiples_eq_powers_of_add {A : Type u_2} [add_monoid A] {x : A} :

⇑multiplicative.of_add '' ↑(add_submonoid.multiples x) = ↑(submonoid.powers (⇑multiplicative.of_add x))