English
For Dedekind domains R, T, and S, the double spanNorm respects the outer spanNorm: spanNorm_R(spanNorm_T(I)) = spanNorm_R(I) holds for every ideal I of S.
Русский
Для зондированных доменов Дедеклина R, T и S выполняется равенство: spanNorm_R(spanNorm_T(I)) = spanNorm_R(I) для каждого идеала I в S.
LaTeX
$$$\mathrm{spanNorm}_R(\mathrm{spanNorm}_T(I)) = \mathrm{spanNorm}_R(I)$$$
Lean4
theorem spanNorm_spanNorm [IsDedekindDomain R] [IsDedekindDomain T] [IsDedekindDomain S] (I : Ideal S) :
spanNorm R (spanNorm T I) = spanNorm R I :=
by
refine eq_of_localization_maximal fun P hP ↦ ?_
by_cases hP : P = ⊥
· subst hP
rw [spanNorm_spanNorm_of_bot_or_top]
exact fun I ↦ or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm
let Rₚ := Localization.AtPrime P
let Tₚ := Localization (algebraMapSubmonoid T P.primeCompl)
let Sₚ := Localization (algebraMapSubmonoid S P.primeCompl)
have : NeZero P := ⟨hP⟩
have h : algebraMapSubmonoid T P.primeCompl ≤ T⁰ :=
algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ (primeCompl_le_nonZeroDivisors P)
rw [← spanIntNorm_localization R (spanNorm T I) _ (primeCompl_le_nonZeroDivisors P) Tₚ, ←
spanIntNorm_localization T (Rₘ := Tₚ) I _ h Sₚ, ←
spanIntNorm_localization R (Rₘ := Rₚ) I _ (primeCompl_le_nonZeroDivisors P) Sₚ, ←
(I.map _).span_singleton_generator, spanNorm_singleton, spanNorm_singleton, intNorm_intNorm, spanNorm_singleton]
