Submonoids: definition and complete_lattice
structure #
This file defines bundled multiplicative and additive submonoids. We also define
a complete_lattice
structure on submonoid
s, 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 thecarrier
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 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 withcarrier
replaced 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 M
and coercioncoe : submonoid M → set M
form agalois_insertion
;monoid_hom.eq_mlocus
: the submonoid of elementsx : M
such thatf x = g x
;monoid_hom.of_mdense
: if a mapf : M → N
between two monoids satisfiesf 1 = 1
andf (x * y) = f x * f y
fory
from some dense sets
, thenf
is a monoid homomorphism. E.g., iff : ℕ → M
satisfiesf 0 = 0
andf (x + 1) = f x + f 1
, thenf
is an additive monoid homomorphism.
Implementation notes #
Submonoid inclusion is denoted ≤
rather than ⊆
, although ∈
is defined as
membership of a submonoid's underlying set.
Note that submonoid M
does not actually require monoid M
, instead requiring only the weaker
mul_one_class M
.
This file is designed to have very few dependencies. In particular, it should not use natural
numbers. submonoid
is implemented by extending subsemigroup
requiring one_mem'
.
Tags #
submonoid, submonoids
- one_mem : ∀ (s : S), 1 ∈ s
one_mem_class S M
says S
is a type of subsets s ≤ M
, such that 1 ∈ s
for all s
.
Instances of this typeclass
Instances of other typeclasses for one_mem_class
- one_mem_class.has_sizeof_inst
- zero_mem : ∀ (s : S), 0 ∈ s
zero_mem_class S M
says S
is a type of subsets s ≤ M
, such that 0 ∈ s
for all s
.
Instances of this typeclass
Instances of other typeclasses for zero_mem_class
- zero_mem_class.has_sizeof_inst
- carrier : set M
- mul_mem' : ∀ {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
- one_mem' : 1 ∈ self.carrier
A submonoid of a monoid M
is a subset containing 1 and closed under multiplication.
Instances for submonoid
- submonoid.has_sizeof_inst
- submonoid.set_like
- submonoid.submonoid_class
- submonoid.has_top
- submonoid.has_bot
- submonoid.inhabited
- submonoid.has_inf
- submonoid.has_Inf
- submonoid.complete_lattice
- submonoid.unique
- submonoid.nontrivial
- submonoid.has_involutive_inv
- submonoid.pointwise_central_scalar
- con.to_submonoid
A submonoid of a monoid M
can be considered as a subsemigroup of that monoid.
- to_mul_mem_class : mul_mem_class S M
- one_mem : ∀ (s : S), 1 ∈ s
submonoid_class S M
says S
is a type of subsets s ≤ M
that contain 1
and are closed under (*)
Instances of this typeclass
Instances of other typeclasses for submonoid_class
- submonoid_class.has_sizeof_inst
An additive submonoid of an additive monoid M
can be considered as an
additive subsemigroup of that additive monoid.
- carrier : set M
- add_mem' : ∀ {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
- zero_mem' : 0 ∈ self.carrier
An additive submonoid of an additive monoid M
is a subset containing 0 and
closed under addition.
Instances for add_submonoid
- add_submonoid.has_sizeof_inst
- add_submonoid.set_like
- add_submonoid.add_submonoid_class
- add_submonoid.has_top
- add_submonoid.has_bot
- add_submonoid.inhabited
- add_submonoid.has_inf
- add_submonoid.has_Inf
- add_submonoid.complete_lattice
- add_submonoid.unique
- add_submonoid.nontrivial
- add_submonoid.has_involutive_neg
- add_submonoid.pointwise_central_scalar
- add_submonoid.has_one
- add_submonoid.has_mul
- add_submonoid.mul_one_class
- add_submonoid.semigroup
- add_submonoid.monoid
- add_con.to_add_submonoid
- to_add_mem_class : add_mem_class S M
- zero_mem : ∀ (s : S), 0 ∈ s
add_submonoid_class S M
says S
is a type of subsets s ≤ M
that contain 0
and are closed under (+)
Instances of this typeclass
Instances of other typeclasses for add_submonoid_class
- add_submonoid_class.has_sizeof_inst
Equations
- add_submonoid_class.to_zero_mem_class S M = {zero_mem := _}
Equations
- submonoid_class.to_one_mem_class S M = {one_mem := _}
Equations
- add_submonoid.set_like = {coe := add_submonoid.carrier _inst_1, coe_injective' := _}
Equations
- submonoid.set_like = {coe := submonoid.carrier _inst_1, coe_injective' := _}
Equations
- add_submonoid.add_submonoid_class = {to_add_mem_class := {add_mem := _}, zero_mem := _}
Equations
- submonoid.submonoid_class = {to_mul_mem_class := {mul_mem := _}, one_mem := _}
See Note [custom simps projection]
Equations
See Note [custom simps projection]
Equations
Two add_submonoid
s are equal if they have the same elements.
Two submonoids are equal if they have the same elements.
Copy an additive submonoid replacing carrier
with a set that is equal to it.
A submonoid contains the monoid's 1.
An add_submonoid
contains the monoid's 0.
An add_submonoid
is closed under addition.
A submonoid is closed under multiplication.
The submonoid M
of the monoid M
.
The additive submonoid M
of the add_monoid M
.
The trivial add_submonoid
{0}
of an add_monoid
M
.
The trivial submonoid {1}
of an monoid M
.
Equations
Equations
The inf of two add_submonoid
s is their intersection.
Equations
- add_submonoid.has_Inf = {Inf := λ (s : set (add_submonoid M)), {carrier := ⋂ (t : add_submonoid M) (H : t ∈ s), ↑t, add_mem' := _, zero_mem' := _}}
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 (preorder.to_has_le (submonoid M)), 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 := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (submonoid M) submonoid.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := has_Inf.Inf submonoid.has_Inf, Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
The add_submonoid
s of an add_monoid
form a complete lattice.
Equations
- add_submonoid.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (add_submonoid M) add_submonoid.complete_lattice._proof_1), le := has_le.le (preorder.to_has_le (add_submonoid M)), lt := has_lt.lt (preorder.to_has_lt (add_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 add_submonoid.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (add_submonoid M) add_submonoid.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := has_Inf.Inf add_submonoid.has_Inf, Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
Equations
- add_submonoid.unique = {to_inhabited := {default := ⊥}, uniq := _}
Equations
- submonoid.unique = {to_inhabited := {default := ⊥}, uniq := _}
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
Equations
- add_submonoid.closure s = has_Inf.Inf {S : add_submonoid M | s ⊆ ↑S}
The submonoid generated by a set includes the set.
The add_submonoid
generated by a set includes the set.
A submonoid S
includes closure s
if and only if it includes s
.
An additive submonoid S
includes closure s
if and only if it includes s
Additive submonoid closure of a set is monotone in its argument: if s ⊆ t
,
then closure s ≤ closure t
Submonoid closure of a set is monotone in its argument: if s ⊆ t
,
then closure s ≤ closure t
.
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
.
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
.
A dependent version of add_submonoid.closure_induction
.
A dependent version of submonoid.closure_induction
.
An induction principle for additive closure membership for predicates with two arguments.
An induction principle for closure membership for predicates with two arguments.
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)
.
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.
Equations
- add_submonoid.gi M = {choice := λ (s : set M) (_x : ↑(add_submonoid.closure s) ≤ s), add_submonoid.closure s, gc := _, le_l_u := _, choice_eq := _}
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 := _}
Closure of a submonoid S
equals S
.
Additive closure of an additive submonoid S
equals S
The additive submonoid of elements x : M
such that f x = g x
The submonoid of elements x : M
such that f x = g x
If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.
If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.
The additive submonoid consisting of the additive units of an additive monoid
Equations
- is_add_unit.add_submonoid M = {carrier := set_of is_add_unit, add_mem' := _, zero_mem' := _}
Instances for ↥is_add_unit.add_submonoid
The submonoid consisting of the units of a monoid
Instances for ↥is_unit.submonoid
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
.
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
.