English
For a submodule N of a free module M over the integers, the absolute determinant of the change of basis from a basis of N to a basis of M equals the cardinality of the quotient M/N.
Русский
Для подмодуля N свободного модуля M над целыми, абсолютный детерминант перехода от базиса N к базису M равен кардинальности фактор-модуля M/N.
LaTeX
$$$$ \operatorname{natAbs}\big( \det\big(b: N \to M\big) \big) = \#(M \;/ N). $$$$
Lean4
/-- 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 natAbs_det_equiv (N : Submodule ℤ M) {E : Type*} [EquivLike E M N] [AddEquivClass E M N] (e : E) :
Int.natAbs (LinearMap.det (N.subtype ∘ₗ AddMonoidHom.toIntLinearMap (e : M →+ N))) = Nat.card (M ⧸ N) :=
by
let b := Module.Free.chooseBasis ℤ M
have h : Module.finrank ℤ N = Module.finrank ℤ M := (AddEquiv.toIntLinearEquiv e : M ≃ₗ[ℤ] N).symm.finrank_eq
let a := smithNormalFormCoeffs b h
let b' := smithNormalFormTopBasis b h
let ab := smithNormalFormBotBasis b h
have ab_eq := smithNormalFormBotBasis_def b h
let e' : M ≃ₗ[ℤ] N := b'.equiv ab (Equiv.refl _)
let f : M →ₗ[ℤ] M := N.subtype.comp (e' : M →ₗ[ℤ] N)
let f_apply : ∀ x, f x = b'.equiv ab (Equiv.refl _) x := fun x ↦ rfl
suffices (LinearMap.det f).natAbs = Nat.card (M ⧸ N) by
calc
_ = (LinearMap.det (N.subtype ∘ₗ (AddEquiv.toIntLinearEquiv e : M ≃ₗ[ℤ] N))).natAbs := rfl
_ = (LinearMap.det (N.subtype ∘ₗ _)).natAbs :=
(Int.natAbs_eq_iff_associated.mpr (LinearMap.associated_det_comp_equiv _ _ _))
_ = Nat.card (M ⧸ N) := this
have ha : ∀ i, f (b' i) = a i • b' i := by
intro i
rw [f_apply, b'.equiv_apply, Equiv.refl_apply]
exact ab_eq i
calc
Int.natAbs (LinearMap.det f) = Int.natAbs (LinearMap.toMatrix b' b' f).det := by rw [LinearMap.det_toMatrix]
_ = Int.natAbs (Matrix.diagonal a).det := ?_
_ = Int.natAbs (∏ i, a i) := by rw [Matrix.det_diagonal]
_ = ∏ i, Int.natAbs (a i) := (map_prod Int.natAbsHom a Finset.univ)
_ = Nat.card (M ⧸ N) :=
?_
-- since `LinearMap.toMatrix b' b' f` is the diagonal matrix with `a` along the diagonal.
· congr 2; ext i j
rw [LinearMap.toMatrix_apply, ha, LinearEquiv.map_smul, Basis.repr_self, Finsupp.smul_single, smul_eq_mul, mul_one]
by_cases h : i = j
· rw [h, Matrix.diagonal_apply_eq, Finsupp.single_eq_same]
·
rw [Matrix.diagonal_apply_ne _ h, Finsupp.single_eq_of_ne h]
-- Now we map everything through the linear equiv `M ≃ₗ (ι → ℤ)`,
-- which maps `(M ⧸ N)` to `Π i, ZMod (a i).nat_abs`.
haveI : ∀ i, NeZero (a i).natAbs := fun i ↦ ⟨Int.natAbs_ne_zero.mpr (smithNormalFormCoeffs_ne_zero b h i)⟩
simp_rw [Nat.card_congr (quotientEquivPiZMod N b h).toEquiv, Nat.card_pi, Nat.card_zmod, a]
