English
The span of the image of D generates the Kaehler differential ideal; more precisely, the S-span of the range of D equals the Kaehler differential ideal.
Русский
Циклом образа D порождает идеал Каehлерова дифференциала; точнее, S-растяжение образа D равно KaehlerDifferential.ideal.
LaTeX
$$Submodule.span S (Set.range (KaehlerDifferential.D R S)) = KaehlerDifferential.ideal R S$$
Lean4
theorem span_range_eq_ideal :
Ideal.span (Set.range fun s : S => (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)) = KaehlerDifferential.ideal R S :=
by
apply le_antisymm
· rw [Ideal.span_le]
rintro _ ⟨s, rfl⟩
exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _
· change (KaehlerDifferential.ideal R S).restrictScalars S ≤ (Ideal.span _).restrictScalars S
rw [← KaehlerDifferential.submodule_span_range_eq_ideal, Ideal.span]
conv_rhs => rw [← Submodule.span_span_of_tower S]
exact Submodule.subset_span
