Subsemigroups: definition and CompleteLattice
structure #
This file defines bundled multiplicative and additive subsemigroups. We also define
a CompleteLattice
structure on Subsemigroup
s,
and define the closure of a set as the minimal subsemigroup that includes this set.
Main definitions #
Subsemigroup M
: the type of bundled subsemigroup of a magmaM
; the underlying set is given in thecarrier
field of the structure, and should be accessed through coercion as in(S : Set M)
.AddSubsemigroup M
: the type of bundled subsemigroups of an additive magmaM
.
For each of the following definitions in the Subsemigroup
namespace, there is a corresponding
definition in the AddSubsemigroup
namespace.
Subsemigroup.copy
: copy of a subsemigroup withcarrier
replaced by a set that is equal but possibly not definitionally equal to the carrier of the originalSubsemigroup
.Subsemigroup.closure
: semigroup closure of a set, i.e., the least subsemigroup that includes the set.Subsemigroup.gi
:closure : Set M → Subsemigroup M
and coercioncoe : Subsemigroup M → Set M
form aGaloisInsertion
;
Implementation notes #
Subsemigroup inclusion is denoted ≤
rather than ⊆
, although ∈
is defined as
membership of a subsemigroup's underlying set.
Note that Subsemigroup M
does not actually require Semigroup M
,
instead requiring only the weaker Mul M
.
This file is designed to have very few dependencies. In particular, it should not use natural numbers.
Tags #
subsemigroup, subsemigroups
MulMemClass S M
says S
is a type of sets s : Set M
that are closed under (*)
A substructure satisfying
MulMemClass
is closed under multiplication.
Instances
A substructure satisfying MulMemClass
is closed under multiplication.
AddMemClass S M
says S
is a type of sets s : Set M
that are closed under (+)
A substructure satisfying
AddMemClass
is closed under addition.
Instances
A substructure satisfying AddMemClass
is closed under addition.
A subsemigroup of a magma M
is a subset closed under multiplication.
- carrier : Set M
The carrier of a subsemigroup.
The product of two elements of a subsemigroup belongs to the subsemigroup.
Instances For
The product of two elements of a subsemigroup belongs to the subsemigroup.
An additive subsemigroup of an additive magma M
is a subset closed under addition.
- carrier : Set M
The carrier of an additive subsemigroup.
The sum of two elements of an additive subsemigroup belongs to the subsemigroup.
Instances For
The sum of two elements of an additive subsemigroup belongs to the subsemigroup.
Equations
- AddSubsemigroup.instSetLike = { coe := AddSubsemigroup.carrier, coe_injective' := ⋯ }
Equations
- Subsemigroup.instSetLike = { coe := Subsemigroup.carrier, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Two AddSubsemigroup
s are equal if they have the same elements.
Two subsemigroups are equal if they have the same elements.
Copy an additive subsemigroup replacing carrier
with a set that is equal to it.
Equations
- S.copy s hs = { carrier := s, add_mem' := ⋯ }
Instances For
Copy a subsemigroup replacing carrier
with a set that is equal to it.
Equations
- S.copy s hs = { carrier := s, mul_mem' := ⋯ }
Instances For
An AddSubsemigroup
is closed under addition.
A subsemigroup is closed under multiplication.
The additive subsemigroup M
of the magma M
.
Equations
- AddSubsemigroup.instTop = { top := { carrier := Set.univ, add_mem' := ⋯ } }
The subsemigroup M
of the magma M
.
Equations
- Subsemigroup.instTop = { top := { carrier := Set.univ, mul_mem' := ⋯ } }
The trivial AddSubsemigroup
∅
of an additive magma M
.
The trivial subsemigroup ∅
of a magma M
.
The inf of two AddSubsemigroup
s is their intersection.
Equations
- AddSubsemigroup.instInf = { inf := fun (S₁ S₂ : AddSubsemigroup M) => { carrier := ↑S₁ ∩ ↑S₂, add_mem' := ⋯ } }
Equations
- ⋯ = ⋯
Instances For
The inf of two subsemigroups is their intersection.
Equations
- Subsemigroup.instInf = { inf := fun (S₁ S₂ : Subsemigroup M) => { carrier := ↑S₁ ∩ ↑S₂, mul_mem' := ⋯ } }
Equations
- AddSubsemigroup.instInfSet = { sInf := fun (s : Set (AddSubsemigroup M)) => { carrier := ⋂ t ∈ s, ↑t, add_mem' := ⋯ } }
Equations
- Subsemigroup.instInfSet = { sInf := fun (s : Set (Subsemigroup M)) => { carrier := ⋂ t ∈ s, ↑t, mul_mem' := ⋯ } }
The AddSubsemigroup
s of an AddMonoid
form a complete lattice.
Equations
- AddSubsemigroup.instCompleteLattice = let __src := completeLatticeOfInf (AddSubsemigroup M) ⋯; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
subsemigroups of a monoid form a complete lattice.
Equations
- Subsemigroup.instCompleteLattice = let __src := completeLatticeOfInf (Subsemigroup M) ⋯; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The AddSubsemigroup
generated by a set
Equations
- AddSubsemigroup.closure s = sInf {S : AddSubsemigroup M | s ⊆ ↑S}
Instances For
The Subsemigroup
generated by a set.
Equations
- Subsemigroup.closure s = sInf {S : Subsemigroup M | s ⊆ ↑S}
Instances For
The AddSubsemigroup
generated by a set includes the set.
The subsemigroup generated by a set includes the set.
An additive subsemigroup S
includes closure s
if and only if it includes s
A subsemigroup S
includes closure s
if and only if it includes s
.
An induction principle for additive closure membership. If p
holds for 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 all elements of s
, and
is preserved under multiplication, then p
holds for all elements of the closure of s
.
Equations
- ⋯ = ⋯
Instances For
A dependent version of AddSubsemigroup.closure_induction
.
A dependent version of Subsemigroup.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
,
AddSubsemigroup.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
, and verify that p x
and p y
imply
p (x + y)
.
If s
is a dense set in a magma M
, Subsemigroup.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
,
and verify that p x
and p y
imply p (x * y)
.
Additive closure of an additive subsemigroup S
equals S
Closure of a subsemigroup S
equals S
.
Let s
be a subset of an additive semigroup M
such that the closure of s
is the whole
semigroup. Then AddHom.ofDense
defines an additive homomorphism from M
asking for a proof
of f (x + y) = f x + f y
only for y ∈ s
.
Equations
- AddHom.ofDense f hs hmul = { toFun := f, map_add' := ⋯ }
Instances For
Let s
be a subset of a semigroup M
such that the closure of s
is the whole semigroup.
Then MulHom.ofDense
defines a mul homomorphism from M
asking for a proof
of f (x * y) = f x * f y
only for y ∈ s
.
Equations
- MulHom.ofDense f hs hmul = { toFun := f, map_mul' := ⋯ }