Cardinal of quotient of free finite ℤ-modules by submodules of full rank

Main results

• Submodule.natAbs_det_basis_change: let b be a ℤ-basis for a module M over ℤ and let bN be a basis for a submodule N of the same dimension. Then the cardinal of M ⧸ N is given by taking the determinant of bN over b.

theorem Submodule.natAbs_det_equiv {M : Type u_1} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (N : Submodule ℤ M) {E : Type u_2} [EquivLike E M ↥N] [AddEquivClass E M ↥N] (e : E) : (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)

Let e : M ≃ N be an additive isomorphism (therefore a ℤ-linear equiv). Then an alternative way to compute the cardinality of the quotient M ⧸ N is given by taking the determinant of e. See natAbs_det_basis_change for a more familiar formulation of this result.

theorem Submodule.natAbs_det_basis_change {M : Type u_1} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ M) (N : Submodule ℤ M) (bN : Module.Basis ι ℤ ↥N) : (b.det (Subtype.val ∘ ⇑bN)).natAbs = Nat.card (M ⧸ N)

Let b be a basis for M over ℤ and bN a basis for N over ℤ of the same dimension. Then an alternative way to compute the cardinality of M ⧸ N is given by taking the determinant of bN over b.

theorem AddSubgroup.index_eq_natAbs_det {E : Type u_1} [AddCommGroup E] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (bE : Module.Basis ι ℤ E) (N : AddSubgroup E) (bN : Module.Basis ι ℤ ↥N) : N.index = (bE.det fun (x : ι) => ↑(bN x)).natAbs

theorem AddSubgroup.relIndex_eq_natAbs_det {E : Type u_1} [AddCommGroup E] (L₁ L₂ : AddSubgroup E) (H : L₁ ≤ L₂) {ι : Type u_2} [DecidableEq ι] [Fintype ι] (b₁ : Module.Basis ι ℤ ↥(toIntSubmodule L₁)) (b₂ : Module.Basis ι ℤ ↥(toIntSubmodule L₂)) : L₁.relIndex L₂ = (b₂.det fun (i : ι) => ⟨↑(b₁ i), ⋯⟩).natAbs

@[deprecated AddSubgroup.relIndex_eq_natAbs_det (since := "2025-08-12")]

theorem AddSubgroup.relindex_eq_natAbs_det {E : Type u_1} [AddCommGroup E] (L₁ L₂ : AddSubgroup E) (H : L₁ ≤ L₂) {ι : Type u_2} [DecidableEq ι] [Fintype ι] (b₁ : Module.Basis ι ℤ ↥(toIntSubmodule L₁)) (b₂ : Module.Basis ι ℤ ↥(toIntSubmodule L₂)) : L₁.relIndex L₂ = (b₂.det fun (i : ι) => ⟨↑(b₁ i), ⋯⟩).natAbs

Alias of AddSubgroup.relIndex_eq_natAbs_det.

theorem AddSubgroup.relIndex_eq_abs_det {E : Type u_1} [AddCommGroup E] [Module ℚ E] (L₁ L₂ : AddSubgroup E) (H : L₁ ≤ L₂) {ι : Type u_2} [DecidableEq ι] [Fintype ι] (b₁ b₂ : Module.Basis ι ℚ E) (h₁ : L₁ = closure (Set.range ⇑b₁)) (h₂ : L₂ = closure (Set.range ⇑b₂)) : ↑(L₁.relIndex L₂) = |b₂.det ⇑b₁|

@[deprecated AddSubgroup.relIndex_eq_abs_det (since := "2025-08-12")]

theorem AddSubgroup.relindex_eq_abs_det {E : Type u_1} [AddCommGroup E] [Module ℚ E] (L₁ L₂ : AddSubgroup E) (H : L₁ ≤ L₂) {ι : Type u_2} [DecidableEq ι] [Fintype ι] (b₁ b₂ : Module.Basis ι ℚ E) (h₁ : L₁ = closure (Set.range ⇑b₁)) (h₂ : L₂ = closure (Set.range ⇑b₂)) : ↑(L₁.relIndex L₂) = |b₂.det ⇑b₁|

Alias of AddSubgroup.relIndex_eq_abs_det.