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.

class LeanPool.Polylean.AddFreeGroup (F : Type u_1) [AddCommGroup F] (X : Type u_2) : Type (max (max 1 u_1) u_2)

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.

• ι : X → F

  The inclusion map from the basis to the free group.

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

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

• induced_extends {A : Type} [AddCommGroup A] (f : X → A) : ⇑(inducedHom A f) ∘ ι = f

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

• unique_extension {A : Type} [AddCommGroup A] (f g : F →+ A) : ⇑f ∘ ι = ⇑g ∘ ι → f = g

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

@[implicit_reducible]

instance LeanPool.Polylean.ℤFree : AddFreeGroup ℤ Unit

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

Equations

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

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

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

Equations

• LeanPool.Polylean.decideHomsEqual f g = if c : ∀ (x : X), f (LeanPool.Polylean.AddFreeGroup.ι x) = g (LeanPool.Polylean.AddFreeGroup.ι x) then isTrue ⋯ else isFalse ⋯

def LeanPool.Polylean.AddFreeGroup.Product.ι {A : Type u_1} {B : Type u_2} [AddCommGroup A] [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

• LeanPool.Polylean.AddFreeGroup.Product.ι (Sum.inl x_a) = (LeanPool.Polylean.AddFreeGroup.ι x_a, 0)
• LeanPool.Polylean.AddFreeGroup.Product.ι (Sum.inr x_b) = (0, LeanPool.Polylean.AddFreeGroup.ι x_b)

def LeanPool.Polylean.AddFreeGroup.Product.inducedProdHom {A : Type u_1} {B : Type u_2} [AddCommGroup A] [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) [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

• LeanPool.Polylean.AddFreeGroup.Product.inducedProdHom G f = (LeanPool.Polylean.AddFreeGroup.inducedHom G (f ∘ Sum.inl)).coprod (LeanPool.Polylean.AddFreeGroup.inducedHom G (f ∘ Sum.inr))

@[implicit_reducible]

instance LeanPool.Polylean.AddFreeGroup.Product.prodFree {A : Type u_1} {B : Type u_2} [AddCommGroup A] [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.