Injective maps between free abelian groups of equal rank

An injective ℤ-linear map f : M → N into a finitely generated free abelian group of the same rank has image of finite index c, so c • y lies in the image of f for every y : N. Dividing by f gives a map g : N → M such that f ∘ g and g ∘ f are both multiplication by c: an inverse of f up to a nonzero scalar. Over ℚ the map f becomes invertible with inverse c⁻¹ • g; over ℤ an inverse up to a scalar is the best available.

The index of the image is the absolute value of the determinant of f in any bases of M and N indexed by the same type.

Main results

• LinearMap.exists_comp_eq_nsmul_id_of_injective: an injective map between finitely generated free abelian groups of equal rank has an inverse up to multiplication by a nonzero natural number.
• LinearMap.index_range_eq_natAbs_det_toMatrix: the index of the image of such a map is the absolute value of the determinant of its matrix.

theorem LinearMap.exists_comp_eq_nsmul_id_of_injective {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] [Module.Free ℤ N] [Module.Finite ℤ N] {f : M →ₗ[ℤ] N} (hf : Function.Injective ⇑f) (hrank : Module.finrank ℤ M = Module.finrank ℤ N) : ∃ (c : ℕ), c ≠ 0 ∧ ∃ (g : N →ₗ[ℤ] M), f ∘ₗ g = c • id ∧ g ∘ₗ f = c • id

An injective ℤ-linear map into a finitely generated free abelian group of the same rank has an inverse up to multiplication by a nonzero natural number c, namely the index of its image.

theorem LinearMap.index_range_eq_natAbs_det_toMatrix {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ M) (c : Module.Basis ι ℤ N) {f : M →ₗ[ℤ] N} (hf : Function.Injective ⇑f) : f.range.toAddSubgroup.index = ((toMatrix b c) f).det.natAbs

The index of the image of an injective map is the absolute value of its determinant: for bases b of M and c of N indexed by the same finite type, the image of an injective ℤ-linear map f : M → N has index |det (toMatrix b c f)|.