English
For a Noetherian ring, the span of the image of a set under the cotangent map is top if and only if the span of the set in the ring is top.
Русский
Для кольца с конечной порождаемостью область образа из котантгенового отображения верхняя; так же как и порождаемость множества в кольце.
LaTeX
$$Submodule.span (ResidueField R) ((maximalIdeal R).toCotangent '' s) = ⊤ \Leftrightarrow Submodule.span R s = ⊤$$
Lean4
theorem span_image_eq_top_iff [IsNoetherianRing R] {s : Set (maximalIdeal R)} :
Submodule.span (ResidueField R) ((maximalIdeal R).toCotangent '' s) = ⊤ ↔ Submodule.span R s = ⊤ :=
by
rw [← map_eq_top_iff, ← (Submodule.restrictScalars_injective R ..).eq_iff, Submodule.restrictScalars_span]
· simp only [Ideal.toCotangent_apply, Submodule.restrictScalars_top, Submodule.map_span]
· exact Ideal.Quotient.mk_surjective
