Orders of the kernel and cokernel of multiplication by a scalar

Let r be an element of a commutative ring R. For an R-module M write M[r] for the r-torsion Submodule.torsionBy R M r and M ⧸ rM for QuotSMulTop r M, the kernel and the cokernel of multiplication by r. When both are finite, the Euler quotient

χ_r(M) = #(M ⧸ rM) / #M[r]

is the Herbrand quotient of the pair of commuting endomorphisms (0, r) of M. This file proves its three basic properties:

• it is 1 on a finite module: #(M ⧸ rM) = #M[r] when M is finite;
• it is multiplicative along a short exact sequence 0 → M₁ → M₂ → M₃ → 0, by counting along the six-term kernel–cokernel sequence TauCeti.torsionByδ of the snake lemma;
• hence it is unchanged by a linear map with finite kernel and cokernel, which factors through its image as a surjection with finite kernel followed by an injection with finite cokernel.

The counting statements are stated for Nat.card with no finiteness hypothesis beyond the one that makes them true, so an infinite kernel or cokernel contributes the factor 0; the rational forms divide them out. A map with finite kernel and cokernel moreover preserves the finiteness of the kernel and of the cokernel of multiplication by r.

Over the Iwasawa algebra Λ = O⟦T⟧ the maps with finite kernel and cokernel are the pseudo-isomorphisms, and r is typically ω_n = (1 + T) ^ pⁿ - 1, for which M ⧸ ω_n M and M[ω_n] are the coinvariants and the invariants of the subgroup of index pⁿ of Γ ≅ ℤ_p. The invariance is what lets the Euler quotient #(M ⧸ ω_n M) / #M[ω_n] be computed on an elementary module, and the finiteness of M ⧸ ω_n M and of M[ω_n] be read off there; the individual orders need not agree.

Main results

• TauCeti.natCard_quotSMulTop_eq_natCard_torsionBy: #(M ⧸ rM) = #M[r] for finite M.
• TauCeti.natCard_torsionBy_mul_natCard_quotSMulTop_of_exact: the count along the six-term sequence of a short exact sequence, #M₁[r] #M₃[r] #(M₂ ⧸ rM₂) = #M₂[r] #(M₁ ⧸ rM₁) #(M₃ ⧸ rM₃).
• TauCeti.natCard_quotSMulTop_div_natCard_torsionBy_of_exact: multiplicativity of the Euler quotient, when the outer torsion groups are finite.
• TauCeti.natCard_quotSMulTop_mul_natCard_torsionBy_of_exact_of_finite_left and TauCeti.natCard_quotSMulTop_mul_natCard_torsionBy_of_exact_of_finite_right: a finite outer term of a short exact sequence may be discarded.
• TauCeti.finite_torsionBy_iff_of_finite_ker_of_finite_coker, TauCeti.finite_quotSMulTop_iff_of_finite_ker_of_finite_coker and TauCeti.natCard_quotSMulTop_div_natCard_torsionBy_eq_of_finite_ker_of_finite_coker: a linear map with finite kernel and cokernel preserves the finiteness of M[r] and of M ⧸ rM, and the Euler quotient.

References

• J.-P. Serre, Local Fields, Chapter VIII, §4, for the Herbrand quotient and its multiplicativity and invariance.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, Chapter V, §3, (5.3.11)–(5.3.16), for the invariants and coinvariants of Iwasawa modules.

theorem TauCeti.natCard_quotSMulTop_eq_natCard_torsionBy {R : Type u_1} [CommRing R] (r : R) {M : Type u_2} [AddCommGroup M] [Module R M] [Finite M] : Nat.card (QuotSMulTop r M) = Nat.card ↥(Submodule.torsionBy R M r)

The Euler quotient of a finite module is 1: for a finite module M, the cokernel and the kernel of multiplication by r have the same order, #(M ⧸ rM) = #M[r].

theorem TauCeti.natCard_torsionBy_mul_natCard_quotSMulTop_of_exact {R : Type u_1} [CommRing R] (r : R) {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : Nat.card ↥(Submodule.torsionBy R M₁ r) * Nat.card ↥(Submodule.torsionBy R M₃ r) * Nat.card (QuotSMulTop r M₂) = Nat.card ↥(Submodule.torsionBy R M₂ r) * Nat.card (QuotSMulTop r M₁) * Nat.card (QuotSMulTop r M₃)

The count along the kernel–cokernel sequence. For a short exact sequence 0 → M₁ → M₂ → M₃ → 0, the six-term sequence 0 → M₁[r] → M₂[r] → M₃[r] → M₁ ⧸ rM₁ → M₂ ⧸ rM₂ → M₃ ⧸ rM₃ → 0 gives #M₁[r] #M₃[r] #(M₂ ⧸ rM₂) = #M₂[r] #(M₁ ⧸ rM₁) #(M₃ ⧸ rM₃). No finiteness is assumed: an infinite group contributes the factor 0 to both sides.

theorem TauCeti.natCard_quotSMulTop_div_natCard_torsionBy_of_exact {R : Type u_1} [CommRing R] (r : R) {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) [Finite ↥(Submodule.torsionBy R M₁ r)] [Finite ↥(Submodule.torsionBy R M₃ r)] : ↑(Nat.card (QuotSMulTop r M₂)) / ↑(Nat.card ↥(Submodule.torsionBy R M₂ r)) = ↑(Nat.card (QuotSMulTop r M₁)) / ↑(Nat.card ↥(Submodule.torsionBy R M₁ r)) * (↑(Nat.card (QuotSMulTop r M₃)) / ↑(Nat.card ↥(Submodule.torsionBy R M₃ r)))

Multiplicativity of the Euler quotient along a short exact sequence 0 → M₁ → M₂ → M₃ → 0 whose outer terms have finite r-torsion: χ_r(M₂) = χ_r(M₁) χ_r(M₃). The cokernels are unconstrained: if one of them is infinite, both sides are 0.

theorem TauCeti.finite_torsionBy_iff_of_exact_of_finite_left {R : Type u_1} [CommRing R] (r : R) {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} [Finite M₁] (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : Finite ↥(Submodule.torsionBy R M₂ r) ↔ Finite ↥(Submodule.torsionBy R M₃ r)

If M₁ is finite in a short exact sequence 0 → M₁ → M₂ → M₃ → 0, then M₂[r] is finite iff M₃[r] is.

theorem TauCeti.finite_quotSMulTop_iff_of_exact_of_finite_left {R : Type u_1} [CommRing R] (r : R) {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} [Finite M₁] (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) : Finite (QuotSMulTop r M₂) ↔ Finite (QuotSMulTop r M₃)

If M₁ is finite in a short exact sequence 0 → M₁ → M₂ → M₃ → 0, then M₂ ⧸ rM₂ is finite iff M₃ ⧸ rM₃ is.

theorem TauCeti.finite_torsionBy_iff_of_exact_of_finite_right {R : Type u_1} [CommRing R] (r : R) {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} [Finite M₃] (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) : Finite ↥(Submodule.torsionBy R M₁ r) ↔ Finite ↥(Submodule.torsionBy R M₂ r)

If M₃ is finite in a short exact sequence 0 → M₁ → M₂ → M₃ → 0, then M₁[r] is finite iff M₂[r] is.

theorem TauCeti.finite_quotSMulTop_iff_of_exact_of_finite_right {R : Type u_1} [CommRing R] (r : R) {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} [Finite M₃] (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : Finite (QuotSMulTop r M₁) ↔ Finite (QuotSMulTop r M₂)

If M₃ is finite in a short exact sequence 0 → M₁ → M₂ → M₃ → 0, then M₁ ⧸ rM₁ is finite iff M₂ ⧸ rM₂ is.

theorem TauCeti.natCard_quotSMulTop_mul_natCard_torsionBy_of_exact_of_finite_left {R : Type u_1} [CommRing R] (r : R) {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} [Finite M₁] (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : Nat.card (QuotSMulTop r M₂) * Nat.card ↥(Submodule.torsionBy R M₃ r) = Nat.card (QuotSMulTop r M₃) * Nat.card ↥(Submodule.torsionBy R M₂ r)

A finite first term may be discarded: if M₁ is finite in a short exact sequence 0 → M₁ → M₂ → M₃ → 0, then #(M₂ ⧸ rM₂) #M₃[r] = #(M₃ ⧸ rM₃) #M₂[r], that is χ_r(M₂) = χ_r(M₃) once the torsion groups are finite.

theorem TauCeti.natCard_quotSMulTop_mul_natCard_torsionBy_of_exact_of_finite_right {R : Type u_1} [CommRing R] (r : R) {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f : M₁ →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} [Finite M₃] (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : Nat.card (QuotSMulTop r M₁) * Nat.card ↥(Submodule.torsionBy R M₂ r) = Nat.card (QuotSMulTop r M₂) * Nat.card ↥(Submodule.torsionBy R M₁ r)

A finite last term may be discarded: if M₃ is finite in a short exact sequence 0 → M₁ → M₂ → M₃ → 0, then #(M₁ ⧸ rM₁) #M₂[r] = #(M₂ ⧸ rM₂) #M₁[r], that is χ_r(M₁) = χ_r(M₂) once the torsion groups are finite.

theorem TauCeti.finite_torsionBy_iff_of_finite_ker_of_finite_coker {R : Type u_1} [CommRing R] (r : R) {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (φ : M →ₗ[R] N) [Finite ↥φ.ker] [Finite (N ⧸ φ.range)] : Finite ↥(Submodule.torsionBy R M r) ↔ Finite ↥(Submodule.torsionBy R N r)

A linear map with finite kernel and cokernel preserves the finiteness of the r-torsion: M[r] is finite iff N[r] is.

theorem TauCeti.finite_quotSMulTop_iff_of_finite_ker_of_finite_coker {R : Type u_1} [CommRing R] (r : R) {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (φ : M →ₗ[R] N) [Finite ↥φ.ker] [Finite (N ⧸ φ.range)] : Finite (QuotSMulTop r M) ↔ Finite (QuotSMulTop r N)

A linear map with finite kernel and cokernel preserves the finiteness of the cokernel of multiplication by r: M ⧸ rM is finite iff N ⧸ rN is.

theorem TauCeti.natCard_quotSMulTop_mul_natCard_torsionBy_of_finite_ker_of_finite_coker {R : Type u_1} [CommRing R] (r : R) {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (φ : M →ₗ[R] N) [Finite ↥φ.ker] [Finite (N ⧸ φ.range)] : Nat.card (QuotSMulTop r M) * Nat.card ↥(Submodule.torsionBy R N r) = Nat.card (QuotSMulTop r N) * Nat.card ↥(Submodule.torsionBy R M r)

Invariance of the Euler quotient, counted. For a linear map φ : M → N with finite kernel and cokernel, #(M ⧸ rM) #N[r] = #(N ⧸ rN) #M[r]. No finiteness of the torsion groups is assumed: M[r] and N[r] are finite or infinite together, and in the infinite case both sides are 0.

theorem TauCeti.natCard_quotSMulTop_div_natCard_torsionBy_eq_of_finite_ker_of_finite_coker {R : Type u_1} [CommRing R] (r : R) {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (φ : M →ₗ[R] N) [Finite ↥φ.ker] [Finite (N ⧸ φ.range)] : ↑(Nat.card (QuotSMulTop r M)) / ↑(Nat.card ↥(Submodule.torsionBy R M r)) = ↑(Nat.card (QuotSMulTop r N)) / ↑(Nat.card ↥(Submodule.torsionBy R N r))

Invariance of the Euler quotient: a linear map φ : M → N with finite kernel and cokernel satisfies χ_r(M) = χ_r(N), that is #(M ⧸ rM) / #M[r] = #(N ⧸ rN) / #N[r]. No finiteness is assumed: when the torsion groups are infinite, both sides are 0.