Submonoids: definition and CompleteLattice
structure #
This file defines bundled multiplicative and additive submonoids. We also define
a CompleteLattice
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
MonoidHom.ofClosureEqTopLeft
/MonoidHom.ofClosureEqTopRight
.
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)
.AddSubmonoid 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 AddSubmonoid
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→ Submonoid M
and coercioncoe : Submonoid M → Set M→ Set M
form aGaloisInsertion
;MonoidHom.eqLocus
: the submonoid of elementsx : M
such thatf x = g x
;MonoidHom.ofClosureEqTopRight
: if a mapf : M → N→ 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→ 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
MulOneClass 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
A submonoid contains
1
.one_mem' : 1 ∈ toSubsemigroup.carrier
A submonoid of a monoid M
is a subset containing 1 and closed under multiplication.
Instances For
SubmonoidClass S M
says S
is a type of subsets s ≤ M≤ M
that contain 1
and are closed under (*)
Instances
An additive submonoid contains
0
.zero_mem' : 0 ∈ toAddSubsemigroup.carrier
An additive submonoid of an additive monoid M
is a subset containing 0 and
closed under addition.
Instances For
AddSubmonoidClass S M
says S
is a type of subsets s ≤ M≤ M
that contain 0
and are closed under (+)
Instances
Equations
- nsmul_mem.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : AddSubmonoidClass (AddSubmonoid M) M) = (_ : AddSubmonoidClass (AddSubmonoid M) M)
Two AddSubmonoid
s are equal if they have the same elements.
Copy an additive submonoid replacing carrier
with a set that is equal to it.
Copy a submonoid replacing carrier
with a set that is equal to it.
An AddSubmonoid
contains the monoid's 0.
A submonoid contains the monoid's 1.
An AddSubmonoid
is closed under addition.
A submonoid is closed under multiplication.
The additive submonoid M
of the AddMonoid M
.
Equations
- One or more equations did not get rendered due to their size.
The submonoid M
of the monoid M
.
Equations
- One or more equations did not get rendered due to their size.
The trivial AddSubmonoid
{0}
of an AddMonoid
M
.
Equations
- One or more equations did not get rendered due to their size.
The trivial submonoid {1}
of an monoid M
.
Equations
- AddSubmonoid.instInfAddSubmonoid.match_1 S₁ S₂ motive x h_1 = And.casesOn x fun left right => h_1 left right
The inf of two AddSubmonoid
s is their intersection.
Equations
- One or more equations did not get rendered due to their size.
The inf of two submonoids is their intersection.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : 0 ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x) = (_ : 0 ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x)
Equations
- (_ : a + b ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x) = (_ : a + b ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x)
Equations
- One or more equations did not get rendered due to their size.
The AddSubmonoid
s of an AddMonoid
form a complete lattice.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (a b : AddSubmonoid M), b ≤ a ⊔ b) = (_ : ∀ (a b : AddSubmonoid M), b ≤ a ⊔ b)
Equations
- (_ : ∀ (a : AddSubmonoid M), a ≤ a) = (_ : ∀ (a : AddSubmonoid M), a ≤ a)
Equations
- (_ : ∀ (a b : AddSubmonoid M), a ≤ a ⊔ b) = (_ : ∀ (a b : AddSubmonoid M), a ≤ a ⊔ b)
Equations
- (_ : ∀ (a b c : AddSubmonoid M), a ≤ b → b ≤ c → a ≤ c) = (_ : ∀ (a b c : AddSubmonoid M), a ≤ b → b ≤ c → a ≤ c)
Equations
- (_ : ∀ (s : Set (AddSubmonoid M)) (a : AddSubmonoid M), a ∈ s → infₛ s ≤ a) = (_ : ∀ (s : Set (AddSubmonoid M)) (a : AddSubmonoid M), a ∈ s → infₛ s ≤ a)
Equations
- (_ : ∀ (s : Set (AddSubmonoid M)) (a : AddSubmonoid M), a ∈ s → a ≤ supₛ s) = (_ : ∀ (s : Set (AddSubmonoid M)) (a : AddSubmonoid M), a ∈ s → a ≤ supₛ s)
Equations
- (_ : ∀ (a b : AddSubmonoid M), a ≤ b → b ≤ a → a = b) = (_ : ∀ (a b : AddSubmonoid M), a ≤ b → b ≤ a → a = b)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Submonoids of a monoid form a complete lattice.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddSubmonoid.instUniqueAddSubmonoid = { toInhabited := { default := ⊥ }, uniq := (_ : ∀ (a : AddSubmonoid M), a = default) }
Equations
- (_ : Nontrivial (AddSubmonoid M)) = (_ : Nontrivial (AddSubmonoid M))
The add_submonoid
generated by a set
Equations
- AddSubmonoid.closure s = infₛ { S | s ⊆ ↑S }
The Submonoid
generated by a set.
Equations
- Submonoid.closure s = infₛ { S | s ⊆ ↑S }
The AddSubmonoid
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
A 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⊆ t
,
then closure s ≤ closure t≤ closure t
Submonoid closure of a set is monotone in its argument: if s ⊆ t⊆ t
,
then closure s ≤ closure t≤ 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
.
A dependent version of AddSubmonoid.closure_induction
.
Equations
- AddSubmonoid.closure_induction'.match_1 s y motive x h_1 = Exists.casesOn x fun w h => h_1 w h
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
, AddSubmonoid.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∈ 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∈ s
, verify p 1
,
and verify that p x
and p y
imply p (x * y)
.
Equations
- (_ : ↑x ⊆ ↑(AddSubmonoid.closure ↑x)) = (_ : ↑x ⊆ ↑(AddSubmonoid.closure ↑x))
Equations
- (_ : AddSubmonoid.closure x ≤ x ↔ x ⊆ ↑x) = (_ : AddSubmonoid.closure x ≤ x ↔ x ⊆ ↑x)
Equations
- (_ : (fun s x => AddSubmonoid.closure s) x x = (fun s x => AddSubmonoid.closure s) x x) = (_ : (fun s x => AddSubmonoid.closure s) x x = (fun s x => AddSubmonoid.closure s) x x)
closure
forms a Galois insertion with the coercion to set.
Equations
- One or more equations did not get rendered due to their size.
closure
forms a Galois insertion with the coercion to set.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The submonoid of elements x : M
such that f x = g x
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Let s
be a subset of an additive monoid M
such that the closure of s
is
the whole monoid. Then AddMonoidHom.ofClosureEqTopLeft
defines an additive monoid
homomorphism from M
asking for a proof of f (x + y) = f x + f y
only for x ∈ s∈ s
.
Equations
- AddMonoidHom.ofClosureMEqTopLeft f hs h1 hmul = { toZeroHom := { toFun := f, map_zero' := h1 }, map_add' := (_ : ∀ (x y : M), f (x + y) = f x + f y) }
Let s
be a subset of a monoid M
such that the closure of s
is the whole monoid.
Then MonoidHom.ofClosureEqTopLeft
defines a monoid homomorphism from M
asking for
a proof of f (x * y) = f x * f y
only for x ∈ s∈ s
.
Equations
- MonoidHom.ofClosureMEqTopLeft f hs h1 hmul = { toOneHom := { toFun := f, map_one' := h1 }, map_mul' := (_ : ∀ (x y : M), f (x * y) = f x * f y) }
Let s
be a subset of an additive monoid M
such that the closure of s
is
the whole monoid. Then AddMonoidHom.ofClosureEqTopRight
defines an additive monoid
homomorphism from M
asking for a proof of f (x + y) = f x + f y
only for y ∈ s∈ s
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Let s
be a subset of a monoid M
such that the closure of s
is the whole monoid.
Then MonoidHom.ofClosureEqTopRight
defines a monoid homomorphism from M
asking for
a proof of f (x * y) = f x * f y
only for y ∈ s∈ s
.
Equations
- One or more equations did not get rendered due to their size.