English
If a ∈ R⁰ and I is a fractional ideal with a I equivalent to the image of I₀ under a linear map, then the AbsNorm ratio matches: absNorm(I.num)/|norm(I.den)| = absNorm(I₀)/|norm(a)|.
Русский
Если a ∈ R⁰ и a I эквивалентно образу I₀ под линейным отображением, то отношение AbsNorm сходно: absNorm(I.num)/|norm(I.den)| = absNorm(I₀)/|norm(a)|.
LaTeX
$$\\text{If } a \\in R^0 \\text{ and } a I = \\mathrm{map}(\\text{Algebra.linearMap } R K) I_0, \\\\ \\frac{\\operatorname{absNorm}(I.num)}{|\\operatorname{norm}(I.den)|} = \\frac{\\operatorname{absNorm}(I_0)}{|\\operatorname{norm}(a)|}$$
Lean4
theorem absNorm_div_norm_eq_absNorm_div_norm {I : FractionalIdeal R⁰ K} (a : R⁰) (I₀ : Ideal R)
(h : a • (I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀) :
(Ideal.absNorm I.num : ℚ) / |Algebra.norm ℤ (I.den : R)| = (Ideal.absNorm I₀ : ℚ) / |Algebra.norm ℤ (a : R)| :=
by
rw [div_eq_div_iff]
· replace h := congr_arg (I.den • ·) h
have h' := congr_arg (a • ·) (den_mul_self_eq_num I)
dsimp only at h h'
rw [smul_comm] at h
rw [h, Submonoid.smul_def, Submonoid.smul_def, ← Submodule.ideal_span_singleton_smul, ←
Submodule.ideal_span_singleton_smul, ← Submodule.map_smul'', ← Submodule.map_smul'',
(LinearMap.map_injective ?_).eq_iff, smul_eq_mul, smul_eq_mul] at h'
· simp_rw [← Int.cast_natAbs, ← Nat.cast_mul, ← Ideal.absNorm_span_singleton]
rw [← map_mul, ← map_mul, mul_comm, ← h', mul_comm]
· exact LinearMap.ker_eq_bot.mpr (IsFractionRing.injective R K)
all_goals simp [Algebra.norm_eq_zero_iff]
