English
For a nice integral basis b of R and a fractional ideal I with a basis bI, the absolute determinant of the localization matrix equals absNorm(I).
Русский
Для базиса b базиса R и дробного идеала I с базисом bI абсолютная детерминанта локализации равна absNorm(I).
LaTeX
$$|(b.localizationLocalization ℚ ℤ⁰ K).det ((↑) ∘ bI)| = \\operatorname{absNorm}(I)$$
Lean4
theorem abs_det_basis_change [NoZeroDivisors K] {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ R)
(I : FractionalIdeal R⁰ K) (bI : Basis ι ℤ I) : |(b.localizationLocalization ℚ ℤ⁰ K).det ((↑) ∘ bI)| = absNorm I :=
by
have := IsFractionRing.nontrivial R K
let b₀ : Basis ι ℚ K := b.localizationLocalization ℚ ℤ⁰ K
let bI.num : Basis ι ℤ I.num := bI.map ((equivNum (nonZeroDivisors.coe_ne_zero _)).restrictScalars ℤ)
rw [absNorm_eq, ← Ideal.natAbs_det_basis_change b I.num bI.num, Int.cast_natAbs, Int.cast_abs, Int.cast_abs,
Basis.det_apply, Basis.det_apply]
change _ = |algebraMap ℤ ℚ _| / _
rw [RingHom.map_det,
show
RingHom.mapMatrix (algebraMap ℤ ℚ) (b.toMatrix ((↑) ∘ bI.num)) =
b₀.toMatrix ((algebraMap R K (den I : R)) • ((↑) ∘ bI))
by
ext : 2
simp_rw [bI.num, RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply, ←
Basis.localizationLocalization_repr_algebraMap ℚ ℤ⁰ K, Function.comp_apply, Basis.map_apply,
LinearEquiv.restrictScalars_apply, equivNum_apply, Submonoid.smul_def, Algebra.smul_def]
rfl]
rw [Basis.toMatrix_smul, Matrix.det_mul, abs_mul, ← Algebra.norm_eq_matrix_det, Algebra.norm_localization ℤ ℤ⁰,
show (Algebra.norm ℤ (den I : R) : ℚ) = algebraMap ℤ ℚ (Algebra.norm ℤ (den I : R)) by rfl, mul_div_assoc,
mul_div_cancel₀ _
(by
rw [ne_eq, abs_eq_zero, IsFractionRing.to_map_eq_zero_iff, Algebra.norm_eq_zero_iff_of_basis b]
exact nonZeroDivisors.coe_ne_zero _)]
