Descending a span from a ring of scalars to ℤ

Let b be a family in an A-module M that is linearly independent over the ring A, let L be the lattice of integer combinations of b, and let V ≤ L be a sublattice. Enlarging the coefficients of V from ℤ to A can only add elements outside L, provided ℤ · 1 is a direct summand of A, that is, provided some additive map t : A → ℤ has t 1 = 1: Submodule.span A V ∩ L = V (TauCeti.mem_of_mem_span_of_mem_closure).

The map t is applied to coordinates: on the A-span of b it sends ∑ aᵢ bᵢ to ∑ t(aᵢ) bᵢ; this fixes L pointwise and carries a • v to t(a) • v for v ∈ L. Without such a retraction the conclusion fails, as A = ℤ[1/2], V = 2L shows.

The standard source of a retraction is a power basis: the coordinate along gen ^ 0 = 1 is one (PowerBasis.exists_linearMap_apply_one). In particular it applies to A = ℤ[ζ] for a root of unity ζ in a field of characteristic zero, through Algebra.adjoin.powerBasis'. This is the descent step in Brauer's induction theorem, where a virtual character is first written as a combination of induced characters with coefficients in ℤ[ζ].

Main statements

• TauCeti.mem_of_mem_span_of_mem_closure: an integer combination of b that is an A-combination of elements of V is already in V.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), Chapter 10, in the proof of Theorem 18, where the case A = ℤ[ζ] is argued with a ℤ-basis of A containing 1.

theorem TauCeti.mem_of_mem_span_of_mem_closure {ι : Type u_1} {A : Type u_2} {M : Type u_3} [Ring A] [AddCommGroup M] [Module A M] {b : ι → M} (hb : LinearIndependent A b) (t : A →+ ℤ) (ht : t 1 = 1) {V : AddSubgroup M} (hV : V ≤ AddSubgroup.closure (Set.range b)) {f : M} (hf : f ∈ AddSubgroup.closure (Set.range b)) (hfA : f ∈ Submodule.span A ↑V) : f ∈ V

Descent of a span from A to ℤ. Let b be linearly independent over A, and let t : A → ℤ be additive with t 1 = 1. If V is an additive subgroup of the integer combinations of b, then an integer combination of b lying in the A-span of V already lies in V.