# 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/GrpCat/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`.

source
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 α))

Instances For

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

- FreeAbelianGroup.addCommGroup α = Additive.addCommGroup

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

- instInhabitedFreeAbelianGroup α = { default := 0 }

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

- instUniqueFreeAbelianGroupOfIsEmpty α = id inferInstance

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

The canonical map from `α` to `FreeAbelianGroup α`.

Equations

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

Instances For

source
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)

Instances For

source
@[simp]
theorem FreeAbelianGroup.lift_apply_of {α : Type u} {β : Type v} [AddCommGroup β] (f : α → β) (x : α) :
(lift f) (of x) = f x
source
@[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`.

source
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
source
@[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`.

source
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].

source
theorem FreeAbelianGroup.lift_ext_iff {α : Type u} {β : Type v} [AddCommGroup β] {g h : FreeAbelianGroup α →+ β} :
g = h ↔ ∀ (x : α), g (of x) = h (of x)
source
@[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].

source
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)
source
@[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
source
theorem FreeAbelianGroup.of_injective {α : Type u} :
Function.Injective of
source
@[simp]
theorem FreeAbelianGroup.of_ne_zero {α : Type u} (x : α) :
of x ≠ 0
source
@[simp]
theorem FreeAbelianGroup.zero_ne_of {α : Type u} (x : α) :
0 ≠ of x
source
instance FreeAbelianGroup.instNontrivialOfNonempty {α : Type u} [Nonempty α] :
Nontrivial (FreeAbelianGroup α)
source
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
source
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
source
@[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`.

source
@[simp]
theorem FreeAbelianGroup.lift_add {α : Type u} {G : Type u_1} [AddCommGroup G] (f g : α → G) :
lift (f + g) = lift f + lift g
source
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' := ⋯ }

Instances For

source
@[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))
source
@[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✝¹))
source
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) ⋯

Instances For

source
@[simp]
theorem FreeAbelianGroup.liftAddGroupHom_apply {α : Type u_2} (β : Type u_3) [AddCommGroup β] (a : FreeAbelianGroup α) (f : α → β) :
(liftAddGroupHom β a) f = (lift f) a
source
@[simp]
theorem FreeAbelianGroup.lift_neg {α : Type u} {G : Type u_1} [AddCommGroup G] (f : α → G) :
lift (-f) = -lift f
source
theorem FreeAbelianGroup.lift_neg_apply {α : Type u} {G : Type u_1} [AddCommGroup G] (f : α → G) (a : FreeAbelianGroup α) :
(lift (-f)) a = -(lift f) a
source
@[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`.

source
instance FreeAbelianGroup.instMonad :
Monad FreeAbelianGroup
Equations

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

source
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
source
@[simp]
theorem FreeAbelianGroup.map_pure {α β : Type u} (f : α → β) (x : α) :
f <$> pure x = pure (f x)
source
@[simp]
theorem FreeAbelianGroup.map_zero {α β : Type u} (f : α → β) :
f <$> 0 = 0
source
@[simp]
theorem FreeAbelianGroup.map_add {α β : Type u} (f : α → β) (x y : FreeAbelianGroup α) :
f <$> (x + y) = f <$> x + f <$> y
source
@[simp]
theorem FreeAbelianGroup.map_neg {α β : Type u} (f : α → β) (x : FreeAbelianGroup α) :
f <$> (-x) = -f <$> x
source
@[simp]
theorem FreeAbelianGroup.map_sub {α β : Type u} (f : α → β) (x y : FreeAbelianGroup α) :
f <$> (x - y) = f <$> x - f <$> y
source
@[simp]
theorem FreeAbelianGroup.map_of {α β : Type u} (f : α → β) (y : α) :
f <$> of y = of (f y)
source
theorem FreeAbelianGroup.pure_bind {α β : Type u} (f : α → FreeAbelianGroup β) (x : α) :
pure x >>= f = f x
source
@[simp]
theorem FreeAbelianGroup.zero_bind {α β : Type u} (f : α → FreeAbelianGroup β) :
0 >>= f = 0
source
@[simp]
theorem FreeAbelianGroup.add_bind {α β : Type u} (f : α → FreeAbelianGroup β) (x y : FreeAbelianGroup α) :
x + y >>= f = (x >>= f) + (y >>= f)
source
@[simp]
theorem FreeAbelianGroup.neg_bind {α β : Type u} (f : α → FreeAbelianGroup β) (x : FreeAbelianGroup α) :
-x >>= f = -(x >>= f)
source
@[simp]
theorem FreeAbelianGroup.sub_bind {α β : Type u} (f : α → FreeAbelianGroup β) (x y : FreeAbelianGroup α) :
x - y >>= f = (x >>= f) - (y >>= f)
source
@[simp]
theorem FreeAbelianGroup.pure_seq {α β : Type u} (f : α → β) (x : FreeAbelianGroup α) :
pure f <*> x = f <$> x
source
@[simp]
theorem FreeAbelianGroup.zero_seq {α β : Type u} (x : FreeAbelianGroup α) :
0 <*> x = 0
source
@[simp]
theorem FreeAbelianGroup.add_seq {α β : Type u} (f g : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) :
f + g <*> x = (f <*> x) + (g <*> x)
source
@[simp]
theorem FreeAbelianGroup.neg_seq {α β : Type u} (f : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) :
-f <*> x = -(f <*> x)
source
@[simp]
theorem FreeAbelianGroup.sub_seq {α β : Type u} (f g : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) :
f - g <*> x = (f <*> x) - (g <*> x)
source
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) ⋯

Instances For

source
@[simp]
theorem FreeAbelianGroup.seq_zero {α β : Type u} (f : FreeAbelianGroup (α → β)) :
f <*> 0 = 0
source
@[simp]
theorem FreeAbelianGroup.seq_add {α β : Type u} (f : FreeAbelianGroup (α → β)) (x y : FreeAbelianGroup α) :
f <*> x + y = (f <*> x) + (f <*> y)
source
@[simp]
theorem FreeAbelianGroup.seq_neg {α β : Type u} (f : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) :
f <*> -x = -(f <*> x)
source
@[simp]
theorem FreeAbelianGroup.seq_sub {α β : Type u} (f : FreeAbelianGroup (α → β)) (x y : FreeAbelianGroup α) :
f <*> x - y = (f <*> x) - (f <*> y)
source
instance FreeAbelianGroup.instLawfulMonad :
LawfulMonad FreeAbelianGroup
source
instance FreeAbelianGroup.instCommApplicative :
CommApplicative FreeAbelianGroup
source
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)

Instances For

source
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)
source
theorem FreeAbelianGroup.map_id {α : Type u} :
map id = AddMonoidHom.id (FreeAbelianGroup α)
source
theorem FreeAbelianGroup.map_id_apply {α : Type u} (x : FreeAbelianGroup α) :
(map id) x = x
source
theorem FreeAbelianGroup.map_comp {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} :
map (g ∘ f) = (map g).comp (map f)
source
theorem FreeAbelianGroup.map_comp_apply {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} (x : FreeAbelianGroup α) :
(map (g ∘ f)) x = (map g) ((map f) x)
source
@[simp]
theorem FreeAbelianGroup.map_of_apply {α : Type u} {β : Type v} {f : α → β} (a : α) :
(map f) (of a) = of (f a)
source
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) }

source
theorem FreeAbelianGroup.mul_def {α : Type u} [Mul α] (x y : FreeAbelianGroup α) :
x * y = (lift fun (x₂ : α) => (lift fun (x₁ : α) => of (x₁ * x₂)) x) y
source
@[simp]
theorem FreeAbelianGroup.of_mul_of {α : Type u} [Mul α] (x y : α) :
of x * of y = of (x * y)
source
theorem FreeAbelianGroup.of_mul {α : Type u} [Mul α] (x y : α) :
of (x * y) = of x * of y
source
instance FreeAbelianGroup.distrib {α : Type u} [Mul α] :
Distrib (FreeAbelianGroup α)
Equations

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

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

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

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

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

source
theorem FreeAbelianGroup.one_def (α : Type u) [One α] :
1 = of 1
source
theorem FreeAbelianGroup.of_one (α : Type u) [One α] :
of 1 = 1
source
instance FreeAbelianGroup.nonUnitalRing (α : Type u) [Semigroup α] :
NonUnitalRing (FreeAbelianGroup α)
Equations

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

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

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

source
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' := ⋯ }

Instances For

source
@[simp]
theorem FreeAbelianGroup.ofMulHom_coe {α : Type u} [Monoid α] :
⇑ofMulHom = of
source
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.

Instances For

source
@[simp]
theorem FreeAbelianGroup.liftMonoid_coe_addMonoidHom {α : Type u} {R : Type u_2} [Monoid α] [Ring R] (f : α →* R) :
↑(liftMonoid f) = lift ⇑f
source
@[simp]
theorem FreeAbelianGroup.liftMonoid_coe {α : Type u} {R : Type u_2} [Monoid α] [Ring R] (f : α →* R) :
⇑(liftMonoid f) = ⇑(lift ⇑f)
source
@[simp]
theorem FreeAbelianGroup.liftMonoid_symm_coe {α : Type u} {R : Type u_2} [Monoid α] [Ring R] (f : FreeAbelianGroup α →+* R) :
⇑(liftMonoid.symm f) = lift.symm ↑f
source
instance FreeAbelianGroup.instCommRingOfCommMonoid (α : Type u) [CommMonoid α] :
CommRing (FreeAbelianGroup α)
Equations

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

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

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

source
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' := ⋯ }

Instances For

source
@[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

Instances For

source
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' := ⋯ }

Instances For