The index of the image of an endomorphism of a free module over a PID

Let R be a principal ideal domain and f an endomorphism of a finite free R-module M with nonzero determinant. Then M ⧸ range f has as many elements as R ⧸ (det f). The Smith normal form of range f inside M splits the quotient into the residue rings R ⧸ (aᵢ) of the diagonal coefficients, whose product is associated to det f, and the cardinality of a quotient of a Dedekind domain is multiplicative in the ideal.

This is the principal ideal domain form of Mathlib's Submodule.natAbs_det_equiv and AddSubgroup.index_eq_natAbs_det, where R = ℤ and Nat.card (ℤ ⧸ (d)) = |d|. Over a discrete valuation ring, when the determinant is associated to ϖ ^ k for a uniformizer ϖ, the quotient has q ^ k elements, where q is the cardinality of the residue field: this is the lattice index behind the scaling law of Haar measure under linear maps of Kⁿ for a non-archimedean local field K. No finiteness of the residue field is needed; when it is infinite both sides are 0 for k ≠ 0.

Main results

• LinearMap.card_quotient_range_eq_card_quotient_span_det: for det f ≠ 0, Nat.card (M ⧸ range f) = Nat.card (R ⧸ Ideal.span {det f}).
• Matrix.card_quotient_range_mulVecLin_eq_card_quotient_span_det: the same for a square matrix acting on ι → R.
• Matrix.card_quotient_range_mulVecLin_eq_pow: over a discrete valuation ring, if det A is associated to ϖ ^ k for a uniformizer ϖ, the quotient has q ^ k elements.
• LinearMap.infinite_quotient_range_of_det_eq_zero: over an infinite domain, if det f = 0 then M ⧸ range f is infinite.

theorem LinearMap.card_quotient_range_eq_card_quotient_span_det {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {f : M →ₗ[R] M} (hf : LinearMap.det f ≠ 0) : Nat.card (M ⧸ f.range) = Nat.card (R ⧸ Ideal.span {LinearMap.det f})

The index of the image of an endomorphism of a finite free module over a principal ideal domain is that of the principal ideal generated by its determinant, provided the determinant is nonzero.

theorem LinearMap.infinite_quotient_range_of_det_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [Infinite R] {f : M →ₗ[R] M} (hf : LinearMap.det f = 0) : Infinite (M ⧸ f.range)

An endomorphism with vanishing determinant has infinite cokernel. Over an infinite domain, if det f = 0 then M ⧸ range f is infinite. Together with card_quotient_range_eq_card_quotient_span_det, over an infinite principal ideal domain the cokernel of f is finite exactly when det f ≠ 0 and R ⧸ (det f) is finite.

theorem Matrix.card_quotient_range_mulVecLin_eq_card_quotient_span_det {R : Type u_1} {ι : Type u_2} [CommRing R] [IsDomain R] [Fintype ι] [DecidableEq ι] [IsPrincipalIdealRing R] {A : Matrix ι ι R} (hA : A.det ≠ 0) : Nat.card ((ι → R) ⧸ A.mulVecLin.range) = Nat.card (R ⧸ Ideal.span {A.det})

The index of the image lattice of a square matrix over a principal ideal domain with nonzero determinant is that of the principal ideal generated by its determinant.

theorem Matrix.card_quotient_range_mulVecLin_eq_pow {R : Type u_1} {ι : Type u_2} [CommRing R] [IsDomain R] [Fintype ι] [DecidableEq ι] [IsDiscreteValuationRing R] {A : Matrix ι ι R} {ϖ : R} (hϖ : Irreducible ϖ) {k : ℕ} (hk : Associated A.det (ϖ ^ k)) : Nat.card ((ι → R) ⧸ A.mulVecLin.range) = Nat.card (IsLocalRing.ResidueField R) ^ k

The index of an image lattice over a discrete valuation ring. For a square matrix A over a discrete valuation ring whose determinant is associated to ϖ ^ k for a uniformizer ϖ, the integer box ι → R modulo the image of A has q ^ k elements, where q is the cardinality of the residue field.