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 Mathlib/Algebra/Category/Grp/Adjunctions.lean.

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} : Step (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁ ++ L₂)

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} : Step (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁ ++ L₂)

def FreeGroup.Red {α : Type u} : List (α × Bool) → List (α × Bool) → Prop

Reflexive-transitive closure of Red.Step

def FreeAddGroup.Red {α : Type u} : List (α × Bool) → List (α × Bool) → Prop

Reflexive-transitive closure of Red.Step

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

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

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

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

theorem FreeGroup.Red.Step.length {α : Type u} {L₁ L₂ : List (α × Bool)} : 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)} : 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} : 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} : Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

theorem FreeGroup.Red.Step.cons_left_iff {α : Type u} {L₁ L₂ : List (α × Bool)} {a : α} {b : Bool} : Step ((a, b) :: L₁) L₂ ↔ (∃ (L : List (α × Bool)), 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} : Step ((a, b) :: L₁) L₂ ↔ (∃ (L : List (α × Bool)), Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

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

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

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

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

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

theorem FreeAddGroup.Red.Step.append_left_iff {α : Type u} {L₁ L₂ : List (α × Bool)} (L : List (α × Bool)) : Step (L ++ L₁) (L ++ L₂) ↔ 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)), Step (L₁ ++ L₂) L₅ ∧ 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)), Step (L₁ ++ L₂) L₅ ∧ Step (L₃ ++ L₄) L₅

theorem FreeGroup.Red.Step.diamond {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)} : Step L₁ L₃ → Step L₂ L₄ → L₁ = L₂ → L₃ = L₄ ∨ ∃ (L₅ : List (α × Bool)), Step L₃ L₅ ∧ Step L₄ L₅

theorem FreeAddGroup.Red.Step.diamond {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)} : Step L₁ L₃ → Step L₂ L₄ → L₁ = L₂ → L₃ = L₄ ∨ ∃ (L₅ : List (α × Bool)), Step L₃ L₅ ∧ Step L₄ L₅

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

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

theorem FreeGroup.Red.church_rosser {α : Type u} {L₁ L₂ L₃ : List (α × Bool)} : Red L₁ L₂ → Red L₁ L₃ → Relation.Join 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)} : Red L₁ L₂ → Red L₁ L₃ → Relation.Join 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} : Red L₁ L₂ → Red (p :: L₁) (p :: L₂)

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

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

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

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

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

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

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

theorem FreeGroup.Red.to_append_iff {α : Type u} {L L₁ L₂ : List (α × Bool)} : Red L (L₁ ++ L₂) ↔ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

theorem FreeAddGroup.Red.to_append_iff {α : Type u} {L L₁ L₂ : List (α × Bool)} : Red L (L₁ ++ L₂) ↔ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

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

The empty word [] only reduces to itself.

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

The empty word [] only reduces to itself.

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

A letter only reduces to itself.

theorem FreeAddGroup.Red.singleton_iff {α : Type u} {L₁ : List (α × Bool)} {x : α × Bool} : 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} : Red ((x, b) :: L) [] ↔ 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} : Red ((x, b) :: L) [] ↔ 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)) : Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]

theorem FreeAddGroup.Red.red_iff_addIrreducible {α : Type u} {L : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} (h : (x1, b1) ≠ (x2, b2)) : 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 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) : 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 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) : 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 : Step L₁ L₂) : L₂.Sublist L₁

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

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

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

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

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

theorem FreeGroup.Red.length {α : Type u} {L₁ L₂ : List (α × Bool)} (h : Red L₁ L₂) : ∃ (n : ℕ), L₁.length = L₂.length + 2 * n

theorem FreeAddGroup.Red.length {α : Type u} {L₁ L₂ : List (α × Bool)} (h : Red L₁ L₂) : ∃ (n : ℕ), L₁.length = L₂.length + 2 * n

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

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

theorem FreeGroup.equivalence_join_red {α : Type u} : Equivalence (Relation.Join Red)

theorem FreeAddGroup.equivalence_join_red {α : Type u} : Equivalence (Relation.Join Red)

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

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

theorem FreeGroup.eqvGen_step_iff_join_red {α : Type u} {L₁ L₂ : List (α × Bool)} : Relation.EqvGen Red.Step L₁ L₂ ↔ Relation.Join Red L₁ L₂

theorem FreeAddGroup.eqvGen_step_iff_join_red {α : Type u} {L₁ L₂ : List (α × Bool)} : Relation.EqvGen Red.Step L₁ L₂ ↔ Relation.Join Red L₁ L₂

Reduced words

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

Predicate asserting that the word L admits no reduction steps, i.e., no two neighboring elements of the word cancel.

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

Predicate asserting the word L admits no reduction steps, i.e., no two neighboring elements of the word cancel.

@[simp]

theorem FreeGroup.IsReduced.nil {α : Type u} : IsReduced []

@[simp]

theorem FreeAddGroup.IsReduced.nil {α : Type u} : IsReduced []

@[simp]

theorem FreeGroup.IsReduced.singleton {α : Type u} {a : α × Bool} : IsReduced [a]

@[simp]

theorem FreeAddGroup.IsReduced.singleton {α : Type u} {a : α × Bool} : IsReduced [a]

@[simp]

theorem FreeGroup.isReduced_cons_cons {α : Type u} {L : List (α × Bool)} {a b : α × Bool} : IsReduced (a :: b :: L) ↔ (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: L)

@[simp]

theorem FreeAddGroup.isReduced_cons_cons {α : Type u} {L : List (α × Bool)} {a b : α × Bool} : IsReduced (a :: b :: L) ↔ (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: L)

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

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

theorem FreeGroup.IsReduced.of_forall_not_step {α : Type u} {L₁ : List (α × Bool)} : (∀ (L₂ : List (α × Bool)), ¬Red.Step L₁ L₂) → IsReduced L₁

theorem FreeAddGroup.IsReduced.of_forall_not_step {α : Type u} {L₁ : List (α × Bool)} : (∀ (L₂ : List (α × Bool)), ¬Red.Step L₁ L₂) → IsReduced L₁

theorem FreeGroup.isReduced_iff_not_step {α : Type u} {L₁ : List (α × Bool)} : IsReduced L₁ ↔ ∀ (L₂ : List (α × Bool)), ¬Red.Step L₁ L₂

theorem FreeAddGroup.isReduced_iff_not_step {α : Type u} {L₁ : List (α × Bool)} : IsReduced L₁ ↔ ∀ (L₂ : List (α × Bool)), ¬Red.Step L₁ L₂

theorem FreeGroup.IsReduced.red_iff_eq {α : Type u} {L₁ L₂ : List (α × Bool)} (h : IsReduced L₁) : Red L₁ L₂ ↔ L₂ = L₁

theorem FreeAddGroup.IsReduced.red_iff_eq {α : Type u} {L₁ L₂ : List (α × Bool)} (h : IsReduced L₁) : Red L₁ L₂ ↔ L₂ = L₁

theorem FreeGroup.IsReduced.append_overlap {α : Type u} {L₁ L₂ L₃ : List (α × Bool)} (h₁ : IsReduced (L₁ ++ L₂)) (h₂ : IsReduced (L₂ ++ L₃)) (hn : L₂ ≠ []) : IsReduced (L₁ ++ L₂ ++ L₃)

theorem FreeAddGroup.IsReduced.append_overlap {α : Type u} {L₁ L₂ L₃ : List (α × Bool)} (h₁ : IsReduced (L₁ ++ L₂)) (h₂ : IsReduced (L₂ ++ L₃)) (hn : L₂ ≠ []) : IsReduced (L₁ ++ L₂ ++ L₃)

theorem FreeGroup.IsReduced.infix {α : Type u} {L₁ L₂ : List (α × Bool)} (h : IsReduced L₂) (h' : L₁ <:+: L₂) : IsReduced L₁

theorem FreeAddGroup.IsReduced.infix {α : Type u} {L₁ L₂ : List (α × Bool)} (h : IsReduced L₂) (h' : L₁ <:+: L₂) : IsReduced L₁

def FreeGroup (α : Type u) : Type u

If α is a type, then FreeGroup α is the free group generated by α. This is a group equipped with a function FreeGroup.of : α → FreeGroup α which has the following universal property: if G is any group, and f : α → G is any function, then this function is the composite of FreeGroup.of and a unique group homomorphism FreeGroup.lift f : FreeGroup α →* G.

A typical element of FreeGroup α is a formal product of elements of α and their formal inverses, quotient by reduction. For example if x and y are terms of type α then x⁻¹ * y * y * x * y⁻¹ is a "typical" element of FreeGroup α. In particular if α is empty then FreeGroup α is isomorphic to the trivial group, and if α has one term then FreeGroup α is isomorphic to Multiplicative ℤ. If α has two or more terms then FreeGroup α is not commutative.

def FreeAddGroup (α : Type u) : Type u

If α is a type, then FreeAddGroup α is the free additive group generated by α. This is a group equipped with a function FreeAddGroup.of : α → FreeAddGroup α which has the following universal property: if G is any group, and f : α → G is any function, then this function is the composite of FreeAddGroup.of and a unique group homomorphism FreeAddGroup.lift f : FreeAddGroup α →+ G.

A typical element of FreeAddGroup α is a formal sum of elements of α and their formal inverses, quotient by reduction. For example if x and y are terms of type α then -x + y + y + x + -y is a "typical" element of FreeAddGroup α. In particular if α is empty then FreeAddGroup α is isomorphic to the trivial group, and if α has one term then FreeAddGroup α is isomorphic to ℤ. If α has two or more terms then FreeAddGroup α is not commutative.

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

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

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

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

@[simp]

theorem FreeGroup.quot_mk_eq_mk {α : Type u} {L : List (α × Bool)} : Quot.mk Red.Step L = mk L

@[simp]

theorem FreeAddGroup.quot_mk_eq_mk {α : Type u} {L : List (α × Bool)} : Quot.mk Red.Step L = mk L

@[simp]

theorem FreeGroup.quot_lift_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → β) (H : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → f L₁ = f L₂) : Quot.lift f H (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)), Red.Step L₁ L₂ → f L₁ = f L₂) : Quot.lift f H (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)), Red.Step L₁ L₂ → f L₁ = f L₂) : Quot.liftOn (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)), Red.Step L₁ L₂ → f L₁ = f L₂) : Quot.liftOn (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 : Relator.LiftFun Red.Step Red.Step f f) : Quot.map f H (mk L) = mk (f L)

@[simp]

theorem FreeAddGroup.quot_map_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → List (β × Bool)) (H : Relator.LiftFun Red.Step Red.Step f f) : Quot.map f H (mk L) = mk (f L)

@[implicit_reducible]

instance FreeGroup.instOne {α : Type u} : One (FreeGroup α)

@[implicit_reducible]

instance FreeAddGroup.instZero {α : Type u} : Zero (FreeAddGroup α)

theorem FreeGroup.one_eq_mk {α : Type u} : 1 = mk []

theorem FreeAddGroup.zero_eq_mk {α : Type u} : 0 = mk []

@[implicit_reducible]

instance FreeGroup.instInhabited {α : Type u} : Inhabited (FreeGroup α)

@[implicit_reducible]

instance FreeAddGroup.instInhabited {α : Type u} : Inhabited (FreeAddGroup α)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance FreeGroup.instMul {α : Type u} : Mul (FreeGroup α)

@[implicit_reducible]

instance FreeAddGroup.instAdd {α : Type u} : Add (FreeAddGroup α)

@[simp]

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

@[simp]

theorem FreeAddGroup.add_mk {α : Type u} {L₁ L₂ : List (α × Bool)} : mk L₁ + mk L₂ = 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.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FreeGroup.invRev_empty {α : Type u} : invRev [] = []

@[simp]

theorem FreeAddGroup.negRev_empty {α : Type u} : negRev [] = []

@[simp]

theorem FreeGroup.invRev_append {α : Type u} {L₁ L₂ : List (α × Bool)} : invRev (L₁ ++ L₂) = invRev L₂ ++ invRev L₁

@[simp]

theorem FreeAddGroup.negRev_append {α : Type u} {L₁ L₂ : List (α × Bool)} : negRev (L₁ ++ L₂) = negRev L₂ ++ negRev L₁

theorem FreeGroup.invRev_cons {α : Type u} {L : List (α × Bool)} {a : α × Bool} : invRev (a :: L) = invRev L ++ invRev [a]

theorem FreeAddGroup.negRev_cons {α : Type u} {L : List (α × Bool)} {a : α × Bool} : negRev (a :: L) = negRev L ++ negRev [a]

theorem FreeGroup.invRev_involutive {α : Type u} : Function.Involutive invRev

theorem FreeAddGroup.negRev_involutive {α : Type u} : Function.Involutive negRev

theorem FreeGroup.invRev_injective {α : Type u} : Function.Injective invRev

theorem FreeAddGroup.negRev_injective {α : Type u} : Function.Injective negRev

theorem FreeGroup.invRev_surjective {α : Type u} : Function.Surjective invRev

theorem FreeAddGroup.negRev_surjective {α : Type u} : Function.Surjective negRev

theorem FreeGroup.invRev_bijective {α : Type u} : Function.Bijective invRev

theorem FreeAddGroup.negRev_bijective {α : Type u} : Function.Bijective negRev

@[implicit_reducible]

instance FreeGroup.instInv {α : Type u} : Inv (FreeGroup α)

@[implicit_reducible]

instance FreeAddGroup.instNeg {α : Type u} : Neg (FreeAddGroup α)

@[simp]

theorem FreeGroup.inv_mk {α : Type u} {L : List (α × Bool)} : (mk L)⁻¹ = mk (invRev L)

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

instance FreeGroup.instGroup {α : Type u} : Group (FreeGroup α)

@[implicit_reducible]

instance FreeAddGroup.instAddGroup {α : Type u} : AddGroup (FreeAddGroup α)

@[simp]

theorem FreeGroup.pow_mk {α : Type u} {L : List (α × Bool)} (n : ℕ) : mk L ^ n = mk (List.replicate n L).flatten

@[simp]

theorem FreeAddGroup.nsmul_mk {α : Type u} {L : List (α × Bool)} (n : ℕ) : n • mk L = mk (List.replicate n L).flatten

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

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.

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.

theorem FreeGroup.induction_on {α : Type u} {C : FreeGroup α → Prop} (z : FreeGroup α) (C1 : C 1) (of : ∀ (x : α), C (of x)) (inv_of : ∀ (x : α), C (FreeGroup.of x) → C (FreeGroup.of x)⁻¹) (mul : ∀ (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) (of : ∀ (x : α), C (of x)) (neg_of : ∀ (x : α), C (FreeAddGroup.of x) → C (-FreeAddGroup.of x)) (add : ∀ (x y : FreeAddGroup α), C x → C y → C (x + y)) : C z

theorem FreeGroup.ext_hom {α : Type u} {M : Type u_1} [Monoid M] (f g : FreeGroup α →* M) (h : ∀ (a : α), f (of a) = g (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.ext_hom {α : Type u} {M : Type u_1} [AddMonoid M] (f g : FreeAddGroup α →+ M) (h : ∀ (a : α), f (of a) = g (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_iff {α : Type u} {M : Type u_1} [Monoid M] {f g : FreeGroup α →* M} : f = g ↔ ∀ (a : α), f (of a) = g (of a)

theorem FreeAddGroup.ext_hom_iff {α : Type u} {M : Type u_1} [AddMonoid M] {f g : FreeAddGroup α →+ M} : f = g ↔ ∀ (a : α), f (of a) = g (of a)

theorem FreeGroup.Red.exact {α : Type u} {L₁ L₂ : List (α × Bool)} : mk L₁ = mk L₂ ↔ Relation.Join Red L₁ L₂

theorem FreeAddGroup.Red.exact {α : Type u} {L₁ L₂ : List (α × Bool)} : mk L₁ = mk L₂ ↔ Relation.Join Red L₁ L₂

theorem FreeGroup.of_injective {α : Type u} : Function.Injective of

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

theorem FreeAddGroup.of_injective {α : Type u} : Function.Injective 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) → β

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

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

theorem FreeGroup.Red.Step.lift {α : Type u} {L₁ L₂ : List (α × Bool)} {β : Type v} [Group β] {f : α → β} (H : Step L₁ L₂) : Lift.aux f L₁ = Lift.aux f L₂

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

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 β

@[simp]

theorem FreeAddGroup.lift_symm_apply {α : Type u} {β : Type v} [AddGroup β] (g : FreeAddGroup α →+ β) (a✝ : α) : lift.symm g a✝ = (⇑g ∘ of) a✝

@[simp]

theorem FreeGroup.lift_symm_apply {α : Type u} {β : Type v} [Group β] (g : FreeGroup α →* β) (a✝ : α) : lift.symm g a✝ = (⇑g ∘ of) a✝

@[simp]

theorem FreeGroup.lift_mk {α : Type u} {L : List (α × Bool)} {β : Type v} [Group β] {f : α → β} : (lift f) (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 : α → β} : (lift f) (mk L) = (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) L).sum

@[simp]

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

@[simp]

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

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

theorem FreeAddGroup.lift_unique {α : Type u} {β : Type v} [AddGroup β] {f : α → β} (g : FreeAddGroup α →+ β) (hg : ∀ (x : α), g (of x) = f x) {x : FreeAddGroup α} : g x = (lift f) x

theorem FreeGroup.lift_of_eq_id (α : Type u_1) : lift of = MonoidHom.id (FreeGroup α)

theorem FreeAddGroup.lift_of_eq_id (α : Type u_1) : lift of = AddMonoidHom.id (FreeAddGroup α)

theorem FreeGroup.lift_of_apply {α : Type u} (x : FreeGroup α) : (lift of) x = x

theorem FreeAddGroup.lift_of_apply {α : Type u} (x : FreeAddGroup α) : (lift of) x = x

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

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

theorem FreeGroup.range_lift_eq_closure {α : Type u} {β : Type v} [Group β] {f : α → β} : (lift f).range = Subgroup.closure (Set.range f)

theorem FreeAddGroup.range_lift_eq_closure {α : Type u} {β : Type v} [AddGroup β] {f : α → β} : (lift f).range = AddSubgroup.closure (Set.range f)

theorem FreeGroup.closure_eq_range {β : Type v} [Group β] (s : Set β) : Subgroup.closure s = (lift Subtype.val).range

theorem FreeAddGroup.closure_eq_range {β : Type v} [AddGroup β] (s : Set β) : AddSubgroup.closure s = (lift Subtype.val).range

@[simp]

theorem FreeGroup.closure_range_of (α : Type u_1) : Subgroup.closure (Set.range 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 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 β.

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

@[simp]

theorem FreeGroup.map.mk {α : Type u} {L : List (α × Bool)} {β : Type v} {f : α → β} : (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 : α → β} : (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 α) : (map _root_.id) x = x

@[simp]

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

@[simp]

theorem FreeGroup.map.id' {α : Type u} (x : FreeGroup α) : (map fun (z : α) => z) x = x

@[simp]

theorem FreeAddGroup.map.id' {α : Type u} (x : FreeAddGroup α) : (map fun (z : α) => z) x = x

theorem FreeGroup.map.comp {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (x : FreeGroup α) : (map g) ((map f) x) = (map (g ∘ f)) x

theorem FreeAddGroup.map.comp {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (x : FreeAddGroup α) : (map g) ((map f) x) = (map (g ∘ f)) x

@[simp]

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

@[simp]

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

theorem FreeGroup.map_eq_lift {α : Type u} {β : Type v} {f : α → β} : map f = lift (of ∘ f)

theorem FreeAddGroup.map_eq_lift {α : Type u} {β : Type v} {f : α → β} : map f = lift (of ∘ f)

theorem FreeGroup.range_map {α : Type u} {β : Type v} {f : α → β} : (map f).range = Subgroup.closure (of '' Set.range f)

theorem FreeAddGroup.range_map {α : Type u} {β : Type v} {f : α → β} : (map f).range = AddSubgroup.closure (of '' Set.range f)

theorem FreeGroup.map_surjective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Surjective f) : Function.Surjective ⇑(map f)

If α and β are arbitrary types and there is a surjection between them, then the induced map on their free groups is also surjective.

theorem FreeAddGroup.map_surjective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Surjective f) : Function.Surjective ⇑(map f)

If α and β are arbitrary types and there is a surjection between them, then the induced map on their additive free groups is also surjective.

theorem FreeGroup.map_injective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Injective f) : Function.Injective ⇑(map f)

If α and β are arbitrary types and there is an injection between them, then the induced map on their free groups is also injective.

theorem FreeAddGroup.map_injective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Injective f) : Function.Injective ⇑(map f)

If α and β are arbitrary types and there is an injection between them, then the induced map on their additive free groups is also injective.

theorem FreeGroup.map_bijective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Bijective f) : Function.Bijective ⇑(map f)

If α and β are arbitrary types and there is a bijection between them, then the induced map on their free groups is also bijective.

theorem FreeAddGroup.map_bijective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Bijective f) : Function.Bijective ⇑(map f)

If α and β are arbitrary types and there is a bijection between them, then the induced map on their additive free groups is also bijective.

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 Mathlib/GroupTheory/FreeGroup/GeneratorEquiv.lean, as Equiv.ofFreeGroupEquiv.

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

Equivalent types give rise to additively equivalent additive free groups.

@[simp]

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

@[simp]

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

@[simp]

theorem FreeGroup.freeGroupCongr_refl {α : Type u} : freeGroupCongr (Equiv.refl α) = MulEquiv.refl (FreeGroup α)

@[simp]

theorem FreeAddGroup.freeAddGroupCongr_refl {α : Type u} : freeAddGroupCongr (Equiv.refl α) = AddEquiv.refl (FreeAddGroup α)

@[simp]

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

@[simp]

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

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

theorem FreeAddGroup.freeAddGroupCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ) : (freeAddGroupCongr e).trans (freeAddGroupCongr f) = 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.

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

@[simp]

theorem FreeGroup.prod_mk {α : Type u} {L : List (α × Bool)} [Group α] : prod (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 α] : sum (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 : α} : prod (FreeGroup.of x) = x

@[simp]

theorem FreeAddGroup.sum.of {α : Type u} [AddGroup α] {x : α} : 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 = prod x

theorem FreeAddGroup.sum.unique {α : Type u} [AddGroup α] (g : FreeAddGroup α →+ α) (hg : ∀ (x : α), g (FreeAddGroup.of x) = x) {x : FreeAddGroup α} : g x = sum x

theorem FreeGroup.lift_eq_prod_map {α : Type u} {β : Type v} [Group β] {f : α → β} {x : FreeGroup α} : (lift f) x = prod ((map f) x)

theorem FreeAddGroup.lift_eq_sum_map {α : Type u} {β : Type v} [AddGroup β] {f : α → β} {x : FreeAddGroup α} : (lift f) x = sum ((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.

@[simp]

theorem FreeGroup.sum_mk {α : Type u} {L : List (α × Bool)} [AddGroup α] : (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 α] : sum 1 = 0

@[simp]

theorem FreeGroup.sum.map_inv {α : Type u} [AddGroup α] {x : FreeGroup α} : x⁻¹.sum = -x.sum

@[reducible, inline, deprecated "Use `Equiv.ofUnique (FreeGroup Empty) Unit` instead, or `MulEquiv.ofUnique (FreeGroup Empty) Unit` for the multiplicative version instead." (since := "2026-02-11")]

abbrev FreeGroup.freeGroupEmptyEquivUnit : FreeGroup Empty ≃ Unit

The bijection between the free group on the empty type, and a type with one element.

@[reducible, inline, deprecated "Use `Equiv.ofUnique (FreeGroup Empty) Unit` instead, or `MulEquiv.ofUnique (FreeGroup Empty) Unit` for the multiplicative version instead." (since := "2026-02-11")]

abbrev FreeAddGroup.freeAddGroupEmptyEquivAddUnit : FreeAddGroup Empty ≃ Unit

The bijection between the additive free group on the empty type, and a type with one element.

def FreeGroup.freeGroupUnitEquivInt : FreeGroup Unit ≃ ℤ

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

def FreeGroup.equivIntOfUnique {α : Type u} [Unique α] : FreeGroup α ≃ ℤ

The bijection between the free group on a unique type and the integers.

def FreeGroup.mulEquivIntOfUnique {α : Type u} [Unique α] : FreeGroup α ≃* Multiplicative ℤ

The isomorphism between the free group on a unique type and the integers.

instance FreeGroup.instIsCyclicOfUnique {α : Type u} [Unique α] : IsCyclic (FreeGroup α)

A free group over one generator is an instance of a cyclic group.

def FreeAddGroup.addEquivIntOfUnique {α : Type u} [Unique α] : FreeAddGroup α ≃+ ℤ

The isomorphism between the free additive group on a unique type and the integers.

instance FreeGroup.instIsAddCyclicFreeAddGroupOfUnique {α : Type u} [Unique α] : IsAddCyclic (FreeAddGroup α)

A free additive group over one generator is an instance of a cyclic group.

@[implicit_reducible]

instance FreeGroup.instMonad : Monad FreeGroup

@[implicit_reducible]

instance FreeAddGroup.instMonad : Monad FreeAddGroup

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

instance FreeAddGroup.instLawfulMonad : LawfulMonad FreeAddGroup