English
With localization at a multiplicative set M in R and corresponding localization in S, spanNorm commutes with this localization: spanNorm(R_M,I.map(S→S_M)) = (spanNorm(R,I)).map(R→R_M).
Русский
При локализации по множеству M в R и соответствующей локализации в S, spanNorm совместим с локализацией: spanNorm(R_M,I.map) = map(spanNorm(R,I)) в локализованном контексте.
LaTeX
$$$$\operatorname{spanNorm}(R_M, I.map(\mathrm{algebraMap}(S,S_M))) = (\operatorname{spanNorm}(R,I)).map(\mathrm{algebraMap}(R,R_M)). $$$$
Lean4
/-- Multiplicativity of `Ideal.spanNorm`. simp-normal form is `map_mul (Ideal.relNorm R)`. -/
theorem spanNorm_mul [IsDedekindDomain R] [IsDedekindDomain S] (I J : Ideal S) :
spanNorm R (I * J) = spanNorm R I * spanNorm R J :=
by
nontriviality R
cases subsingleton_or_nontrivial S
· have : ∀ I : Ideal S, I = ⊤ := fun I ↦ Subsingleton.elim I ⊤
simp [this I, this J]
refine eq_of_localization_maximal (fun P hP ↦ ?_)
by_cases hP0 : P = ⊥
· subst hP0
rw [spanNorm_mul_of_bot_or_top]
intro I
exact or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm
have : NeZero P := ⟨hP0⟩
let P' := Algebra.algebraMapSubmonoid S P.primeCompl
simp only [Ideal.map_mul,
← spanIntNorm_localization (R := R) (Sₘ := Localization P') _ _ P.primeCompl_le_nonZeroDivisors]
rw [← (I.map _).span_singleton_generator, ← (J.map _).span_singleton_generator, span_singleton_mul_span_singleton,
spanNorm_singleton, spanNorm_singleton, spanNorm_singleton, span_singleton_mul_span_singleton, map_mul]
