Free constructions #
Main definitions #
free_magma α
: free magma (structure with binary operation without any axioms) over alphabetα
, defined inductively, with traversable instance and decidable equality.magma.free_semigroup α
: free semigroup over magmaα
.free_semigroup α
: free semigroup over alphabetα
, defined as a synonym forα × list α
(i.e. nonempty lists), with traversable instance and decidable equality.free_semigroup_free_magma α
: isomorphism betweenmagma.free_semigroup (free_magma α)
andfree_semigroup α
.free_magma.lift
: the universal property of the free magma, expressing its adjointness.
- of : Π {α : Type u}, α → free_magma α
- mul : Π {α : Type u}, free_magma α → free_magma α → free_magma α
Free magma over a given alphabet.
Instances for free_magma
- of : Π {α : Type u}, α → free_add_magma α
- add : Π {α : Type u}, free_add_magma α → free_add_magma α → free_add_magma α
Free nonabelian additive magma over a given alphabet.
Instances for free_add_magma
Equations
Equations
Equations
Equations
Recursor for free_add_magma
using x + y
instead of free_add_magma.add x y
.
Equations
- x.rec_on_add ih1 ih2 = x.rec_on ih1 ih2
Recursor for free_magma
using x * y
instead of free_magma.mul x y
.
Equations
- x.rec_on_mul ih1 ih2 = x.rec_on ih1 ih2
Lifts a function α → β
to a magma homomorphism free_magma α → β
given a magma β
.
Equations
- free_magma.lift_aux f (x * y) = free_magma.lift_aux f x * free_magma.lift_aux f y
- free_magma.lift_aux f (free_magma.of x) = f x
Lifts a function α → β
to an additive magma homomorphism free_add_magma α → β
given
an additive magma β
.
Equations
- free_add_magma.lift_aux f (x + y) = free_add_magma.lift_aux f x + free_add_magma.lift_aux f y
- free_add_magma.lift_aux f (free_add_magma.of x) = f x
The universal property of the free additive magma expressing its adjointness.
Equations
- free_add_magma.lift = {to_fun := λ (f : α → β), {to_fun := free_add_magma.lift_aux f, map_add' := _}, inv_fun := λ (F : add_hom (free_add_magma α) β), ⇑F ∘ free_add_magma.of, left_inv := _, right_inv := _}
The universal property of the free magma expressing its adjointness.
Equations
- free_magma.lift = {to_fun := λ (f : α → β), {to_fun := free_magma.lift_aux f, map_mul' := _}, inv_fun := λ (F : free_magma α →ₙ* β), ⇑F ∘ free_magma.of, left_inv := _, right_inv := _}
The unique magma homomorphism free_magma α → free_magma β
that sends
each of x
to of (f x)
.
Equations
- free_magma.map f (x * y) = free_magma.map f x * free_magma.map f y
- free_magma.map f (free_magma.of x) = free_magma.of (f x)
The unique additive magma homomorphism free_add_magma α → free_add_magma β
that sends
each of x
to of (f x)
.
Equations
- free_add_magma.map f (x + y) = free_add_magma.map f x + free_add_magma.map f y
- free_add_magma.map f (free_add_magma.of x) = free_add_magma.of (f x)
Equations
Equations
Recursor on free_add_magma
using pure
instead of of
.
Equations
- x.rec_on_pure ih1 ih2 = x.rec_on_add ih1 ih2
Recursor on free_magma
using pure
instead of of
.
Equations
- x.rec_on_pure ih1 ih2 = x.rec_on_mul ih1 ih2
free_magma
is traversable.
Equations
- free_magma.traverse F (x * y) = has_mul.mul <$> free_magma.traverse F x <*> free_magma.traverse F y
- free_magma.traverse F (free_magma.of x) = free_magma.of <$> F x
free_add_magma
is traversable.
Equations
- free_add_magma.traverse F (x + y) = has_add.add <$> free_add_magma.traverse F x <*> free_add_magma.traverse F y
- free_add_magma.traverse F (free_add_magma.of x) = free_add_magma.of <$> F x
Equations
- free_magma.is_lawful_traversable = {to_is_lawful_functor := free_magma.is_lawful_traversable._proof_1, id_traverse := free_magma.is_lawful_traversable._proof_2, comp_traverse := free_magma.is_lawful_traversable._proof_3, traverse_eq_map_id := free_magma.is_lawful_traversable._proof_4, naturality := free_magma.is_lawful_traversable._proof_5}
Equations
- free_add_magma.is_lawful_traversable = {to_is_lawful_functor := free_add_magma.is_lawful_traversable._proof_1, id_traverse := free_add_magma.is_lawful_traversable._proof_2, comp_traverse := free_add_magma.is_lawful_traversable._proof_3, traverse_eq_map_id := free_add_magma.is_lawful_traversable._proof_4, naturality := free_add_magma.is_lawful_traversable._proof_5}
Equations
- free_magma.has_repr = {repr := free_magma.repr _inst_1}
Equations
- free_add_magma.has_repr = {repr := free_add_magma.repr _inst_1}
Length of an element of a free magma.
Length of an element of a free additive magma.
Free semigroup over a magma.
Equations
- magma.free_semigroup α = quot (magma.free_semigroup.r α)
Instances for magma.free_semigroup
Free additive semigroup over an additive magma.
Equations
Instances for add_magma.free_add_semigroup
Embedding from magma to its free semigroup.
Equations
- magma.free_semigroup.of = quot.mk (magma.free_semigroup.r α)
Embedding from additive magma to its free additive semigroup.
Equations
Equations
- add_magma.free_add_semigroup.add_semigroup = {add := λ (x y : add_magma.free_add_semigroup α), quot.lift_on x (λ (p : α), quot.lift_on y (λ (q : α), quot.mk (add_magma.free_add_semigroup.r α) (p + q)) _) _, add_assoc := _}
Equations
- magma.free_semigroup.semigroup = {mul := λ (x y : magma.free_semigroup α), quot.lift_on x (λ (p : α), quot.lift_on y (λ (q : α), quot.mk (magma.free_semigroup.r α) (p * q)) _) _, mul_assoc := _}
Lifts a magma homomorphism α → β
to a semigroup homomorphism magma.free_semigroup α → β
given a semigroup β
.
Equations
- magma.free_semigroup.lift f hf = quot.lift f _
Lifts an additive magma homomorphism α → β
to an additive semigroup homomorphism
add_magma.free_add_semigroup α → β
given an additive semigroup β
.
Equations
- add_magma.free_add_semigroup.lift f hf = quot.lift f _
From an additive magma homomorphism α → β
to an additive semigroup homomorphism
add_magma.free_add_semigroup α → add_magma.free_add_semigroup β
.
Equations
From a magma homomorphism α → β
to a semigroup homomorphism
magma.free_semigroup α → magma.free_semigroup β
.
Equations
Free additive semigroup over a given alphabet.
Equations
- free_add_semigroup α = (α × list α)
Free semigroup over a given alphabet. (Note: In this definition, the free semigroup does not contain the empty word.)
Equations
- free_semigroup α = (α × list α)
The embedding α → free_semigroup α
.
Equations
- free_semigroup.of x = (x, list.nil α)
The embedding α → free_add_semigroup α
.
Equations
- free_add_semigroup.of x = (x, list.nil α)
Equations
Recursor for free additive semigroup using of
and +
.
Recursor for free semigroup using of
and *
.
Auxiliary function for free_semigroup.lift
.
Equations
- free_semigroup.lift' f x (hd :: tl) = f x * free_semigroup.lift' f hd tl
- free_semigroup.lift' f x list.nil = f x
Auxiliary function for free_semigroup.lift
.
Equations
- free_add_semigroup.lift' f x (hd :: tl) = f x + free_add_semigroup.lift' f hd tl
- free_add_semigroup.lift' f x list.nil = f x
Lifts a function α → β
to a semigroup homomorphism free_semigroup α → β
given
a semigroup β
.
Equations
- free_semigroup.lift f x = free_semigroup.lift' f x.fst x.snd
Lifts a function α → β
to an additive semigroup homomorphism
free_add_semigroup α → β
given an additive semigroup β
.
Equations
- free_add_semigroup.lift f x = free_add_semigroup.lift' f x.fst x.snd
The unique semigroup homomorphism that sends of x
to of (f x)
.
Equations
The unique additive semigroup homomorphism that sends of x
to of (f x)
.
Equations
Equations
Equations
Recursor that uses pure
instead of of
.
Equations
- x.rec_on_pure ih1 ih2 = x.rec_on ih1 ih2
Recursor that uses pure
instead of of
.
Equations
- x.rec_on_pure ih1 ih2 = x.rec_on ih1 ih2
free_add_semigroup
is traversable.
Equations
- free_add_semigroup.traverse F x = x.rec_on_pure (λ (x : α), has_pure.pure <$> F x) (λ (x : α) (y : free_add_semigroup α) (ihx ihy : m (free_add_semigroup β)), has_add.add <$> ihx <*> ihy)
free_semigroup
is traversable.
Equations
- free_semigroup.traverse F x = x.rec_on_pure (λ (x : α), has_pure.pure <$> F x) (λ (x : α) (y : free_semigroup α) (ihx ihy : m (free_semigroup β)), has_mul.mul <$> ihx <*> ihy)
Equations
- free_add_semigroup.is_lawful_traversable = {to_is_lawful_functor := free_add_semigroup.is_lawful_traversable._proof_1, id_traverse := free_add_semigroup.is_lawful_traversable._proof_2, comp_traverse := free_add_semigroup.is_lawful_traversable._proof_3, traverse_eq_map_id := free_add_semigroup.is_lawful_traversable._proof_4, naturality := free_add_semigroup.is_lawful_traversable._proof_5}
Equations
- free_semigroup.is_lawful_traversable = {to_is_lawful_functor := free_semigroup.is_lawful_traversable._proof_1, id_traverse := free_semigroup.is_lawful_traversable._proof_2, comp_traverse := free_semigroup.is_lawful_traversable._proof_3, traverse_eq_map_id := free_semigroup.is_lawful_traversable._proof_4, naturality := free_semigroup.is_lawful_traversable._proof_5}
Equations
Isomorphism between magma.free_semigroup (free_magma α)
and free_semigroup α
.
Equations
Isomorphism between
add_magma.free_add_semigroup (free_add_magma α)
and free_add_semigroup α
.