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
Algebra.Category.Group.Adjunctions
.
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 mapf : α → A
.map (f : α → β) : FreeAbelianGroup α →+ FreeAbelianGroup β
: functoriality ofFreeAbelianGroup
.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
.
The free abelian group on a type.
Equations
- FreeAbelianGroup α = Additive (Abelianization (FreeGroup α))
Instances For
Equations
- FreeAbelianGroup.addCommGroup α = Additive.addCommGroup
Equations
- instInhabitedFreeAbelianGroup α = { default := 0 }
Equations
- instUniqueFreeAbelianGroupOfIsEmpty α = id inferInstance
The canonical map from α
to FreeAbelianGroup α
.
Equations
- FreeAbelianGroup.of x = Abelianization.of (FreeGroup.of x)
Instances For
The map FreeAbelianGroup α →+ A
induced by a map of types α → A
.
Equations
- FreeAbelianGroup.lift = FreeGroup.lift.trans (Abelianization.lift.trans MonoidHom.toAdditive)
Instances For
See note [partially-applied ext lemmas].
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) ⋯
Instances For
Equations
- FreeAbelianGroup.instMonad = Monad.mk
If f : FreeAbelianGroup (α → β)
, then f <*>
is an additive morphism
FreeAbelianGroup α →+ FreeAbelianGroup β
.
Equations
- f.seqAddGroupHom = AddMonoidHom.mk' (fun (x : FreeAbelianGroup α) => Seq.seq f fun (x_1 : Unit) => x) ⋯
Instances For
The additive group homomorphism FreeAbelianGroup α →+ FreeAbelianGroup β
induced from a
map α → β
.
Equations
- FreeAbelianGroup.map f = FreeAbelianGroup.lift (FreeAbelianGroup.of ∘ f)
Instances For
Equations
- FreeAbelianGroup.mul α = { mul := fun (x : FreeAbelianGroup α) => ⇑(FreeAbelianGroup.lift fun (x₂ : α) => (FreeAbelianGroup.lift fun (x₁ : α) => FreeAbelianGroup.of (x₁ * x₂)) x) }
Equations
- FreeAbelianGroup.distrib = Distrib.mk ⋯ ⋯
Equations
- FreeAbelianGroup.nonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯
Equations
- FreeAbelianGroup.one α = { one := FreeAbelianGroup.of 1 }
Equations
Equations
- FreeAbelianGroup.ring α = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
FreeAbelianGroup.of
is a MonoidHom
when α
is a Monoid
.
Equations
- FreeAbelianGroup.ofMulHom = { toFun := FreeAbelianGroup.of, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Equations
Equations
- FreeAbelianGroup.pemptyUnique = { default := 0, uniq := FreeAbelianGroup.pemptyUnique.proof_1 }
The free abelian group on a type with one term is isomorphic to ℤ
.
Equations
- FreeAbelianGroup.punitEquiv T = { toFun := ⇑(FreeAbelianGroup.lift fun (x : T) => 1), invFun := fun (n : ℤ) => n • FreeAbelianGroup.of default, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
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' := ⋯ }