English
Assuming separability at the fraction rings, spanNorm(I) ≤ comap(algebraMap R S, I) for any I ∈ Ideal S.
Русский
При условии сепарабельности дробных колец, spanNorm(I) ≤ comap(algebraMap R S, I).
LaTeX
$$$$\operatorname{spanNorm}(R,I) \le \operatorname{comap}(\operatorname{algebraMap}(R,S), I). $$$$
Lean4
theorem spanNorm_le_comap [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (I : Ideal S) :
spanNorm R I ≤ comap (algebraMap R S) I :=
by
rw [spanNorm, Ideal.map, Ideal.span_le, ← Submodule.span_le]
intro x hx
induction hx using Submodule.span_induction with
| mem _ h =>
obtain ⟨x, hx, rfl⟩ := h
exact mem_comap.mpr <| mem_of_dvd _ (Algebra.dvd_algebraMap_intNorm_self _ _ x) hx
| zero => simp
| add _ _ _ _ hx hy => exact Submodule.add_mem _ hx hy
| smul _ _ _ hx => exact Submodule.smul_mem _ _ hx
