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: ifx ∈ SwhereSis a multiplicative (resp., additive) submonoid andnis a natural number, thenx^n(resp.,n • x) belongs toS;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 submonoidsS,Tof 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) ofx.
Tags #
submonoid, submonoids
@[simp, norm_cast]
theorem
add_submonoid.coe_nsmul
{M : Type u_1}
[add_monoid M]
(S : add_submonoid M)
(x : ↥S)
(n : ℕ) :
@[simp, norm_cast]
theorem
add_submonoid.coe_list_sum
{M : Type u_1}
[add_monoid M]
(S : add_submonoid M)
(l : list ↥S) :
@[simp, norm_cast]
theorem
add_submonoid.coe_multiset_sum
{M : Type u_1}
[add_comm_monoid M]
(S : add_submonoid M)
(m : multiset ↥S) :
@[simp, norm_cast]
theorem
submonoid.coe_multiset_prod
{M : Type u_1}
[comm_monoid M]
(S : submonoid M)
(m : multiset ↥S) :
@[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 ι) :
@[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 ι) :
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) :
Sum of a list of elements in an add_submonoid is in the add_submonoid.
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) :
Product of a multiset of elements in a submonoid of a comm_monoid is in the submonoid.
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) :
Sum of a multiset of elements in an add_submonoid of an add_comm_monoid is
in the add_submonoid.
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.
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.
theorem
add_submonoid.nsmul_mem
{M : Type u_1}
[add_monoid M]
(S : add_submonoid M)
{x : M}
(hx : x ∈ S)
(n : ℕ) :
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} :
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} :
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) :
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) :
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} :
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} :
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) :
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) :
theorem
add_submonoid.mem_sup_left
{M : Type u_1}
[add_zero_class M]
{S T : add_submonoid M}
{x : M} :
theorem
add_submonoid.mem_sup_right
{M : Type u_1}
[add_zero_class M]
{S T : add_submonoid M}
{x : M} :
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) :
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) :
theorem
submonoid.mem_supr_of_mem
{M : Type u_1}
[mul_one_class M]
{ι : Sort u_2}
{S : ι → submonoid M}
(i : ι)
{x : M} :
theorem
add_submonoid.mem_supr_of_mem
{M : Type u_1}
[add_zero_class M]
{ι : Sort u_2}
{S : ι → add_submonoid M}
(i : ι)
{x : M} :
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} :
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} :
theorem
submonoid.supr_induction
{M : Type u_1}
[mul_one_class M]
{ι : Sort u_2}
(S : ι → submonoid M)
{C : M → Prop}
{x : M}
(hx : x ∈ ⨆ (i : ι), S i)
(hp : ∀ (i : ι) (x : M), x ∈ S i → C x)
(h1 : C 1)
(hmul : ∀ (x y : M), C x → C y → C (x * y)) :
C x
An induction principle for elements of ⨆ i, S i.
If C holds for 1 and all elements of S i for all i, and is preserved under multiplication,
then it holds for all elements of the supremum of S.
theorem
add_submonoid.supr_induction
{M : Type u_1}
[add_zero_class M]
{ι : Sort u_2}
(S : ι → add_submonoid M)
{C : M → Prop}
{x : M}
(hx : x ∈ ⨆ (i : ι), S i)
(hp : ∀ (i : ι) (x : M), x ∈ S i → C x)
(h1 : C 0)
(hmul : ∀ (x y : M), C x → C y → C (x + y)) :
C x
An induction principle for elements of ⨆ i, S i.
If C holds for 0 and all elements of S i for all i, and is preserved under addition,
then it holds for all elements of the supremum of S.
theorem
submonoid.supr_induction'
{M : Type u_1}
[mul_one_class M]
{ι : Sort u_2}
(S : ι → submonoid M)
{C : Π (x : M), (x ∈ ⨆ (i : ι), S i) → Prop}
(hp : ∀ (i : ι) (x : M) (H : x ∈ S i), C x _)
(h1 : C 1 _)
(hmul : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), C x hx → C y hy → C (x * y) _)
{x : M}
(hx : x ∈ ⨆ (i : ι), S i) :
C x hx
A dependent version of submonoid.supr_induction.
theorem
add_submonoid.supr_induction'
{M : Type u_1}
[add_zero_class M]
{ι : Sort u_2}
(S : ι → add_submonoid M)
{C : Π (x : M), (x ∈ ⨆ (i : ι), S i) → Prop}
(hp : ∀ (i : ι) (x : M) (H : x ∈ S i), C x _)
(h1 : C 0 _)
(hmul : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), C x hx → C y hy → C (x + y) _)
{x : M}
(hx : x ∈ ⨆ (i : ι), S i) :
C x hx
A dependent version of add_submonoid.supr_induction.
theorem
submonoid.closure_singleton_eq
{M : Type u_1}
[monoid M]
(x : M) :
submonoid.closure {x} = (⇑(powers_hom M) x).mrange
The submonoid generated by an element of a monoid equals the set of natural number powers of the element.
theorem
submonoid.mem_closure_singleton_self
{M : Type u_1}
[monoid M]
{y : M} :
y ∈ submonoid.closure {y}
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) :
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) :
theorem
submonoid.exists_multiset_of_mem_closure
{M : Type u_1}
[comm_monoid M]
{s : set M}
{x : M}
(hx : x ∈ submonoid.closure s) :
The submonoid generated by an element.
Equations
- submonoid.powers n = (⇑(powers_hom M) n).mrange.copy (set.range (pow n)) _
@[simp]
theorem
submonoid.powers_subset
{M : Type u_1}
[monoid M]
{n : M}
{P : submonoid M}
(h : n ∈ P) :
submonoid.powers n ≤ P
Exponentiation map from natural numbers to powers.
Equations
- submonoid.pow n m = ⇑((⇑(powers_hom M) n).mrange_restrict) (⇑multiplicative.of_add m)
@[simp]
theorem
submonoid.pow_apply
{M : Type u_1}
[monoid M]
(n : M)
(m : ℕ) :
submonoid.pow n m = ⟨n ^ m, _⟩
Logarithms from powers to natural numbers.
Equations
- submonoid.log p = nat.find _
@[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
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)
@[simp]
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
def
submonoid.pow_log_equiv
{M : Type u_1}
[monoid M]
[decidable_eq M]
{n : M}
(h : function.injective (λ (m : ℕ), n ^ m)) :
The exponentiation map is an isomorphism from the additive monoid on natural numbers to powers when it is injective. The inverse is given by the logarithms.
Equations
- submonoid.pow_log_equiv h = {to_fun := λ (m : multiplicative ℕ), submonoid.pow n (⇑multiplicative.to_add m), inv_fun := λ (m : ↥(submonoid.powers n)), ⇑multiplicative.of_add (submonoid.log m), left_inv := _, right_inv := _, map_mul' := _}
@[simp]
theorem
submonoid.pow_log_equiv_symm_apply
{M : Type u_1}
[monoid M]
[decidable_eq M]
{n : M}
(h : function.injective (λ (m : ℕ), n ^ m))
(m : ↥(submonoid.powers n)) :
⇑((submonoid.pow_log_equiv h).symm) m = ⇑multiplicative.of_add (submonoid.log m)
@[simp]
theorem
submonoid.pow_log_equiv_apply
{M : Type u_1}
[monoid M]
[decidable_eq M]
{n : M}
(h : function.injective (λ (m : ℕ), n ^ m))
(m : multiplicative ℕ) :
⇑(submonoid.pow_log_equiv h) m = submonoid.pow n (⇑multiplicative.to_add m)
theorem
submonoid.log_mul
{M : Type u_1}
[monoid M]
[decidable_eq M]
{n : M}
(h : function.injective (λ (m : ℕ), n ^ m))
(x y : ↥(submonoid.powers n)) :
submonoid.log (x * y) = submonoid.log x + submonoid.log y
theorem
submonoid.log_pow_int_eq_self
{x : ℤ}
(h : 1 < x.nat_abs)
(m : ℕ) :
submonoid.log (submonoid.pow x m) = m
@[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)
theorem
add_submonoid.closure_singleton_eq
{A : Type u_2}
[add_monoid A]
(x : A) :
add_submonoid.closure {x} = (⇑(multiples_hom A) x).mrange
The add_submonoid generated by an element of an add_monoid equals the set of
natural number multiples of the element.
theorem
add_submonoid.closure_singleton_zero
{A : Type u_2}
[add_monoid A] :
add_submonoid.closure {0} = ⊥
The additive submonoid generated by an element.
Equations
- add_submonoid.multiples x = (⇑(multiples_hom A) x).mrange.copy (set.range (λ (i : ℕ), i • x)) _
@[simp]
theorem
add_submonoid.multiples_subset
{A : Type u_2}
[add_monoid A]
{x : A}
{P : add_submonoid A}
(h : x ∈ P) :
Lemmas about additive closures of submonoid.
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.
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.
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.