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 : α × Boolmodulo the relationa * x * x⁻¹ * b = a * b.FreeGroup.mk/FreeAddGroup.mk: the canonical quotient mapList (α × Bool) → FreeGroup α.FreeGroup.of/FreeAddGroup.of: the canonical injectionα → FreeGroup α.FreeGroup.lift f/FreeAddGroup.lift: the canonical group homomorphismFreeGroup α →* Ggiven a groupGand a functionf : α → 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, 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
Reduction step for the additive free group relation: w + x + (-x) + v ~> w + v
Reflexive-transitive closure of Red.Step
Equations
- FreeGroup.Red = Relation.ReflTransGen FreeGroup.Red.Step
Instances For
theorem
FreeAddGroup.Red.trans
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{L₃ : List (α × Bool)}
:
FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₂ L₃ → FreeAddGroup.Red L₁ L₃
theorem
FreeGroup.Red.trans
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{L₃ : List (α × Bool)}
:
FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ L₃ → FreeGroup.Red L₁ L₃
abbrev
FreeAddGroup.Red.Step.length.match_1
{α : Type u_1}
(motive : (x x_1 : List (α × Bool)) → FreeAddGroup.Red.Step x x_1 → Prop)
:
Equations
- ⋯ = ⋯
theorem
FreeAddGroup.Red.Step.length
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeAddGroup.Red.Step L₁ L₂ → List.length L₂ + 2 = List.length 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
FreeGroup.Red.Step.length
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeGroup.Red.Step L₁ L₂ → List.length L₂ + 2 = List.length 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₃xx⁻¹w₄ and w₂ = w₃w₄
theorem
FreeAddGroup.Red.Step.cons
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{x : α × Bool}
(H : FreeAddGroup.Red.Step L₁ L₂)
:
FreeAddGroup.Red.Step (x :: L₁) (x :: L₂)
theorem
FreeGroup.Red.Step.cons
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{x : α × Bool}
(H : FreeGroup.Red.Step L₁ L₂)
:
FreeGroup.Red.Step (x :: L₁) (x :: L₂)
theorem
FreeAddGroup.Red.not_step_singleton
{α : Type u}
{L : List (α × Bool)}
{p : α × Bool}
:
¬FreeAddGroup.Red.Step [p] L
theorem
FreeGroup.Red.not_step_singleton
{α : Type u}
{L : List (α × Bool)}
{p : α × Bool}
:
¬FreeGroup.Red.Step [p] L
abbrev
FreeAddGroup.Red.Step.diamond_aux.match_3
{α : Type u_1}
(motive : (x x_1 x_2 x_3 : List (α × Bool)) →
(x_4 : α) →
(x_5 : Bool) →
(x_6 : α) → (x_7 : Bool) → x ++ (x_4, x_5) :: (x_4, !x_5) :: x_1 = x_2 ++ (x_6, x_7) :: (x_6, !x_7) :: x_3 → Prop)
:
∀ (x x_1 x_2 x_3 : List (α × Bool)) (x_4 : α) (x_5 : Bool) (x_6 : α) (x_7 : Bool)
(x_8 : x ++ (x_4, x_5) :: (x_4, !x_5) :: x_1 = x_2 ++ (x_6, x_7) :: (x_6, !x_7) :: x_3),
(∀ (x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool)
(H : [] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
motive [] x [] x_9 x_10 x_11 x_12 x_13 H) →
(∀ (x : List (α × Bool)) (x3 : α) (b3 : Bool) (x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α)
(x_13 : Bool)
(H : [] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [(x3, b3)] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
motive [] x [(x3, b3)] x_9 x_10 x_11 x_12 x_13 H) →
(∀ (x3 : α) (b3 : Bool) (x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool)
(H : [(x3, b3)] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
motive [(x3, b3)] x [] x_9 x_10 x_11 x_12 x_13 H) →
(∀ (x : List (α × Bool)) (x3 : α) (b3 : Bool) (x4 : α) (b4 : Bool) (tl x_9 : List (α × Bool)) (x_10 : α)
(x_11 : Bool) (x_12 : α) (x_13 : Bool)
(H :
[] ++ (x_10, x_11) :: (x_10, !x_11) :: x = (x3, b3) :: (x4, b4) :: tl ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
motive [] x ((x3, b3) :: (x4, b4) :: tl) x_9 x_10 x_11 x_12 x_13 H) →
(∀ (x3 : α) (b3 : Bool) (x4 : α) (b4 : Bool) (tl x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α)
(x_13 : Bool)
(H :
(x3, b3) :: (x4, b4) :: tl ++ (x_10, x_11) :: (x_10, !x_11) :: x = [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
motive ((x3, b3) :: (x4, b4) :: tl) x [] x_9 x_10 x_11 x_12 x_13 H) →
(∀ (x3 : α) (b3 : Bool) (tl x : List (α × Bool)) (x4 : α) (b4 : Bool) (tl2 x_9 : List (α × Bool)) (x_10 : α)
(x_11 : Bool) (x_12 : α) (x_13 : Bool)
(H :
(x3, b3) :: tl ++ (x_10, x_11) :: (x_10, !x_11) :: x = (x4, b4) :: tl2 ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
motive ((x3, b3) :: tl) x ((x4, b4) :: tl2) x_9 x_10 x_11 x_12 x_13 H) →
motive x x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8
Equations
- ⋯ = ⋯
abbrev
FreeAddGroup.Red.Step.diamond_aux.match_1
{α : Type u_1}
(tl : List (α × Bool))
:
∀ (x tl2 x_1 : List (α × Bool))
(motive :
(tl ++ x = tl2 ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step (tl ++ x) L₅ ∧ FreeAddGroup.Red.Step (tl2 ++ x_1) L₅) →
Prop)
(x_2 :
tl ++ x = tl2 ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step (tl ++ x) L₅ ∧ FreeAddGroup.Red.Step (tl2 ++ x_1) L₅),
(∀ (H3 : tl ++ x = tl2 ++ x_1), motive ⋯) →
(∀ (L₅ : List (α × Bool)) (H3 : FreeAddGroup.Red.Step (tl ++ x) L₅) (H4 : FreeAddGroup.Red.Step (tl2 ++ x_1) L₅),
motive ⋯) →
motive x_2
Equations
- ⋯ = ⋯
abbrev
FreeAddGroup.Red.Step.diamond_aux.match_2
{α : Type u_1}
(x3 : α)
(b3 : Bool)
(tl : List (α × Bool))
:
∀ (x : List (α × Bool)) (x4 : α) (b4 : Bool) (tl2 x_1 : List (α × Bool)) (x_2 : α) (x_3 : Bool) (x_4 : α) (x_5 : Bool)
(motive :
(x3, b3) = (x4, b4) ∧ List.append tl ((x_2, x_3) :: (x_2, !x_3) :: x) = List.append tl2 ((x_4, x_5) :: (x_4, !x_5) :: x_1) →
Prop)
(x_6 :
(x3, b3) = (x4, b4) ∧ List.append tl ((x_2, x_3) :: (x_2, !x_3) :: x) = List.append tl2 ((x_4, x_5) :: (x_4, !x_5) :: x_1)),
(∀ (H1 : (x3, b3) = (x4, b4))
(H2 : List.append tl ((x_2, x_3) :: (x_2, !x_3) :: x) = List.append tl2 ((x_4, x_5) :: (x_4, !x_5) :: x_1)),
motive ⋯) →
motive x_6
Equations
- ⋯ = ⋯
theorem
FreeAddGroup.Red.Step.diamond
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{L₃ : List (α × Bool)}
{L₄ : List (α × Bool)}
:
FreeAddGroup.Red.Step L₁ L₃ →
FreeAddGroup.Red.Step L₂ L₄ →
L₁ = L₂ → L₃ = L₄ ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step L₃ L₅ ∧ FreeAddGroup.Red.Step L₄ L₅
abbrev
FreeAddGroup.Red.Step.diamond.match_1
{α : Type u_1}
(motive : (x x_1 x_2 x_3 : List (α × Bool)) → FreeAddGroup.Red.Step x x_2 → FreeAddGroup.Red.Step x_1 x_3 → x = x_1 → Prop)
:
∀ (x x_1 x_2 x_3 : List (α × Bool)) (x_4 : FreeAddGroup.Red.Step x x_2) (x_5 : FreeAddGroup.Red.Step x_1 x_3)
(x_6 : x = x_1),
(∀ (L₁ L₂ : List (α × Bool)) (x : α) (b : Bool) (L₁_1 L₂_1 : List (α × Bool)) (x_7 : α) (b_1 : Bool)
(H : L₁ ++ (x, b) :: (x, !b) :: L₂ = L₁_1 ++ (x_7, b_1) :: (x_7, !b_1) :: L₂_1),
motive (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁_1 ++ (x_7, b_1) :: (x_7, !b_1) :: L₂_1) (L₁ ++ L₂) (L₁_1 ++ L₂_1) ⋯ ⋯
H) →
motive x x_1 x_2 x_3 x_4 x_5 x_6
Equations
- ⋯ = ⋯
theorem
FreeAddGroup.Red.Step.to_red
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Red L₁ L₂
theorem
FreeGroup.Red.Step.to_red
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red L₁ L₂
theorem
FreeAddGroup.Red.church_rosser
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{L₃ : List (α × Bool)}
:
FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₁ L₃ → Relation.Join FreeAddGroup.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.
abbrev
FreeAddGroup.Red.church_rosser.match_1
{α : Type u_1}
(a : List (α × Bool))
(motive : (b c : List (α × Bool)) →
(b = c ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step b L₅ ∧ FreeAddGroup.Red.Step c L₅) →
FreeAddGroup.Red.Step a b → FreeAddGroup.Red.Step a c → Prop)
:
∀ (b c : List (α × Bool))
(x : b = c ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step b L₅ ∧ FreeAddGroup.Red.Step c L₅)
(hab : FreeAddGroup.Red.Step a b) (hac : FreeAddGroup.Red.Step a c),
(∀ (b : List (α × Bool)) (hab hac : FreeAddGroup.Red.Step a b), motive b b ⋯ hab hac) →
(∀ (b c d : List (α × Bool)) (hbd : FreeAddGroup.Red.Step b d) (hcd : FreeAddGroup.Red.Step c d)
(hab : FreeAddGroup.Red.Step a b) (hac : FreeAddGroup.Red.Step a c), motive b c ⋯ hab hac) →
motive b c x hab hac
Equations
- ⋯ = ⋯
theorem
FreeGroup.Red.church_rosser
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{L₃ : List (α × Bool)}
:
FreeGroup.Red L₁ L₂ → FreeGroup.Red L₁ L₃ → Relation.Join FreeGroup.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
FreeAddGroup.Red.cons_cons
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{p : α × Bool}
:
FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red (p :: L₁) (p :: L₂)
theorem
FreeGroup.Red.cons_cons
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{p : α × Bool}
:
FreeGroup.Red L₁ L₂ → FreeGroup.Red (p :: L₁) (p :: L₂)
theorem
FreeAddGroup.Red.append_append
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{L₃ : List (α × Bool)}
{L₄ : List (α × Bool)}
(h₁ : FreeAddGroup.Red L₁ L₃)
(h₂ : FreeAddGroup.Red L₂ L₄)
:
FreeAddGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)
theorem
FreeGroup.Red.append_append
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{L₃ : List (α × Bool)}
{L₄ : List (α × Bool)}
(h₁ : FreeGroup.Red L₁ L₃)
(h₂ : FreeGroup.Red L₂ L₄)
:
FreeGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)
abbrev
FreeAddGroup.Red.to_append_iff.match_1
{α : Type u_1}
{L : List (α × Bool)}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(motive : (∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ FreeAddGroup.Red L₃ L₁ ∧ FreeAddGroup.Red L₄ L₂) → Prop)
:
∀ (x : ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ FreeAddGroup.Red L₃ L₁ ∧ FreeAddGroup.Red L₄ L₂),
(∀ (L₃ L₄ : List (α × Bool)) (Eq : L = L₃ ++ L₄) (h₃ : FreeAddGroup.Red L₃ L₁) (h₄ : FreeAddGroup.Red L₄ L₂),
motive ⋯) →
motive x
Equations
- ⋯ = ⋯
The empty word [] only reduces to itself.
The empty word [] only reduces to itself.
theorem
FreeAddGroup.Red.cons_nil_iff_singleton
{α : Type u}
{L : List (α × Bool)}
{x : α}
{b : Bool}
:
FreeAddGroup.Red ((x, b) :: L) [] ↔ FreeAddGroup.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.
abbrev
FreeAddGroup.Red.cons_nil_iff_singleton.match_1
{α : Type u_1}
{L : List (α × Bool)}
{x : α}
{b : Bool}
(motive : Relation.Join FreeAddGroup.Red [(x, !b)] L → Prop)
:
∀ (x_1 : Relation.Join FreeAddGroup.Red [(x, !b)] L),
(∀ (L' : List (α × Bool)) (h₁ : FreeAddGroup.Red [(x, !b)] L') (h₂ : FreeAddGroup.Red L L'), motive ⋯) → motive x_1
Equations
- ⋯ = ⋯
theorem
FreeGroup.Red.cons_nil_iff_singleton
{α : Type u}
{L : List (α × Bool)}
{x : α}
{b : Bool}
:
FreeGroup.Red ((x, b) :: L) [] ↔ FreeGroup.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
FreeAddGroup.Red.neg_of_red_of_ne
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{x1 : α}
{b1 : Bool}
{x2 : α}
{b2 : Bool}
(H1 : (x1, b1) ≠ (x2, b2))
(H2 : FreeAddGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂))
:
FreeAddGroup.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
FreeGroup.Red.inv_of_red_of_ne
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{x1 : α}
{b1 : Bool}
{x2 : α}
{b2 : Bool}
(H1 : (x1, b1) ≠ (x2, b2))
(H2 : FreeGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂))
:
FreeGroup.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
FreeAddGroup.Red.Step.sublist
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(H : FreeAddGroup.Red.Step L₁ L₂)
:
List.Sublist L₂ L₁
theorem
FreeGroup.Red.Step.sublist
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(H : FreeGroup.Red.Step L₁ L₂)
:
List.Sublist L₂ L₁
theorem
FreeAddGroup.Red.sublist
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeAddGroup.Red L₁ L₂ → List.Sublist L₂ L₁
If w₁ w₂ are words such that w₁ reduces to w₂, then w₂ is a sublist of
w₁.
theorem
FreeGroup.Red.sublist
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeGroup.Red L₁ L₂ → List.Sublist L₂ L₁
If w₁ w₂ are words such that w₁ reduces to w₂, then w₂ is a sublist of w₁.
theorem
FreeAddGroup.Red.length_le
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h : FreeAddGroup.Red L₁ L₂)
:
List.length L₂ ≤ List.length L₁
theorem
FreeGroup.Red.length_le
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h : FreeGroup.Red L₁ L₂)
:
List.length L₂ ≤ List.length L₁
theorem
FreeAddGroup.Red.length
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h : FreeAddGroup.Red L₁ L₂)
:
∃ (n : ℕ), List.length L₁ = List.length L₂ + 2 * n
theorem
FreeGroup.Red.length
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h : FreeGroup.Red L₁ L₂)
:
∃ (n : ℕ), List.length L₁ = List.length L₂ + 2 * n
theorem
FreeAddGroup.Red.antisymm
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h₁₂ : FreeAddGroup.Red L₁ L₂)
(h₂₁ : FreeAddGroup.Red L₂ L₁)
:
L₁ = L₂
theorem
FreeGroup.Red.antisymm
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h₁₂ : FreeGroup.Red L₁ L₂)
(h₂₁ : FreeGroup.Red L₂ L₁)
:
L₁ = L₂
theorem
FreeAddGroup.equivalence_join_red
{α : Type u}
:
Equivalence (Relation.Join FreeAddGroup.Red)
theorem
FreeAddGroup.join_red_of_step
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h : FreeAddGroup.Red.Step L₁ L₂)
:
Relation.Join FreeAddGroup.Red L₁ L₂
theorem
FreeGroup.join_red_of_step
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h : FreeGroup.Red.Step L₁ L₂)
:
Relation.Join FreeGroup.Red L₁ L₂
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
Instances For
- FreeAddGroup.instAddFreeAddGroup
- FreeAddGroup.instAddGroupFreeAddGroup
- FreeAddGroup.instInhabitedFreeAddGroup
- FreeAddGroup.instLawfulMonadFreeAddGroupInstMonadFreeAddGroup
- FreeAddGroup.instMonadFreeAddGroup
- FreeAddGroup.instNegFreeAddGroup
- FreeAddGroup.instUniqueFreeAddGroup
- FreeAddGroup.instZeroFreeAddGroup
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.
The canonical map from list (α × bool) to the free additive group on α.
Equations
- FreeAddGroup.mk L = Quot.mk FreeAddGroup.Red.Step L
@[simp]
theorem
FreeAddGroup.quot_mk_eq_mk
{α : Type u}
{L : List (α × Bool)}
:
Quot.mk FreeAddGroup.Red.Step L = FreeAddGroup.mk L
@[simp]
theorem
FreeGroup.quot_mk_eq_mk
{α : Type u}
{L : List (α × Bool)}
:
Quot.mk FreeGroup.Red.Step L = FreeGroup.mk L
@[simp]
theorem
FreeAddGroup.quot_liftOn_mk
{α : Type u}
{L : List (α × Bool)}
(β : Type v)
(f : List (α × Bool) → β)
(H : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → f L₁ = f L₂)
:
Quot.liftOn (FreeAddGroup.mk L) f H = f L
@[simp]
theorem
FreeGroup.quot_liftOn_mk
{α : Type u}
{L : List (α × Bool)}
(β : Type v)
(f : List (α × Bool) → β)
(H : ∀ (L₁ L₂ : List (α × Bool)), FreeGroup.Red.Step L₁ L₂ → f L₁ = f L₂)
:
Quot.liftOn (FreeGroup.mk L) f H = f L
Equations
- FreeAddGroup.instZeroFreeAddGroup = { zero := FreeAddGroup.mk [] }
Equations
- FreeGroup.instOneFreeGroup = { one := FreeGroup.mk [] }
Equations
- FreeAddGroup.instInhabitedFreeAddGroup = { default := 0 }
theorem
FreeAddGroup.instAddFreeAddGroup.proof_2
{α : Type u_1}
(y : FreeAddGroup α)
(_L₁ : List (α × Bool))
(_L₂ : List (α × Bool))
(H : FreeAddGroup.Red.Step _L₁ _L₂)
:
(fun (L₁ : List (α × Bool)) => Quot.liftOn y (fun (L₂ : List (α × Bool)) => FreeAddGroup.mk (L₁ ++ L₂)) ⋯) _L₁ = (fun (L₁ : List (α × Bool)) => Quot.liftOn y (fun (L₂ : List (α × Bool)) => FreeAddGroup.mk (L₁ ++ L₂)) ⋯) _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.
@[simp]
theorem
FreeAddGroup.add_mk
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeAddGroup.mk L₁ + FreeAddGroup.mk L₂ = FreeAddGroup.mk (L₁ ++ L₂)
@[simp]
theorem
FreeGroup.mul_mk
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeGroup.mk L₁ * FreeGroup.mk L₂ = FreeGroup.mk (L₁ ++ L₂)
@[simp]
theorem
FreeAddGroup.negRev_length
{α : Type u}
{L₁ : List (α × Bool)}
:
List.length (FreeAddGroup.negRev L₁) = List.length L₁
@[simp]
theorem
FreeGroup.invRev_length
{α : Type u}
{L₁ : List (α × Bool)}
:
List.length (FreeGroup.invRev L₁) = List.length L₁
@[simp]
theorem
FreeAddGroup.negRev_negRev
{α : Type u}
{L₁ : List (α × Bool)}
:
FreeAddGroup.negRev (FreeAddGroup.negRev L₁) = L₁
@[simp]
theorem
FreeGroup.invRev_invRev
{α : Type u}
{L₁ : List (α × Bool)}
:
FreeGroup.invRev (FreeGroup.invRev L₁) = L₁
theorem
FreeAddGroup.instNegFreeAddGroup.proof_1
{α : Type u_1}
⦃a : List (α × Bool)⦄
⦃b : List (α × Bool)⦄
(h : FreeAddGroup.Red.Step a b)
:
@[simp]
@[simp]
theorem
FreeGroup.inv_mk
{α : Type u}
{L : List (α × Bool)}
:
(FreeGroup.mk L)⁻¹ = FreeGroup.mk (FreeGroup.invRev L)
theorem
FreeAddGroup.Red.Step.negRev
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h : FreeAddGroup.Red.Step L₁ L₂)
:
theorem
FreeGroup.Red.Step.invRev
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h : FreeGroup.Red.Step L₁ L₂)
:
theorem
FreeAddGroup.Red.negRev
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h : FreeAddGroup.Red L₁ L₂)
:
theorem
FreeGroup.Red.invRev
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(h : FreeGroup.Red L₁ L₂)
:
FreeGroup.Red (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
@[simp]
theorem
FreeGroup.Red.step_invRev_iff
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeGroup.Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ FreeGroup.Red.Step L₁ L₂
@[simp]
theorem
FreeAddGroup.red_negRev_iff
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeAddGroup.Red (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂) ↔ FreeAddGroup.Red L₁ L₂
@[simp]
theorem
FreeGroup.red_invRev_iff
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeGroup.Red (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ FreeGroup.Red L₁ L₂
theorem
FreeAddGroup.instAddGroupFreeAddGroup.proof_4
{α : Type u_1}
:
∀ (x : FreeAddGroup α), nsmulRec 0 x = nsmulRec 0 x
theorem
FreeAddGroup.instAddGroupFreeAddGroup.proof_6
{α : Type u_1}
:
∀ (a b : FreeAddGroup α), a - b = a - b
theorem
FreeAddGroup.instAddGroupFreeAddGroup.proof_2
{α : Type u_1}
:
∀ (a : FreeAddGroup α), 0 + a = a
theorem
FreeAddGroup.instAddGroupFreeAddGroup.proof_10
{α : Type u_1}
:
∀ (a : FreeAddGroup α), -a + a = 0
theorem
FreeAddGroup.instAddGroupFreeAddGroup.proof_7
{α : Type u_1}
:
∀ (a : FreeAddGroup α), zsmulRec 0 a = zsmulRec 0 a
theorem
FreeAddGroup.instAddGroupFreeAddGroup.proof_3
{α : Type u_1}
:
∀ (a : FreeAddGroup α), a + 0 = a
Equations
- FreeAddGroup.instAddGroupFreeAddGroup = AddGroup.mk ⋯
theorem
FreeAddGroup.instAddGroupFreeAddGroup.proof_5
{α : Type u_1}
:
∀ (n : ℕ) (x : FreeAddGroup α), nsmulRec (n + 1) x = nsmulRec (n + 1) x
theorem
FreeAddGroup.instAddGroupFreeAddGroup.proof_9
{α : Type u_1}
:
∀ (n : ℕ) (a : FreeAddGroup α), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
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)]
theorem
FreeAddGroup.Red.exact
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂ ↔ Relation.Join FreeAddGroup.Red L₁ L₂
theorem
FreeGroup.Red.exact
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
:
FreeGroup.mk L₁ = FreeGroup.mk L₂ ↔ Relation.Join FreeGroup.Red L₁ L₂
The canonical map from the type to the additive free group is an injection.
abbrev
FreeAddGroup.of_injective.match_1
{α : Type u_1}
:
∀ (x x_1 : α) (motive : Relation.Join FreeAddGroup.Red [(x, true)] [(x_1, true)] → Prop)
(x_2 : Relation.Join FreeAddGroup.Red [(x, true)] [(x_1, true)]),
(∀ (L₁ : List (α × Bool)) (hx : FreeAddGroup.Red [(x, true)] L₁) (hy : FreeAddGroup.Red [(x_1, true)] L₁), motive ⋯) →
motive x_2
Equations
- ⋯ = ⋯
The canonical map from the type to the free group is an injection.
theorem
FreeAddGroup.Red.Step.lift
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{β : Type v}
[AddGroup β]
{f : α → β}
(H : FreeAddGroup.Red.Step L₁ L₂)
:
FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂
theorem
FreeGroup.Red.Step.lift
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{β : Type v}
[Group β]
{f : α → β}
(H : FreeGroup.Red.Step L₁ L₂)
:
FreeGroup.Lift.aux f L₁ = FreeGroup.Lift.aux f L₂
theorem
FreeAddGroup.lift.proof_1
{α : Type u_1}
{β : Type u_2}
[AddGroup β]
(f : α → β)
:
∀ (a b : FreeAddGroup α),
Quot.lift (FreeAddGroup.Lift.aux f) ⋯ (a + b) = Quot.lift (FreeAddGroup.Lift.aux f) ⋯ a + Quot.lift (FreeAddGroup.Lift.aux f) ⋯ b
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.
theorem
FreeAddGroup.lift.proof_3
{α : Type u_2}
{β : Type u_1}
[AddGroup β]
(g : FreeAddGroup α →+ β)
:
(fun (f : α → β) => AddMonoidHom.mk' (Quot.lift (FreeAddGroup.Lift.aux f) ⋯) ⋯)
((fun (g : FreeAddGroup α →+ β) => ⇑g ∘ FreeAddGroup.of) g) = g
@[simp]
theorem
FreeAddGroup.lift_symm_apply
{α : Type u}
{β : Type v}
[AddGroup β]
(g : FreeAddGroup α →+ β)
:
@[simp]
theorem
FreeAddGroup.lift.of
{α : Type u}
{β : Type v}
[AddGroup β]
{f : α → β}
{x : α}
:
(FreeAddGroup.lift f) (FreeAddGroup.of x) = f x
@[simp]
theorem
FreeGroup.lift.of
{α : Type u}
{β : Type v}
[Group β]
{f : α → β}
{x : α}
:
(FreeGroup.lift f) (FreeGroup.of x) = f x
theorem
FreeAddGroup.lift.unique
{α : Type u}
{β : Type v}
[AddGroup β]
{f : α → β}
(g : FreeAddGroup α →+ β)
(hg : ∀ (x : α), g (FreeAddGroup.of x) = f x)
{x : FreeAddGroup α}
:
g x = (FreeAddGroup.lift f) x
theorem
FreeAddGroup.ext_hom
{α : Type u}
{G : Type u_1}
[AddGroup G]
(f : FreeAddGroup α →+ G)
(g : FreeAddGroup α →+ G)
(h : ∀ (a : α), f (FreeAddGroup.of a) = g (FreeAddGroup.of a))
:
f = g
Two homomorphisms out of a free additive group are equal if they are equal on generators. See note [partially-applied ext lemmas].
theorem
FreeGroup.ext_hom
{α : Type u}
{G : Type u_1}
[Group G]
(f : FreeGroup α →* G)
(g : FreeGroup α →* G)
(h : ∀ (a : α), f (FreeGroup.of a) = g (FreeGroup.of a))
:
f = g
Two homomorphisms out of a free group are equal if they are equal on generators.
See note [partially-applied ext lemmas].
theorem
FreeAddGroup.lift_of_eq_id
(α : Type u_1)
:
FreeAddGroup.lift FreeAddGroup.of = AddMonoidHom.id (FreeAddGroup α)
theorem
FreeGroup.lift_of_eq_id
(α : Type u_1)
:
FreeGroup.lift FreeGroup.of = MonoidHom.id (FreeGroup α)
theorem
FreeAddGroup.lift.of_eq
{α : Type u}
(x : FreeAddGroup α)
:
(FreeAddGroup.lift FreeAddGroup.of) x = x
theorem
FreeAddGroup.lift.range_le
{α : Type u}
{β : Type v}
[AddGroup β]
{f : α → β}
{s : AddSubgroup β}
(H : Set.range f ⊆ ↑s)
:
AddMonoidHom.range (FreeAddGroup.lift f) ≤ s
theorem
FreeGroup.lift.range_le
{α : Type u}
{β : Type v}
[Group β]
{f : α → β}
{s : Subgroup β}
(H : Set.range f ⊆ ↑s)
:
MonoidHom.range (FreeGroup.lift f) ≤ s
theorem
FreeAddGroup.lift.range_eq_closure
{α : Type u}
{β : Type v}
[AddGroup β]
{f : α → β}
:
AddMonoidHom.range (FreeAddGroup.lift f) = AddSubgroup.closure (Set.range f)
theorem
FreeGroup.lift.range_eq_closure
{α : Type u}
{β : Type v}
[Group β]
{f : α → β}
:
MonoidHom.range (FreeGroup.lift f) = Subgroup.closure (Set.range f)
@[simp]
theorem
FreeAddGroup.closure_range_of
(α : Type u_1)
:
AddSubgroup.closure (Set.range FreeAddGroup.of) = ⊤
Any function from α to β extends uniquely to an additive group homomorphism from
the additive free group over α to the additive free group over β.
Equations
- FreeAddGroup.map f = AddMonoidHom.mk' (Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) ⋯) ⋯
Any function from α to β extends uniquely to a group homomorphism from the free group over
α to the free group over β.
Equations
- FreeGroup.map f = MonoidHom.mk' (Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) ⋯) ⋯
@[simp]
theorem
FreeAddGroup.map.mk
{α : Type u}
{L : List (α × Bool)}
{β : Type v}
{f : α → β}
:
(FreeAddGroup.map f) (FreeAddGroup.mk L) = FreeAddGroup.mk (List.map (fun (x : α × Bool) => (f x.1, x.2)) L)
@[simp]
theorem
FreeGroup.map.mk
{α : Type u}
{L : List (α × Bool)}
{β : Type v}
{f : α → β}
:
(FreeGroup.map f) (FreeGroup.mk L) = FreeGroup.mk (List.map (fun (x : α × Bool) => (f x.1, x.2)) L)
@[simp]
@[simp]
theorem
FreeAddGroup.map.id'
{α : Type u}
(x : FreeAddGroup α)
:
(FreeAddGroup.map fun (z : α) => z) x = x
@[simp]
theorem
FreeAddGroup.map.comp
{α : Type u}
{β : Type v}
{γ : Type w}
(f : α → β)
(g : β → γ)
(x : FreeAddGroup α)
:
(FreeAddGroup.map g) ((FreeAddGroup.map f) x) = (FreeAddGroup.map (g ∘ f)) x
theorem
FreeGroup.map.comp
{α : Type u}
{β : Type v}
{γ : Type w}
(f : α → β)
(g : β → γ)
(x : FreeGroup α)
:
(FreeGroup.map g) ((FreeGroup.map f) x) = (FreeGroup.map (g ∘ f)) x
@[simp]
theorem
FreeAddGroup.map.of
{α : Type u}
{β : Type v}
{f : α → β}
{x : α}
:
(FreeAddGroup.map f) (FreeAddGroup.of x) = FreeAddGroup.of (f x)
@[simp]
theorem
FreeGroup.map.of
{α : Type u}
{β : Type v}
{f : α → β}
{x : α}
:
(FreeGroup.map f) (FreeGroup.of x) = FreeGroup.of (f x)
theorem
FreeAddGroup.map.unique
{α : Type u}
{β : Type v}
{f : α → β}
(g : FreeAddGroup α →+ FreeAddGroup β)
(hg : ∀ (x : α), g (FreeAddGroup.of x) = FreeAddGroup.of (f x))
{x : FreeAddGroup α}
:
g x = (FreeAddGroup.map f) x
theorem
FreeGroup.map.unique
{α : Type u}
{β : Type v}
{f : α → β}
(g : FreeGroup α →* FreeGroup β)
(hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x))
{x : FreeGroup α}
:
g x = (FreeGroup.map f) x
theorem
FreeAddGroup.map_eq_lift
{α : Type u}
{β : Type v}
{f : α → β}
{x : FreeAddGroup α}
:
(FreeAddGroup.map f) x = (FreeAddGroup.lift (FreeAddGroup.of ∘ f)) x
theorem
FreeGroup.map_eq_lift
{α : Type u}
{β : Type v}
{f : α → β}
{x : FreeGroup α}
:
(FreeGroup.map f) x = (FreeGroup.lift (FreeGroup.of ∘ f)) x
theorem
FreeAddGroup.freeAddGroupCongr.proof_2
{α : Type u_2}
{β : Type u_1}
(e : α ≃ β)
(x : FreeAddGroup β)
:
(FreeAddGroup.map ⇑e) ((FreeAddGroup.map ⇑e.symm) x) = x
Equivalent types give rise to additively equivalent additive free groups.
Equations
- FreeAddGroup.freeAddGroupCongr e = { toEquiv := { toFun := ⇑(FreeAddGroup.map ⇑e), invFun := ⇑(FreeAddGroup.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }
theorem
FreeAddGroup.freeAddGroupCongr.proof_3
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β)
(a : FreeAddGroup α)
(b : FreeAddGroup α)
:
(FreeAddGroup.map ⇑e) (a + b) = (FreeAddGroup.map ⇑e) a + (FreeAddGroup.map ⇑e) b
theorem
FreeAddGroup.freeAddGroupCongr.proof_1
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β)
(x : FreeAddGroup α)
:
(FreeAddGroup.map ⇑e.symm) ((FreeAddGroup.map ⇑e) x) = x
@[simp]
theorem
FreeGroup.freeGroupCongr_apply
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β)
(a : FreeGroup α)
:
(FreeGroup.freeGroupCongr e) a = (FreeGroup.map ⇑e) a
@[simp]
theorem
FreeAddGroup.freeAddGroupCongr_apply
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β)
(a : FreeAddGroup α)
:
(FreeAddGroup.freeAddGroupCongr e) a = (FreeAddGroup.map ⇑e) a
Equivalent types give rise to multiplicatively equivalent free groups.
The converse can be found in GroupTheory.FreeAbelianGroupFinsupp,
as Equiv.of_freeGroupEquiv
Equations
- FreeGroup.freeGroupCongr e = { toEquiv := { toFun := ⇑(FreeGroup.map ⇑e), invFun := ⇑(FreeGroup.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯ }
@[simp]
@[simp]
@[simp]
@[simp]
theorem
FreeGroup.freeGroupCongr_trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(e : α ≃ β)
(f : β ≃ γ)
:
MulEquiv.trans (FreeGroup.freeGroupCongr e) (FreeGroup.freeGroupCongr f) = FreeGroup.freeGroupCongr (e.trans f)
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
@[simp]
theorem
FreeAddGroup.sum.of
{α : Type u}
[AddGroup α]
{x : α}
:
FreeAddGroup.sum (FreeAddGroup.of x) = x
@[simp]
theorem
FreeAddGroup.sum.unique
{α : Type u}
[AddGroup α]
(g : FreeAddGroup α →+ α)
(hg : ∀ (x : α), g (FreeAddGroup.of x) = x)
{x : FreeAddGroup α}
:
g x = FreeAddGroup.sum x
theorem
FreeGroup.prod.unique
{α : Type u}
[Group α]
(g : FreeGroup α →* α)
(hg : ∀ (x : α), g (FreeGroup.of x) = x)
{x : FreeGroup α}
:
g x = FreeGroup.prod x
theorem
FreeAddGroup.lift_eq_sum_map
{α : Type u}
{β : Type v}
[AddGroup β]
{f : α → β}
{x : FreeAddGroup α}
:
(FreeAddGroup.lift f) x = FreeAddGroup.sum ((FreeAddGroup.map f) x)
theorem
FreeGroup.lift_eq_prod_map
{α : Type u}
{β : Type v}
[Group β]
{f : α → β}
{x : FreeGroup α}
:
(FreeGroup.lift f) x = FreeGroup.prod ((FreeGroup.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
- FreeGroup.sum x = FreeGroup.prod x
@[simp]
theorem
FreeGroup.sum_mk
{α : Type u}
{L : List (α × Bool)}
[AddGroup α]
:
FreeGroup.sum (FreeGroup.mk L) = List.sum (List.map (fun (x : α × Bool) => bif x.2 then x.1 else -x.1) L)
@[simp]
@[simp]
theorem
FreeGroup.sum.map_mul
{α : Type u}
[AddGroup α]
{x : FreeGroup α}
{y : FreeGroup α}
:
FreeGroup.sum (x * y) = FreeGroup.sum x + FreeGroup.sum y
@[simp]
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.
theorem
FreeAddGroup.freeAddGroupEmptyEquivAddUnit.proof_1 :
∀ (x : FreeAddGroup Empty), (fun (x : Unit) => 0) ((fun (x : FreeAddGroup Empty) => ()) x) = x
abbrev
FreeAddGroup.freeAddGroupEmptyEquivAddUnit.match_1
(motive : Unit → Prop)
:
∀ (x : Unit), (Unit → motive PUnit.unit) → motive x
Equations
- ⋯ = ⋯
Equations
- FreeAddGroup.instMonadFreeAddGroup = Monad.mk
Equations
- FreeGroup.instMonadFreeGroup = Monad.mk
theorem
FreeAddGroup.induction_on
{α : Type u}
{C : FreeAddGroup α → Prop}
(z : FreeAddGroup α)
(C1 : C 0)
(Cp : ∀ (x : α), C (pure x))
(Ci : ∀ (x : α), C (pure x) → C (-pure x))
(Cm : ∀ (x y : FreeAddGroup α), C x → C y → C (x + y))
:
C z
@[simp]
theorem
FreeAddGroup.map_add
{α : Type u}
{β : Type u}
(f : α → β)
(x : FreeAddGroup α)
(y : FreeAddGroup α)
:
@[simp]
@[simp]
@[simp]
theorem
FreeAddGroup.add_bind
{α : Type u}
{β : Type u}
(f : α → FreeAddGroup β)
(x : FreeAddGroup α)
(y : FreeAddGroup α)
:
@[simp]
theorem
FreeAddGroup.neg_bind
{α : Type u}
{β : Type u}
(f : α → FreeAddGroup β)
(x : FreeAddGroup α)
:
The maximal reduction of a word. It is computable iff α has decidable equality.
Equations
- One or more equations did not get rendered due to their size.
The maximal reduction of a word. It is computable
iff α has decidable equality.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
FreeAddGroup.reduce.cons
{α : Type u}
{L : List (α × Bool)}
[DecidableEq α]
(x : α × Bool)
:
@[simp]
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
FreeAddGroup.reduce.min
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeAddGroup.Red (FreeAddGroup.reduce L₁) L₂)
:
FreeAddGroup.reduce L₁ = L₂
The second theorem that characterises the function reduce: the maximal reduction of
a word only reduces to itself.
theorem
FreeGroup.reduce.min
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeGroup.Red (FreeGroup.reduce L₁) L₂)
:
FreeGroup.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
FreeAddGroup.reduce.Step.eq
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeAddGroup.Red.Step L₁ L₂)
:
abbrev
FreeAddGroup.reduce.Step.eq.match_1
{α : Type u_1}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(motive : Relation.Join FreeAddGroup.Red (FreeAddGroup.reduce L₁) (FreeAddGroup.reduce L₂) → Prop)
:
∀ (x : Relation.Join FreeAddGroup.Red (FreeAddGroup.reduce L₁) (FreeAddGroup.reduce L₂)),
(∀ (_L₃ : List (α × Bool)) (HR13 : FreeAddGroup.Red (FreeAddGroup.reduce L₁) _L₃)
(HR23 : FreeAddGroup.Red (FreeAddGroup.reduce L₂) _L₃), motive ⋯) →
motive x
Equations
- ⋯ = ⋯
theorem
FreeGroup.reduce.Step.eq
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeGroup.Red.Step L₁ L₂)
:
theorem
FreeAddGroup.reduce.eq_of_red
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeAddGroup.Red L₁ L₂)
:
If a word reduces to another word, then they have a common maximal reduction.
theorem
FreeGroup.reduce.eq_of_red
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeGroup.Red L₁ L₂)
:
If a word reduces to another word, then they have a common maximal reduction.
theorem
FreeGroup.red.reduce_eq
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeGroup.Red L₁ L₂)
:
Alias of FreeGroup.reduce.eq_of_red.
If a word reduces to another word, then they have a common maximal reduction.
theorem
FreeGroup.freeAddGroup.red.reduce_eq
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeAddGroup.Red L₁ L₂)
:
Alias of FreeAddGroup.reduce.eq_of_red.
If a word reduces to another word, then they have a common maximal reduction.
theorem
FreeAddGroup.Red.reduce_right
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(h : FreeAddGroup.Red L₁ L₂)
:
FreeAddGroup.Red L₁ (FreeAddGroup.reduce L₂)
theorem
FreeGroup.Red.reduce_right
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(h : FreeGroup.Red L₁ L₂)
:
FreeGroup.Red L₁ (FreeGroup.reduce L₂)
theorem
FreeAddGroup.Red.reduce_left
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(h : FreeAddGroup.Red L₁ L₂)
:
FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁)
theorem
FreeGroup.Red.reduce_left
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(h : FreeGroup.Red L₁ L₂)
:
FreeGroup.Red L₂ (FreeGroup.reduce L₁)
theorem
FreeAddGroup.reduce.sound
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeAddGroup.mk L₁ = FreeAddGroup.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.
abbrev
FreeAddGroup.reduce.sound.match_1
{α : Type u_1}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
(motive : Relation.Join FreeAddGroup.Red L₁ L₂ → Prop)
:
∀ (x : Relation.Join FreeAddGroup.Red L₁ L₂),
(∀ (_L₃ : List (α × Bool)) (H13 : FreeAddGroup.Red L₁ _L₃) (H23 : FreeAddGroup.Red L₂ _L₃), motive ⋯) → motive x
Equations
- ⋯ = ⋯
theorem
FreeGroup.reduce.sound
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeGroup.mk L₁ = FreeGroup.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
FreeAddGroup.reduce.exact
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂)
:
FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂
If two words have a common maximal reduction, then they correspond to the same element in the additive free group.
theorem
FreeGroup.reduce.exact
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeGroup.reduce L₁ = FreeGroup.reduce L₂)
:
FreeGroup.mk L₁ = FreeGroup.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 additive free group.
A word and its maximal reduction correspond to the same element of the free group.
theorem
FreeAddGroup.reduce.rev
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeAddGroup.Red L₁ L₂)
:
FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁)
If words w₁ w₂ are such that w₁ reduces to w₂, then w₂ reduces to the maximal
reduction of w₁.
theorem
FreeGroup.reduce.rev
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeGroup.Red L₁ L₂)
:
FreeGroup.Red L₂ (FreeGroup.reduce 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.
theorem
FreeAddGroup.toWord.proof_1
{α : Type u_1}
[DecidableEq α]
(_L₁ : List (α × Bool))
(_L₂ : List (α × Bool))
(H : FreeAddGroup.Red.Step _L₁ _L₂)
:
FreeAddGroup.reduce _L₁ = FreeAddGroup.reduce _L₂
The function that sends an element of the free group to its maximal reduction.
theorem
FreeGroup.mk_toWord
{α : Type u}
[DecidableEq α]
{x : FreeGroup α}
:
FreeGroup.mk (FreeGroup.toWord x) = x
theorem
FreeAddGroup.toWord_injective
{α : Type u}
[DecidableEq α]
:
Function.Injective FreeAddGroup.toWord
theorem
FreeGroup.toWord_injective
{α : Type u}
[DecidableEq α]
:
Function.Injective FreeGroup.toWord
@[simp]
theorem
FreeAddGroup.toWord_inj
{α : Type u}
[DecidableEq α]
{x : FreeAddGroup α}
{y : FreeAddGroup α}
:
FreeAddGroup.toWord x = FreeAddGroup.toWord y ↔ x = y
@[simp]
theorem
FreeGroup.toWord_inj
{α : Type u}
[DecidableEq α]
{x : FreeGroup α}
{y : FreeGroup α}
:
FreeGroup.toWord x = FreeGroup.toWord y ↔ x = y
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
FreeAddGroup.toWord_eq_nil_iff
{α : Type u}
[DecidableEq α]
{x : FreeAddGroup α}
:
FreeAddGroup.toWord x = [] ↔ x = 0
@[simp]
theorem
FreeGroup.toWord_eq_nil_iff
{α : Type u}
[DecidableEq α]
{x : FreeGroup α}
:
FreeGroup.toWord x = [] ↔ x = 1
theorem
FreeAddGroup.reduce.churchRosser.proof_1
{α : Type u_1}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{L₃ : List (α × Bool)}
[DecidableEq α]
(H12 : FreeAddGroup.Red L₁ L₂)
(H13 : FreeAddGroup.Red L₁ L₃)
:
FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁) ∧ FreeAddGroup.Red L₃ (FreeAddGroup.reduce L₁)
def
FreeAddGroup.reduce.churchRosser
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{L₃ : List (α × Bool)}
[DecidableEq α]
(H12 : FreeAddGroup.Red L₁ L₂)
(H13 : FreeAddGroup.Red L₁ L₃)
:
{ L₄ : List (α × Bool) // FreeAddGroup.Red L₂ L₄ ∧ FreeAddGroup.Red L₃ L₄ }
Constructive Church-Rosser theorem (compare church_rosser).
Equations
- FreeAddGroup.reduce.churchRosser H12 H13 = { val := FreeAddGroup.reduce L₁, property := ⋯ }
def
FreeGroup.reduce.churchRosser
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
{L₃ : List (α × Bool)}
[DecidableEq α]
(H12 : FreeGroup.Red L₁ L₂)
(H13 : FreeGroup.Red L₁ L₃)
:
{ L₄ : List (α × Bool) // FreeGroup.Red L₂ L₄ ∧ FreeGroup.Red L₃ L₄ }
Constructive Church-Rosser theorem (compare church_rosser).
Equations
- FreeGroup.reduce.churchRosser H12 H13 = { val := FreeGroup.reduce L₁, property := ⋯ }
Equations
- FreeAddGroup.instDecidableEqFreeAddGroup = Function.Injective.decidableEq ⋯
theorem
FreeAddGroup.instDecidableEqFreeAddGroup.proof_1
{α : Type u_1}
[DecidableEq α]
:
Function.Injective FreeAddGroup.toWord
Equations
- FreeGroup.instDecidableEqFreeGroup = Function.Injective.decidableEq ⋯
Equations
- One or more equations did not get rendered due to their size.
- FreeGroup.Red.decidableRel [] [] = isTrue ⋯
- FreeGroup.Red.decidableRel [] (_hd2 :: _tl2) = isFalse ⋯
- FreeGroup.Red.decidableRel ((x_2, b) :: tl) [] = match FreeGroup.Red.decidableRel tl [(x_2, !b)] with | isTrue H => isTrue ⋯ | isFalse H => isFalse ⋯
A list containing every word that w₁ reduces to.
Equations
- FreeGroup.Red.enum L₁ = List.filter (fun (b : List (α × Bool)) => decide (FreeGroup.Red L₁ b)) (List.sublists L₁)
theorem
FreeGroup.Red.enum.sound
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : L₂ ∈ List.filter (fun (b : List (α × Bool)) => decide (FreeGroup.Red L₁ b)) (List.sublists L₁))
:
FreeGroup.Red L₁ L₂
theorem
FreeGroup.Red.enum.complete
{α : Type u}
{L₁ : List (α × Bool)}
{L₂ : List (α × Bool)}
[DecidableEq α]
(H : FreeGroup.Red L₁ L₂)
:
L₂ ∈ FreeGroup.Red.enum L₁
instance
FreeGroup.instFintypeSubtypeListProdBoolRed
{α : Type u}
{L₁ : List (α × Bool)}
[DecidableEq α]
:
Fintype { L₂ : List (α × Bool) // FreeGroup.Red L₁ L₂ }
Equations
- FreeGroup.instFintypeSubtypeListProdBoolRed = Fintype.subtype (List.toFinset (FreeGroup.Red.enum L₁)) ⋯
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.
Equations
@[simp]
@[simp]
@[simp]
theorem
FreeAddGroup.norm_eq_zero
{α : Type u}
[DecidableEq α]
{x : FreeAddGroup α}
:
FreeAddGroup.norm x = 0 ↔ x = 0
@[simp]
theorem
FreeGroup.norm_eq_zero
{α : Type u}
[DecidableEq α]
{x : FreeGroup α}
:
FreeGroup.norm x = 0 ↔ x = 1
theorem
FreeAddGroup.norm_mk_le
{α : Type u}
{L₁ : List (α × Bool)}
[DecidableEq α]
:
FreeAddGroup.norm (FreeAddGroup.mk L₁) ≤ List.length L₁
theorem
FreeGroup.norm_mk_le
{α : Type u}
{L₁ : List (α × Bool)}
[DecidableEq α]
:
FreeGroup.norm (FreeGroup.mk L₁) ≤ List.length L₁
theorem
FreeAddGroup.norm_add_le
{α : Type u}
[DecidableEq α]
(x : FreeAddGroup α)
(y : FreeAddGroup α)
:
FreeAddGroup.norm (x + y) ≤ FreeAddGroup.norm x + FreeAddGroup.norm y
theorem
FreeGroup.norm_mul_le
{α : Type u}
[DecidableEq α]
(x : FreeGroup α)
(y : FreeGroup α)
:
FreeGroup.norm (x * y) ≤ FreeGroup.norm x + FreeGroup.norm y