English
Let R, S, T be integral domains with R ⊆ S ⊆ T in a finite, integrally closed setting. If every ideal of R is either 0 or the whole ring, then applying spanNorm twice, first over T and then over R, does not change spanNorm of an ideal of S: spanNorm_R(spanNorm_T(I)) = spanNorm_R(I) for all I ≤ S.
Русский
Пусть R, S, T — целочисленные домены, удовлетворяющие необходимым условиям конечности и интегральной замкнутости, и пусть каждый идеал R равен 0 или единице. Тогда применение spanNorm дважды, сначала по T, затем по R, не изменяет spanNorm(I) для любого идеала I в S: spanNorm_R(spanNorm_T(I)) = spanNorm_R(I) для всех I.
LaTeX
$$$\left( \forall I \in \mathrm{Idl}(R), I = \bot \lor I = \top \right) \Rightarrow \forall I \in \mathrm{Idl}(S), \mathrm{spanNorm}_R(\mathrm{spanNorm}_T(I)) = \mathrm{spanNorm}_R(I).$$
Lean4
/-- This condition `eq_bot_or_top` is equivalent to being a field. However,
`Ideal.spanNorm_spanNorm_of_field` would be harder to apply since we'd need to upgrade
a `CommRing R` instance to a `Field R` instance.
-/
theorem spanNorm_spanNorm_of_bot_or_top (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I : Ideal S) :
spanNorm R (spanNorm T I) = spanNorm R I :=
by
obtain h | h := eq_bot_or_top (spanNorm R I)
· rw [h, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff.mp h]
· exact h ▸ (eq_top_iff_one _).mpr <| le_spanNorm_spanNorm R T I <| (eq_top_iff_one _).mp h
