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 monoidM; the underlying set is given in thecarrierfield 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 monoidM.
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 withcarrierreplaced by a set that is equal but possibly not definitionally equal to the carrier of the originalsubmonoid.submonoid.closure: monoid closure of a set, i.e., the least submonoid that includes the set.submonoid.gi:closure : set M → submonoid Mand coercioncoe : submonoid M → set Mform agalois_insertion;monoid_hom.eq_mlocus: the submonoid of elementsx : Msuch thatf x = g x;monoid_hom.of_mdense: if a mapf : M → Nbetween two monoids satisfiesf 1 = 1andf (x * y) = f x * f yforyfrom some dense sets, thenfis a monoid homomorphism. E.g., iff : ℕ → Msatisfiesf 0 = 0andf (x + 1) = f x + f 1, thenfis 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
Equations
- submonoid.has_coe = {coe := submonoid.carrier _inst_1}
Two add_submonoids are equal if the underlying subsets are equal.
Two add_submonoids are equal if and only if the underlying subsets are equal.
Two add_submonoids are equal if they have the same elements.
Copy an additive submonoid replacing carrier with a set that is equal to it.
An add_submonoid contains the monoid's 0.
A submonoid contains the monoid's 1.
An add_submonoid is closed under addition.
Equations
- submonoid.partial_order = {le := λ (S T : submonoid M), ∀ ⦃x : M⦄, x ∈ S → x ∈ T, lt := partial_order.lt (partial_order.lift coe submonoid.ext'), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
The additive submonoid M of the add_monoid M.
The trivial add_submonoid {0} of an add_monoid M.
Equations
The inf of two add_submonoids is their intersection.
The add_submonoids of an add_monoid form a complete lattice.
Submonoids of a monoid form a complete lattice.
Equations
- submonoid.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (submonoid M) submonoid.complete_lattice._proof_1), le := has_le.le submonoid.has_le, lt := has_lt.lt (preorder.to_has_lt (submonoid M)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf submonoid.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, top := ⊤, le_top := _, bot := ⊥, bot_le := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (submonoid M) submonoid.complete_lattice._proof_1), Inf := has_Inf.Inf submonoid.has_Inf, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
The add_submonoid generated by a set
The submonoid generated by a set.
Equations
- submonoid.closure s = has_Inf.Inf {S : submonoid M | s ⊆ ↑S}
The add_submonoid generated by a set includes the set.
The submonoid generated by a set includes the set.
An additive submonoid S includes closure s if and only if it includes s
Submonoid closure of a set is monotone in its argument: if s ⊆ t,
then closure s ≤ closure t.
Additive submonoid closure of a set is monotone in its argument: if s ⊆ t,
then closure s ≤ closure t
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.
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.
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).
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).
closure forms a Galois insertion with the coercion to set.
closure forms a Galois insertion with the coercion to set.
Equations
- submonoid.gi M = {choice := λ (s : set M) (_x : ↑(submonoid.closure s) ≤ s), submonoid.closure s, gc := _, le_l_u := _, choice_eq := _}
Additive closure of an additive submonoid S equals S
Closure of a submonoid S equals S.
The additive submonoid of elements x : M such that f x = g x
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.
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.