Free groups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 free_group is the left adjoint to the forgetful
functor from groups to types, see algebra/category/Group/adjunctions.
Main definitions #
free_group/free_add_group: the free group (resp. free additive group) associated to a typeαdefined as the words overa : α × boolmodulo the relationa * x * x⁻¹ * b = a * b.free_group.mk/free_add_group.mk: the canonical quotient maplist (α × bool) → free_group α.free_group.of/free_add_group.of: the canonical injectionα → free_group α.free_group.lift f/free_add_group.lift: the canonical group homomorphismfree_group α →* Ggiven a groupGand a functionf : α → G.
Main statements #
free_group.church_rosser/free_add_group.church_rosser: The Church-Rosser theorem for word reduction (also known as Newman's diamond lemma).free_group.free_group_unit_equiv_int: 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 free_group.red.step:
w * x * x⁻¹ * v ~> w * v, its reflexive transitive closure free_group.red.trans
and prove that its join is an equivalence relation. Then we introduce free_group α as a quotient
over free_group.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
Reflexive-transitive closure of red.step
Instances for free_group.red
Reflexive-transitive closure of red.step
@[refl]
@[trans]
theorem
free_group.red.trans
{α : Type u}
{L₁ L₂ L₃ : list (α × bool)} :
free_group.red L₁ L₂ → free_group.red L₂ L₃ → free_group.red L₁ L₃
@[trans]
theorem
free_add_group.red.trans
{α : Type u}
{L₁ L₂ L₃ : list (α × bool)} :
free_add_group.red L₁ L₂ → free_add_group.red L₂ L₃ → free_add_group.red L₁ L₃
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₄
theorem
free_group.red.step.append_left
{α : Type u}
{L₁ L₂ L₃ : list (α × bool)} :
free_group.red.step L₂ L₃ → free_group.red.step (L₁ ++ L₂) (L₁ ++ L₃)
theorem
free_add_group.red.step.append_left
{α : Type u}
{L₁ L₂ L₃ : list (α × bool)} :
free_add_group.red.step L₂ L₃ → free_add_group.red.step (L₁ ++ L₂) (L₁ ++ L₃)
theorem
free_group.red.step.cons
{α : Type u}
{L₁ L₂ : list (α × bool)}
{x : α × bool}
(H : free_group.red.step L₁ L₂) :
free_group.red.step (x :: L₁) (x :: L₂)
theorem
free_add_group.red.step.cons
{α : Type u}
{L₁ L₂ : list (α × bool)}
{x : α × bool}
(H : free_add_group.red.step L₁ L₂) :
free_add_group.red.step (x :: L₁) (x :: L₂)
theorem
free_add_group.red.step.append_right
{α : Type u}
{L₁ L₂ L₃ : list (α × bool)} :
free_add_group.red.step L₁ L₂ → free_add_group.red.step (L₁ ++ L₃) (L₂ ++ L₃)
theorem
free_group.red.step.append_right
{α : Type u}
{L₁ L₂ L₃ : list (α × bool)} :
free_group.red.step L₁ L₂ → free_group.red.step (L₁ ++ L₃) (L₂ ++ L₃)
theorem
free_add_group.red.step.cons_cons_iff
{α : Type u}
{L₁ L₂ : list (α × bool)}
{p : α × bool} :
free_add_group.red.step (p :: L₁) (p :: L₂) ↔ free_add_group.red.step L₁ L₂
theorem
free_group.red.step.cons_cons_iff
{α : Type u}
{L₁ L₂ : list (α × bool)}
{p : α × bool} :
free_group.red.step (p :: L₁) (p :: L₂) ↔ free_group.red.step L₁ L₂
theorem
free_add_group.red.step.append_left_iff
{α : Type u}
{L₁ L₂ : list (α × bool)}
(L : list (α × bool)) :
free_add_group.red.step (L ++ L₁) (L ++ L₂) ↔ free_add_group.red.step L₁ L₂
theorem
free_group.red.step.append_left_iff
{α : Type u}
{L₁ L₂ : list (α × bool)}
(L : list (α × bool)) :
free_group.red.step (L ++ L₁) (L ++ L₂) ↔ free_group.red.step L₁ L₂
theorem
free_group.red.step.diamond
{α : Type u}
{L₁ L₂ L₃ L₄ : list (α × bool)} :
free_group.red.step L₁ L₃ → free_group.red.step L₂ L₄ → L₁ = L₂ → (L₃ = L₄ ∨ ∃ (L₅ : list (α × bool)), free_group.red.step L₃ L₅ ∧ free_group.red.step L₄ L₅)
theorem
free_add_group.red.step.diamond
{α : Type u}
{L₁ L₂ L₃ L₄ : list (α × bool)} :
free_add_group.red.step L₁ L₃ → free_add_group.red.step L₂ L₄ → L₁ = L₂ → (L₃ = L₄ ∨ ∃ (L₅ : list (α × bool)), free_add_group.red.step L₃ L₅ ∧ free_add_group.red.step L₄ L₅)
theorem
free_add_group.red.step.to_red
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_add_group.red.step L₁ L₂ → free_add_group.red L₁ L₂
theorem
free_group.red.step.to_red
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_group.red.step L₁ L₂ → free_group.red L₁ L₂
theorem
free_group.red.church_rosser
{α : Type u}
{L₁ L₂ L₃ : list (α × bool)} :
free_group.red L₁ L₂ → free_group.red L₁ L₃ → relation.join free_group.red L₂ L₃
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.
theorem
free_add_group.red.church_rosser
{α : Type u}
{L₁ L₂ L₃ : list (α × bool)} :
free_add_group.red L₁ L₂ → free_add_group.red L₁ L₃ → relation.join free_add_group.red L₂ L₃
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.
theorem
free_add_group.red.cons_cons
{α : Type u}
{L₁ L₂ : list (α × bool)}
{p : α × bool} :
free_add_group.red L₁ L₂ → free_add_group.red (p :: L₁) (p :: L₂)
theorem
free_group.red.cons_cons
{α : Type u}
{L₁ L₂ : list (α × bool)}
{p : α × bool} :
free_group.red L₁ L₂ → free_group.red (p :: L₁) (p :: L₂)
theorem
free_group.red.cons_cons_iff
{α : Type u}
{L₁ L₂ : list (α × bool)}
(p : α × bool) :
free_group.red (p :: L₁) (p :: L₂) ↔ free_group.red L₁ L₂
theorem
free_add_group.red.cons_cons_iff
{α : Type u}
{L₁ L₂ : list (α × bool)}
(p : α × bool) :
free_add_group.red (p :: L₁) (p :: L₂) ↔ free_add_group.red L₁ L₂
theorem
free_add_group.red.append_append_left_iff
{α : Type u}
{L₁ L₂ : list (α × bool)}
(L : list (α × bool)) :
free_add_group.red (L ++ L₁) (L ++ L₂) ↔ free_add_group.red L₁ L₂
theorem
free_group.red.append_append_left_iff
{α : Type u}
{L₁ L₂ : list (α × bool)}
(L : list (α × bool)) :
free_group.red (L ++ L₁) (L ++ L₂) ↔ free_group.red L₁ L₂
theorem
free_group.red.append_append
{α : Type u}
{L₁ L₂ L₃ L₄ : list (α × bool)}
(h₁ : free_group.red L₁ L₃)
(h₂ : free_group.red L₂ L₄) :
free_group.red (L₁ ++ L₂) (L₃ ++ L₄)
theorem
free_add_group.red.append_append
{α : Type u}
{L₁ L₂ L₃ L₄ : list (α × bool)}
(h₁ : free_add_group.red L₁ L₃)
(h₂ : free_add_group.red L₂ L₄) :
free_add_group.red (L₁ ++ L₂) (L₃ ++ L₄)
theorem
free_add_group.red.to_append_iff
{α : Type u}
{L L₁ L₂ : list (α × bool)} :
free_add_group.red L (L₁ ++ L₂) ↔ ∃ (L₃ L₄ : list (α × bool)), L = L₃ ++ L₄ ∧ free_add_group.red L₃ L₁ ∧ free_add_group.red L₄ L₂
theorem
free_group.red.to_append_iff
{α : Type u}
{L L₁ L₂ : list (α × bool)} :
free_group.red L (L₁ ++ L₂) ↔ ∃ (L₃ L₄ : list (α × bool)), L = L₃ ++ L₄ ∧ free_group.red L₃ L₁ ∧ free_group.red L₄ L₂
theorem
free_group.red.cons_nil_iff_singleton
{α : Type u}
{L : list (α × bool)}
{x : α}
{b : bool} :
free_group.red ((x, b) :: L) list.nil ↔ free_group.red L [(x, !b)]
If x is a letter and w is a word such that xw reduces to the empty word, then w reduces
to x⁻¹
theorem
free_add_group.red.cons_nil_iff_singleton
{α : Type u}
{L : list (α × bool)}
{x : α}
{b : bool} :
free_add_group.red ((x, b) :: L) list.nil ↔ free_add_group.red L [(x, !b)]
If x is a letter and w is a word such that x + w reduces to the empty word,
then w reduces to -x.
theorem
free_group.red.inv_of_red_of_ne
{α : Type u}
{L₁ L₂ : list (α × bool)}
{x1 : α}
{b1 : bool}
{x2 : α}
{b2 : bool}
(H1 : (x1, b1) ≠ (x2, b2))
(H2 : free_group.red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) :
free_group.red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
If x and y are distinct letters and w₁ w₂ are words such that xw₁ reduces to yw₂, then
w₁ reduces to x⁻¹yw₂.
theorem
free_add_group.red.neg_of_red_of_ne
{α : Type u}
{L₁ L₂ : list (α × bool)}
{x1 : α}
{b1 : bool}
{x2 : α}
{b2 : bool}
(H1 : (x1, b1) ≠ (x2, b2))
(H2 : free_add_group.red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) :
free_add_group.red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
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₂.
theorem
free_add_group.red.step.sublist
{α : Type u}
{L₁ L₂ : list (α × bool)}
(H : free_add_group.red.step L₁ L₂) :
L₂ <+ L₁
theorem
free_group.red.step.sublist
{α : Type u}
{L₁ L₂ : list (α × bool)}
(H : free_group.red.step L₁ L₂) :
L₂ <+ L₁
@[protected]
theorem
free_add_group.red.sublist
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_add_group.red L₁ L₂ → L₂ <+ L₁
If w₁ w₂ are words such that w₁ reduces to w₂,
then w₂ is a sublist of w₁.
@[protected]
theorem
free_group.red.sublist
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_group.red L₁ L₂ → L₂ <+ L₁
If w₁ w₂ are words such that w₁ reduces to w₂, then w₂ is a sublist of w₁.
theorem
free_add_group.red.length_le
{α : Type u}
{L₁ L₂ : list (α × bool)}
(h : free_add_group.red L₁ L₂) :
theorem
free_group.red.length_le
{α : Type u}
{L₁ L₂ : list (α × bool)}
(h : free_group.red L₁ L₂) :
theorem
free_group.red.sizeof_of_step
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_group.red.step L₁ L₂ → L₂.sizeof < L₁.sizeof
theorem
free_add_group.red.sizeof_of_step
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_add_group.red.step L₁ L₂ → L₂.sizeof < L₁.sizeof
theorem
free_add_group.red.antisymm
{α : Type u}
{L₁ L₂ : list (α × bool)}
(h₁₂ : free_add_group.red L₁ L₂)
(h₂₁ : free_add_group.red L₂ L₁) :
L₁ = L₂
theorem
free_group.red.antisymm
{α : Type u}
{L₁ L₂ : list (α × bool)}
(h₁₂ : free_group.red L₁ L₂)
(h₂₁ : free_group.red L₂ L₁) :
L₁ = L₂
theorem
free_group.join_red_of_step
{α : Type u}
{L₁ L₂ : list (α × bool)}
(h : free_group.red.step L₁ L₂) :
relation.join free_group.red L₁ L₂
theorem
free_add_group.join_red_of_step
{α : Type u}
{L₁ L₂ : list (α × bool)}
(h : free_add_group.red.step L₁ L₂) :
theorem
free_add_group.eqv_gen_step_iff_join_red
{α : Type u}
{L₁ L₂ : list (α × bool)} :
eqv_gen free_add_group.red.step L₁ L₂ ↔ relation.join free_add_group.red L₁ L₂
theorem
free_group.eqv_gen_step_iff_join_red
{α : Type u}
{L₁ L₂ : list (α × bool)} :
eqv_gen free_group.red.step L₁ L₂ ↔ relation.join free_group.red L₁ L₂
The free 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
- free_group α = quot free_group.red.step
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
The canonical map from list (α × bool) to the free group on α.
Equations
- free_group.mk L = quot.mk free_group.red.step L
The canonical map from list (α × bool) to the free additive group on α.
Equations
- free_add_group.mk L = quot.mk free_add_group.red.step L
@[simp]
theorem
free_add_group.quot_mk_eq_mk
{α : Type u}
{L : list (α × bool)} :
quot.mk free_add_group.red.step L = free_add_group.mk L
@[simp]
theorem
free_group.quot_mk_eq_mk
{α : Type u}
{L : list (α × bool)} :
quot.mk free_group.red.step L = free_group.mk L
@[simp]
theorem
free_add_group.quot_map_mk
{α : Type u}
{L : list (α × bool)}
(β : Type v)
(f : list (α × bool) → list (β × bool))
(H : (free_add_group.red.step ⇒ free_add_group.red.step) f f) :
quot.map f H (free_add_group.mk L) = free_add_group.mk (f L)
@[simp]
theorem
free_group.quot_map_mk
{α : Type u}
{L : list (α × bool)}
(β : Type v)
(f : list (α × bool) → list (β × bool))
(H : (free_group.red.step ⇒ free_group.red.step) f f) :
quot.map f H (free_group.mk L) = free_group.mk (f L)
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- free_group.inhabited = {default := 1}
@[protected, instance]
Equations
- free_add_group.has_add = {add := λ (x y : free_add_group α), quot.lift_on x (λ (L₁ : list (α × bool)), quot.lift_on y (λ (L₂ : list (α × bool)), free_add_group.mk (L₁ ++ L₂)) _) _}
@[protected, instance]
Equations
- free_group.has_mul = {mul := λ (x y : free_group α), quot.lift_on x (λ (L₁ : list (α × bool)), quot.lift_on y (λ (L₂ : list (α × bool)), free_group.mk (L₁ ++ L₂)) _) _}
@[simp]
theorem
free_group.mul_mk
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_group.mk L₁ * free_group.mk L₂ = free_group.mk (L₁ ++ L₂)
@[simp]
theorem
free_add_group.add_mk
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_add_group.mk L₁ + free_add_group.mk L₂ = free_add_group.mk (L₁ ++ L₂)
@[simp]
theorem
free_group.inv_rev_length
{α : Type u}
{L₁ : list (α × bool)} :
(free_group.inv_rev L₁).length = L₁.length
@[simp]
theorem
free_add_group.neg_rev_length
{α : Type u}
{L₁ : list (α × bool)} :
(free_add_group.neg_rev L₁).length = L₁.length
@[simp]
@[simp]
theorem
free_group.inv_rev_inv_rev
{α : Type u}
{L₁ : list (α × bool)} :
free_group.inv_rev (free_group.inv_rev L₁) = L₁
@[simp]
@[simp]
@[protected, instance]
Equations
- free_add_group.has_neg = {neg := quot.map free_add_group.neg_rev free_add_group.has_neg._proof_1}
@[protected, instance]
Equations
- free_group.has_inv = {inv := quot.map free_group.inv_rev free_group.has_inv._proof_1}
@[simp]
@[simp]
theorem
free_add_group.red.step.neg_rev
{α : Type u}
{L₁ L₂ : list (α × bool)}
(h : free_add_group.red.step L₁ L₂) :
theorem
free_group.red.step.inv_rev
{α : Type u}
{L₁ L₂ : list (α × bool)}
(h : free_group.red.step L₁ L₂) :
theorem
free_add_group.red.neg_rev
{α : Type u}
{L₁ L₂ : list (α × bool)}
(h : free_add_group.red L₁ L₂) :
@[simp]
@[simp]
theorem
free_group.red.step_inv_rev_iff
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_group.red.step (free_group.inv_rev L₁) (free_group.inv_rev L₂) ↔ free_group.red.step L₁ L₂
@[simp]
theorem
free_group.red_inv_rev_iff
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_group.red (free_group.inv_rev L₁) (free_group.inv_rev L₂) ↔ free_group.red L₁ L₂
@[simp]
@[protected, instance]
Equations
- free_group.group = {mul := has_mul.mul free_group.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default 1 has_mul.mul free_group.group._proof_4 free_group.group._proof_5, npow_zero' := _, npow_succ' := _, inv := has_inv.inv free_group.has_inv, div := div_inv_monoid.div._default has_mul.mul free_group.group._proof_8 1 free_group.group._proof_9 free_group.group._proof_10 (div_inv_monoid.npow._default 1 has_mul.mul free_group.group._proof_4 free_group.group._proof_5) free_group.group._proof_11 free_group.group._proof_12 has_inv.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default has_mul.mul free_group.group._proof_14 1 free_group.group._proof_15 free_group.group._proof_16 (div_inv_monoid.npow._default 1 has_mul.mul free_group.group._proof_4 free_group.group._proof_5) free_group.group._proof_17 free_group.group._proof_18 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[protected, instance]
Equations
- free_add_group.add_group = {add := has_add.add free_add_group.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul._default 0 has_add.add free_add_group.add_group._proof_4 free_add_group.add_group._proof_5, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg free_add_group.has_neg, sub := sub_neg_monoid.sub._default has_add.add free_add_group.add_group._proof_8 0 free_add_group.add_group._proof_9 free_add_group.add_group._proof_10 (sub_neg_monoid.nsmul._default 0 has_add.add free_add_group.add_group._proof_4 free_add_group.add_group._proof_5) free_add_group.add_group._proof_11 free_add_group.add_group._proof_12 has_neg.neg, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul._default has_add.add free_add_group.add_group._proof_14 0 free_add_group.add_group._proof_15 free_add_group.add_group._proof_16 (sub_neg_monoid.nsmul._default 0 has_add.add free_add_group.add_group._proof_4 free_add_group.add_group._proof_5) free_add_group.add_group._proof_17 free_add_group.add_group._proof_18 has_neg.neg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
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
- free_group.of x = free_group.mk [(x, bool.tt)]
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
- free_add_group.of x = free_add_group.mk [(x, bool.tt)]
theorem
free_add_group.red.exact
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_add_group.mk L₁ = free_add_group.mk L₂ ↔ relation.join free_add_group.red L₁ L₂
theorem
free_group.red.exact
{α : Type u}
{L₁ L₂ : list (α × bool)} :
free_group.mk L₁ = free_group.mk L₂ ↔ relation.join free_group.red L₁ L₂
The canonical map from the type to the additive free group is an injection.
The canonical map from the type to the free group is an injection.
theorem
free_add_group.red.step.lift
{α : Type u}
{L₁ L₂ : list (α × bool)}
{β : Type v}
[add_group β]
{f : α → β}
(H : free_add_group.red.step L₁ L₂) :
free_add_group.lift.aux f L₁ = free_add_group.lift.aux f L₂
theorem
free_group.red.step.lift
{α : Type u}
{L₁ L₂ : list (α × bool)}
{β : Type v}
[group β]
{f : α → β}
(H : free_group.red.step L₁ L₂) :
free_group.lift.aux f L₁ = free_group.lift.aux f L₂
@[simp]
theorem
free_group.lift_symm_apply
{α : Type u}
{β : Type v}
[group β]
(g : free_group α →* β)
(ᾰ : α) :
⇑(free_group.lift.symm) g ᾰ = (⇑g ∘ free_group.of) ᾰ
If β is a group, then any function from α to β
extends uniquely to a group homomorphism from
the free group over α to β
Equations
- free_group.lift = {to_fun := λ (f : α → β), monoid_hom.mk' (quot.lift (free_group.lift.aux f) _) _, inv_fun := λ (g : free_group α →* β), ⇑g ∘ free_group.of, left_inv := _, right_inv := _}
@[simp]
theorem
free_add_group.lift_symm_apply
{α : Type u}
{β : Type v}
[add_group β]
(g : free_add_group α →+ β)
(ᾰ : α) :
⇑(free_add_group.lift.symm) g ᾰ = (⇑g ∘ free_add_group.of) ᾰ
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
- free_add_group.lift = {to_fun := λ (f : α → β), add_monoid_hom.mk' (quot.lift (free_add_group.lift.aux f) _) _, inv_fun := λ (g : free_add_group α →+ β), ⇑g ∘ free_add_group.of, left_inv := _, right_inv := _}
@[simp]
theorem
free_group.lift.of
{α : Type u}
{β : Type v}
[group β]
{f : α → β}
{x : α} :
⇑(⇑free_group.lift f) (free_group.of x) = f x
@[simp]
theorem
free_add_group.lift.of
{α : Type u}
{β : Type v}
[add_group β]
{f : α → β}
{x : α} :
⇑(⇑free_add_group.lift f) (free_add_group.of x) = f x
theorem
free_add_group.lift.unique
{α : Type u}
{β : Type v}
[add_group β]
{f : α → β}
(g : free_add_group α →+ β)
(hg : ∀ (x : α), ⇑g (free_add_group.of x) = f x)
{x : free_add_group α} :
⇑g x = ⇑(⇑free_add_group.lift f) x
theorem
free_group.lift.unique
{α : Type u}
{β : Type v}
[group β]
{f : α → β}
(g : free_group α →* β)
(hg : ∀ (x : α), ⇑g (free_group.of x) = f x)
{x : free_group α} :
⇑g x = ⇑(⇑free_group.lift f) x
@[ext]
theorem
free_group.ext_hom
{α : Type u}
{G : Type u_1}
[group G]
(f g : free_group α →* G)
(h : ∀ (a : α), ⇑f (free_group.of a) = ⇑g (free_group.of a)) :
f = g
Two homomorphisms out of a free group are equal if they are equal on generators.
@[ext]
theorem
free_add_group.ext_hom
{α : Type u}
{G : Type u_1}
[add_group G]
(f g : free_add_group α →+ G)
(h : ∀ (a : α), ⇑f (free_add_group.of a) = ⇑g (free_add_group.of a)) :
f = g
Two homomorphisms out of a free additive group are equal if they are equal on generators.
theorem
free_group.lift.of_eq
{α : Type u}
(x : free_group α) :
⇑(⇑free_group.lift free_group.of) x = x
theorem
free_add_group.lift.range_le
{α : Type u}
{β : Type v}
[add_group β]
{f : α → β}
{s : add_subgroup β}
(H : set.range f ⊆ ↑s) :
(⇑free_add_group.lift f).range ≤ s
theorem
free_group.lift.range_eq_closure
{α : Type u}
{β : Type v}
[group β]
{f : α → β} :
(⇑free_group.lift f).range = subgroup.closure (set.range f)
Any function from α to β extends uniquely
to a group homomorphism from the free group
over α to the free group over β.
Equations
- free_group.map f = monoid_hom.mk' (quot.map (list.map (λ (x : α × bool), (f x.fst, x.snd))) _) _
Any function from α to β extends uniquely to an additive group homomorphism
from the additive free group over α to the additive free group over β.
Equations
- free_add_group.map f = add_monoid_hom.mk' (quot.map (list.map (λ (x : α × bool), (f x.fst, x.snd))) _) _
@[simp]
theorem
free_group.map.mk
{α : Type u}
{L : list (α × bool)}
{β : Type v}
{f : α → β} :
⇑(free_group.map f) (free_group.mk L) = free_group.mk (list.map (λ (x : α × bool), (f x.fst, x.snd)) L)
@[simp]
theorem
free_add_group.map.mk
{α : Type u}
{L : list (α × bool)}
{β : Type v}
{f : α → β} :
⇑(free_add_group.map f) (free_add_group.mk L) = free_add_group.mk (list.map (λ (x : α × bool), (f x.fst, x.snd)) L)
@[simp]
@[simp]
@[simp]
@[simp]
theorem
free_add_group.map.id'
{α : Type u}
(x : free_add_group α) :
⇑(free_add_group.map (λ (z : α), z)) x = x
theorem
free_group.map.comp
{α : Type u}
{β : Type v}
{γ : Type w}
(f : α → β)
(g : β → γ)
(x : free_group α) :
⇑(free_group.map g) (⇑(free_group.map f) x) = ⇑(free_group.map (g ∘ f)) x
theorem
free_add_group.map.comp
{α : Type u}
{β : Type v}
{γ : Type w}
(f : α → β)
(g : β → γ)
(x : free_add_group α) :
⇑(free_add_group.map g) (⇑(free_add_group.map f) x) = ⇑(free_add_group.map (g ∘ f)) x
@[simp]
theorem
free_add_group.map.of
{α : Type u}
{β : Type v}
{f : α → β}
{x : α} :
⇑(free_add_group.map f) (free_add_group.of x) = free_add_group.of (f x)
@[simp]
theorem
free_group.map.of
{α : Type u}
{β : Type v}
{f : α → β}
{x : α} :
⇑(free_group.map f) (free_group.of x) = free_group.of (f x)
theorem
free_group.map.unique
{α : Type u}
{β : Type v}
{f : α → β}
(g : free_group α →* free_group β)
(hg : ∀ (x : α), ⇑g (free_group.of x) = free_group.of (f x))
{x : free_group α} :
⇑g x = ⇑(free_group.map f) x
theorem
free_add_group.map.unique
{α : Type u}
{β : Type v}
{f : α → β}
(g : free_add_group α →+ free_add_group β)
(hg : ∀ (x : α), ⇑g (free_add_group.of x) = free_add_group.of (f x))
{x : free_add_group α} :
⇑g x = ⇑(free_add_group.map f) x
theorem
free_group.map_eq_lift
{α : Type u}
{β : Type v}
{f : α → β}
{x : free_group α} :
⇑(free_group.map f) x = ⇑(⇑free_group.lift (free_group.of ∘ f)) x
theorem
free_add_group.map_eq_lift
{α : Type u}
{β : Type v}
{f : α → β}
{x : free_add_group α} :
⇑(free_add_group.map f) x = ⇑(⇑free_add_group.lift (free_add_group.of ∘ f)) x
@[simp]
theorem
free_group.free_group_congr_apply
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β)
(ᾰ : free_group α) :
⇑(free_group.free_group_congr e) ᾰ = ⇑(free_group.map ⇑e) ᾰ
@[simp]
theorem
free_add_group.free_add_group_congr_apply
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β)
(ᾰ : free_add_group α) :
def
free_group.free_group_congr
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β) :
free_group α ≃* free_group β
Equivalent types give rise to multiplicatively equivalent free groups.
The converse can be found in group_theory.free_abelian_group_finsupp,
as equiv.of_free_group_equiv
Equations
- free_group.free_group_congr e = {to_fun := ⇑(free_group.map ⇑e), inv_fun := ⇑(free_group.map ⇑(e.symm)), left_inv := _, right_inv := _, map_mul' := _}
Equivalent types give rise to additively equivalent additive free groups.
Equations
- free_add_group.free_add_group_congr e = {to_fun := ⇑(free_add_group.map ⇑e), inv_fun := ⇑(free_add_group.map ⇑(e.symm)), left_inv := _, right_inv := _, map_add' := _}
@[simp]
@[simp]
@[simp]
@[simp]
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 free_group.sum.
Equations
If α is an additive group, then any function from α to α
extends uniquely to an additive homomorphism from the
additive free group over α to α.
Equations
@[simp]
@[simp]
theorem
free_group.prod.unique
{α : Type u}
[group α]
(g : free_group α →* α)
(hg : ∀ (x : α), ⇑g (free_group.of x) = x)
{x : free_group α} :
⇑g x = ⇑free_group.prod x
theorem
free_add_group.sum.unique
{α : Type u}
[add_group α]
(g : free_add_group α →+ α)
(hg : ∀ (x : α), ⇑g (free_add_group.of x) = x)
{x : free_add_group α} :
⇑g x = ⇑free_add_group.sum x
theorem
free_add_group.lift_eq_sum_map
{α : Type u}
{β : Type v}
[add_group β]
{f : α → β}
{x : free_add_group α} :
⇑(⇑free_add_group.lift f) x = ⇑free_add_group.sum (⇑(free_add_group.map f) x)
theorem
free_group.lift_eq_prod_map
{α : Type u}
{β : Type v}
[group β]
{f : α → β}
{x : free_group α} :
⇑(⇑free_group.lift f) x = ⇑free_group.prod (⇑(free_group.map f) x)
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
- x.sum = ⇑free_group.prod x
@[simp]
@[simp]
The bijection between the additive free group on the empty type, and a type with one element.
Equations
- free_add_group.free_add_group_empty_equiv_add_unit = {to_fun := λ (_x : free_add_group empty), unit.star(), inv_fun := λ (_x : unit), 0, left_inv := free_add_group.free_add_group_empty_equiv_add_unit._proof_1, right_inv := free_add_group.free_add_group_empty_equiv_add_unit._proof_2}
The bijection between the free group on the empty type, and a type with one element.
Equations
- free_group.free_group_empty_equiv_unit = {to_fun := λ (_x : free_group empty), unit.star(), inv_fun := λ (_x : unit), 1, left_inv := free_group.free_group_empty_equiv_unit._proof_1, right_inv := free_group.free_group_empty_equiv_unit._proof_2}
The bijection between the free group on a singleton, and the integers.
Equations
- free_group.free_group_unit_equiv_int = {to_fun := λ (x : free_group unit), ((free_group.map (λ (_x : unit), 1)).to_fun x).sum, inv_fun := λ (x : ℤ), free_group.of unit.star() ^ x, left_inv := free_group.free_group_unit_equiv_int._proof_1, right_inv := free_group.free_group_unit_equiv_int._proof_2}
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
theorem
free_group.induction_on
{α : Type u}
{C : free_group α → Prop}
(z : free_group α)
(C1 : C 1)
(Cp : ∀ (x : α), C (has_pure.pure x))
(Ci : ∀ (x : α), C (has_pure.pure x) → C (has_pure.pure x)⁻¹)
(Cm : ∀ (x y : free_group α), C x → C y → C (x * y)) :
C z
@[protected]
theorem
free_add_group.induction_on
{α : Type u}
{C : free_add_group α → Prop}
(z : free_add_group α)
(C1 : C 0)
(Cp : ∀ (x : α), C (has_pure.pure x))
(Ci : ∀ (x : α), C (has_pure.pure x) → C (-has_pure.pure x))
(Cm : ∀ (x y : free_add_group α), C x → C y → C (x + y)) :
C z
@[simp]
theorem
free_group.map_pure
{α β : Type u}
(f : α → β)
(x : α) :
f <$> has_pure.pure x = has_pure.pure (f x)
@[simp]
theorem
free_add_group.map_pure
{α β : Type u}
(f : α → β)
(x : α) :
f <$> has_pure.pure x = has_pure.pure (f x)
@[simp]
@[simp]
@[simp]
theorem
free_group.pure_bind
{α β : Type u}
(f : α → free_group β)
(x : α) :
has_pure.pure x >>= f = f x
@[simp]
theorem
free_add_group.pure_bind
{α β : Type u}
(f : α → free_add_group β)
(x : α) :
has_pure.pure x >>= f = f x
@[simp]
@[simp]
@[simp]
theorem
free_add_group.add_bind
{α β : Type u}
(f : α → free_add_group β)
(x y : free_add_group α) :
@[simp]
@[simp]
The maximal reduction of a word. It is computable
iff α has decidable equality.
The maximal reduction of a word. It is computable
iff α has decidable equality.
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.
theorem
free_add_group.reduce.not
{α : Type u}
[decidable_eq α]
{p : Prop}
{L₁ L₂ L₃ : list (α × bool)}
{x : α}
{b : bool} :
theorem
free_group.reduce.not
{α : Type u}
[decidable_eq α]
{p : Prop}
{L₁ L₂ L₃ : list (α × bool)}
{x : α}
{b : bool} :
theorem
free_add_group.reduce.min
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_add_group.red (free_add_group.reduce L₁) L₂) :
free_add_group.reduce L₁ = L₂
The second theorem that characterises the
function reduce: the maximal reduction of a word
only reduces to itself.
theorem
free_group.reduce.min
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_group.red (free_group.reduce L₁) L₂) :
free_group.reduce L₁ = L₂
The second theorem that characterises the
function reduce: the maximal reduction of a word
only reduces to itself.
@[simp]
reduce is idempotent, i.e. the maximal reduction
of the maximal reduction of a word is the maximal
reduction of the word.
@[simp]
reduce is idempotent, i.e. the maximal reduction
of the maximal reduction of a word is the maximal
reduction of the word.
theorem
free_add_group.reduce.step.eq
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_add_group.red.step L₁ L₂) :
theorem
free_group.reduce.step.eq
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_group.red.step L₁ L₂) :
theorem
free_add_group.reduce.eq_of_red
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_add_group.red L₁ L₂) :
If a word reduces to another word, then they have a common maximal reduction.
theorem
free_group.reduce.eq_of_red
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_group.red L₁ L₂) :
If a word reduces to another word, then they have a common maximal reduction.
theorem
free_group.red.reduce_eq
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_group.red L₁ L₂) :
Alias of free_group.reduce.eq_of_red.
theorem
free_group.free_add_group.red.reduce_eq
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_add_group.red L₁ L₂) :
Alias of free_add_group.reduce.eq_of_red.
theorem
free_add_group.red.reduce_right
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(h : free_add_group.red L₁ L₂) :
theorem
free_group.red.reduce_right
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(h : free_group.red L₁ L₂) :
free_group.red L₁ (free_group.reduce L₂)
theorem
free_add_group.red.reduce_left
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(h : free_add_group.red L₁ L₂) :
theorem
free_group.red.reduce_left
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(h : free_group.red L₁ L₂) :
free_group.red L₂ (free_group.reduce L₁)
theorem
free_group.reduce.sound
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_group.mk L₁ = free_group.mk L₂) :
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.
theorem
free_add_group.reduce.sound
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_add_group.mk L₁ = free_add_group.mk L₂) :
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.
theorem
free_add_group.reduce.exact
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_add_group.reduce L₁ = free_add_group.reduce L₂) :
If two words have a common maximal reduction, then they correspond to the same element in the additive free group.
theorem
free_group.reduce.exact
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_group.reduce L₁ = free_group.reduce L₂) :
free_group.mk L₁ = free_group.mk L₂
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 free group.
A word and its maximal reduction correspond to the same element of the additive free group.
theorem
free_group.reduce.rev
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_group.red L₁ L₂) :
free_group.red L₂ (free_group.reduce L₁)
If words w₁ w₂ are such that w₁ reduces to w₂,
then w₂ reduces to the maximal reduction of w₁.
theorem
free_add_group.reduce.rev
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_add_group.red L₁ L₂) :
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
- free_add_group.to_word = quot.lift free_add_group.reduce free_add_group.to_word._proof_1
The function that sends an element of the free group to its maximal reduction.
Equations
- free_group.to_word = quot.lift free_group.reduce free_group.to_word._proof_1
theorem
free_group.mk_to_word
{α : Type u}
[decidable_eq α]
{x : free_group α} :
free_group.mk x.to_word = x
@[simp]
@[simp]
@[simp]
@[simp]
theorem
free_group.to_word_mk
{α : Type u}
{L₁ : list (α × bool)}
[decidable_eq α] :
(free_group.mk L₁).to_word = free_group.reduce L₁
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
def
free_group.reduce.church_rosser
{α : Type u}
{L₁ L₂ L₃ : list (α × bool)}
[decidable_eq α]
(H12 : free_group.red L₁ L₂)
(H13 : free_group.red L₁ L₃) :
{L₄ // free_group.red L₂ L₄ ∧ free_group.red L₃ L₄}
Constructive Church-Rosser theorem (compare church_rosser).
Equations
- free_group.reduce.church_rosser H12 H13 = ⟨free_group.reduce L₁, _⟩
def
free_add_group.reduce.church_rosser
{α : Type u}
{L₁ L₂ L₃ : list (α × bool)}
[decidable_eq α]
(H12 : free_add_group.red L₁ L₂)
(H13 : free_add_group.red L₁ L₃) :
{L₄ // free_add_group.red L₂ L₄ ∧ free_add_group.red L₃ L₄}
Constructive Church-Rosser theorem (compare church_rosser).
Equations
- free_add_group.reduce.church_rosser H12 H13 = ⟨free_add_group.reduce L₁, _⟩
@[protected, instance]
Equations
- free_group.decidable_eq = free_group.decidable_eq._proof_1.decidable_eq
@[protected, instance]
Equations
- free_add_group.decidable_eq = free_add_group.decidable_eq._proof_1.decidable_eq
@[protected, instance]
Equations
- free_group.red.decidable_rel ((x1, b1) :: tl1) ((x2, b2) :: tl2) = dite ((x1, b1) = (x2, b2)) (λ (h : (x1, b1) = (x2, b2)), free_group.red.decidable_rel._match_2 x1 b1 tl1 x2 b2 tl2 h (free_group.red.decidable_rel tl1 tl2)) (λ (h : ¬(x1, b1) = (x2, b2)), free_group.red.decidable_rel._match_3 x1 b1 tl1 x2 b2 tl2 h (free_group.red.decidable_rel tl1 ((x1, !b1) :: (x2, b2) :: tl2)))
- free_group.red.decidable_rel ((x, b) :: tl) list.nil = free_group.red.decidable_rel._match_1 x b tl (free_group.red.decidable_rel tl [(x, !b)])
- free_group.red.decidable_rel list.nil (hd2 :: tl2) = decidable.is_false _
- free_group.red.decidable_rel list.nil list.nil = decidable.is_true free_group.red.decidable_rel._main._proof_1
- free_group.red.decidable_rel._match_2 x1 b1 tl1 x2 b2 tl2 h (decidable.is_true H) = decidable.is_true _
- free_group.red.decidable_rel._match_2 x1 b1 tl1 x2 b2 tl2 h (decidable.is_false H) = decidable.is_false _
- free_group.red.decidable_rel._match_3 x1 b1 tl1 x2 b2 tl2 h (decidable.is_true H) = decidable.is_true _
- free_group.red.decidable_rel._match_3 x1 b1 tl1 x2 b2 tl2 h (decidable.is_false H) = decidable.is_false _
- free_group.red.decidable_rel._match_1 x b tl (decidable.is_true H) = decidable.is_true _
- free_group.red.decidable_rel._match_1 x b tl (decidable.is_false H) = decidable.is_false _
A list containing every word that w₁ reduces to.
Equations
- free_group.red.enum L₁ = list.filter (λ (L₂ : list (α × bool)), free_group.red L₁ L₂) L₁.sublists
theorem
free_group.red.enum.sound
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : L₂ ∈ free_group.red.enum L₁) :
free_group.red L₁ L₂
theorem
free_group.red.enum.complete
{α : Type u}
{L₁ L₂ : list (α × bool)}
[decidable_eq α]
(H : free_group.red L₁ L₂) :
L₂ ∈ free_group.red.enum L₁
@[protected, instance]
def
free_group.subtype.fintype
{α : Type u}
{L₁ : list (α × bool)}
[decidable_eq α] :
fintype {L₂ // free_group.red L₁ L₂}
Equations
- free_group.subtype.fintype = fintype.subtype (free_group.red.enum L₁).to_finset free_group.subtype.fintype._proof_1
The length of reduced words provides a norm on an additive free group.
The length of reduced words provides a norm on a free group.
@[simp]
@[simp]
@[simp]
@[simp]
theorem
free_group.norm_mk_le
{α : Type u}
{L₁ : list (α × bool)}
[decidable_eq α] :
(free_group.mk L₁).norm ≤ L₁.length
theorem
free_add_group.norm_mk_le
{α : Type u}
{L₁ : list (α × bool)}
[decidable_eq α] :
(free_add_group.mk L₁).norm ≤ L₁.length