English
Let R be a local ring with maximal ideal p and S a finite R-algebra. For any subset s ⊆ S, the span of the image of s in S/pS over R/p equals the whole quotient if and only if the span of s in S over R equals the whole S.
Русский
Пусть R — локальное кольцо с максимальной идеальной p, и S — конечное над R кольцо. Для любого подмножества s ⊆ S выполнение порождений в S/pS над R/p эквивалентно порождению в S над R: span_{R/p} (образы s) = ⊤ ⇔ span_R(s) = ⊤.
LaTeX
$$$\\operatorname{span}_{R/\\mathfrak p} \\big( (\\mathrm{Ideal.Quotient.mk} (I := \\mathfrak p S))'' s \\big) = \\top \\iff \\operatorname{span}_R s = \\top$$$
Lean4
theorem quotient_span_eq_top_iff_span_eq_top (s : Set S) :
span (R ⧸ p) ((Ideal.Quotient.mk (I := pS)) '' s) = ⊤ ↔ span R s = ⊤ :=
by
have H :
(span (R ⧸ p) ((Ideal.Quotient.mk (I := pS)) '' s)).restrictScalars R =
(span R s).map (IsScalarTower.toAlgHom R S (S ⧸ pS)) :=
by
rw [map_span, ← restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective, IsScalarTower.coe_toAlgHom',
Ideal.Quotient.algebraMap_eq]
constructor
· intro hs
rw [← top_le_iff]
apply le_of_le_smul_of_le_jacobson_bot
· exact Module.finite_def.mp ‹_›
· exact (jacobson_eq_maximalIdeal ⊥ bot_ne_top).ge
· rw [Ideal.smul_top_eq_map]
rintro x -
have : LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ pS)) = restrictScalars R pS := by ext;
simp [Ideal.Quotient.eq_zero_iff_mem]
rw [← this, ← comap_map_eq, mem_comap, ← H, hs, restrictScalars_top]
exact mem_top
· intro hs
rwa [hs, Submodule.map_top, LinearMap.range_eq_top.mpr, restrictScalars_eq_top_iff] at H
rw [IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]
exact Ideal.Quotient.mk_surjective
