English
Let b be a basis of M and N a submodule basis of N; then the determinant of the transition from b to bN is related to the quotient cardinality by natAbs of the determinant.
Русский
Пусть b — базис M, a базис N подмодуля; детерминант перехода связан с кардинальностьюкости частого модуля через natAbs(det).
LaTeX
$$$$ (b.det ( (\uparrow) \circ bN ) ).natAbs = \mathrm{Nat.card}(M / N). $$$$
Lean4
/-- 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 natAbs_det_basis_change {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ M) (N : Submodule ℤ M)
(bN : Basis ι ℤ N) : (b.det ((↑) ∘ bN)).natAbs = Nat.card (M ⧸ N) :=
by
let e := b.equiv bN (Equiv.refl _)
calc
(b.det (N.subtype ∘ bN)).natAbs = (LinearMap.det (N.subtype ∘ₗ (e : M →ₗ[ℤ] N))).natAbs := by
rw [Basis.det_comp_basis]
_ = _ := natAbs_det_equiv N e
