English
A morphism of commutative rings g: A → B induces a map on Kaehler differentials, and two differential maps from Kaehler differentials to a module M are equal if they agree on all elements of the form d b, where b runs through B.
Русский
Гомоморфизм колмодовых дифференциалов g: A → B индуцирует отображение на Kaehler differentiable, и два отображения дифференциалов равны, если они совпадают на всех элементах вида d b, где b ∈ B.
LaTeX
$$$\\forall b \\in B:\\; \\alpha(d(b)) = \\beta(d(b)) \\Rightarrow \\alpha = \\beta.$$$
Lean4
@[ext]
theorem ext {M : ModuleCat B} {α β : KaehlerDifferential f ⟶ M} (h : ∀ (b : B), α (d b) = β (d b)) : α = β :=
by
rw [← sub_eq_zero]
have : ⊤ ≤ LinearMap.ker (α - β).hom :=
by
rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]
rintro _ ⟨y, rfl⟩
rw [SetLike.mem_coe, LinearMap.mem_ker, ModuleCat.hom_sub, LinearMap.sub_apply, sub_eq_zero]
apply h
rw [top_le_iff, LinearMap.ker_eq_top] at this
ext : 1
exact this
