English
If two linear maps f and f' from Ω[S⁄R] to M agree on the differential D, they are equal.
Русский
Если две линейные отображения совпадают на дифференциале D, они равны.
LaTeX
$$liftKaehlerDifferential_unique (f f' : Ω[S⁄R] →ₗ[S] M) (hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)) : f = f'$$
Lean4
@[ext]
theorem liftKaehlerDifferential_unique (f f' : Ω[S⁄R] →ₗ[S] M)
(hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)) : f = f' :=
by
apply LinearMap.ext
intro x
have : x ∈ Submodule.span S (Set.range <| KaehlerDifferential.D R S) := by
rw [KaehlerDifferential.span_range_derivation]; trivial
refine Submodule.span_induction ?_ ?_ ?_ ?_ this
· rintro _ ⟨x, rfl⟩; exact congr_arg (fun D : Derivation R S M => D x) hf
· rw [map_zero, map_zero]
· intro x y _ _ hx hy; rw [map_add, map_add, hx, hy]
· intro a x _ e; simp [e]
