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
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
- ⋯ = ⋯
Instances For
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
- ⋯ = ⋯
Instances For
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
- ⋯ = ⋯
Instances For
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
- ⋯ = ⋯
Instances For
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
- ⋯ = ⋯
Instances For
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
- ⋯ = ⋯
Instances For
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
- ⋯ = ⋯
Instances For
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
- ⋯ = ⋯
Instances For
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
The canonical map from list (α × bool) to the free additive group on α.
Equations
- FreeAddGroup.mk L = Quot.mk FreeAddGroup.Red.Step L
Instances For
@[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)]
Instances For
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)]
Instances For
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
- ⋯ = ⋯
Instances For
The canonical map from the type to the free group is an injection.
Given f : α → β with β an additive group, the canonical map
list (α × bool) → β
Equations
Instances For
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.
Instances For
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)) ⋯) ⋯
Instances For
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)) ⋯) ⋯
Instances For
@[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' := ⋯ }
Instances For
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' := ⋯ }
Instances For
@[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
Instances For
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
Instances For
@[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
Instances For
@[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.
Instances For
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
- ⋯ = ⋯
Instances For
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.
Instances For
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.
Instances For
@[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
- ⋯ = ⋯
Instances For
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
- ⋯ = ⋯
Instances For
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.
Instances For
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.
Instances For
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 := ⋯ }
Instances For
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 := ⋯ }
Instances For
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₁)
Instances For
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
Instances For
The length of reduced words provides a norm on a free group.
Equations
Instances For
@[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