English
For a given I and suitable E, the determinant of a basis-change map computes absNorm I via natAbs.
Русский
Для заданного I и подходящего E детерминант отображения смены базиса вычисляет absNorm I через natAbs.
LaTeX
$$natAbs(det((Submodule.subtype I).restrictScalars ℤ ∘ₗ AddMonoidHom.toIntLinearMap (e))) = absNorm(I)$$
Lean4
/-- Let `e : S ≃ I` be an additive isomorphism (therefore a `ℤ`-linear equiv).
Then an alternative way to compute the norm of `I` 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 (I : Ideal S) {E : Type*} [EquivLike E S I] [AddEquivClass E S I] (e : E) :
Int.natAbs (LinearMap.det ((Submodule.subtype I).restrictScalars ℤ ∘ₗ AddMonoidHom.toIntLinearMap (e : S →+ I))) =
Ideal.absNorm I :=
by
-- `S ⧸ I` might be infinite if `I = ⊥`, but then `e` can't be an equiv.
by_cases hI : I = ⊥
· subst hI
have : (1 : S) ≠ 0 := one_ne_zero
have : (1 : S) = 0 := EquivLike.injective e (Subsingleton.elim _ _)
contradiction
exact Submodule.natAbs_det_equiv (I.restrictScalars ℤ) e
