Vanishing of the lattice defect for finite modules

The difference between the reduction and torsion classes of a finite module is zero in the exact Grothendieck group, even though the two representations need not be isomorphic. Together with additivity, this is the finite-module input to invariance of lattice defects under inclusions with finite cokernel. The same argument shows invariance under inclusions whose cokernel is uniquely ℓ-divisible, such as ℤ[X] ⊆ ℤ_ℓ[X].

The coefficient ring and the acting monoid are arbitrary.

Main results

• TauCeti.latticeDefect_eq_zero_of_bijective_zsmul: a module on which multiplication by ℓ is bijective, such as a uniquely ℓ-divisible one, has zero defect.
• TauCeti.latticeDefect_eq_zero_of_finite: a finite module has zero defect.
• TauCeti.latticeDefect_eq_of_exact_of_finite and TauCeti.latticeDefect_eq_of_finiteIndex: an injective equivariant map with finite cokernel preserves the defect.
• TauCeti.latticeDefect_eq_of_bijective_zsmul_quotient: so does an injective equivariant map whose cokernel is uniquely ℓ-divisible.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, Section VII.3, (7.3.3).

theorem TauCeti.latticeDefect_eq_zero_of_isTorsionBy (k G : Type u) [CommRing k] [Monoid G] (ℓ : ℕ) (V : Type u) [AddCommGroup V] [DistribMulAction G V] [Finite V] (hV : Module.IsTorsionBy ℤ V ↑ℓ) : latticeDefect k G ℓ V = 0

A module killed by ℓ has zero lattice defect: both its ℓ-torsion and its reduction modulo ℓ are equivariantly isomorphic to the original module.

theorem TauCeti.latticeDefect_eq_zero_of_bijective_zsmul (k G : Type u) [CommRing k] [Monoid G] (ℓ : ℕ) (V : Type u) [AddCommGroup V] [DistribMulAction G V] (hV : Function.Bijective fun (x : V) => ↑ℓ • x) : latticeDefect k G ℓ V = 0

A module on which multiplication by ℓ is bijective has zero lattice defect: both its reduction modulo ℓ and its ℓ-torsion vanish. Bijectivity alone makes both of them trivial, hence finite, so no finiteness hypothesis is needed.

@[simp]

theorem TauCeti.latticeDefect_eq_zero_of_finite (k G : Type u) [CommRing k] [Monoid G] (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (V : Type u) [AddCommGroup V] [DistribMulAction G V] [Finite V] : latticeDefect k G ℓ V = 0

A finite module has zero lattice defect in the exact Grothendieck group. The torsion and reduction representations have the same class; no equivariant isomorphism is asserted.

theorem TauCeti.latticeDefect_eq_of_exact_of_finite (k G : Type u) [CommRing k] [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] [Finite 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 ↑ℓ)] : latticeDefect k G ℓ A = latticeDefect k G ℓ B

An inclusion with finite cokernel preserves the lattice defect. The short exact sequence is given by equivariant maps, so neither its source nor its middle term needs to be finite.

theorem TauCeti.latticeDefect_eq_of_finiteIndex (k G : Type u) [CommRing k] [Monoid G] (ℓ : ℕ) [Fact (Nat.Prime ℓ)] {W V : Type u} [AddCommGroup W] [DistribMulAction G W] [AddCommGroup V] [DistribMulAction G V] (f : W →+[G] V) (hf : Function.Injective ⇑f) [(↑f).range.FiniteIndex] [Finite (QuotSMulTop (↑ℓ) W)] [Finite ↥(Submodule.torsionBy ℤ W ↑ℓ)] [Finite (QuotSMulTop (↑ℓ) V)] [Finite ↥(Submodule.torsionBy ℤ V ↑ℓ)] : latticeDefect k G ℓ W = latticeDefect k G ℓ V

Finite index preserves the lattice defect: an injective equivariant map whose image has finite index does not change the defect. The cokernel is the quotient by the image, with the induced action.

theorem TauCeti.latticeDefect_eq_of_bijective_zsmul_quotient (k G : Type u) [CommRing k] [Monoid G] (ℓ : ℕ) [Fact (Nat.Prime ℓ)] {W V : Type u} [AddCommGroup W] [DistribMulAction G W] [AddCommGroup V] [DistribMulAction G V] (f : W →+[G] V) (hf : Function.Injective ⇑f) (h : Function.Bijective fun (x : V ⧸ (↑f).range) => ↑ℓ • x) [Finite (QuotSMulTop (↑ℓ) W)] [Finite ↥(Submodule.torsionBy ℤ W ↑ℓ)] [Finite (QuotSMulTop (↑ℓ) V)] [Finite ↥(Submodule.torsionBy ℤ V ↑ℓ)] : latticeDefect k G ℓ W = latticeDefect k G ℓ V

A uniquely ℓ-divisible cokernel preserves the lattice defect: an injective equivariant map whose cokernel is uniquely ℓ-divisible does not change the defect. The cokernel, which need not be finite, has zero defect (TauCeti.latticeDefect_eq_zero_of_bijective_zsmul).