English
The differential D applied to an element s ∈ S corresponds to the cotangent class of 1 ⊗ s − s ⊗ 1 in the Kaehler differential picture.
Русский
Дифференциал D применяется к элементу s ∈ S и соответствует классу 1 ⊗ s − s ⊗ 1 в коэлинейном дифференциале.
LaTeX
$$D_apply (s) = (KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ s - s ⊗ₜ 1, ...⟩$$
Lean4
/-- The kernel of `S ⊗[R] S →ₐ[R] S` is generated by `1 ⊗ s - s ⊗ 1` as a `S`-module. -/
theorem submodule_span_range_eq_ideal :
Submodule.span S (Set.range fun s : S => (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)) =
(KaehlerDifferential.ideal R S).restrictScalars S :=
by
apply le_antisymm
· rw [Submodule.span_le]
rintro _ ⟨s, rfl⟩
exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _
· rintro x (hx : _ = _)
have : x - TensorProduct.lmul' (S := S) R x ⊗ₜ[R] (1 : S) = x := by rw [hx, TensorProduct.zero_tmul, sub_zero]
rw [← this]
clear this hx
refine TensorProduct.induction_on x ?_ ?_ ?_
· rw [map_zero, TensorProduct.zero_tmul, sub_zero]; exact zero_mem _
· intro x y
have : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] (1 : S) = x • ((1 : S) ⊗ₜ y - y ⊗ₜ (1 : S)) := by
simp_rw [smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
rw [TensorProduct.lmul'_apply_tmul, this]
refine Submodule.smul_mem _ x ?_
apply Submodule.subset_span
exact Set.mem_range_self y
· intro x y hx hy
rw [map_add, TensorProduct.add_tmul, ← sub_add_sub_comm]
exact add_mem hx hy
