Free groups #
This file defines free groups over a type. Furthermore, it is shown that the free group construction
is an instance of a monad. For the result that FreeGroup
is the left adjoint to the forgetful
functor from groups to types, see Algebra/Category/Group/Adjunctions
.
Main definitions #
FreeGroup
/FreeAddGroup
: the free group (resp. free additive group) associated to a typeα
defined as the words overa : α × Bool× Bool
modulo the relationa * x * x⁻¹ * b = a * b⁻¹ * b = a * b
.FreeGroup.mk
/FreeAddGroup.mk
: the canonical quotient mapList (α × Bool) → FreeGroup α× Bool) → FreeGroup α→ FreeGroup α
.FreeGroup.of
/FreeAddGroup.of
: the canonical injectionα → FreeGroup α→ FreeGroup α
.FreeGroup.lift f
/FreeAddGroup.lift
: the canonical group homomorphismFreeGroup α →* G→* G
given a groupG
and a functionf : α → G→ G
.
Main statements #
FreeGroup.Red.church_rosser
/FreeAddGroup.Red.church_rosser
: The Church-Rosser theorem for word reduction (also known as Newman's diamond lemma).FreeGroup.freeGroupUnitEquivInt
: The free group over the one-point type is isomorphic to the integers.- The free group construction is an instance of a monad.
Implementation details #
First we introduce the one step reduction relation FreeGroup.Red.Step
:
w * x * x⁻¹ * v ~> w * v⁻¹ * v ~> w * v
, its reflexive transitive closure FreeGroup.Red.trans
and prove that its join is an equivalence relation. Then we introduce FreeGroup α
as a quotient
over FreeGroup.Red.Step
.
For the additive version we introduce the same relation under a different name so that we can distinguish the quotient types more easily.
Tags #
free group, Newman's diamond lemma, Church-Rosser theorem
Equations
- One or more equations did not get rendered due to their size.
Predicate asserting that the word w₁
can be reduced to w₂
in one step, i.e. there
are words w₃ w₄
and letter x
such that w₁ = w₃ + x + (-x) + w₄
and w₂ = w₃w₄
Predicate asserting that the word w₁
can be reduced to w₂
in one step, i.e. there are words
w₃ w₄
and letter x
such that w₁ = w₃xx⁻¹w₄⁻¹w₄
and w₂ = w₃w₄
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
- FreeAddGroup.Red.not_step_singleton.match_1 motive x h_1 = Prod.casesOn x fun fst snd => h_1 fst snd
Equations
- FreeAddGroup.Red.Step.append_left_iff.match_1 motive x h_1 h_2 = List.casesOn x (h_1 ()) fun head tail => h_2 head tail
Equations
- FreeAddGroup.Red.Step.diamond_aux.match_1 tl x tl2 x motive x h_1 h_2 = Or.casesOn x (fun h => h_1 h) fun h => Exists.casesOn h fun w h => And.casesOn h fun left right => h_2 w left right
Equations
- FreeAddGroup.Red.Step.diamond_aux.match_2 x3 b3 tl x x4 b4 tl2 x x x x x motive x h_1 = And.casesOn x fun left right => h_1 left right
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.
Church-Rosser theorem for word reduction: If w1 w2 w3
are words such that w1
reduces
to w2
and w3
respectively, then there is a word w4
such that w2
and w3
reduce to w4
respectively. This is also known as Newman's diamond lemma.
Equations
- One or more equations did not get rendered due to their size.
Church-Rosser theorem for word reduction: If w1 w2 w3
are words such that w1
reduces
to w2
and w3
respectively, then there is a word w4
such that w2
and w3
reduce to w4
respectively. This is also known as Newman's diamond lemma.
Equations
- One or more equations did not get rendered due to their size.
The empty word []
only reduces to itself.
The empty word []
only reduces to itself.
If x
is a letter and w
is a word such that x + w
reduces to the empty word, then w
reduces to -x
.
Equations
- FreeAddGroup.Red.cons_nil_iff_singleton.match_1 motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
If x
is a letter and w
is a word such that xw
reduces to the empty word, then w
reduces
to x⁻¹⁻¹
If x
and y
are distinct letters and w₁ w₂
are words such that x + w₁
reduces
to y + w₂
, then w₁
reduces to -x + y + w₂
.
If x
and y
are distinct letters and w₁ w₂
are words such that xw₁
reduces to yw₂
, then
w₁
reduces to x⁻¹yw₂⁻¹yw₂
.
If w₁ w₂
are words such that w₁
reduces to w₂
, then w₂
is a sublist of
w₁
.
If w₁ w₂
are words such that w₁
reduces to w₂
, then w₂
is a sublist of w₁
.
The free additive group over a type, i.e. the words formed by the elements of the type and their formal inverses, quotient by one step reduction.
Equations
- FreeAddGroup α = Quot FreeAddGroup.Red.Step
The canonical map from list (α × bool)× bool)
to the free additive group on α
.
Equations
- FreeAddGroup.mk L = Quot.mk FreeAddGroup.Red.Step L
Equations
- FreeAddGroup.instZeroFreeAddGroup = { zero := FreeAddGroup.mk [] }
Equations
- FreeGroup.instOneFreeGroup = { one := FreeGroup.mk [] }
Equations
- FreeAddGroup.instInhabitedFreeAddGroup = { default := 0 }
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.
Transform a word representing a free group element into a word representing its negative.
Equations
- FreeAddGroup.negRev w = List.reverse (List.map (fun g => (g.fst, !g.snd)) w)
Transform a word representing a free group element into a word representing its inverse.
Equations
- FreeGroup.invRev w = List.reverse (List.map (fun g => (g.fst, !g.snd)) w)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : FreeAddGroup.Red.Step (FreeAddGroup.negRev a) (FreeAddGroup.negRev b)) = (_ : FreeAddGroup.Red.Step (FreeAddGroup.negRev a) (FreeAddGroup.negRev b))
Equations
- (_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a) = (_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a)
Equations
- FreeAddGroup.instAddGroupFreeAddGroup = AddGroup.mk (_ : ∀ (a : FreeAddGroup α), -a + a = 0)
of
is the canonical injection from the type to the free group over that type
by sending each element to the equivalence class of the letter that is the element.
Equations
- FreeAddGroup.of x = FreeAddGroup.mk [(x, true)]
of
is the canonical injection from the type to the free group over that type by sending each
element to the equivalence class of the letter that is the element.
Equations
- FreeGroup.of x = FreeGroup.mk [(x, true)]
The canonical map from the type to the additive free group is an injection.
Equations
- FreeAddGroup.of_injective.match_1 x x motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
The canonical map from the type to the free group is an injection.
Given f : α → β→ β
with β
an additive group, the canonical map
list (α × bool) → β× bool) → β→ β
Equations
- FreeAddGroup.Lift.aux f L = List.sum (List.map (fun x => bif x.snd then f x.fst else -f x.fst) L)
Given f : α → β→ β
with β
a group, the canonical map list (α × bool) → β× bool) → β→ β
Equations
- FreeGroup.Lift.aux f L = List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) L)
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
- One or more equations did not get rendered due to their size.
Equations
- (_ : FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂) = (_ : FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂)
If β
is an additive group, then any function from α
to β
extends uniquely to an
additive group homomorphism from the free additive group over α
to β
Equations
- One or more equations did not get rendered due to their size.
Two homomorphisms out of a free additive group are equal if they are equal on generators. See note [partially-applied ext lemmas].
Two homomorphisms out of a free group are equal if they are equal on generators.
See note [partially-applied ext lemmas].
Any function from α
to β
extends uniquely to an additive group homomorphism from
the additive free group over α
to the additive free group over β
.
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
- One or more equations did not get rendered due to their size.
Equations
- (_ : ↑(FreeAddGroup.map ↑e) (↑(FreeAddGroup.map ↑(Equiv.symm e)) x) = x) = (_ : ↑(FreeAddGroup.map ↑e) (↑(FreeAddGroup.map ↑(Equiv.symm e)) x) = x)
Equivalent types give rise to additively equivalent additive free groups.
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
- (_ : ↑(FreeAddGroup.map ↑(Equiv.symm e)) (↑(FreeAddGroup.map ↑e) x) = x) = (_ : ↑(FreeAddGroup.map ↑(Equiv.symm e)) (↑(FreeAddGroup.map ↑e) x) = x)
Equivalent types give rise to multiplicatively equivalent free groups.
The converse can be found in GroupTheory.FreeAbelianGroupFinsupp
,
as Equiv.of_freeGroupEquiv
Equations
- One or more equations did not get rendered due to their size.
If α
is an additive group, then any function from α
to α
extends uniquely to an
additive homomorphism from the additive free group over α
to α
.
Equations
- FreeAddGroup.sum = ↑FreeAddGroup.lift id
If α
is a group, then any function from α
to α
extends uniquely to a homomorphism from the
free group over α
to α
. This is the multiplicative version of FreeGroup.sum
.
Equations
- FreeGroup.prod = ↑FreeGroup.lift id
If α
is a group, then any function from α
to α
extends uniquely to a homomorphism from the
free group over α
to α
. This is the additive version of prod
.
Equations
- FreeGroup.sum x = ↑FreeGroup.prod x
The bijection between the additive free group on the empty type, and a type with one element.
Equations
- One or more equations did not get rendered due to their size.
Equations
- FreeAddGroup.freeAddGroupEmptyEquivAddUnit.match_1 motive x h_1 = PUnit.casesOn x (h_1 ())
Equations
- FreeAddGroup.instMonadFreeAddGroup = Monad.mk
Equations
- FreeGroup.instMonadFreeGroup = Monad.mk
The maximal reduction of a word. It is computable iff α
has decidable equality.
Equations
- FreeAddGroup.reduce t = List.rec [] (fun hd1 _tl1 ih => List.casesOn ih [hd1] fun hd2 tl2 => if hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd then tl2 else hd1 :: hd2 :: tl2) t
The maximal reduction of a word. It is computable
iff α
has decidable equality.
Equations
- FreeGroup.reduce t = List.rec [] (fun hd1 _tl1 ih => List.casesOn ih [hd1] fun hd2 tl2 => if hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd then tl2 else hd1 :: hd2 :: tl2) t
The first theorem that characterises the function reduce
: a word reduces to its
maximal reduction.
The first theorem that characterises the function reduce
: a word reduces to its maximal
reduction.
Equations
- FreeAddGroup.reduce.not.match_1 motive x x x x x h_1 h_2 = List.casesOn x (h_1 x x x x) fun head tail => Prod.casesOn head fun fst snd => h_2 fst snd tail x x x x
The second theorem that characterises the function reduce
: the maximal reduction of
a word only reduces to itself.
The second theorem that characterises the function reduce
: the maximal reduction of a word
only reduces to itself.
reduce
is idempotent, i.e. the maximal reduction of the maximal
reduction of a word is the maximal reduction of the word.
reduce
is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the
maximal reduction of the word.
Equations
- FreeAddGroup.reduce.Step.eq.match_1 motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
If a word reduces to another word, then they have a common maximal reduction.
If a word reduces to another word, then they have a common maximal reduction.
Alias of FreeGroup.reduce.eq_of_red
.
Alias of FreeAddGroup.reduce.eq_of_red
.
Equations
- FreeAddGroup.reduce.sound.match_1 motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
If two words correspond to the same element in the additive free group, then they have a common maximal reduction. This is the proof that the function that sends an element of the free group to its maximal reduction is well-defined.
If two words correspond to the same element in the free group, then they have a common maximal reduction. This is the proof that the function that sends an element of the free group to its maximal reduction is well-defined.
If two words have a common maximal reduction, then they correspond to the same element in the additive free group.
If two words have a common maximal reduction, then they correspond to the same element in the free group.
A word and its maximal reduction correspond to the same element of the additive free group.
A word and its maximal reduction correspond to the same element of the free group.
If words w₁ w₂
are such that w₁
reduces to w₂
, then w₂
reduces to the maximal
reduction of w₁
.
If words w₁ w₂
are such that w₁
reduces to w₂
, then w₂
reduces to the maximal reduction
of w₁
.
The function that sends an element of the additive free group to its maximal reduction.
Equations
- FreeAddGroup.toWord = Quot.lift FreeAddGroup.reduce (_ : ∀ (_L₁ _L₂ : List (α × Bool)), FreeAddGroup.Red.Step _L₁ _L₂ → FreeAddGroup.reduce _L₁ = FreeAddGroup.reduce _L₂)
Equations
- (_ : FreeAddGroup.reduce _L₁ = FreeAddGroup.reduce _L₂) = (_ : FreeAddGroup.reduce _L₁ = FreeAddGroup.reduce _L₂)
The function that sends an element of the free group to its maximal reduction.
Equations
- FreeGroup.toWord = Quot.lift FreeGroup.reduce (_ : ∀ (_L₁ _L₂ : List (α × Bool)), FreeGroup.Red.Step _L₁ _L₂ → FreeGroup.reduce _L₁ = FreeGroup.reduce _L₂)
Constructive Church-Rosser theorem (compare church_rosser
).
Equations
- FreeAddGroup.reduce.churchRosser H12 H13 = { val := FreeAddGroup.reduce L₁, property := (_ : FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁) ∧ FreeAddGroup.Red L₃ (FreeAddGroup.reduce L₁)) }
Equations
- (_ : FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁) ∧ FreeAddGroup.Red L₃ (FreeAddGroup.reduce L₁)) = (_ : FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁) ∧ FreeAddGroup.Red L₃ (FreeAddGroup.reduce L₁))
Constructive Church-Rosser theorem (compare church_rosser
).
Equations
- FreeGroup.reduce.churchRosser H12 H13 = { val := FreeGroup.reduce L₁, property := (_ : FreeGroup.Red L₂ (FreeGroup.reduce L₁) ∧ FreeGroup.Red L₃ (FreeGroup.reduce L₁)) }
Equations
- FreeAddGroup.instDecidableEqFreeAddGroup = Function.Injective.decidableEq (_ : Function.Injective FreeAddGroup.toWord)
Equations
- (_ : Function.Injective FreeAddGroup.toWord) = (_ : Function.Injective FreeAddGroup.toWord)
Equations
- FreeGroup.instDecidableEqFreeGroup = Function.Injective.decidableEq (_ : Function.Injective FreeGroup.toWord)
Equations
- One or more equations did not get rendered due to their size.
- FreeGroup.Red.decidableRel [] [] = isTrue (_ : FreeGroup.Red [] [])
- FreeGroup.Red.decidableRel [] (_hd2 :: _tl2) = isFalse (_ : FreeGroup.Red [] (_hd2 :: _tl2) → List.noConfusionType False (_hd2 :: _tl2) [])
A list containing every word that w₁
reduces to.
Equations
- FreeGroup.Red.enum L₁ = List.filter (fun b => decide (FreeGroup.Red L₁ b)) (List.sublists L₁)
Equations
- One or more equations did not get rendered due to their size.
The length of reduced words provides a norm on an additive free group.
Equations
The length of reduced words provides a norm on a free group.