Reduction classes and the lattice defect of a G-module

Let G be a monoid and k a commutative ring, typically a field. A representation ρ of G on an abelian group W has a reduction k ⊗_ℤ W, with G acting on the second factor (Representation.baseChange). When it is finitely generated over k, for instance because W is a finitely generated abelian group, it has a class

TauCeti.reductionK0 k ρ = [k ⊗_ℤ W] ∈ G₀(k[G])

in the exact Grothendieck group of finitely generated k[G]-modules.

For a G-module V (an abelian group with a distributive G-action) and a natural number ℓ such that V ⧸ ℓV and the ℓ-torsion V[ℓ] are finite, the lattice defect is

TauCeti.latticeDefect k G ℓ V = [k ⊗_ℤ (V ⧸ ℓV)] - [k ⊗_ℤ V[ℓ]] ∈ G₀(k[G]).

Here V ⧸ ℓV is QuotSMulTop ℓ V and V[ℓ] is Submodule.torsionBy ℤ V ℓ, with the G-actions Representation.quotSMulTop and Representation.torsionBy. At k = 𝔽_ℓ the defect is [V ⧸ ℓV] - [V[ℓ]], the invariant of Neukirch–Schmidt–Wingberg (7.3.3).

Its main property is additivity (TauCeti.latticeDefect_add_of_exact): for a prime ℓ and a short exact sequence 0 → A → B → C → 0 of G-modules, the defect of B is the sum of the defects of A and C. The snake lemma for multiplication by ℓ gives the six-term exact sequence of representations

0 → A[ℓ] → B[ℓ] → C[ℓ] → A ⧸ ℓA → B ⧸ ℓB → C ⧸ ℓC → 0

(Representation.IntertwiningMap.torsionByδ). Every term is killed by ℓ, so tensoring over ℤ with k keeps it exact, although k need not be flat over ℤ (TauCeti.lTensor_exact_of_isTorsionBy). Along a six-term exact sequence of finitely generated k[G]-modules the odd-indexed and even-indexed classes have the same sum (TauCeti.exactK0_add_add_eq_add_add_of_exact), and the six classes regroup into the three defects. Neither the characteristic of k nor finiteness of G is used.

Main definitions

• TauCeti.reductionK0: the class in G₀(k[G]) of the reduction k ⊗_ℤ W.
• TauCeti.latticeDefect: the class [k ⊗_ℤ (V ⧸ ℓV)] - [k ⊗_ℤ V[ℓ]].

Main results

• TauCeti.reductionK0_congr: equivalent representations have equal reduction classes.
• TauCeti.reductionK0_quotSMulTop: in characteristic ℓ, the reduction class of W ⧸ ℓW is that of W.
• TauCeti.latticeDefect_eq_reductionK0_sub: in characteristic ℓ, the lattice defect is [k ⊗_ℤ V] - [k ⊗_ℤ V[ℓ]].
• TauCeti.latticeDefect_add_of_exact: additivity of the lattice defect.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), §VII.3, (7.3.3).

The reduction class

instance TauCeti.instModuleFiniteAsModuleBaseChange (k : Type u) [CommRing k] {G : Type u} [Monoid G] {W : Type u} [AddCommGroup W] [Module ℤ W] [Module.Finite k (TensorProduct ℤ k W)] (ρ : Representation ℤ G W) : Module.Finite (MonoidAlgebra k G) (Representation.baseChange k ρ).asModule

The module of a reduction k ⊗_ℤ W that is finitely generated over k, for instance because W is a finitely generated abelian group, is finitely generated over k[G].

noncomputable def TauCeti.reductionK0 (k : Type u) [CommRing k] {G : Type u} [Monoid G] {W : Type u} [AddCommGroup W] [Module ℤ W] [Module.Finite k (TensorProduct ℤ k W)] (ρ : Representation ℤ G W) : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))

The reduction class of a representation ρ of G on an abelian group W whose reduction k ⊗_ℤ W is finitely generated over k, for instance because W is finitely generated: the class in G₀(k[G]) of its scalar extension k ⊗_ℤ W, with G acting on the second factor.

theorem TauCeti.reductionK0_def (k : Type u) [CommRing k] {G : Type u} [Monoid G] {W : Type u} [AddCommGroup W] [Module ℤ W] [Module.Finite k (TensorProduct ℤ k W)] (ρ : Representation ℤ G W) : reductionK0 k ρ = ExactK0.of ↧(Representation.baseChange k ρ).asModule

The reduction class is the class of the k[G]-module of the base-changed representation.

theorem TauCeti.reductionK0_congr_baseChange (k : Type u) [CommRing k] {G : Type u} [Monoid G] {W : Type u} [AddCommGroup W] [Module ℤ W] [Module.Finite k (TensorProduct ℤ k W)] {W' : Type u} [AddCommGroup W'] [Module ℤ W'] [Module.Finite k (TensorProduct ℤ k W')] {ρ : Representation ℤ G W} {σ : Representation ℤ G W'} (e : (Representation.baseChange k ρ).Equiv (Representation.baseChange k σ)) : reductionK0 k ρ = reductionK0 k σ

Equivalent scalar extensions have equal reduction classes.

theorem TauCeti.reductionK0_congr (k : Type u) [CommRing k] {G : Type u} [Monoid G] {W : Type u} [AddCommGroup W] [Module ℤ W] [Module.Finite k (TensorProduct ℤ k W)] {W' : Type u} [AddCommGroup W'] [Module ℤ W'] [Module.Finite k (TensorProduct ℤ k W')] {ρ : Representation ℤ G W} {σ : Representation ℤ G W'} (e : ρ.Equiv σ) : reductionK0 k ρ = reductionK0 k σ

Equivalent representations have equal reduction classes.

@[simp]

theorem TauCeti.reductionK0_eq_zero_of_subsingleton (k : Type u) [CommRing k] {G : Type u} [Monoid G] {W : Type u} [AddCommGroup W] [Module ℤ W] [Module.Finite k (TensorProduct ℤ k W)] [Subsingleton W] (ρ : Representation ℤ G W) : reductionK0 k ρ = 0

The reduction class of a zero module is zero.

theorem TauCeti.reductionK0_quotSMulTop (k : Type u) [CommRing k] {G : Type u} [Monoid G] (ℓ : ℕ) [CharP k ℓ] {W : Type u} [AddCommGroup W] [Module ℤ W] [Module.Finite k (TensorProduct ℤ k (QuotSMulTop (↑ℓ) W))] (ρ : Representation ℤ G W) : reductionK0 k (ρ.quotSMulTop ↑ℓ) = reductionK0 k ρ

The reduction of W ⧸ ℓW is that of W in characteristic ℓ: the reduction classes of ρ.quotSMulTop ℓ and of ρ agree. Here k ⊗_ℤ W is finitely generated over k as soon as k ⊗_ℤ (W ⧸ ℓW) is, even when W is not.

The six-term sequence of reductions

The lattice defect

noncomputable def TauCeti.latticeDefect (k : Type u) [CommRing k] (G : Type u) [Monoid G] (ℓ : ℕ) (V : Type u) [AddCommGroup V] [DistribMulAction G V] [Finite (QuotSMulTop (↑ℓ) V)] [Finite ↥(Submodule.torsionBy ℤ V ↑ℓ)] : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))

The lattice defect [k ⊗_ℤ (V ⧸ ℓV)] - [k ⊗_ℤ V[ℓ]] of a G-module V with V ⧸ ℓV and V[ℓ] finite, in G₀(k[G]). At k = 𝔽_ℓ it is [V ⧸ ℓV] - [V[ℓ]]; it is additive in short exact sequences (TauCeti.latticeDefect_add_of_exact).

theorem TauCeti.latticeDefect_def (k : Type u) [CommRing k] (G : Type u) [Monoid G] (ℓ : ℕ) (V : Type u) [AddCommGroup V] [DistribMulAction G V] [Finite (QuotSMulTop (↑ℓ) V)] [Finite ↥(Submodule.torsionBy ℤ V ↑ℓ)] : latticeDefect k G ℓ V = reductionK0 k ((Representation.ofDistribMulAction ℤ G V).quotSMulTop ↑ℓ) - reductionK0 k ((Representation.ofDistribMulAction ℤ G V).torsionBy ↑ℓ)

The lattice defect is the difference of the reduction classes of V ⧸ ℓV and of V[ℓ].

theorem TauCeti.latticeDefect_eq_reductionK0_sub (k : Type u) [CommRing k] (G : Type u) [Monoid G] (ℓ : ℕ) [CharP k ℓ] (V : Type u) [AddCommGroup V] [DistribMulAction G V] [Finite (QuotSMulTop (↑ℓ) V)] [Finite ↥(Submodule.torsionBy ℤ V ↑ℓ)] : latticeDefect k G ℓ V = reductionK0 k (Representation.ofDistribMulAction ℤ G V) - reductionK0 k ((Representation.ofDistribMulAction ℤ G V).torsionBy ↑ℓ)

The lattice defect is [k ⊗_ℤ V] - [k ⊗_ℤ V[ℓ]] in characteristic ℓ: the reduction of V ⧸ ℓV in the definition of TauCeti.latticeDefect may be replaced by the reduction of V itself, which is then finitely generated over k (TauCeti.finite_baseChange_of_finite_quotSMulTop).

theorem TauCeti.latticeDefect_add_of_exact (k : Type u) [CommRing k] (G : Type u) [Monoid G] (ℓ : ℕ) [Fact (Nat.Prime ℓ)] {A B C : Type u} [AddCommGroup A] [DistribMulAction G A] [AddCommGroup B] [DistribMulAction G B] [AddCommGroup C] [DistribMulAction G C] (f : A →+[G] B) (g : B →+[G] C) (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) [Finite (QuotSMulTop (↑ℓ) A)] [Finite ↥(Submodule.torsionBy ℤ A ↑ℓ)] [Finite (QuotSMulTop (↑ℓ) B)] [Finite ↥(Submodule.torsionBy ℤ B ↑ℓ)] [Finite (QuotSMulTop (↑ℓ) C)] [Finite ↥(Submodule.torsionBy ℤ C ↑ℓ)] : latticeDefect k G ℓ B = latticeDefect k G ℓ A + latticeDefect k G ℓ C

Additivity of the lattice defect (Neukirch–Schmidt–Wingberg (7.3.3)): for a short exact sequence 0 → A → B → C → 0 of G-modules whose reductions modulo ℓ and ℓ-torsion are finite, the defect of B is the sum of the defects of A and C.