Free groups

The definition of a free group on a basis, along with a few properties.

Free groups are defined constructively to allow automatic equality checking of homomorphisms on finitely generated free groups.

Overview

• AddFreeGroup - the main definition.
• decideHomsEqual - the crucial result that allows the automatic comparison of homomorphisms by checking their values on the basis.
• ℤFree - a proof that the additive group of integers is a free group on the one-element type.
• prodFree - a proof that the product of free groups is free.

ink

class AddFreeGroup (F : Type u_1) [inst : AddCommGroup F] (X : Type u_2) : Type (max(max1u_1)u_2)

• The inclusion map from the basis to the free group.

  ι : X → F

• The homomorphism from the free group induced by a map from the basis.

  inducedHom : (A : Type) → [inst : AddCommGroup A] → (X → A) → F →+ A

• A proof that the induced homomorphism extends the map from the basis.

  induced_extends : ∀ {A : Type} [inst : AddCommGroup A] (f : X → A), ↑(inducedHom A inst f) ∘ ι = f

• A proof that any homomorphism extending a map from the basis must be unique.

  unique_extension : ∀ {A : Type} [inst : AddCommGroup A] (f g : F →+ A), ↑f ∘ ι = ↑g ∘ ι → f = g

Free (Additive) Groups, implemented as a typeclass. A free additive group with a basis X is an additive group F with an inclusion map ι : X → F, such that any map f : X → A from the basis to any Abelian group A extends uniquely to an additive group homomorphism φ : F →+ A.

ink

instance ℤFree : AddFreeGroup ℤ Unit

The additive group of integers ℤ is the free group on a singleton basis.

Equations

• ℤFree = { ι := fun x => 1, inducedHom := fun A x f => Equiv.toFun (zmultiplesHom A) (f ()), induced_extends := @ℤFree.proof_1, unique_extension := @ℤFree.proof_2 }

ink

instance decideHomsEqual {F : Type u_1} [inst : AddCommGroup F] {X : Type u_2} [inst : EnumDecide.DecideForall X] [fgp : AddFreeGroup F X] {A : Type} [inst : AddCommGroup A] [inst : DecidableEq A] : DecidableEq (F →+ A)

Equality of homomorphisms from a free group on an exhaustively searchable basis is decidable.

Equations

• decideHomsEqual f g = if c : ∀ (x : X), ↑f (AddFreeGroup.ι x) = ↑g (AddFreeGroup.ι x) then isTrue (_ : f = g) else isFalse (_ : f = g → False)

ink

def AddFreeGroup.Product.ι {A : Type u_1} {B : Type u_2} [inst : AddCommGroup A] [inst : AddCommGroup B] {X_A : Type u_3} {X_B : Type u_4} [FAb_A : AddFreeGroup A X_A] [FAb_B : AddFreeGroup B X_B] : X_A ⊕ X_B → A × B

The inclusion map from the direct sum of the bases of two free groups into their product.

Equations

• AddFreeGroup.Product.ι x = match x with | Sum.inl x_a => (AddFreeGroup.ι x_a, 0) | Sum.inr x_b => (0, AddFreeGroup.ι x_b)

ink

def AddFreeGroup.Product.inducedProdHom {A : Type u_1} {B : Type u_2} [inst : AddCommGroup A] [inst : AddCommGroup B] {X_A : Type u_3} {X_B : Type u_4} [FAb_A : AddFreeGroup A X_A] [FAb_B : AddFreeGroup B X_B] (G : Type) [inst : AddCommGroup G] (f : X_A ⊕ X_B → G) : A × B →+ G

The group homomorphism from the product of two free groups induced by a map from the basis.

Equations

• AddFreeGroup.Product.inducedProdHom G f = let f_A := f ∘ Sum.inl; let f_B := f ∘ Sum.inr; AddMonoidHom.coprod (AddFreeGroup.inducedHom G f_A) (AddFreeGroup.inducedHom G f_B)

ink

instance AddFreeGroup.Product.prodFree {A : Type u_1} {B : Type u_2} [inst : AddCommGroup A] [inst : AddCommGroup B] {X_A : Type u_3} {X_B : Type u_4} [FAb_A : AddFreeGroup A X_A] [FAb_B : AddFreeGroup B X_B] : AddFreeGroup (A × B) (X_A ⊕ X_B)

The product of free groups is free.

Equations

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