mathlib3 documentation

group_theory.free_abelian_group

Free abelian groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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*) [add_comm_group A]

free_abelian_group α : 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 : free_abelian_group α →+ A : the group homomorphism induced by the map f : α → A.
map (f : α → β) : free_abelian_group α →+ free_abelian_group β : functoriality of free_abelian_group
instance [monoid α] : semigroup (free_abelian_group α)
instance [comm_monoid α] : comm_ring (free_abelian_group α)

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

Implementation issues #

The definition is def free_abelian_group : Type u := additive $ abelianization $ free_group α

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 free_abelian_group.map (f : α → β) is defined to be the add_group homomorphism free_abelian_group α →+ free_abelian_group β (with α and β now allowed to be in different universes), so (map f).map_add etc can be used to prove that free_abelian_group.map preserves addition. The functions map_id, map_id_apply, map_comp, map_comp_apply and map_of_apply are about free_abelian_group.map.

def free_abelian_group (α : Type u) :

The free abelian group on a type.

Equations

free_abelian_group α = additive (abelianization (free_group α))

Instances for free_abelian_group

@[protected, instance]

def free_abelian_group.add_comm_group (α : Type u) :

add_comm_group (free_abelian_group α)

Equations

free_abelian_group.add_comm_group α = additive.add_comm_group

@[protected, instance]

def free_abelian_group.inhabited (α : Type u) :

inhabited (free_abelian_group α)

Equations

free_abelian_group.inhabited α = {default := 0}

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

free_abelian_group α

The canonical map from α to free_abelian_group α

Equations

free_abelian_group.of x = ⇑abelianization.of (free_group.of x)

def free_abelian_group.lift {α : Type u} {β : Type v} [add_comm_group β] :

(α → β) ≃ (free_abelian_group α →+ β)

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

Equations

free_abelian_group.lift = free_group.lift.trans (abelianization.lift.trans monoid_hom.to_additive)

@[protected, simp]

theorem free_abelian_group.lift.of {α : Type u} {β : Type v} [add_comm_group β] (f : α → β) (x : α) :

⇑(⇑free_abelian_group.lift f) (free_abelian_group.of x) = f x

@[protected]

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

⇑g x = ⇑(⇑free_abelian_group.lift f) x

@[protected, ext]

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

g = h

See note [partially-applied ext lemmas].

theorem free_abelian_group.lift.map_hom {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group β] [add_comm_group γ] (a : free_abelian_group α) (f : α → β) (g : β →+ γ) :

⇑g (⇑(⇑free_abelian_group.lift f) a) = ⇑(⇑free_abelian_group.lift (⇑g ∘ f)) a

theorem free_abelian_group.of_injective {α : Type u} :

function.injective free_abelian_group.of

@[protected]

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

C z

theorem free_abelian_group.lift.add' {α : Type u_1} {β : Type u_2} [add_comm_group β] (a : free_abelian_group α) (f g : α → β) :

⇑(⇑free_abelian_group.lift (f + g)) a = ⇑(⇑free_abelian_group.lift f) a + ⇑(⇑free_abelian_group.lift g) a

@[simp]

theorem free_abelian_group.lift_add_group_hom_apply {α : Type u_1} (β : Type u_2) [add_comm_group β] (a : free_abelian_group α) (f : α → β) :

⇑(free_abelian_group.lift_add_group_hom β a) f = ⇑(⇑free_abelian_group.lift f) a

def free_abelian_group.lift_add_group_hom {α : Type u_1} (β : Type u_2) [add_comm_group β] (a : free_abelian_group α) :

(α → β) →+ β

If g : free_abelian_group X and A is an abelian group then lift_add_group_hom 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 free_abelian_group X → A at g.

Equations

free_abelian_group.lift_add_group_hom β a = add_monoid_hom.mk' (λ (f : α → β), ⇑(⇑free_abelian_group.lift f) a) _

theorem free_abelian_group.lift_neg' {α : Type u} {β : Type u_1} [add_comm_group β] (f : α → β) :

⇑free_abelian_group.lift (-f) = -⇑free_abelian_group.lift f

@[protected, instance]

def free_abelian_group.monad :

monad free_abelian_group

Equations

free_abelian_group.monad = monad.mk

@[protected]

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

C z

@[simp]

theorem free_abelian_group.map_pure {α β : Type u} (f : α → β) (x : α) :

f <$> has_pure.pure x = has_pure.pure (f x)

@[protected, simp]

theorem free_abelian_group.map_zero {α β : Type u} (f : α → β) :

f <$> 0 = 0

@[protected, simp]

theorem free_abelian_group.map_add {α β : Type u} (f : α → β) (x y : free_abelian_group α) :

f <$> (x + y) = f <$> x + f <$> y

@[protected, simp]

theorem free_abelian_group.map_neg {α β : Type u} (f : α → β) (x : free_abelian_group α) :

f <$> -x = -f <$> x

@[protected, simp]

theorem free_abelian_group.map_sub {α β : Type u} (f : α → β) (x y : free_abelian_group α) :

f <$> (x - y) = f <$> x - f <$> y

@[simp]

theorem free_abelian_group.map_of {α β : Type u} (f : α → β) (y : α) :

f <$> free_abelian_group.of y = free_abelian_group.of (f y)

@[simp]

theorem free_abelian_group.pure_bind {α β : Type u} (f : α → free_abelian_group β) (x : α) :

has_pure.pure x >>= f = f x

@[simp]

theorem free_abelian_group.zero_bind {α β : Type u} (f : α → free_abelian_group β) :

0 >>= f = 0

@[simp]

theorem free_abelian_group.add_bind {α β : Type u} (f : α → free_abelian_group β) (x y : free_abelian_group α) :

x + y >>= f = (x >>= f) + (y >>= f)

@[simp]

theorem free_abelian_group.neg_bind {α β : Type u} (f : α → free_abelian_group β) (x : free_abelian_group α) :

-x >>= f = -(x >>= f)

@[simp]

theorem free_abelian_group.sub_bind {α β : Type u} (f : α → free_abelian_group β) (x y : free_abelian_group α) :

x - y >>= f = (x >>= f) - (y >>= f)

@[simp]

theorem free_abelian_group.pure_seq {α β : Type u} (f : α → β) (x : free_abelian_group α) :

has_pure.pure f <*> x = f <$> x

@[simp]

theorem free_abelian_group.zero_seq {α β : Type u} (x : free_abelian_group α) :

0 <*> x = 0

@[simp]

theorem free_abelian_group.add_seq {α β : Type u} (f g : free_abelian_group (α → β)) (x : free_abelian_group α) :

f + g <*> x = (f <*> x) + (g <*> x)

@[simp]

theorem free_abelian_group.neg_seq {α β : Type u} (f : free_abelian_group (α → β)) (x : free_abelian_group α) :

-f <*> x = -(f <*> x)

@[simp]

theorem free_abelian_group.sub_seq {α β : Type u} (f g : free_abelian_group (α → β)) (x : free_abelian_group α) :

f - g <*> x = (f <*> x) - (g <*> x)

def free_abelian_group.seq_add_group_hom {α β : Type u} (f : free_abelian_group (α → β)) :

free_abelian_group α →+ free_abelian_group β

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

Equations

f.seq_add_group_hom = add_monoid_hom.mk' (has_seq.seq f) _

@[simp]

theorem free_abelian_group.seq_zero {α β : Type u} (f : free_abelian_group (α → β)) :

f <*> 0 = 0

@[simp]

theorem free_abelian_group.seq_add {α β : Type u} (f : free_abelian_group (α → β)) (x y : free_abelian_group α) :

f <*> x + y = (f <*> x) + (f <*> y)

@[simp]

theorem free_abelian_group.seq_neg {α β : Type u} (f : free_abelian_group (α → β)) (x : free_abelian_group α) :

f <*> -x = -(f <*> x)

@[simp]

theorem free_abelian_group.seq_sub {α β : Type u} (f : free_abelian_group (α → β)) (x y : free_abelian_group α) :

f <*> x - y = (f <*> x) - (f <*> y)

@[protected, instance]

def free_abelian_group.is_lawful_monad :

is_lawful_monad free_abelian_group

@[protected, instance]

def free_abelian_group.is_comm_applicative :

is_comm_applicative free_abelian_group

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

free_abelian_group α →+ free_abelian_group β

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

Equations

free_abelian_group.map f = ⇑free_abelian_group.lift (free_abelian_group.of ∘ f)

theorem free_abelian_group.lift_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group γ] (f : α → β) (g : β → γ) (x : free_abelian_group α) :

⇑(⇑free_abelian_group.lift (g ∘ f)) x = ⇑(⇑free_abelian_group.lift g) (⇑(free_abelian_group.map f) x)

theorem free_abelian_group.map_id {α : Type u} :

free_abelian_group.map id = add_monoid_hom.id (free_abelian_group α)

theorem free_abelian_group.map_id_apply {α : Type u} (x : free_abelian_group α) :

⇑(free_abelian_group.map id) x = x

theorem free_abelian_group.map_comp {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} :

free_abelian_group.map (g ∘ f) = (free_abelian_group.map g).comp (free_abelian_group.map f)

theorem free_abelian_group.map_comp_apply {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} (x : free_abelian_group α) :

⇑(free_abelian_group.map (g ∘ f)) x = ⇑(free_abelian_group.map g) (⇑(free_abelian_group.map f) x)

@[simp]

theorem free_abelian_group.map_of_apply {α : Type u} {β : Type v} {f : α → β} (a : α) :

⇑(free_abelian_group.map f) (free_abelian_group.of a) = free_abelian_group.of (f a)

@[protected, instance]

def free_abelian_group.has_mul (α : Type u) [has_mul α] :

has_mul (free_abelian_group α)

Equations

free_abelian_group.has_mul α = {mul := λ (x : free_abelian_group α), ⇑(⇑free_abelian_group.lift (λ (x₂ : α), ⇑(⇑free_abelian_group.lift (λ (x₁ : α), free_abelian_group.of (x₁ * x₂))) x))}

theorem free_abelian_group.mul_def {α : Type u} [has_mul α] (x y : free_abelian_group α) :

x * y = ⇑(⇑free_abelian_group.lift (λ (x₂ : α), ⇑(⇑free_abelian_group.lift (λ (x₁ : α), free_abelian_group.of (x₁ * x₂))) x)) y

@[simp]

theorem free_abelian_group.of_mul_of {α : Type u} [has_mul α] (x y : α) :

free_abelian_group.of x * free_abelian_group.of y = free_abelian_group.of (x * y)

theorem free_abelian_group.of_mul {α : Type u} [has_mul α] (x y : α) :

free_abelian_group.of (x * y) = free_abelian_group.of x * free_abelian_group.of y

@[protected, instance]

def free_abelian_group.distrib {α : Type u} [has_mul α] :

distrib (free_abelian_group α)

Equations

free_abelian_group.distrib = {mul := has_mul.mul (free_abelian_group.has_mul α), add := has_add.add (add_zero_class.to_has_add (free_abelian_group α)), left_distrib := _, right_distrib := _}

@[protected, instance]

def free_abelian_group.non_unital_non_assoc_ring {α : Type u} [has_mul α] :

non_unital_non_assoc_ring (free_abelian_group α)

Equations

free_abelian_group.non_unital_non_assoc_ring = {add := distrib.add free_abelian_group.distrib, add_assoc := _, zero := add_comm_group.zero (free_abelian_group.add_comm_group α), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (free_abelian_group.add_comm_group α), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (free_abelian_group.add_comm_group α), sub := add_comm_group.sub (free_abelian_group.add_comm_group α), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (free_abelian_group.add_comm_group α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := distrib.mul free_abelian_group.distrib, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}

@[protected, instance]

def free_abelian_group.has_one (α : Type u) [has_one α] :

has_one (free_abelian_group α)

Equations

free_abelian_group.has_one α = {one := free_abelian_group.of 1}

@[protected, instance]

def free_abelian_group.non_unital_ring (α : Type u) [semigroup α] :

non_unital_ring (free_abelian_group α)

Equations

free_abelian_group.non_unital_ring α = {add := non_unital_non_assoc_ring.add free_abelian_group.non_unital_non_assoc_ring, add_assoc := _, zero := non_unital_non_assoc_ring.zero free_abelian_group.non_unital_non_assoc_ring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_ring.nsmul free_abelian_group.non_unital_non_assoc_ring, nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_non_assoc_ring.neg free_abelian_group.non_unital_non_assoc_ring, sub := non_unital_non_assoc_ring.sub free_abelian_group.non_unital_non_assoc_ring, sub_eq_add_neg := _, zsmul := non_unital_non_assoc_ring.zsmul free_abelian_group.non_unital_non_assoc_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul (free_abelian_group.has_mul α), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}

@[protected, instance]

def free_abelian_group.ring (α : Type u) [monoid α] :

ring (free_abelian_group α)

Equations

free_abelian_group.ring α = {add := non_unital_ring.add (free_abelian_group.non_unital_ring α), add_assoc := _, zero := non_unital_ring.zero (free_abelian_group.non_unital_ring α), zero_add := _, add_zero := _, nsmul := non_unital_ring.nsmul (free_abelian_group.non_unital_ring α), nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_ring.neg (free_abelian_group.non_unital_ring α), sub := non_unital_ring.sub (free_abelian_group.non_unital_ring α), sub_eq_add_neg := _, zsmul := non_unital_ring.zsmul (free_abelian_group.non_unital_ring α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_comm_group_with_one.int_cast._default (add_comm_group_with_one.nat_cast._default 1 non_unital_ring.add _ non_unital_ring.zero _ _ non_unital_ring.nsmul _ _) non_unital_ring.add _ non_unital_ring.zero _ _ non_unital_ring.nsmul _ _ 1 _ _ non_unital_ring.neg non_unital_ring.sub _ non_unital_ring.zsmul _ _ _ _, nat_cast := add_comm_group_with_one.nat_cast._default 1 non_unital_ring.add _ non_unital_ring.zero _ _ non_unital_ring.nsmul _ _, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul (free_abelian_group.has_mul α), mul_assoc := _, one_mul := _, mul_one := _, npow := monoid.npow._default 1 has_mul.mul _ _, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}

def free_abelian_group.of_mul_hom {α : Type u} [monoid α] :

α →* free_abelian_group α

free_abelian_group.of is a monoid_hom when α is a monoid.

Equations

free_abelian_group.of_mul_hom = {to_fun := free_abelian_group.of α, map_one' := _, map_mul' := _}

@[simp]

theorem free_abelian_group.of_mul_hom_coe {α : Type u} [monoid α] :

⇑free_abelian_group.of_mul_hom = free_abelian_group.of

def free_abelian_group.lift_monoid {α : Type u} {R : Type u_1} [monoid α] [ring R] :

(α →* R) ≃ (free_abelian_group α →+* R)

If f preserves multiplication, then so does lift f.

Equations

free_abelian_group.lift_monoid = {to_fun := λ (f : α →* R), {to_fun := ⇑(⇑free_abelian_group.lift ⇑f), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, inv_fun := λ (F : free_abelian_group α →+* R), ↑F.comp free_abelian_group.of_mul_hom, left_inv := _, right_inv := _}

@[simp]

theorem free_abelian_group.lift_monoid_coe_add_monoid_hom {α : Type u} {R : Type u_1} [monoid α] [ring R] (f : α →* R) :

↑(⇑free_abelian_group.lift_monoid f) = ⇑free_abelian_group.lift ⇑f

@[simp]

theorem free_abelian_group.lift_monoid_coe {α : Type u} {R : Type u_1} [monoid α] [ring R] (f : α →* R) :

⇑(⇑free_abelian_group.lift_monoid f) = ⇑(⇑free_abelian_group.lift ⇑f)

@[simp]

theorem free_abelian_group.lift_monoid_symm_coe {α : Type u} {R : Type u_1} [monoid α] [ring R] (f : free_abelian_group α →+* R) :

⇑(⇑(free_abelian_group.lift_monoid.symm) f) = ⇑(free_abelian_group.lift.symm) ↑f

theorem free_abelian_group.one_def {α : Type u} [monoid α] :

1 = free_abelian_group.of 1

theorem free_abelian_group.of_one {α : Type u} [monoid α] :

free_abelian_group.of 1 = 1

@[protected, instance]

def free_abelian_group.comm_ring (α : Type u) [comm_monoid α] :

comm_ring (free_abelian_group α)

Equations

free_abelian_group.comm_ring α = {add := ring.add (free_abelian_group.ring α), add_assoc := _, zero := ring.zero (free_abelian_group.ring α), zero_add := _, add_zero := _, nsmul := ring.nsmul (free_abelian_group.ring α), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (free_abelian_group.ring α), sub := ring.sub (free_abelian_group.ring α), sub_eq_add_neg := _, zsmul := ring.zsmul (free_abelian_group.ring α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (free_abelian_group.ring α), nat_cast := ring.nat_cast (free_abelian_group.ring α), one := ring.one (free_abelian_group.ring α), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul (free_abelian_group.ring α), mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow (free_abelian_group.ring α), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

@[protected, instance]

def free_abelian_group.pempty_unique :

unique (free_abelian_group pempty)

Equations

free_abelian_group.pempty_unique = {to_inhabited := {default := 0}, uniq := free_abelian_group.pempty_unique._proof_1}

def free_abelian_group.punit_equiv (T : Type u_1) [unique T] :

free_abelian_group T ≃+ ℤ

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

Equations

free_abelian_group.punit_equiv T = {to_fun := ⇑(⇑free_abelian_group.lift (λ (_x : T), 1)), inv_fun := λ (n : ℤ), n • free_abelian_group.of inhabited.default, left_inv := _, right_inv := _, map_add' := _}

def free_abelian_group.equiv_of_equiv {α : Type u_1} {β : Type u_2} (f : α ≃ β) :

free_abelian_group α ≃+ free_abelian_group β

Isomorphic types have isomorphic free abelian groups.

Equations

free_abelian_group.equiv_of_equiv f = {to_fun := ⇑(free_abelian_group.map ⇑f), inv_fun := ⇑(free_abelian_group.map ⇑(f.symm)), left_inv := _, right_inv := _, map_add' := _}