Free abelian groups

The free abelian group on a type α, defined as the abelianisation of the free group on α.

The free abelian group on α can be abstractly defined as the left adjoint of the forgetful functor from abelian groups to types. Alternatively, one could define it as the functions α → ℤ which send all but finitely many (a : α) to 0, under pointwise addition. In this file, it is defined as the abelianisation of the free group on α. All the constructions and theorems required to show the adjointness of the construction and the forgetful functor are proved in this file, but the category-theoretic adjunction statement is in Mathlib/Algebra/Category/Grp/Adjunctions.lean.

Main definitions

Here we use the following variables: (α β : Type*) (A : Type*) [AddCommGroup A]

• FreeAbelianGroup α : the free abelian group on a type α. As an abelian group it is α →₀ ℤ, the functions from α to ℤ such that all but finitely many elements get mapped to zero, however this is not how it is implemented.

• lift f : FreeAbelianGroup α →+ A : the group homomorphism induced by the map f : α → A.

• map (f : α → β) : FreeAbelianGroup α →+ FreeAbelianGroup β : functoriality of FreeAbelianGroup.

• instance [Monoid α] : Semigroup (FreeAbelianGroup α)

• instance [CommMonoid α] : CommRing (FreeAbelianGroup α)

It has been suggested that we would be better off refactoring this file and using Finsupp instead.

Implementation issues

The definition is def FreeAbelianGroup : Type u := Additive <| Abelianization <| FreeGroup α.

Chris Hughes has suggested that this all be rewritten in terms of Finsupp. Johan Commelin has written all the API relating the definition to Finsupp in the lean-liquid repo.

The lemmas map_pure, map_of, map_zero, map_add, map_neg and map_sub are proved about the Functor.map <$> construction, and need α and β to be in the same universe. But FreeAbelianGroup.map (f : α → β) is defined to be the AddGroup homomorphism FreeAbelianGroup α →+ FreeAbelianGroup β (with α and β now allowed to be in different universes), so (map f).map_add etc. can be used to prove that FreeAbelianGroup.map preserves addition. The functions map_id, map_id_apply, map_comp, map_comp_apply and map_of_apply are about FreeAbelianGroup.map.

def FreeAbelianGroup (α : Type u) : Type u

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

A typical element of FreeAbelianGroup α is a formal sum of elements of α and their formal inverses. For example if x and y are terms of type α then x + x + x - y is a "typical" element of FreeAbelianGroup α. In particular if α is empty then FreeAbelianGroup α is isomorphic to the trivial group, and if α has one term then FreeAbelianGroup α is isomorphic to ℤ. One can think of FreeAbelianGroup α as the functions α →₀ ℤ with finite support, and addition given pointwise.

TODO: rename to FreeAddCommGroup and introduce a multiplicative version

Equations

• FreeAbelianGroup α = Additive (Abelianization (FreeGroup α))

instance FreeAbelianGroup.addCommGroup (α : Type u) : AddCommGroup (FreeAbelianGroup α)

Equations

• FreeAbelianGroup.addCommGroup α = Additive.addCommGroup

instance instInhabitedFreeAbelianGroup (α : Type u) : Inhabited (FreeAbelianGroup α)

Equations

• instInhabitedFreeAbelianGroup α = { default := 0 }

instance instUniqueFreeAbelianGroupOfIsEmpty (α : Type u) [IsEmpty α] : Unique (FreeAbelianGroup α)

Equations

• instUniqueFreeAbelianGroupOfIsEmpty α = id inferInstance

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

The canonical map from α to FreeAbelianGroup α.

Equations

• FreeAbelianGroup.of x = Additive.ofMul (Abelianization.of (FreeGroup.of x))

def FreeAbelianGroup.lift {α : Type u} {β : Type v} [AddCommGroup β] : (α → β) ≃ (FreeAbelianGroup α →+ β)

The map FreeAbelianGroup α →+ A induced by a map of types α → A.

Equations

• FreeAbelianGroup.lift = FreeGroup.lift.trans (Abelianization.lift.trans MonoidHom.toAdditive)

@[simp]

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

@[deprecated FreeAbelianGroup.lift_apply_of (since := "2025-07-23")]

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

Alias of FreeAbelianGroup.lift_apply_of.

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

@[deprecated FreeAbelianGroup.lift_unique (since := "2025-07-23")]

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

Alias of FreeAbelianGroup.lift_unique.

theorem FreeAbelianGroup.lift_ext {α : Type u} {β : Type v} [AddCommGroup β] (g h : FreeAbelianGroup α →+ β) (H : ∀ (x : α), g (of x) = h (of x)) : g = h

See note [partially-applied ext lemmas].

theorem FreeAbelianGroup.lift_ext_iff {α : Type u} {β : Type v} [AddCommGroup β] {g h : FreeAbelianGroup α →+ β} : g = h ↔ ∀ (x : α), g (of x) = h (of x)

@[deprecated FreeAbelianGroup.lift_ext (since := "2025-07-23")]

theorem FreeAbelianGroup.lift.ext {α : Type u} {β : Type v} [AddCommGroup β] (g h : FreeAbelianGroup α →+ β) (H : ∀ (x : α), g (of x) = h (of x)) : g = h

Alias of FreeAbelianGroup.lift_ext.

---

See note [partially-applied ext lemmas].

theorem FreeAbelianGroup.lift_comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommGroup β] [AddCommGroup γ] (a : FreeAbelianGroup α) (f : α → β) (g : β →+ γ) : (lift (⇑g ∘ f)) a = g ((lift f) a)

@[deprecated FreeAbelianGroup.lift_comp_apply (since := "2025-07-23")]

theorem FreeAbelianGroup.lift.map_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommGroup β] [AddCommGroup γ] (a : FreeAbelianGroup α) (f : α → β) (g : β →+ γ) : g ((lift f) a) = (lift (⇑g ∘ f)) a

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

@[simp]

theorem FreeAbelianGroup.of_ne_zero {α : Type u} (x : α) : of x ≠ 0

@[simp]

theorem FreeAbelianGroup.zero_ne_of {α : Type u} (x : α) : 0 ≠ of x

instance FreeAbelianGroup.instNontrivialOfNonempty {α : Type u} [Nonempty α] : Nontrivial (FreeAbelianGroup α)

theorem FreeAbelianGroup.induction_on {α : Type u} {C : FreeAbelianGroup α → Prop} (z : FreeAbelianGroup α) (C0 : C 0) (C1 : ∀ (x : α), C (of x)) (Cn : ∀ (x : α), C (of x) → C (-of x)) (Cp : ∀ (x y : FreeAbelianGroup α), C x → C y → C (x + y)) : C z

theorem FreeAbelianGroup.lift_add_apply {α : Type u} {G : Type u_1} [AddCommGroup G] (f g : α → G) (a : FreeAbelianGroup α) : (lift (f + g)) a = (lift f) a + (lift g) a

@[deprecated FreeAbelianGroup.lift_add_apply (since := "2025-07-13")]

theorem FreeAbelianGroup.lift.add' {α : Type u} {G : Type u_1} [AddCommGroup G] (f g : α → G) (a : FreeAbelianGroup α) : (lift (f + g)) a = (lift f) a + (lift g) a

Alias of FreeAbelianGroup.lift_add_apply.

@[simp]

theorem FreeAbelianGroup.lift_add {α : Type u} {G : Type u_1} [AddCommGroup G] (f g : α → G) : lift (f + g) = lift f + lift g

def FreeAbelianGroup.liftAddEquiv {α : Type u} {G : Type u_1} [AddCommGroup G] : (α → G) ≃+ (FreeAbelianGroup α →+ G)

FreeAbelianGroup.lift as an equivalence of groups.

Equations

• FreeAbelianGroup.liftAddEquiv = { toEquiv := FreeAbelianGroup.lift, map_add' := ⋯ }

@[simp]

theorem FreeAbelianGroup.liftAddEquiv_apply_apply {α : Type u} {G : Type u_1} [AddCommGroup G] (a✝ : α → Multiplicative G) (a : Additive (Abelianization (FreeGroup α))) : (liftAddEquiv a✝) a = Additive.ofMul ((Abelianization.lift (FreeGroup.lift a✝)) (Additive.toMul a))

@[simp]

theorem FreeAbelianGroup.liftAddEquiv_symm_apply {α : Type u} {G : Type u_1} [AddCommGroup G] (a✝ : FreeAbelianGroup α →+ G) (a✝¹ : α) : liftAddEquiv.symm a✝ a✝¹ = (MonoidHom.toAdditive.symm a✝) (Abelianization.of (FreeGroup.of a✝¹))

def FreeAbelianGroup.liftAddGroupHom {α : Type u_2} (β : Type u_3) [AddCommGroup β] (a : FreeAbelianGroup α) : (α → β) →+ β

If g : FreeAbelianGroup X and A is an abelian group then liftAddGroupHom g is the additive group homomorphism sending a function X → A to the term of type A corresponding to the evaluation of the induced map FreeAbelianGroup X → A at g.

Equations

• FreeAbelianGroup.liftAddGroupHom β a = AddMonoidHom.mk' (fun (f : α → β) => (FreeAbelianGroup.lift f) a) ⋯

@[simp]

theorem FreeAbelianGroup.liftAddGroupHom_apply {α : Type u_2} (β : Type u_3) [AddCommGroup β] (a : FreeAbelianGroup α) (f : α → β) : (liftAddGroupHom β a) f = (lift f) a

@[simp]

theorem FreeAbelianGroup.lift_neg {α : Type u} {G : Type u_1} [AddCommGroup G] (f : α → G) : lift (-f) = -lift f

theorem FreeAbelianGroup.lift_neg_apply {α : Type u} {G : Type u_1} [AddCommGroup G] (f : α → G) (a : FreeAbelianGroup α) : (lift (-f)) a = -(lift f) a

@[deprecated FreeAbelianGroup.lift_neg (since := "2025-07-13")]

theorem FreeAbelianGroup.lift_neg' {α : Type u} {G : Type u_1} [AddCommGroup G] (f : α → G) : lift (-f) = -lift f

Alias of FreeAbelianGroup.lift_neg.

instance FreeAbelianGroup.instMonad : Monad FreeAbelianGroup

Equations

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

theorem FreeAbelianGroup.induction_on' {α : Type u} {C : FreeAbelianGroup α → Prop} (z : FreeAbelianGroup α) (C0 : C 0) (C1 : ∀ (x : α), C (pure x)) (Cn : ∀ (x : α), C (pure x) → C (-pure x)) (Cp : ∀ (x y : FreeAbelianGroup α), C x → C y → C (x + y)) : C z

@[simp]

theorem FreeAbelianGroup.map_pure {α β : Type u} (f : α → β) (x : α) : f <$> pure x = pure (f x)

@[simp]

theorem FreeAbelianGroup.map_zero {α β : Type u} (f : α → β) : f <$> 0 = 0

@[simp]

theorem FreeAbelianGroup.map_add {α β : Type u} (f : α → β) (x y : FreeAbelianGroup α) : f <$> (x + y) = f <$> x + f <$> y

@[simp]

theorem FreeAbelianGroup.map_neg {α β : Type u} (f : α → β) (x : FreeAbelianGroup α) : f <$> (-x) = -f <$> x

@[simp]

theorem FreeAbelianGroup.map_sub {α β : Type u} (f : α → β) (x y : FreeAbelianGroup α) : f <$> (x - y) = f <$> x - f <$> y

@[simp]

theorem FreeAbelianGroup.map_of {α β : Type u} (f : α → β) (y : α) : f <$> of y = of (f y)

theorem FreeAbelianGroup.pure_bind {α β : Type u} (f : α → FreeAbelianGroup β) (x : α) : pure x >>= f = f x

@[simp]

theorem FreeAbelianGroup.zero_bind {α β : Type u} (f : α → FreeAbelianGroup β) : 0 >>= f = 0

@[simp]

theorem FreeAbelianGroup.add_bind {α β : Type u} (f : α → FreeAbelianGroup β) (x y : FreeAbelianGroup α) : x + y >>= f = (x >>= f) + (y >>= f)

@[simp]

theorem FreeAbelianGroup.neg_bind {α β : Type u} (f : α → FreeAbelianGroup β) (x : FreeAbelianGroup α) : -x >>= f = -(x >>= f)

@[simp]

theorem FreeAbelianGroup.sub_bind {α β : Type u} (f : α → FreeAbelianGroup β) (x y : FreeAbelianGroup α) : x - y >>= f = (x >>= f) - (y >>= f)

@[simp]

theorem FreeAbelianGroup.pure_seq {α β : Type u} (f : α → β) (x : FreeAbelianGroup α) : pure f <*> x = f <$> x

@[simp]

theorem FreeAbelianGroup.zero_seq {α β : Type u} (x : FreeAbelianGroup α) : 0 <*> x = 0

@[simp]

theorem FreeAbelianGroup.add_seq {α β : Type u} (f g : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) : f + g <*> x = (f <*> x) + (g <*> x)

@[simp]

theorem FreeAbelianGroup.neg_seq {α β : Type u} (f : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) : -f <*> x = -(f <*> x)

@[simp]

theorem FreeAbelianGroup.sub_seq {α β : Type u} (f g : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) : f - g <*> x = (f <*> x) - (g <*> x)

def FreeAbelianGroup.seqAddGroupHom {α β : Type u} (f : FreeAbelianGroup (α → β)) : FreeAbelianGroup α →+ FreeAbelianGroup β

If f : FreeAbelianGroup (α → β), then f <*> is an additive morphism FreeAbelianGroup α →+ FreeAbelianGroup β.

Equations

• f.seqAddGroupHom = AddMonoidHom.mk' (fun (x : FreeAbelianGroup α) => f <*> x) ⋯

@[simp]

theorem FreeAbelianGroup.seq_zero {α β : Type u} (f : FreeAbelianGroup (α → β)) : f <*> 0 = 0

@[simp]

theorem FreeAbelianGroup.seq_add {α β : Type u} (f : FreeAbelianGroup (α → β)) (x y : FreeAbelianGroup α) : f <*> x + y = (f <*> x) + (f <*> y)

@[simp]

theorem FreeAbelianGroup.seq_neg {α β : Type u} (f : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) : f <*> -x = -(f <*> x)

@[simp]

theorem FreeAbelianGroup.seq_sub {α β : Type u} (f : FreeAbelianGroup (α → β)) (x y : FreeAbelianGroup α) : f <*> x - y = (f <*> x) - (f <*> y)

instance FreeAbelianGroup.instLawfulMonad : LawfulMonad FreeAbelianGroup

instance FreeAbelianGroup.instCommApplicative : CommApplicative FreeAbelianGroup

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

The additive group homomorphism FreeAbelianGroup α →+ FreeAbelianGroup β induced from a map α → β.

Equations

• FreeAbelianGroup.map f = FreeAbelianGroup.lift (FreeAbelianGroup.of ∘ f)

theorem FreeAbelianGroup.lift_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommGroup γ] (f : α → β) (g : β → γ) (x : FreeAbelianGroup α) : (lift (g ∘ f)) x = (lift g) ((map f) x)

theorem FreeAbelianGroup.map_id {α : Type u} : map id = AddMonoidHom.id (FreeAbelianGroup α)

theorem FreeAbelianGroup.map_id_apply {α : Type u} (x : FreeAbelianGroup α) : (map id) x = x

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

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

@[simp]

theorem FreeAbelianGroup.map_of_apply {α : Type u} {β : Type v} {f : α → β} (a : α) : (map f) (of a) = of (f a)

instance FreeAbelianGroup.mul (α : Type u) [Mul α] : Mul (FreeAbelianGroup α)

Equations

• FreeAbelianGroup.mul α = { mul := fun (x : FreeAbelianGroup α) => ⇑(FreeAbelianGroup.lift fun (x₂ : α) => (FreeAbelianGroup.lift fun (x₁ : α) => FreeAbelianGroup.of (x₁ * x₂)) x) }

theorem FreeAbelianGroup.mul_def {α : Type u} [Mul α] (x y : FreeAbelianGroup α) : x * y = (lift fun (x₂ : α) => (lift fun (x₁ : α) => of (x₁ * x₂)) x) y

@[simp]

theorem FreeAbelianGroup.of_mul_of {α : Type u} [Mul α] (x y : α) : of x * of y = of (x * y)

theorem FreeAbelianGroup.of_mul {α : Type u} [Mul α] (x y : α) : of (x * y) = of x * of y

instance FreeAbelianGroup.distrib {α : Type u} [Mul α] : Distrib (FreeAbelianGroup α)

Equations

• FreeAbelianGroup.distrib = { toMul := FreeAbelianGroup.mul α, toAdd := (FreeAbelianGroup.addCommGroup α).toAdd, left_distrib := ⋯, right_distrib := ⋯ }

instance FreeAbelianGroup.nonUnitalNonAssocRing {α : Type u} [Mul α] : NonUnitalNonAssocRing (FreeAbelianGroup α)

Equations

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

instance FreeAbelianGroup.one (α : Type u) [One α] : One (FreeAbelianGroup α)

Equations

• FreeAbelianGroup.one α = { one := FreeAbelianGroup.of 1 }

theorem FreeAbelianGroup.one_def (α : Type u) [One α] : 1 = of 1

theorem FreeAbelianGroup.of_one (α : Type u) [One α] : of 1 = 1

instance FreeAbelianGroup.nonUnitalRing (α : Type u) [Semigroup α] : NonUnitalRing (FreeAbelianGroup α)

Equations

• FreeAbelianGroup.nonUnitalRing α = { toNonUnitalNonAssocRing := FreeAbelianGroup.nonUnitalNonAssocRing, mul_assoc := ⋯ }

instance FreeAbelianGroup.ring (α : Type u) [Monoid α] : Ring (FreeAbelianGroup α)

Equations

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

def FreeAbelianGroup.ofMulHom {α : Type u} [Monoid α] : α →* FreeAbelianGroup α

FreeAbelianGroup.of is a MonoidHom when α is a Monoid.

Equations

• FreeAbelianGroup.ofMulHom = { toFun := FreeAbelianGroup.of, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem FreeAbelianGroup.ofMulHom_coe {α : Type u} [Monoid α] : ⇑ofMulHom = of

def FreeAbelianGroup.liftMonoid {α : Type u} {R : Type u_2} [Monoid α] [Ring R] : (α →* R) ≃ (FreeAbelianGroup α →+* R)

If f preserves multiplication, then so does lift f.

Equations

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

@[simp]

theorem FreeAbelianGroup.liftMonoid_coe_addMonoidHom {α : Type u} {R : Type u_2} [Monoid α] [Ring R] (f : α →* R) : ↑(liftMonoid f) = lift ⇑f

@[simp]

theorem FreeAbelianGroup.liftMonoid_coe {α : Type u} {R : Type u_2} [Monoid α] [Ring R] (f : α →* R) : ⇑(liftMonoid f) = ⇑(lift ⇑f)

@[simp]

theorem FreeAbelianGroup.liftMonoid_symm_coe {α : Type u} {R : Type u_2} [Monoid α] [Ring R] (f : FreeAbelianGroup α →+* R) : ⇑(liftMonoid.symm f) = lift.symm ↑f

instance FreeAbelianGroup.instCommRingOfCommMonoid (α : Type u) [CommMonoid α] : CommRing (FreeAbelianGroup α)

Equations

• FreeAbelianGroup.instCommRingOfCommMonoid α = { toRing := FreeAbelianGroup.ring α, mul_comm := ⋯ }

instance FreeAbelianGroup.pemptyUnique : Unique (FreeAbelianGroup PEmpty.{u_2 + 1})

Equations

• FreeAbelianGroup.pemptyUnique = { default := 0, uniq := FreeAbelianGroup.pemptyUnique._proof_1 }

def FreeAbelianGroup.uniqueEquiv (T : Type u_2) [Unique T] : FreeAbelianGroup T ≃+ ℤ

The free abelian group on a type with one term is isomorphic to ℤ.

Equations

• FreeAbelianGroup.uniqueEquiv T = { toFun := ⇑(FreeAbelianGroup.lift fun (x : T) => 1), invFun := fun (n : ℤ) => n • FreeAbelianGroup.of default, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[deprecated FreeAbelianGroup.uniqueEquiv (since := "2025-06-16")]

def FreeAbelianGroup.punitEquiv (T : Type u_2) [Unique T] : FreeAbelianGroup T ≃+ ℤ

Alias of FreeAbelianGroup.uniqueEquiv.

---

The free abelian group on a type with one term is isomorphic to ℤ.

Equations

• FreeAbelianGroup.punitEquiv = FreeAbelianGroup.uniqueEquiv

def FreeAbelianGroup.equivOfEquiv {α : Type u_2} {β : Type u_3} (f : α ≃ β) : FreeAbelianGroup α ≃+ FreeAbelianGroup β

Isomorphic types have isomorphic free abelian groups.

Equations

• FreeAbelianGroup.equivOfEquiv f = { toFun := ⇑(FreeAbelianGroup.map ⇑f), invFun := ⇑(FreeAbelianGroup.map ⇑f.symm), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }