English
The absolute norm of the different ideal equals the discriminant of K in absolute value, i.e., absNorm(differentIdeal) = |discr K|.
Русский
Абсолютная норма дифференциального идеала равна модулю дискриминанта, то есть absNorm(differentIdeal) = |discr K|.
LaTeX
$$$$\\operatorname{absNorm}(\\text{differentIdeal } \\mathbb{Z}, \\mathcal{O}) = |\\operatorname{discr} K|.$$$$
Lean4
theorem absNorm_differentIdeal : (differentIdeal ℤ 𝒪).absNorm = (discr K).natAbs :=
by
refine (differentIdeal ℤ 𝒪).toAddSubgroup.relIndex_top_right.symm.trans ?_
rw [←
Submodule.comap_map_eq_of_injective (f := Algebra.linearMap 𝒪 K) (FaithfulSMul.algebraMap_injective 𝒪 K)
(differentIdeal ℤ 𝒪)]
refine
(AddSubgroup.relIndex_comap (IsLocalization.coeSubmodule K (differentIdeal ℤ 𝒪)).toAddSubgroup
(algebraMap 𝒪 K).toAddMonoidHom ⊤).trans
?_
have :=
FractionalIdeal.quotientEquiv (R := 𝒪) (K := K) 1 (differentIdeal ℤ 𝒪) (differentIdeal ℤ 𝒪)⁻¹ 1
(by simp [differentIdeal_ne_bot]) FractionalIdeal.coeIdeal_le_one
(le_inv_of_le_inv₀ (by simp [pos_iff_ne_zero, differentIdeal_ne_bot])
(by simpa using FractionalIdeal.coeIdeal_le_one))
one_ne_zero one_ne_zero
have := Nat.card_congr this.toEquiv
refine this.trans ?_
rw [FractionalIdeal.coe_one, coeIdeal_differentIdeal (K := ℚ), inv_inv]
let b := integralBasis K
let b' := (Algebra.traceForm ℚ K).dualBasis (traceForm_nondegenerate ℚ K) b
have hb : Submodule.span ℤ (Set.range b) = (1 : Submodule 𝒪 K).restrictScalars ℤ :=
by
ext
let e := IsIntegralClosure.equiv ℤ (RingOfIntegers K) K 𝒪
simpa [e.symm.exists_congr_left, e] using mem_span_integralBasis K
qify
refine
(AddSubgroup.relIndex_eq_abs_det (1 : Submodule 𝒪 K).toAddSubgroup
(FractionalIdeal.dual ℤ ℚ 1 : FractionalIdeal 𝒪⁰ K).coeToSubmodule.toAddSubgroup ?_ b b' ?_ ?_).trans
?_
· rw [Submodule.toAddSubgroup_le, ← FractionalIdeal.coe_one]
exact FractionalIdeal.one_le_dual_one ℤ ℚ (L := K) (B := 𝒪)
· apply AddSubgroup.toIntSubmodule.injective
rw [AddSubgroup.toIntSubmodule_closure, hb, Submodule.toIntSubmodule_toAddSubgroup]
· apply AddSubgroup.toIntSubmodule.injective
rw [AddSubgroup.toIntSubmodule_closure, ← LinearMap.BilinForm.dualSubmodule_span_of_basis, hb]
simp
· simp only [Module.Basis.det_apply, discr, Algebra.discr]
rw [← eq_intCast (algebraMap ℤ ℚ), RingHom.map_det]
congr! 2
ext i j
simp [b', Module.Basis.toMatrix_apply, mul_comm (RingOfIntegers.basis K i), b, integralBasis_apply, ← map_mul,
Algebra.trace_localization ℤ ℤ⁰]
