Documentation

Mathlib.GroupTheory.FreeGroup.Basic

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 over a : α × Bool modulo the relation a * x * x⁻¹ * b = a * b.
FreeGroup.mk/FreeAddGroup.mk: the canonical quotient map List (α × Bool) → FreeGroup α.
FreeGroup.of/FreeAddGroup.of: the canonical injection α → FreeGroup α.
FreeGroup.lift f/FreeAddGroup.lift: the canonical group homomorphism FreeGroup α →* G given a group G and a function f : α → 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

inductive FreeAddGroup.Red.Step {α : Type u} :

List (α × Bool) → List (α × Bool) → Prop

Reduction step for the additive free group relation: w + x + (-x) + v ~> w + v

not: ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool}, FreeAddGroup.Red.Step (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁ ++ L₂)

Instances For

inductive FreeGroup.Red.Step {α : Type u} :

List (α × Bool) → List (α × Bool) → Prop

Reduction step for the multiplicative free group relation: w * x * x⁻¹ * v ~> w * v

not: ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool}, FreeGroup.Red.Step (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁ ++ L₂)

Instances For

def FreeGroup.Red {α : Type u} :

List (α × Bool) → List (α × Bool) → Prop

Reflexive-transitive closure of Red.Step

Equations

FreeGroup.Red = Relation.ReflTransGen FreeGroup.Red.Step

Instances For

def FreeAddGroup.Red {α : Type u} :

List (α × Bool) → List (α × Bool) → Prop

Reflexive-transitive closure of Red.Step

Equations

FreeAddGroup.Red = Relation.ReflTransGen FreeAddGroup.Red.Step

Instances For

theorem FreeGroup.Red.refl {α : Type u} {L : List (α × Bool)} :

FreeGroup.Red L L

theorem FreeAddGroup.Red.refl {α : Type u} {L : List (α × Bool)} :

FreeAddGroup.Red L L

theorem FreeGroup.Red.trans {α : Type u} {L₁ L₂ L₃ : List (α × Bool)} :

FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ L₃ → FreeGroup.Red L₁ L₃

theorem FreeAddGroup.Red.trans {α : Type u} {L₁ L₂ L₃ : List (α × Bool)} :

FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₂ L₃ → FreeAddGroup.Red L₁ L₃

theorem FreeGroup.Red.Step.length {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeGroup.Red.Step L₁ L₂ → L₂.length + 2 = L₁.length

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.length {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeAddGroup.Red.Step L₁ L₂ → L₂.length + 2 = L₁.length

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₄

@[simp]

theorem FreeGroup.Red.Step.not_rev {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool} :

FreeGroup.Red.Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)

@[simp]

theorem FreeAddGroup.Red.Step.not_rev {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool} :

FreeAddGroup.Red.Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)

@[simp]

theorem FreeGroup.Red.Step.cons_not {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} :

FreeGroup.Red.Step ((x, b) :: (x, !b) :: L) L

@[simp]

theorem FreeAddGroup.Red.Step.cons_not {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} :

FreeAddGroup.Red.Step ((x, b) :: (x, !b) :: L) L

@[simp]

theorem FreeGroup.Red.Step.cons_not_rev {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} :

FreeGroup.Red.Step ((x, !b) :: (x, b) :: L) L

@[simp]

theorem FreeAddGroup.Red.Step.cons_not_rev {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} :

FreeAddGroup.Red.Step ((x, !b) :: (x, b) :: L) L

theorem FreeGroup.Red.Step.append_left {α : Type u} {L₁ L₂ L₃ : List (α × Bool)} :

FreeGroup.Red.Step L₂ L₃ → FreeGroup.Red.Step (L₁ ++ L₂) (L₁ ++ L₃)

theorem FreeAddGroup.Red.Step.append_left {α : Type u} {L₁ L₂ L₃ : List (α × Bool)} :

FreeAddGroup.Red.Step L₂ L₃ → FreeAddGroup.Red.Step (L₁ ++ L₂) (L₁ ++ L₃)

theorem FreeGroup.Red.Step.cons {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α × Bool} (H : FreeGroup.Red.Step L₁ L₂) :

FreeGroup.Red.Step (x :: L₁) (x :: L₂)

theorem FreeAddGroup.Red.Step.cons {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α × Bool} (H : FreeAddGroup.Red.Step L₁ L₂) :

FreeAddGroup.Red.Step (x :: L₁) (x :: L₂)

theorem FreeGroup.Red.Step.append_right {α : Type u} {L₁ L₂ L₃ : List (α × Bool)} :

FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red.Step (L₁ ++ L₃) (L₂ ++ L₃)

theorem FreeAddGroup.Red.Step.append_right {α : Type u} {L₁ L₂ L₃ : List (α × Bool)} :

FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Red.Step (L₁ ++ L₃) (L₂ ++ L₃)

theorem FreeGroup.Red.not_step_nil {α : Type u} {L : List (α × Bool)} :

¬FreeGroup.Red.Step [] L

theorem FreeAddGroup.Red.not_step_nil {α : Type u} {L : List (α × Bool)} :

¬FreeAddGroup.Red.Step [] L

theorem FreeGroup.Red.Step.cons_left_iff {α : Type u} {L₁ L₂ : List (α × Bool)} {a : α} {b : Bool} :

FreeGroup.Red.Step ((a, b) :: L₁) L₂ ↔ (∃ (L : List (α × Bool)), FreeGroup.Red.Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

theorem FreeAddGroup.Red.Step.cons_left_iff {α : Type u} {L₁ L₂ : List (α × Bool)} {a : α} {b : Bool} :

FreeAddGroup.Red.Step ((a, b) :: L₁) L₂ ↔ (∃ (L : List (α × Bool)), FreeAddGroup.Red.Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

theorem FreeGroup.Red.not_step_singleton {α : Type u} {L : List (α × Bool)} {p : α × Bool} :

¬FreeGroup.Red.Step [p] L

theorem FreeAddGroup.Red.not_step_singleton {α : Type u} {L : List (α × Bool)} {p : α × Bool} :

¬FreeAddGroup.Red.Step [p] L

theorem FreeGroup.Red.Step.cons_cons_iff {α : Type u} {L₁ L₂ : List (α × Bool)} {p : α × Bool} :

FreeGroup.Red.Step (p :: L₁) (p :: L₂) ↔ FreeGroup.Red.Step L₁ L₂

theorem FreeAddGroup.Red.Step.cons_cons_iff {α : Type u} {L₁ L₂ : List (α × Bool)} {p : α × Bool} :

FreeAddGroup.Red.Step (p :: L₁) (p :: L₂) ↔ FreeAddGroup.Red.Step L₁ L₂

theorem FreeGroup.Red.Step.append_left_iff {α : Type u} {L₁ L₂ : List (α × Bool)} (L : List (α × Bool)) :

FreeGroup.Red.Step (L ++ L₁) (L ++ L₂) ↔ FreeGroup.Red.Step L₁ L₂

theorem FreeAddGroup.Red.Step.append_left_iff {α : Type u} {L₁ L₂ : List (α × Bool)} (L : List (α × Bool)) :

FreeAddGroup.Red.Step (L ++ L₁) (L ++ L₂) ↔ FreeAddGroup.Red.Step L₁ L₂

theorem FreeGroup.Red.Step.diamond_aux {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} :

L₁ ++ (x1, b1) :: (x1, !b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, !b2) :: L₄ → L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ (L₅ : List (α × Bool)), FreeGroup.Red.Step (L₁ ++ L₂) L₅ ∧ FreeGroup.Red.Step (L₃ ++ L₄) L₅

theorem FreeAddGroup.Red.Step.diamond_aux {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} :

L₁ ++ (x1, b1) :: (x1, !b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, !b2) :: L₄ → L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step (L₁ ++ L₂) L₅ ∧ FreeAddGroup.Red.Step (L₃ ++ L₄) L₅

theorem FreeGroup.Red.Step.diamond {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)} :

FreeGroup.Red.Step L₁ L₃ → FreeGroup.Red.Step L₂ L₄ → L₁ = L₂ → L₃ = L₄ ∨ ∃ (L₅ : List (α × Bool)), FreeGroup.Red.Step L₃ L₅ ∧ FreeGroup.Red.Step L₄ L₅

theorem FreeAddGroup.Red.Step.diamond {α : Type u} {L₁ L₂ L₃ 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₅

theorem FreeGroup.Red.Step.to_red {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red L₁ L₂

theorem FreeAddGroup.Red.Step.to_red {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Red L₁ L₂

theorem FreeGroup.Red.church_rosser {α : Type u} {L₁ L₂ 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.church_rosser {α : Type u} {L₁ L₂ 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.

theorem FreeGroup.Red.cons_cons {α : Type u} {L₁ L₂ : List (α × Bool)} {p : α × Bool} :

FreeGroup.Red L₁ L₂ → FreeGroup.Red (p :: L₁) (p :: L₂)

theorem FreeAddGroup.Red.cons_cons {α : Type u} {L₁ L₂ : List (α × Bool)} {p : α × Bool} :

FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red (p :: L₁) (p :: L₂)

theorem FreeGroup.Red.cons_cons_iff {α : Type u} {L₁ L₂ : List (α × Bool)} (p : α × Bool) :

FreeGroup.Red (p :: L₁) (p :: L₂) ↔ FreeGroup.Red L₁ L₂

theorem FreeAddGroup.Red.cons_cons_iff {α : Type u} {L₁ L₂ : List (α × Bool)} (p : α × Bool) :

FreeAddGroup.Red (p :: L₁) (p :: L₂) ↔ FreeAddGroup.Red L₁ L₂

theorem FreeGroup.Red.append_append_left_iff {α : Type u} {L₁ L₂ : List (α × Bool)} (L : List (α × Bool)) :

FreeGroup.Red (L ++ L₁) (L ++ L₂) ↔ FreeGroup.Red L₁ L₂

theorem FreeAddGroup.Red.append_append_left_iff {α : Type u} {L₁ L₂ : List (α × Bool)} (L : List (α × Bool)) :

FreeAddGroup.Red (L ++ L₁) (L ++ L₂) ↔ FreeAddGroup.Red L₁ L₂

theorem FreeGroup.Red.append_append {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)} (h₁ : FreeGroup.Red L₁ L₃) (h₂ : FreeGroup.Red L₂ L₄) :

FreeGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)

theorem FreeAddGroup.Red.append_append {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)} (h₁ : FreeAddGroup.Red L₁ L₃) (h₂ : FreeAddGroup.Red L₂ L₄) :

FreeAddGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)

theorem FreeGroup.Red.to_append_iff {α : Type u} {L L₁ L₂ : List (α × Bool)} :

FreeGroup.Red L (L₁ ++ L₂) ↔ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ FreeGroup.Red L₃ L₁ ∧ FreeGroup.Red L₄ L₂

theorem FreeAddGroup.Red.to_append_iff {α : Type u} {L L₁ L₂ : List (α × Bool)} :

FreeAddGroup.Red L (L₁ ++ L₂) ↔ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ FreeAddGroup.Red L₃ L₁ ∧ FreeAddGroup.Red L₄ L₂

theorem FreeGroup.Red.nil_iff {α : Type u} {L : List (α × Bool)} :

FreeGroup.Red [] L ↔ L = []

The empty word [] only reduces to itself.

theorem FreeAddGroup.Red.nil_iff {α : Type u} {L : List (α × Bool)} :

FreeAddGroup.Red [] L ↔ L = []

The empty word [] only reduces to itself.

theorem FreeGroup.Red.singleton_iff {α : Type u} {L₁ : List (α × Bool)} {x : α × Bool} :

FreeGroup.Red [x] L₁ ↔ L₁ = [x]

A letter only reduces to itself.

theorem FreeAddGroup.Red.singleton_iff {α : Type u} {L₁ : List (α × Bool)} {x : α × Bool} :

FreeAddGroup.Red [x] L₁ ↔ L₁ = [x]

A letter only reduces to itself.

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.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.

theorem FreeGroup.Red.red_iff_irreducible {α : Type u} {L : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} (h : (x1, b1) ≠ (x2, b2)) :

FreeGroup.Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]

theorem FreeAddGroup.Red.red_iff_irreducible {α : Type u} {L : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} (h : (x1, b1) ≠ (x2, b2)) :

FreeAddGroup.Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]

theorem FreeGroup.Red.inv_of_red_of_ne {α : Type u} {L₁ 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.neg_of_red_of_ne {α : Type u} {L₁ 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.Step.sublist {α : Type u} {L₁ L₂ : List (α × Bool)} (H : FreeGroup.Red.Step L₁ L₂) :

L₂.Sublist L₁

theorem FreeAddGroup.Red.Step.sublist {α : Type u} {L₁ L₂ : List (α × Bool)} (H : FreeAddGroup.Red.Step L₁ L₂) :

L₂.Sublist L₁

theorem FreeGroup.Red.sublist {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeGroup.Red L₁ L₂ → L₂.Sublist L₁

If w₁ w₂ are words such that w₁ reduces to w₂, then w₂ is a sublist of w₁.

theorem FreeAddGroup.Red.sublist {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeAddGroup.Red L₁ L₂ → L₂.Sublist L₁

If w₁ w₂ are words such that w₁ reduces to w₂, then w₂ is a sublist of w₁.

theorem FreeGroup.Red.length_le {α : Type u} {L₁ L₂ : List (α × Bool)} (h : FreeGroup.Red L₁ L₂) :

L₂.length ≤ L₁.length

theorem FreeAddGroup.Red.length_le {α : Type u} {L₁ L₂ : List (α × Bool)} (h : FreeAddGroup.Red L₁ L₂) :

L₂.length ≤ L₁.length

theorem FreeGroup.Red.sizeof_of_step {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeGroup.Red.Step L₁ L₂ → sizeOf L₂ < sizeOf L₁

theorem FreeAddGroup.Red.sizeof_of_step {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeAddGroup.Red.Step L₁ L₂ → sizeOf L₂ < sizeOf L₁

theorem FreeGroup.Red.length {α : Type u} {L₁ L₂ : List (α × Bool)} (h : FreeGroup.Red L₁ L₂) :

∃ (n : ℕ), L₁.length = L₂.length + 2 * n

theorem FreeAddGroup.Red.length {α : Type u} {L₁ L₂ : List (α × Bool)} (h : FreeAddGroup.Red L₁ L₂) :

∃ (n : ℕ), L₁.length = L₂.length + 2 * n

theorem FreeGroup.Red.antisymm {α : Type u} {L₁ L₂ : List (α × Bool)} (h₁₂ : FreeGroup.Red L₁ L₂) (h₂₁ : FreeGroup.Red L₂ L₁) :

L₁ = L₂

theorem FreeAddGroup.Red.antisymm {α : Type u} {L₁ L₂ : List (α × Bool)} (h₁₂ : FreeAddGroup.Red L₁ L₂) (h₂₁ : FreeAddGroup.Red L₂ L₁) :

L₁ = L₂

theorem FreeGroup.equivalence_join_red {α : Type u} :

Equivalence (Relation.Join FreeGroup.Red)

theorem FreeAddGroup.equivalence_join_red {α : Type u} :

Equivalence (Relation.Join FreeAddGroup.Red)

theorem FreeGroup.join_red_of_step {α : Type u} {L₁ L₂ : List (α × Bool)} (h : FreeGroup.Red.Step L₁ L₂) :

Relation.Join FreeGroup.Red L₁ L₂

theorem FreeAddGroup.join_red_of_step {α : Type u} {L₁ L₂ : List (α × Bool)} (h : FreeAddGroup.Red.Step L₁ L₂) :

Relation.Join FreeAddGroup.Red L₁ L₂

theorem FreeGroup.eqvGen_step_iff_join_red {α : Type u} {L₁ L₂ : List (α × Bool)} :

Relation.EqvGen FreeGroup.Red.Step L₁ L₂ ↔ Relation.Join FreeGroup.Red L₁ L₂

theorem FreeAddGroup.eqvGen_step_iff_join_red {α : Type u} {L₁ L₂ : List (α × Bool)} :

Relation.EqvGen FreeAddGroup.Red.Step L₁ L₂ ↔ Relation.Join FreeAddGroup.Red L₁ L₂

def FreeGroup (α : Type u) :

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

FreeGroup α = Quot FreeGroup.Red.Step

Instances For

def FreeAddGroup (α : Type u) :

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

def FreeGroup.mk {α : Type u} (L : List (α × Bool)) :

The canonical map from List (α × Bool) to the free group on α.

Equations

FreeGroup.mk L = Quot.mk FreeGroup.Red.Step L

Instances For

def FreeAddGroup.mk {α : Type u} (L : List (α × Bool)) :

FreeAddGroup α

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 FreeGroup.quot_mk_eq_mk {α : Type u} {L : List (α × Bool)} :

Quot.mk FreeGroup.Red.Step L = FreeGroup.mk 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_lift_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.lift f H (FreeGroup.mk L) = f L

@[simp]

theorem FreeAddGroup.quot_lift_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.lift f H (FreeAddGroup.mk L) = 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

@[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_map_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → List (β × Bool)) (H : (FreeGroup.Red.Step ⇒ FreeGroup.Red.Step) f f) :

Quot.map f H (FreeGroup.mk L) = FreeGroup.mk (f L)

@[simp]

theorem FreeAddGroup.quot_map_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → List (β × Bool)) (H : (FreeAddGroup.Red.Step ⇒ FreeAddGroup.Red.Step) f f) :

Quot.map f H (FreeAddGroup.mk L) = FreeAddGroup.mk (f L)

instance FreeGroup.instOne {α : Type u} :

One (FreeGroup α)

Equations

FreeGroup.instOne = { one := FreeGroup.mk [] }

instance FreeAddGroup.instZero {α : Type u} :

Zero (FreeAddGroup α)

Equations

FreeAddGroup.instZero = { zero := FreeAddGroup.mk [] }

theorem FreeGroup.one_eq_mk {α : Type u} :

1 = FreeGroup.mk []

theorem FreeAddGroup.zero_eq_mk {α : Type u} :

0 = FreeAddGroup.mk []

instance FreeGroup.instInhabited {α : Type u} :

Inhabited (FreeGroup α)

Equations

FreeGroup.instInhabited = { default := 1 }

instance FreeAddGroup.instInhabited {α : Type u} :

Inhabited (FreeAddGroup α)

Equations

FreeAddGroup.instInhabited = { default := 0 }

instance FreeGroup.instUniqueOfIsEmpty {α : Type u} [IsEmpty α] :

Unique (FreeGroup α)

Equations

FreeGroup.instUniqueOfIsEmpty = id inferInstance

instance FreeAddGroup.instUniqueOfIsEmpty {α : Type u} [IsEmpty α] :

Unique (FreeAddGroup α)

Equations

FreeAddGroup.instUniqueOfIsEmpty = id inferInstance

instance FreeGroup.instMul {α : Type u} :

Mul (FreeGroup α)

Equations

FreeGroup.instMul = { mul := fun (x y : FreeGroup α) => Quot.liftOn x (fun (L₁ : List (α × Bool)) => Quot.liftOn y (fun (L₂ : List (α × Bool)) => FreeGroup.mk (L₁ ++ L₂)) ⋯) ⋯ }

instance FreeAddGroup.instAdd {α : Type u} :

Add (FreeAddGroup α)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem FreeGroup.mul_mk {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeGroup.mk L₁ * FreeGroup.mk L₂ = FreeGroup.mk (L₁ ++ L₂)

@[simp]

theorem FreeAddGroup.add_mk {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeAddGroup.mk L₁ + FreeAddGroup.mk L₂ = FreeAddGroup.mk (L₁ ++ L₂)

def FreeGroup.invRev {α : Type u} (w : List (α × Bool)) :

List (α × Bool)

Transform a word representing a free group element into a word representing its inverse.

Equations

FreeGroup.invRev w = (List.map (fun (g : α × Bool) => (g.1, !g.2)) w).reverse

Instances For

def FreeAddGroup.negRev {α : Type u} (w : List (α × Bool)) :

List (α × Bool)

Transform a word representing a free group element into a word representing its negative.

Equations

FreeAddGroup.negRev w = (List.map (fun (g : α × Bool) => (g.1, !g.2)) w).reverse

Instances For

@[simp]

theorem FreeGroup.invRev_length {α : Type u} {L₁ : List (α × Bool)} :

(FreeGroup.invRev L₁).length = L₁.length

@[simp]

theorem FreeAddGroup.negRev_length {α : Type u} {L₁ : List (α × Bool)} :

(FreeAddGroup.negRev L₁).length = L₁.length

@[simp]

theorem FreeGroup.invRev_invRev {α : Type u} {L₁ : List (α × Bool)} :

FreeGroup.invRev (FreeGroup.invRev L₁) = L₁

@[simp]

theorem FreeAddGroup.negRev_negRev {α : Type u} {L₁ : List (α × Bool)} :

FreeAddGroup.negRev (FreeAddGroup.negRev L₁) = L₁

@[simp]

theorem FreeGroup.invRev_empty {α : Type u} :

FreeGroup.invRev [] = []

@[simp]

theorem FreeAddGroup.negRev_empty {α : Type u} :

FreeAddGroup.negRev [] = []

theorem FreeGroup.invRev_involutive {α : Type u} :

Function.Involutive FreeGroup.invRev

theorem FreeAddGroup.negRev_involutive {α : Type u} :

Function.Involutive FreeAddGroup.negRev

theorem FreeGroup.invRev_injective {α : Type u} :

Function.Injective FreeGroup.invRev

theorem FreeAddGroup.negRev_injective {α : Type u} :

Function.Injective FreeAddGroup.negRev

theorem FreeGroup.invRev_surjective {α : Type u} :

Function.Surjective FreeGroup.invRev

theorem FreeAddGroup.negRev_surjective {α : Type u} :

Function.Surjective FreeAddGroup.negRev

theorem FreeGroup.invRev_bijective {α : Type u} :

Function.Bijective FreeGroup.invRev

theorem FreeAddGroup.negRev_bijective {α : Type u} :

Function.Bijective FreeAddGroup.negRev

instance FreeGroup.instInv {α : Type u} :

Inv (FreeGroup α)

Equations

FreeGroup.instInv = { inv := Quot.map FreeGroup.invRev ⋯ }

instance FreeAddGroup.instNeg {α : Type u} :

Neg (FreeAddGroup α)

Equations

FreeAddGroup.instNeg = { neg := Quot.map FreeAddGroup.negRev ⋯ }

@[simp]

theorem FreeGroup.inv_mk {α : Type u} {L : List (α × Bool)} :

(FreeGroup.mk L)⁻¹ = FreeGroup.mk (FreeGroup.invRev L)

@[simp]

theorem FreeAddGroup.neg_mk {α : Type u} {L : List (α × Bool)} :

-FreeAddGroup.mk L = FreeAddGroup.mk (FreeAddGroup.negRev L)

theorem FreeGroup.Red.Step.invRev {α : Type u} {L₁ L₂ : List (α × Bool)} (h : FreeGroup.Red.Step L₁ L₂) :

FreeGroup.Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)

theorem FreeAddGroup.Red.Step.negRev {α : Type u} {L₁ L₂ : List (α × Bool)} (h : FreeAddGroup.Red.Step L₁ L₂) :

FreeAddGroup.Red.Step (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂)

theorem FreeGroup.Red.invRev {α : Type u} {L₁ L₂ : List (α × Bool)} (h : FreeGroup.Red L₁ L₂) :

FreeGroup.Red (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)

theorem FreeAddGroup.Red.negRev {α : Type u} {L₁ L₂ : List (α × Bool)} (h : FreeAddGroup.Red L₁ L₂) :

FreeAddGroup.Red (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂)

@[simp]

theorem FreeGroup.Red.step_invRev_iff {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeGroup.Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ FreeGroup.Red.Step L₁ L₂

@[simp]

theorem FreeAddGroup.Red.step_negRev_iff {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeAddGroup.Red.Step (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂) ↔ FreeAddGroup.Red.Step L₁ L₂

@[simp]

theorem FreeGroup.red_invRev_iff {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeGroup.Red (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ FreeGroup.Red L₁ L₂

@[simp]

theorem FreeAddGroup.red_negRev_iff {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeAddGroup.Red (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂) ↔ FreeAddGroup.Red L₁ L₂

instance FreeGroup.instGroup {α : Type u} :

Group (FreeGroup α)

Equations

FreeGroup.instGroup = Group.mk ⋯

instance FreeAddGroup.instAddGroup {α : Type u} :

AddGroup (FreeAddGroup α)

Equations

FreeAddGroup.instAddGroup = AddGroup.mk ⋯

@[simp]

theorem FreeGroup.pow_mk {α : Type u} {L : List (α × Bool)} (n : ℕ) :

FreeGroup.mk L ^ n = FreeGroup.mk (List.replicate n L).flatten

@[simp]

theorem FreeAddGroup.nsmul_mk {α : Type u} {L : List (α × Bool)} (n : ℕ) :

n • FreeAddGroup.mk L = FreeAddGroup.mk (List.replicate n L).flatten

def FreeGroup.of {α : Type u} (x : α) :

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

def FreeAddGroup.of {α : Type u} (x : α) :

FreeAddGroup α

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

theorem FreeGroup.Red.exact {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeGroup.mk L₁ = FreeGroup.mk L₂ ↔ Relation.Join FreeGroup.Red L₁ L₂

theorem FreeAddGroup.Red.exact {α : Type u} {L₁ L₂ : List (α × Bool)} :

FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂ ↔ Relation.Join FreeAddGroup.Red L₁ L₂

theorem FreeGroup.of_injective {α : Type u} :

Function.Injective FreeGroup.of

The canonical map from the type to the free group is an injection.

theorem FreeAddGroup.of_injective {α : Type u} :

Function.Injective FreeAddGroup.of

The canonical map from the type to the additive free group is an injection.

def FreeGroup.Lift.aux {α : Type u} {β : Type v} [Group β] (f : α → β) :

List (α × Bool) → β

Given f : α → β with β a group, the canonical map List (α × Bool) → β

Equations

FreeGroup.Lift.aux f L = (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else (f x.1)⁻¹) L).prod

Instances For

def FreeAddGroup.Lift.aux {α : Type u} {β : Type v} [AddGroup β] (f : α → β) :

List (α × Bool) → β

Given f : α → β with β an additive group, the canonical map list (α × bool) → β

Equations

FreeAddGroup.Lift.aux f L = (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) L).sum

Instances For

theorem FreeGroup.Red.Step.lift {α : Type u} {L₁ 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.Red.Step.lift {α : Type u} {L₁ L₂ : List (α × Bool)} {β : Type v} [AddGroup β] {f : α → β} (H : FreeAddGroup.Red.Step L₁ L₂) :

FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂

def FreeGroup.lift {α : Type u} {β : Type v} [Group β] :

(α → β) ≃ (FreeGroup α →* β)

If β is a group, then any function from α to β extends uniquely to a group homomorphism from the free group over α to β

Equations

FreeGroup.lift = { toFun := fun (f : α → β) => MonoidHom.mk' (Quot.lift (FreeGroup.Lift.aux f) ⋯) ⋯, invFun := fun (g : FreeGroup α →* β) => ⇑g ∘ FreeGroup.of, left_inv := ⋯, right_inv := ⋯ }

Instances For

def FreeAddGroup.lift {α : Type u} {β : Type v} [AddGroup β] :

(α → β) ≃ (FreeAddGroup α →+ β)

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

@[simp]

theorem FreeGroup.lift_symm_apply {α : Type u} {β : Type v} [Group β] (g : FreeGroup α →* β) (a✝ : α) :

FreeGroup.lift.symm g a✝ = (⇑g ∘ FreeGroup.of) a✝

@[simp]

theorem FreeAddGroup.lift_symm_apply {α : Type u} {β : Type v} [AddGroup β] (g : FreeAddGroup α →+ β) (a✝ : α) :

FreeAddGroup.lift.symm g a✝ = (⇑g ∘ FreeAddGroup.of) a✝

@[simp]

theorem FreeGroup.lift.mk {α : Type u} {L : List (α × Bool)} {β : Type v} [Group β] {f : α → β} :

(FreeGroup.lift f) (FreeGroup.mk L) = (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else (f x.1)⁻¹) L).prod

@[simp]

theorem FreeAddGroup.lift.mk {α : Type u} {L : List (α × Bool)} {β : Type v} [AddGroup β] {f : α → β} :

(FreeAddGroup.lift f) (FreeAddGroup.mk L) = (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) L).sum

@[simp]

theorem FreeGroup.lift.of {α : Type u} {β : Type v} [Group β] {f : α → β} {x : α} :

(FreeGroup.lift f) (FreeGroup.of x) = f x

@[simp]

theorem FreeAddGroup.lift.of {α : Type u} {β : Type v} [AddGroup β] {f : α → β} {x : α} :

(FreeAddGroup.lift f) (FreeAddGroup.of x) = f x

theorem FreeGroup.lift.unique {α : Type u} {β : Type v} [Group β] {f : α → β} (g : FreeGroup α →* β) (hg : ∀ (x : α), g (FreeGroup.of x) = f x) {x : FreeGroup α} :

g x = (FreeGroup.lift 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 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 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 FreeGroup.lift_of_eq_id (α : Type u_1) :

FreeGroup.lift FreeGroup.of = MonoidHom.id (FreeGroup α)

theorem FreeAddGroup.lift_of_eq_id (α : Type u_1) :

FreeAddGroup.lift FreeAddGroup.of = AddMonoidHom.id (FreeAddGroup α)

theorem FreeGroup.lift.of_eq {α : Type u} (x : FreeGroup α) :

(FreeGroup.lift FreeGroup.of) x = x

theorem FreeAddGroup.lift.of_eq {α : Type u} (x : FreeAddGroup α) :

(FreeAddGroup.lift FreeAddGroup.of) x = x

theorem FreeGroup.lift.range_le {α : Type u} {β : Type v} [Group β] {f : α → β} {s : Subgroup β} (H : Set.range f ⊆ ↑s) :

(FreeGroup.lift f).range ≤ s

theorem FreeAddGroup.lift.range_le {α : Type u} {β : Type v} [AddGroup β] {f : α → β} {s : AddSubgroup β} (H : Set.range f ⊆ ↑s) :

(FreeAddGroup.lift f).range ≤ s

theorem FreeGroup.lift.range_eq_closure {α : Type u} {β : Type v} [Group β] {f : α → β} :

(FreeGroup.lift f).range = Subgroup.closure (Set.range f)

theorem FreeAddGroup.lift.range_eq_closure {α : Type u} {β : Type v} [AddGroup β] {f : α → β} :

(FreeAddGroup.lift f).range = AddSubgroup.closure (Set.range f)

@[simp]

theorem FreeGroup.closure_range_of (α : Type u_1) :

Subgroup.closure (Set.range FreeGroup.of) = ⊤

The generators of FreeGroup α generate FreeGroup α. That is, the subgroup closure of the set of generators equals ⊤.

@[simp]

theorem FreeAddGroup.closure_range_of (α : Type u_1) :

AddSubgroup.closure (Set.range FreeAddGroup.of) = ⊤

def FreeGroup.map {α : Type u} {β : Type v} (f : α → β) :

FreeGroup α →* FreeGroup β

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

def FreeAddGroup.map {α : Type u} {β : Type v} (f : α → β) :

FreeAddGroup α →+ FreeAddGroup β

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

@[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]

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.id {α : Type u} (x : FreeGroup α) :

(FreeGroup.map id) x = x

@[simp]

theorem FreeAddGroup.map.id {α : Type u} (x : FreeAddGroup α) :

(FreeAddGroup.map id) x = x

@[simp]

theorem FreeGroup.map.id' {α : Type u} (x : FreeGroup α) :

(FreeGroup.map fun (z : α) => z) x = x

@[simp]

theorem FreeAddGroup.map.id' {α : Type u} (x : FreeAddGroup α) :

(FreeAddGroup.map fun (z : α) => z) x = 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

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

@[simp]

theorem FreeGroup.map.of {α : Type u} {β : Type v} {f : α → β} {x : α} :

(FreeGroup.map f) (FreeGroup.of x) = FreeGroup.of (f x)

@[simp]

theorem FreeAddGroup.map.of {α : Type u} {β : Type v} {f : α → β} {x : α} :

(FreeAddGroup.map f) (FreeAddGroup.of x) = FreeAddGroup.of (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.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_eq_lift {α : Type u} {β : Type v} {f : α → β} {x : FreeGroup α} :

(FreeGroup.map f) x = (FreeGroup.lift (FreeGroup.of ∘ f)) x

theorem FreeAddGroup.map_eq_lift {α : Type u} {β : Type v} {f : α → β} {x : FreeAddGroup α} :

(FreeAddGroup.map f) x = (FreeAddGroup.lift (FreeAddGroup.of ∘ f)) x

def FreeGroup.freeGroupCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

FreeGroup α ≃* FreeGroup β

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 = { toFun := ⇑(FreeGroup.map ⇑e), invFun := ⇑(FreeGroup.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

def FreeAddGroup.freeAddGroupCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

FreeAddGroup α ≃+ FreeAddGroup β

Equivalent types give rise to additively equivalent additive free groups.

Equations

FreeAddGroup.freeAddGroupCongr e = { toFun := ⇑(FreeAddGroup.map ⇑e), invFun := ⇑(FreeAddGroup.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem FreeAddGroup.freeAddGroupCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : FreeAddGroup α) :

(FreeAddGroup.freeAddGroupCongr e) a = (FreeAddGroup.map ⇑e) a

@[simp]

theorem FreeGroup.freeGroupCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : FreeGroup α) :

(FreeGroup.freeGroupCongr e) a = (FreeGroup.map ⇑e) a

@[simp]

theorem FreeGroup.freeGroupCongr_refl {α : Type u} :

FreeGroup.freeGroupCongr (Equiv.refl α) = MulEquiv.refl (FreeGroup α)

@[simp]

theorem FreeAddGroup.freeAddGroupCongr_refl {α : Type u} :

FreeAddGroup.freeAddGroupCongr (Equiv.refl α) = AddEquiv.refl (FreeAddGroup α)

@[simp]

theorem FreeGroup.freeGroupCongr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

(FreeGroup.freeGroupCongr e).symm = FreeGroup.freeGroupCongr e.symm

@[simp]

theorem FreeAddGroup.freeAddGroupCongr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

(FreeAddGroup.freeAddGroupCongr e).symm = FreeAddGroup.freeAddGroupCongr e.symm

theorem FreeGroup.freeGroupCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ) :

(FreeGroup.freeGroupCongr e).trans (FreeGroup.freeGroupCongr f) = FreeGroup.freeGroupCongr (e.trans f)

theorem FreeAddGroup.freeAddGroupCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ) :

(FreeAddGroup.freeAddGroupCongr e).trans (FreeAddGroup.freeAddGroupCongr f) = FreeAddGroup.freeAddGroupCongr (e.trans f)

def FreeGroup.prod {α : Type u} [Group α] :

FreeGroup α →* α

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

def FreeAddGroup.sum {α : Type u} [AddGroup α] :

FreeAddGroup α →+ α

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

@[simp]

theorem FreeGroup.prod_mk {α : Type u} {L : List (α × Bool)} [Group α] :

FreeGroup.prod (FreeGroup.mk L) = (List.map (fun (x : α × Bool) => bif x.2 then x.1 else x.1⁻¹) L).prod

@[simp]

theorem FreeAddGroup.sum_mk {α : Type u} {L : List (α × Bool)} [AddGroup α] :

FreeAddGroup.sum (FreeAddGroup.mk L) = (List.map (fun (x : α × Bool) => bif x.2 then x.1 else -x.1) L).sum

@[simp]

theorem FreeGroup.prod.of {α : Type u} [Group α] {x : α} :

FreeGroup.prod (FreeGroup.of x) = x

@[simp]

theorem FreeAddGroup.sum.of {α : Type u} [AddGroup α] {x : α} :

FreeAddGroup.sum (FreeAddGroup.of x) = 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.sum.unique {α : Type u} [AddGroup α] (g : FreeAddGroup α →+ α) (hg : ∀ (x : α), g (FreeAddGroup.of x) = x) {x : FreeAddGroup α} :

g x = FreeAddGroup.sum 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)

theorem FreeAddGroup.lift_eq_sum_map {α : Type u} {β : Type v} [AddGroup β] {f : α → β} {x : FreeAddGroup α} :

(FreeAddGroup.lift f) x = FreeAddGroup.sum ((FreeAddGroup.map f) x)

def FreeGroup.sum {α : Type u} [AddGroup α] (x : FreeGroup α) :

α

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 = FreeGroup.prod x

Instances For

@[simp]

theorem FreeGroup.sum_mk {α : Type u} {L : List (α × Bool)} [AddGroup α] :

(FreeGroup.mk L).sum = (List.map (fun (x : α × Bool) => bif x.2 then x.1 else -x.1) L).sum

@[simp]

theorem FreeGroup.sum.of {α : Type u} [AddGroup α] {x : α} :

(FreeGroup.of x).sum = x

@[simp]

theorem FreeGroup.sum.map_mul {α : Type u} [AddGroup α] {x y : FreeGroup α} :

(x * y).sum = x.sum + y.sum

@[simp]

theorem FreeGroup.sum.map_one {α : Type u} [AddGroup α] :

FreeGroup.sum 1 = 0

@[simp]

theorem FreeGroup.sum.map_inv {α : Type u} [AddGroup α] {x : FreeGroup α} :

x⁻¹.sum = -x.sum

def FreeGroup.freeGroupEmptyEquivUnit :

FreeGroup Empty ≃ Unit

The bijection between the 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

def FreeAddGroup.freeAddGroupEmptyEquivAddUnit :

FreeAddGroup Empty ≃ Unit

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

def FreeGroup.freeGroupUnitEquivInt :

FreeGroup Unit ≃ ℤ

The bijection between the free group on a singleton, and the integers.

Equations

One or more equations did not get rendered due to their size.

Instances For

instance FreeGroup.instMonad :

Monad FreeGroup

Equations

FreeGroup.instMonad = Monad.mk

instance FreeAddGroup.instMonad :

Monad FreeAddGroup

Equations

FreeAddGroup.instMonad = Monad.mk

theorem FreeGroup.induction_on {α : Type u} {C : FreeGroup α → Prop} (z : FreeGroup α) (C1 : C 1) (Cp : ∀ (x : α), C (pure x)) (Ci : ∀ (x : α), C (pure x) → C (pure x)⁻¹) (Cm : ∀ (x y : FreeGroup α), C x → C y → C (x * y)) :

C z

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

theorem FreeGroup.map_pure {α β : Type u} (f : α → β) (x : α) :

f <$> pure x = pure (f x)

theorem FreeAddGroup.map_pure {α β : Type u} (f : α → β) (x : α) :

f <$> pure x = pure (f x)

@[simp]

theorem FreeGroup.map_one {α β : Type u} (f : α → β) :

f <$> 1 = 1

@[simp]

theorem FreeAddGroup.map_zero {α β : Type u} (f : α → β) :

f <$> 0 = 0

@[simp]

theorem FreeGroup.map_mul {α β : Type u} (f : α → β) (x y : FreeGroup α) :

f <$> (x * y) = f <$> x * f <$> y

@[simp]

theorem FreeAddGroup.map_add {α β : Type u} (f : α → β) (x y : FreeAddGroup α) :

f <$> (x + y) = f <$> x + f <$> y

@[simp]

theorem FreeGroup.map_inv {α β : Type u} (f : α → β) (x : FreeGroup α) :

f <$> x⁻¹ = (f <$> x)⁻¹

@[simp]

theorem FreeAddGroup.map_neg {α β : Type u} (f : α → β) (x : FreeAddGroup α) :

f <$> (-x) = -f <$> x

theorem FreeGroup.pure_bind {α β : Type u} (f : α → FreeGroup β) (x : α) :

pure x >>= f = f x

theorem FreeAddGroup.pure_bind {α β : Type u} (f : α → FreeAddGroup β) (x : α) :

pure x >>= f = f x

@[simp]

theorem FreeGroup.one_bind {α β : Type u} (f : α → FreeGroup β) :

1 >>= f = 1

@[simp]

theorem FreeAddGroup.zero_bind {α β : Type u} (f : α → FreeAddGroup β) :

0 >>= f = 0

@[simp]

theorem FreeGroup.mul_bind {α β : Type u} (f : α → FreeGroup β) (x y : FreeGroup α) :

x * y >>= f = (x >>= f) * (y >>= f)

@[simp]

theorem FreeAddGroup.add_bind {α β : Type u} (f : α → FreeAddGroup β) (x y : FreeAddGroup α) :

x + y >>= f = (x >>= f) + (y >>= f)

@[simp]

theorem FreeGroup.inv_bind {α β : Type u} (f : α → FreeGroup β) (x : FreeGroup α) :

x⁻¹ >>= f = (x >>= f)⁻¹

@[simp]

theorem FreeAddGroup.neg_bind {α β : Type u} (f : α → FreeAddGroup β) (x : FreeAddGroup α) :

-x >>= f = -(x >>= f)

instance FreeGroup.instLawfulMonad :

LawfulMonad FreeGroup

Equations

FreeGroup.instLawfulMonad = ⋯

instance FreeAddGroup.instLawfulMonad :

LawfulMonad FreeAddGroup

Equations

FreeAddGroup.instLawfulMonad = ⋯

def FreeGroup.reduce {α : Type u} [DecidableEq α] (L : List (α × Bool)) :

List (α × Bool)

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

def FreeAddGroup.reduce {α : Type u} [DecidableEq α] (L : List (α × Bool)) :

List (α × Bool)

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 FreeGroup.reduce.cons {α : Type u} {L : List (α × Bool)} [DecidableEq α] (x : α × Bool) :

FreeGroup.reduce (x :: L) = List.casesOn (FreeGroup.reduce L) [x] fun (hd : α × Bool) (tl : List (α × Bool)) => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl

@[simp]

theorem FreeAddGroup.reduce.cons {α : Type u} {L : List (α × Bool)} [DecidableEq α] (x : α × Bool) :

FreeAddGroup.reduce (x :: L) = List.casesOn (FreeAddGroup.reduce L) [x] fun (hd : α × Bool) (tl : List (α × Bool)) => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl

@[simp]

theorem FreeGroup.reduce_replicate {α : Type u} [DecidableEq α] (n : ℕ) (x : α × Bool) :

FreeGroup.reduce (List.replicate n x) = List.replicate n x

@[simp]

theorem FreeAddGroup.reduce_replicate {α : Type u} [DecidableEq α] (n : ℕ) (x : α × Bool) :

FreeAddGroup.reduce (List.replicate n x) = List.replicate n x

theorem FreeGroup.reduce.red {α : Type u} {L : List (α × Bool)} [DecidableEq α] :

FreeGroup.Red L (FreeGroup.reduce L)

The first theorem that characterises the function reduce: a word reduces to its maximal reduction.

theorem FreeAddGroup.reduce.red {α : Type u} {L : List (α × Bool)} [DecidableEq α] :

FreeAddGroup.Red L (FreeAddGroup.reduce L)

The first theorem that characterises the function reduce: a word reduces to its maximal reduction.

theorem FreeGroup.reduce.not {α : Type u} [DecidableEq α] {p : Prop} {L₁ L₂ L₃ : List (α × Bool)} {x : α} {b : Bool} :

FreeGroup.reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p

theorem FreeAddGroup.reduce.not {α : Type u} [DecidableEq α] {p : Prop} {L₁ L₂ L₃ : List (α × Bool)} {x : α} {b : Bool} :

FreeAddGroup.reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p

theorem FreeGroup.reduce.min {α : Type u} {L₁ 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.

theorem FreeAddGroup.reduce.min {α : Type u} {L₁ 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.

@[simp]

theorem FreeGroup.reduce.idem {α : Type u} {L : List (α × Bool)} [DecidableEq α] :

FreeGroup.reduce (FreeGroup.reduce L) = FreeGroup.reduce L

reduce is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the maximal reduction of the word.

@[simp]

theorem FreeAddGroup.reduce.idem {α : Type u} {L : List (α × Bool)} [DecidableEq α] :

FreeAddGroup.reduce (FreeAddGroup.reduce L) = FreeAddGroup.reduce L

reduce is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the maximal reduction of the word.

theorem FreeGroup.reduce.Step.eq {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.Red.Step L₁ L₂) :

FreeGroup.reduce L₁ = FreeGroup.reduce L₂

theorem FreeAddGroup.reduce.Step.eq {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.Red.Step L₁ L₂) :

FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂

theorem FreeGroup.reduce.eq_of_red {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.Red L₁ L₂) :

FreeGroup.reduce L₁ = FreeGroup.reduce L₂

If a word reduces to another word, then they have a common maximal reduction.

theorem FreeAddGroup.reduce.eq_of_red {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.Red L₁ L₂) :

FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂

If a word reduces to another word, then they have a common maximal reduction.

theorem FreeGroup.red.reduce_eq {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.Red L₁ L₂) :

FreeGroup.reduce L₁ = FreeGroup.reduce 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₁ L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.Red L₁ L₂) :

FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂

Alias of FreeAddGroup.reduce.eq_of_red.

If a word reduces to another word, then they have a common maximal reduction.

theorem FreeGroup.Red.reduce_right {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : FreeGroup.Red L₁ L₂) :

FreeGroup.Red L₁ (FreeGroup.reduce L₂)

theorem FreeAddGroup.Red.reduce_right {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : FreeAddGroup.Red L₁ L₂) :

FreeAddGroup.Red L₁ (FreeAddGroup.reduce L₂)

theorem FreeGroup.Red.reduce_left {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : FreeGroup.Red L₁ L₂) :

FreeGroup.Red L₂ (FreeGroup.reduce L₁)

theorem FreeAddGroup.Red.reduce_left {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : FreeAddGroup.Red L₁ L₂) :

FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁)

theorem FreeGroup.reduce.sound {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.mk L₁ = FreeGroup.mk L₂) :

FreeGroup.reduce L₁ = FreeGroup.reduce 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.sound {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂) :

FreeAddGroup.reduce L₁ = FreeAddGroup.reduce 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 FreeGroup.reduce.exact {α : Type u} {L₁ 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.

theorem FreeAddGroup.reduce.exact {α : Type u} {L₁ 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.self {α : Type u} {L : List (α × Bool)} [DecidableEq α] :

FreeGroup.mk (FreeGroup.reduce L) = FreeGroup.mk L

A word and its maximal reduction correspond to the same element of the free group.

theorem FreeAddGroup.reduce.self {α : Type u} {L : List (α × Bool)} [DecidableEq α] :

FreeAddGroup.mk (FreeAddGroup.reduce L) = FreeAddGroup.mk L

A word and its maximal reduction correspond to the same element of the additive free group.

theorem FreeGroup.reduce.rev {α : Type u} {L₁ 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₁.

theorem FreeAddGroup.reduce.rev {α : Type u} {L₁ 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₁.

def FreeGroup.toWord {α : Type u} [DecidableEq α] :

FreeGroup α → List (α × Bool)

The function that sends an element of the free group to its maximal reduction.

Equations

FreeGroup.toWord = Quot.lift FreeGroup.reduce ⋯

Instances For

def FreeAddGroup.toWord {α : Type u} [DecidableEq α] :

FreeAddGroup α → List (α × Bool)

The function that sends an element of the additive free group to its maximal reduction.

Equations

FreeAddGroup.toWord = Quot.lift FreeAddGroup.reduce ⋯

Instances For

theorem FreeGroup.mk_toWord {α : Type u} [DecidableEq α] {x : FreeGroup α} :

FreeGroup.mk x.toWord = x

theorem FreeAddGroup.mk_toWord {α : Type u} [DecidableEq α] {x : FreeAddGroup α} :

FreeAddGroup.mk x.toWord = x

theorem FreeGroup.toWord_injective {α : Type u} [DecidableEq α] :

Function.Injective FreeGroup.toWord

theorem FreeAddGroup.toWord_injective {α : Type u} [DecidableEq α] :

Function.Injective FreeAddGroup.toWord

@[simp]

theorem FreeGroup.toWord_inj {α : Type u} [DecidableEq α] {x y : FreeGroup α} :

x.toWord = y.toWord ↔ x = y

@[simp]

theorem FreeAddGroup.toWord_inj {α : Type u} [DecidableEq α] {x y : FreeAddGroup α} :

x.toWord = y.toWord ↔ x = y

@[simp]

theorem FreeGroup.toWord_mk {α : Type u} {L₁ : List (α × Bool)} [DecidableEq α] :

(FreeGroup.mk L₁).toWord = FreeGroup.reduce L₁

@[simp]

theorem FreeAddGroup.toWord_mk {α : Type u} {L₁ : List (α × Bool)} [DecidableEq α] :

(FreeAddGroup.mk L₁).toWord = FreeAddGroup.reduce L₁

@[simp]

theorem FreeGroup.toWord_of {α : Type u} [DecidableEq α] (a : α) :

(FreeGroup.of a).toWord = [(a, true)]

@[simp]

theorem FreeAddGroup.toWord_of {α : Type u} [DecidableEq α] (a : α) :

(FreeAddGroup.of a).toWord = [(a, true)]

@[simp]

theorem FreeGroup.reduce_toWord {α : Type u} [DecidableEq α] (x : FreeGroup α) :

FreeGroup.reduce x.toWord = x.toWord

@[simp]

theorem FreeAddGroup.reduce_toWord {α : Type u} [DecidableEq α] (x : FreeAddGroup α) :

FreeAddGroup.reduce x.toWord = x.toWord

@[simp]

theorem FreeGroup.toWord_one {α : Type u} [DecidableEq α] :

FreeGroup.toWord 1 = []

@[simp]

theorem FreeAddGroup.toWord_zero {α : Type u} [DecidableEq α] :

FreeAddGroup.toWord 0 = []

@[simp]

theorem FreeGroup.toWord_of_pow {α : Type u} [DecidableEq α] (a : α) (n : ℕ) :

(FreeGroup.of a ^ n).toWord = List.replicate n (a, true)

@[simp]

theorem FreeAddGroup.toWord_of_nsmul {α : Type u} [DecidableEq α] (a : α) (n : ℕ) :

(n • FreeAddGroup.of a).toWord = List.replicate n (a, true)

@[simp]

theorem FreeGroup.toWord_eq_nil_iff {α : Type u} [DecidableEq α] {x : FreeGroup α} :

x.toWord = [] ↔ x = 1

@[simp]

theorem FreeAddGroup.toWord_eq_nil_iff {α : Type u} [DecidableEq α] {x : FreeAddGroup α} :

x.toWord = [] ↔ x = 0

theorem FreeGroup.reduce_invRev {α : Type u} [DecidableEq α] {w : List (α × Bool)} :

FreeGroup.reduce (FreeGroup.invRev w) = FreeGroup.invRev (FreeGroup.reduce w)

theorem FreeAddGroup.reduce_negRev {α : Type u} [DecidableEq α] {w : List (α × Bool)} :

FreeAddGroup.reduce (FreeAddGroup.negRev w) = FreeAddGroup.negRev (FreeAddGroup.reduce w)

theorem FreeGroup.toWord_inv {α : Type u} [DecidableEq α] {x : FreeGroup α} :

x⁻¹.toWord = FreeGroup.invRev x.toWord

theorem FreeAddGroup.toWord_neg {α : Type u} [DecidableEq α] {x : FreeAddGroup α} :

(-x).toWord = FreeAddGroup.negRev x.toWord

def FreeGroup.reduce.churchRosser {α : Type u} {L₁ L₂ 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 = ⟨FreeGroup.reduce L₁, ⋯⟩

Instances For

def FreeAddGroup.reduce.churchRosser {α : Type u} {L₁ L₂ 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 = ⟨FreeAddGroup.reduce L₁, ⋯⟩

Instances For

instance FreeGroup.instDecidableEq {α : Type u} [DecidableEq α] :

DecidableEq (FreeGroup α)

Equations

FreeGroup.instDecidableEq = ⋯.decidableEq

instance FreeAddGroup.instDecidableEq {α : Type u} [DecidableEq α] :

DecidableEq (FreeAddGroup α)

Equations

FreeAddGroup.instDecidableEq = ⋯.decidableEq

instance FreeGroup.Red.decidableRel {α : Type u} [DecidableEq α] :

DecidableRel FreeGroup.Red

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 ⋯

def FreeGroup.Red.enum {α : Type u} [DecidableEq α] (L₁ : List (α × Bool)) :

List (List (α × Bool))

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)) L₁.sublists

Instances For

theorem FreeGroup.Red.enum.sound {α : Type u} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : L₂ ∈ List.filter (fun (b : List (α × Bool)) => decide (FreeGroup.Red L₁ b)) L₁.sublists) :

FreeGroup.Red L₁ L₂

theorem FreeGroup.Red.enum.complete {α : Type u} {L₁ 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 (FreeGroup.Red.enum L₁).toFinset ⋯

@[simp]

theorem FreeGroup.one_ne_of {α : Type u} (a : α) :

1 ≠ FreeGroup.of a

@[simp]

theorem FreeAddGroup.zero_ne_of {α : Type u} (a : α) :

0 ≠ FreeAddGroup.of a

@[simp]

theorem FreeGroup.of_ne_one {α : Type u} (a : α) :

FreeGroup.of a ≠ 1

@[simp]

theorem FreeAddGroup.of_ne_zero {α : Type u} (a : α) :

FreeAddGroup.of a ≠ 0

instance FreeGroup.instNontrivialOfNonempty {α : Type u} [Nonempty α] :

Nontrivial (FreeGroup α)

Equations

⋯ = ⋯

instance FreeAddGroup.instNontrivialOfNonempty {α : Type u} [Nonempty α] :

Nontrivial (FreeAddGroup α)

Equations

⋯ = ⋯

def FreeGroup.norm {α : Type u} [DecidableEq α] (x : FreeGroup α) :

The length of reduced words provides a norm on a free group.

Equations

x.norm = x.toWord.length

Instances For

def FreeAddGroup.norm {α : Type u} [DecidableEq α] (x : FreeAddGroup α) :

The length of reduced words provides a norm on an additive free group.

Equations

x.norm = x.toWord.length

Instances For

@[simp]

theorem FreeGroup.norm_inv_eq {α : Type u} [DecidableEq α] {x : FreeGroup α} :

x⁻¹.norm = x.norm

@[simp]

theorem FreeAddGroup.norm_neg_eq {α : Type u} [DecidableEq α] {x : FreeAddGroup α} :

(-x).norm = x.norm

@[simp]

theorem FreeGroup.norm_eq_zero {α : Type u} [DecidableEq α] {x : FreeGroup α} :

x.norm = 0 ↔ x = 1

@[simp]

theorem FreeAddGroup.norm_eq_zero {α : Type u} [DecidableEq α] {x : FreeAddGroup α} :

x.norm = 0 ↔ x = 0

@[simp]

theorem FreeGroup.norm_one {α : Type u} [DecidableEq α] :

FreeGroup.norm 1 = 0

@[simp]

theorem FreeAddGroup.norm_zero {α : Type u} [DecidableEq α] :

FreeAddGroup.norm 0 = 0

@[simp]

theorem FreeGroup.norm_of {α : Type u} [DecidableEq α] (a : α) :

(FreeGroup.of a).norm = 1

@[simp]

theorem FreeAddGroup.norm_of {α : Type u} [DecidableEq α] (a : α) :

(FreeAddGroup.of a).norm = 1

theorem FreeGroup.norm_mk_le {α : Type u} {L₁ : List (α × Bool)} [DecidableEq α] :

(FreeGroup.mk L₁).norm ≤ L₁.length

theorem FreeAddGroup.norm_mk_le {α : Type u} {L₁ : List (α × Bool)} [DecidableEq α] :

(FreeAddGroup.mk L₁).norm ≤ L₁.length

theorem FreeGroup.norm_mul_le {α : Type u} [DecidableEq α] (x y : FreeGroup α) :

(x * y).norm ≤ x.norm + y.norm

theorem FreeAddGroup.norm_add_le {α : Type u} [DecidableEq α] (x y : FreeAddGroup α) :

(x + y).norm ≤ x.norm + y.norm

@[simp]

theorem FreeGroup.norm_of_pow {α : Type u} [DecidableEq α] (a : α) (n : ℕ) :

(FreeGroup.of a ^ n).norm = n

@[simp]

theorem FreeAddGroup.norm_of_nsmul {α : Type u} [DecidableEq α] (a : α) (n : ℕ) :

(n • FreeAddGroup.of a).norm = n

theorem FreeGroup.norm_surjective {α : Type u} [DecidableEq α] [Nonempty α] :

Function.Surjective FreeGroup.norm

theorem FreeAddGroup.norm_surjective {α : Type u} [DecidableEq α] [Nonempty α] :

Function.Surjective FreeAddGroup.norm