Free constructions #
Main definitions #
FreeMagma α
: free magma (structure with binary operation without any axioms) over alphabetα
, defined inductively, with traversable instance and decidable equality.MagmaAssocQuotient α
: quotient of a magmaα
by the associativity equivalence relation.FreeSemigroup α
: free semigroup over alphabetα
, defined as a structure with two fieldshead : α
andtail : List α
(i.e. nonempty lists), with traversable instance and decidable equality.FreeMagmaAssocQuotientEquiv α
: isomorphism betweenMagmaAssocQuotient (FreeMagma α)
andFreeSemigroup α
.FreeMagma.lift
: the universal property of the free magma, expressing its adjointness.
- of: {α : Type u} → α → FreeAddMagma α
- add: {α : Type u} → FreeAddMagma α → FreeAddMagma α → FreeAddMagma α
Free nonabelian additive magma over a given alphabet.
Instances For
Equations
- instDecidableEqFreeAddMagma = decEqFreeAddMagma✝
Equations
- instDecidableEqFreeMagma = decEqFreeMagma✝
Equations
- FreeAddMagma.instInhabitedFreeAddMagma = { default := FreeAddMagma.of default }
Equations
- FreeMagma.instInhabitedFreeMagma = { default := FreeMagma.of default }
Equations
- FreeAddMagma.instAddFreeAddMagma = { add := FreeAddMagma.add }
Recursor for FreeAddMagma
using x + y
instead of
FreeAddMagma.add x y
.
Equations
- FreeAddMagma.recOnAdd x ih1 ih2 = FreeAddMagma.recOn x ih1 ih2
Instances For
Recursor for FreeMagma
using x * y
instead of FreeMagma.mul x y
.
Equations
- FreeMagma.recOnMul x ih1 ih2 = FreeMagma.recOn x ih1 ih2
Instances For
Lifts a function α → β
to a magma homomorphism FreeMagma α → β
given a magma β
.
Equations
- FreeMagma.liftAux f (FreeMagma.of x_1) = f x_1
- FreeMagma.liftAux f (FreeMagma.mul x_1 y) = FreeMagma.liftAux f x_1 * FreeMagma.liftAux f y
Instances For
Lifts a function α → β
to an additive magma homomorphism FreeAddMagma α → β
given
an additive magma β
.
Equations
- FreeAddMagma.liftAux f (FreeAddMagma.of x_1) = f x_1
- FreeAddMagma.liftAux f (FreeAddMagma.add x_1 y) = FreeAddMagma.liftAux f x_1 + FreeAddMagma.liftAux f y
Instances For
The universal property of the free additive magma expressing its adjointness.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unique additive magma homomorphism FreeAddMagma α → FreeAddMagma β
that sends
each of x
to of (f x)
.
Equations
- FreeAddMagma.map f = ↑FreeAddMagma.lift (FreeAddMagma.of ∘ f)
Instances For
Equations
- FreeAddMagma.instMonadFreeAddMagma = Monad.mk
Equations
- FreeMagma.instMonadFreeMagma = Monad.mk
Recursor on FreeAddMagma
using pure
instead of of
.
Equations
- FreeAddMagma.recOnPure x ih1 ih2 = FreeAddMagma.recOnAdd x ih1 ih2
Instances For
Recursor on FreeMagma
using pure
instead of of
.
Equations
- FreeMagma.recOnPure x ih1 ih2 = FreeMagma.recOnMul x ih1 ih2
Instances For
FreeMagma
is traversable.
Equations
- FreeMagma.traverse F (FreeMagma.of x_1) = FreeMagma.of <$> F x_1
- FreeMagma.traverse F (FreeMagma.mul x_1 y) = Seq.seq ((fun x x_1 => x * x_1) <$> FreeMagma.traverse F x_1) fun x => FreeMagma.traverse F y
Instances For
FreeAddMagma
is traversable.
Equations
- FreeAddMagma.traverse F (FreeAddMagma.of x_1) = FreeAddMagma.of <$> F x_1
- FreeAddMagma.traverse F (FreeAddMagma.add x_1 y) = Seq.seq ((fun x x_1 => x + x_1) <$> FreeAddMagma.traverse F x_1) fun x => FreeAddMagma.traverse F y
Instances For
Representation of an element of a free magma.
Equations
- FreeMagma.repr (FreeMagma.of x_1) = repr x_1
- FreeMagma.repr (FreeMagma.mul x_1 y) = Std.Format.text "( " ++ FreeMagma.repr x_1 ++ Std.Format.text " * " ++ FreeMagma.repr y ++ Std.Format.text " )"
Instances For
Representation of an element of a free additive magma.
Equations
- FreeAddMagma.repr (FreeAddMagma.of x_1) = repr x_1
- FreeAddMagma.repr (FreeAddMagma.add x_1 y) = Std.Format.text "( " ++ FreeAddMagma.repr x_1 ++ Std.Format.text " + " ++ FreeAddMagma.repr y ++ Std.Format.text " )"
Instances For
Equations
- instReprFreeAddMagma = { reprPrec := fun o x => FreeAddMagma.repr o }
Equations
- instReprFreeMagma = { reprPrec := fun o x => FreeMagma.repr o }
Length of an element of a free magma.
Equations
- FreeMagma.length (FreeMagma.of x_1) = 1
- FreeMagma.length (FreeMagma.mul x_1 y) = FreeMagma.length x_1 + FreeMagma.length y
Instances For
Length of an element of a free additive magma.
Equations
- FreeAddMagma.length (FreeAddMagma.of x_1) = 1
- FreeAddMagma.length (FreeAddMagma.add x_1 y) = FreeAddMagma.length x_1 + FreeAddMagma.length y
Instances For
Additive semigroup quotient of an additive magma.
Equations
Instances For
Semigroup quotient of a magma.
Equations
Instances For
Equations
- AddMagma.FreeAddSemigroup.instAddSemigroupAssocQuotient = AddSemigroup.mk (_ : ∀ (x y z : AddMagma.FreeAddSemigroup α), x + y + z = x + (y + z))
Equations
- Magma.AssocQuotient.instSemigroupAssocQuotient = Semigroup.mk (_ : ∀ (x y z : Magma.AssocQuotient α), x * y * z = x * (y * z))
Embedding from additive magma to its free additive semigroup.
Equations
- AddMagma.FreeAddSemigroup.of = { toFun := Quot.mk (AddMagma.AssocRel α), map_add' := (_ : ∀ (_x _y : α), Quot.mk (AddMagma.AssocRel α) (_x + _y) = Quot.mk (AddMagma.AssocRel α) (_x + _y)) }
Instances For
Embedding from magma to its free semigroup.
Equations
- Magma.AssocQuotient.of = { toFun := Quot.mk (Magma.AssocRel α), map_mul' := (_ : ∀ (_x _y : α), Quot.mk (Magma.AssocRel α) (_x * _y) = Quot.mk (Magma.AssocRel α) (_x * _y)) }
Instances For
Equations
- AddMagma.FreeAddSemigroup.instInhabitedAssocQuotient = { default := ↑AddMagma.FreeAddSemigroup.of default }
Equations
- Magma.AssocQuotient.instInhabitedAssocQuotient = { default := ↑Magma.AssocQuotient.of default }
Lifts an additive magma homomorphism α → β
to an
additive semigroup homomorphism AddMagma.AssocQuotient α → β
given an additive semigroup β
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lifts a magma homomorphism α → β
to a semigroup homomorphism Magma.AssocQuotient α → β
given a semigroup β
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
From an additive magma homomorphism α → β
to an additive semigroup homomorphism
AddMagma.AssocQuotient α → AddMagma.AssocQuotient β
.
Equations
- AddMagma.FreeAddSemigroup.map f = ↑AddMagma.FreeAddSemigroup.lift (AddHom.comp AddMagma.FreeAddSemigroup.of f)
Instances For
From a magma homomorphism α →ₙ* β
to a semigroup homomorphism
Magma.AssocQuotient α →ₙ* Magma.AssocQuotient β
.
Equations
- Magma.AssocQuotient.map f = ↑Magma.AssocQuotient.lift (MulHom.comp Magma.AssocQuotient.of f)
Instances For
- head : α
The head of the element
- tail : List α
The tail of the element
Free additive semigroup over a given alphabet.
Instances For
- head : α
The head of the element
- tail : List α
The tail of the element
Free semigroup over a given alphabet.
Instances For
Equations
- FreeAddSemigroup.instAddSemigroupFreeAddSemigroup = AddSemigroup.mk (_ : ∀ (_L1 _L2 _L3 : FreeAddSemigroup α), _L1 + _L2 + _L3 = _L1 + (_L2 + _L3))
Equations
- FreeSemigroup.instSemigroupFreeSemigroup = Semigroup.mk (_ : ∀ (_L1 _L2 _L3 : FreeSemigroup α), _L1 * _L2 * _L3 = _L1 * (_L2 * _L3))
The embedding α → FreeAddSemigroup α
.
Equations
- FreeAddSemigroup.of x = { head := x, tail := [] }
Instances For
The embedding α → FreeSemigroup α
.
Equations
- FreeSemigroup.of x = { head := x, tail := [] }
Instances For
Length of an element of free additive semigroup
Equations
- FreeAddSemigroup.length x = List.length x.tail + 1
Instances For
Length of an element of free semigroup.
Equations
- FreeSemigroup.length x = List.length x.tail + 1
Instances For
Equations
- FreeAddSemigroup.instInhabitedFreeAddSemigroup = { default := FreeAddSemigroup.of default }
Equations
- FreeSemigroup.instInhabitedFreeSemigroup = { default := FreeSemigroup.of default }
Recursor for free additive semigroup using of
and +
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Recursor for free semigroup using of
and *
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lifts a function α → β
to an additive semigroup
homomorphism FreeAddSemigroup α → β
given an additive semigroup β
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lifts a function α → β
to a semigroup homomorphism FreeSemigroup α → β
given
a semigroup β
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unique additive semigroup homomorphism that sends of x
to of (f x)
.
Equations
- FreeAddSemigroup.map f = ↑FreeAddSemigroup.lift (FreeAddSemigroup.of ∘ f)
Instances For
The unique semigroup homomorphism that sends of x
to of (f x)
.
Equations
- FreeSemigroup.map f = ↑FreeSemigroup.lift (FreeSemigroup.of ∘ f)
Instances For
Equations
Equations
- FreeSemigroup.instMonadFreeSemigroup = Monad.mk
Recursor that uses pure
instead of of
.
Equations
- FreeAddSemigroup.recOnPure x ih1 ih2 = FreeAddSemigroup.recOnAdd x ih1 ih2
Instances For
Recursor that uses pure
instead of of
.
Equations
- FreeSemigroup.recOnPure x ih1 ih2 = FreeSemigroup.recOnMul x ih1 ih2
Instances For
FreeAddSemigroup
is traversable.
Equations
- FreeAddSemigroup.traverse F x = FreeAddSemigroup.recOnPure x (fun x => pure <$> F x) fun _x _y ihx ihy => Seq.seq ((fun x x_1 => x + x_1) <$> ihx) fun x => ihy
Instances For
FreeSemigroup
is traversable.
Equations
- FreeSemigroup.traverse F x = FreeSemigroup.recOnPure x (fun x => pure <$> F x) fun _x _y ihx ihy => Seq.seq ((fun x x_1 => x * x_1) <$> ihx) fun x => ihy
Instances For
The canonical additive morphism from FreeAddMagma α
to FreeAddSemigroup α
.
Equations
- FreeAddMagma.toFreeAddSemigroup = ↑FreeAddMagma.lift FreeAddSemigroup.of
Instances For
The canonical multiplicative morphism from FreeMagma α
to FreeSemigroup α
.
Equations
- FreeMagma.toFreeSemigroup = ↑FreeMagma.lift FreeSemigroup.of
Instances For
Isomorphism between AddMagma.AssocQuotient (FreeAddMagma α)
and
FreeAddSemigroup α
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Isomorphism between Magma.AssocQuotient (FreeMagma α)
and FreeSemigroup α
.
Equations
- One or more equations did not get rendered due to their size.