English
The absolute norm absNorm is the multiplicative map from FractionalIdeal to ℚ defined by absNorm(I) = (Ideal.absNorm I.num) / |Algebra.norm ℤ (I.den)|, with the usual properties absNorm(0) = 0, absNorm(1) = 1, and absNorm(IJ) = absNorm(I) · absNorm(J).
Русский
Абсолютная норма absNorm есть мултипликативное отображение от дробных идеалов к ℚ, определяемое как absNorm(I) = (Ideal.absNorm I.num) / |Algebra.norm ℤ (I.den)|, с свойствами absNorm(0) = 0, absNorm(1) = 1 и absNorm(IJ) = absNorm(I)·absNorm(J).
LaTeX
$$\\operatorname{absNorm} : FractionalIdeal R^0 K \\to^*_{0} \\mathbb{Q}, \\quad \\operatorname{absNorm}(I) = (\\operatorname{Ideal.absNorm} I.num) / |\\operatorname{Algebra.norm} \\mathbb{Z} (I.den)|$$
Lean4
/-- The absolute norm of the fractional ideal `I` extending by multiplicativity the absolute norm
on (integral) ideals. -/
noncomputable def absNorm : FractionalIdeal R⁰ K →*₀ ℚ
where
toFun I := (Ideal.absNorm I.num : ℚ) / |Algebra.norm ℤ (I.den : R)|
map_zero' := by
rw [num_zero_eq, Submodule.zero_eq_bot, Ideal.absNorm_bot, Nat.cast_zero, zero_div]
exact IsFractionRing.injective R K
map_one' := by
rw [absNorm_div_norm_eq_absNorm_div_norm 1 ⊤ (by simp [Submodule.one_eq_range]), Ideal.absNorm_top, Nat.cast_one,
OneMemClass.coe_one, map_one, abs_one, Int.cast_one, one_div_one]
map_mul' I
J := by
rw [absNorm_div_norm_eq_absNorm_div_norm (I.den * J.den) (I.num * J.num)
(by
have : Algebra.linearMap R K = (IsScalarTower.toAlgHom R R K).toLinearMap := rfl
rw [coe_mul, this, Submodule.map_mul, ← this, ← den_mul_self_eq_num, ← den_mul_self_eq_num]
exact Submodule.mul_smul_mul_eq_smul_mul_smul _ _ _ _),
Submonoid.coe_mul, map_mul, map_mul, Nat.cast_mul, div_mul_div_comm, Int.cast_abs, Int.cast_abs, Int.cast_abs, ←
abs_mul, Int.cast_mul]
