Characters of a free abelian group

The free abelian group on an index type σ is modelled as Multiplicative (σ →₀ ℤ): its underlying additive group σ →₀ ℤ is the free ℤ-module on σ. This file records its universal property in the form most useful for the functor of points of a split torus: a homomorphism Multiplicative (σ →₀ ℤ) →* M to a commutative group M is the same data as a family σ → M, naturally and multiplicatively.

The equivalence sends a homomorphism χ to its values i ↦ χ (ofAdd (single i 1)) on the standard generators, and a family c : σ → M to the unique homomorphism extending it. This is the many-generator version of Mathlib's zpowersHom : M ≃ (Multiplicative ℤ →* M) (the case of one generator).

Main definitions

• TauCeti.freeAbelianCharEquiv: the multiplicative equivalence (Multiplicative (σ →₀ ℤ) →* M) ≃* (σ → M).

References

The construction reuses Mathlib's group-algebra-free toolkit: the Finsupp.liftAddHom universal property of σ →₀ ℤ, the ℤ-power homomorphism zmultiplesHom, and the type-tag adjunction AddMonoidHom.toMultiplicativeLeft from Mathlib.Algebra.Group.TypeTags.Hom.

The additive shadow of this equivalence is the R = ℤ case of Mathlib's Finsupp.lift : (σ → M) ≃+ ((σ →₀ ℤ) →ₗ[ℤ] M), transported across addMonoidHomLequivInt and the Multiplicative/Additive type-tag adjunctions. We build it directly from the same underlying pieces (Finsupp.liftAddHom and zmultiplesHom) rather than transporting that chain of isomorphisms so that the forward map is definitionally generator evaluation χ ↦ fun i => χ (ofAdd (single i 1)). That keeps freeAbelianCharEquiv_apply, map_mul', and freeAbelianCharEquiv_comp true by rfl; a transported equivalence would route every evaluation through the composite transport maps and lose that defeq.

noncomputable def TauCeti.freeAbelianCharEquiv {σ : Type u_1} {M : Type u_2} [CommGroup M] : (Multiplicative (σ →₀ ℤ) →* M) ≃* (σ → M)

The universal property of the free abelian group Multiplicative (σ →₀ ℤ): a homomorphism to a commutative group M is the same data as a family σ → M. The forward map reads off the values on the standard generators ofAdd (single i 1); the inverse extends a family to the unique homomorphism through Finsupp.liftAddHom and the ℤ-power homomorphism.

Equations

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

@[simp]

theorem TauCeti.freeAbelianCharEquiv_apply {σ : Type u_1} {M : Type u_2} [CommGroup M] (χ : Multiplicative (σ →₀ ℤ) →* M) (i : σ) : freeAbelianCharEquiv χ i = χ (Multiplicative.ofAdd (Finsupp.single i 1))

The forward direction of freeAbelianCharEquiv evaluates a character on the standard generator indexed by i.

theorem TauCeti.freeAbelianCharEquiv_symm_apply_ofAdd_single {σ : Type u_1} {M : Type u_2} [CommGroup M] (c : σ → M) (i : σ) : (freeAbelianCharEquiv.symm c) (Multiplicative.ofAdd (Finsupp.single i 1)) = c i

The inverse of freeAbelianCharEquiv sends the standard generator indexed by i to the chosen coordinate c i.

@[simp]

theorem TauCeti.freeAbelianCharEquiv_symm_apply_ofAdd {σ : Type u_1} {M : Type u_2} [CommGroup M] (c : σ → M) (m : σ →₀ ℤ) : (freeAbelianCharEquiv.symm c) (Multiplicative.ofAdd m) = m.prod fun (i : σ) (n : ℤ) => c i ^ n

The inverse of freeAbelianCharEquiv evaluates an arbitrary finitely supported integer combination as the corresponding product of powers of the chosen coordinates.

@[simp]

theorem TauCeti.freeAbelianCharEquiv_comp {σ : Type u_1} {M : Type u_2} [CommGroup M] {N : Type u_3} [CommGroup N] (ψ : M →* N) (χ : Multiplicative (σ →₀ ℤ) →* M) (i : σ) : freeAbelianCharEquiv (ψ.comp χ) i = ψ (freeAbelianCharEquiv χ i)

Reading off generator values is natural in the target group: post-composing with a homomorphism ψ : M →* N commutes with freeAbelianCharEquiv.