English
Span of the range of the derivation D equals the whole module, i.e., the derivatives generate the whole differential module.
Русский
Равенство пространства порождено производными: диапазон D покрывает весь модуль Дифференциальных Каэлеровых.
LaTeX
$$Submodule.span S (Set.range <| KaehlerDifferential.D R S) = ⊤$$
Lean4
theorem span_range_derivation : Submodule.span S (Set.range <| KaehlerDifferential.D R S) = ⊤ :=
by
rw [_root_.eq_top_iff]
rintro x -
obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
have : x ∈ (KaehlerDifferential.ideal R S).restrictScalars S := hx
rw [← KaehlerDifferential.submodule_span_range_eq_ideal] at this
suffices
∃ hx,
(KaehlerDifferential.ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range <| KaehlerDifferential.D R S)
by exact this.choose_spec
refine Submodule.span_induction ?_ ?_ ?_ ?_ this
· rintro _ ⟨x, rfl⟩
refine ⟨KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x, ?_⟩
apply Submodule.subset_span
exact ⟨x, KaehlerDifferential.DLinearMap_apply R S x⟩
· exact ⟨zero_mem _, Submodule.zero_mem _⟩
· rintro x y - - ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩; exact ⟨add_mem hx₁ hy₁, Submodule.add_mem _ hx₂ hy₂⟩
· rintro r x - ⟨hx₁, hx₂⟩
exact ⟨((KaehlerDifferential.ideal R S).restrictScalars S).smul_mem r hx₁, Submodule.smul_mem _ r hx₂⟩
