feat(ring_theory/derivation): Construction of the module of Kähler di…

…fferentials. (#16047)




Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/ring_theory/derivation.lean

@@ -7,22 +7,33 @@ Authors: Nicolò Cavalleri, Andrew Yang
 import ring_theory.adjoin.basic
 import algebra.lie.of_associative
 import ring_theory.tensor_product
+import ring_theory.ideal.cotangent
 
 /-!
 # Derivations
 
 This file defines derivation. A derivation `D` from the `R`-algebra `A` to the `A`-module `M` is an
 `R`-linear map that satisfy the Leibniz rule `D (a * b) = a * D b + D a * b`.
 
-## Notation
-
-The notation `⁅D1, D2⁆` is used for the commutator of two derivations.
-
-TODO: this file is just a stub to go on with some PRs in the geometry section. It only
-implements the definition of derivations in commutative algebra. This will soon change: as soon
-as bimodules will be there in mathlib I will change this file to take into account the
-non-commutative case. Any development on the theory of derivations is discouraged until the
-definitive definition of derivation will be implemented.
+## Main results
+
+- `derivation`: The type of `R`-derivations from `A` to `M`. This has an `A`-module structure.
+- `derivation.llcomp`: We may compose linear maps and derivations to obtain a derivation,
+  and the composition is bilinear.
+- `derivation.lie_algebra`: The `R`-derivations from `A` to `A` form an lie algebra over `R`.
+- `derivation_to_square_zero_equiv_lift`: The `R`-derivations from `A` into a square-zero ideal `I`
+  of `B` corresponds to the lifts `A →ₐ[R] B` of the map `A →ₐ[R] B ⧸ I`.
+- `kaehler_differential`: The module of kaehler differentials. For an `R`-algebra `S`, we provide
+  the notation `Ω[S⁄R]` for `kaehler_differential R S`.
+  Note that the slash is `\textfractionsolidus`.
+- `kaehler_differential.D`: The derivation into the module of kaehler differentials.
+- `kaehler_differential.span_range_derivation`: The image of `D` spans `Ω[S⁄R]` as an `S`-module.
+- `kaehler_differential.linear_map_equiv_derivation`:
+  The isomorphism `Hom_R(Ω[S⁄R], M) ≃ₗ[S] Der_R(S, M)`.
+
+## Future project
+
+Generalize this into bimodules.
 -/
 
 open algebra
@@ -448,20 +459,20 @@ end
 
 end to_square_zero
 
-section derivation_module
+section kaehler_differential
 
 open_locale tensor_product
 
 variables (R S : Type*) [comm_ring R] [comm_ring S] [algebra R S]
 
 /-- The kernel of the multiplication map `S ⊗[R] S →ₐ[R] S`. -/
-abbreviation derivation_module.ideal : ideal (S ⊗[R] S) :=
+abbreviation kaehler_differential.ideal : ideal (S ⊗[R] S) :=
 ring_hom.ker (tensor_product.lmul' R : S ⊗[R] S →ₐ[R] S)
 
 variable {S}
 
-lemma derivation_module.one_smul_sub_smul_one_mem_ideal (a : S) :
-  (1 : S) ⊗ₜ[R] a - a ⊗ₜ[R] (1 : S) ∈ derivation_module.ideal R S :=
+lemma kaehler_differential.one_smul_sub_smul_one_mem_ideal (a : S) :
+  (1 : S) ⊗ₜ[R] a - a ⊗ₜ[R] (1 : S) ∈ kaehler_differential.ideal R S :=
 by simp [ring_hom.mem_ker]
 
 variables {R}
@@ -499,14 +510,14 @@ end
 variables (R S)
 
 /-- The kernel of `S ⊗[R] S →ₐ[R] S` is generated by `1 ⊗ s - s ⊗ 1` as a `S`-module. -/
-lemma derivation_module.submodule_span_range_eq_ideal :
+lemma kaehler_differential.submodule_span_range_eq_ideal :
   submodule.span S (set.range $ λ s : S, (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)) =
-    (derivation_module.ideal R S).restrict_scalars S :=
+    (kaehler_differential.ideal R S).restrict_scalars S :=
 begin
   apply le_antisymm,
   { rw submodule.span_le,
     rintros _ ⟨s, rfl⟩,
-    exact derivation_module.one_smul_sub_smul_one_mem_ideal _ _ },
+    exact kaehler_differential.one_smul_sub_smul_one_mem_ideal _ _ },
   { rintros x (hx : _ = _),
     have : x - (tensor_product.lmul' R x) ⊗ₜ[R] (1 : S)   = x,
     { rw [hx, tensor_product.zero_tmul, sub_zero] },
@@ -526,18 +537,188 @@ begin
       exact add_mem hx hy } }
 end
 
-lemma derivation_module.span_range_eq_ideal :
+lemma kaehler_differential.span_range_eq_ideal :
   ideal.span (set.range $ λ s : S, (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)) =
-    derivation_module.ideal R S :=
+    kaehler_differential.ideal R S :=
 begin
   apply le_antisymm,
   { rw ideal.span_le,
     rintros _ ⟨s, rfl⟩,
-    exact derivation_module.one_smul_sub_smul_one_mem_ideal _ _ },
-  { change (derivation_module.ideal R S).restrict_scalars S ≤ (ideal.span _).restrict_scalars S,
-    rw [← derivation_module.submodule_span_range_eq_ideal, ideal.span],
+    exact kaehler_differential.one_smul_sub_smul_one_mem_ideal _ _ },
+  { change (kaehler_differential.ideal R S).restrict_scalars S ≤ (ideal.span _).restrict_scalars S,
+    rw [← kaehler_differential.submodule_span_range_eq_ideal, ideal.span],
     conv_rhs { rw ← submodule.span_span_of_tower S },
     exact submodule.subset_span }
 end
 
-end derivation_module
+/--
+The module of Kähler differentials (Kahler differentials, Kaehler differentials).
+This is implemented as `I / I ^ 2` with `I` the kernel of the multiplication map `S ⊗[R] S →ₐ[R] S`.
+To view elements as a linear combination of the form `s • D s'`, use
+`kaehler_differential.tensor_product_to_surjective` and `derivation.tensor_product_to_tmul`.
+
+We also provide the notation `Ω[S⁄R]` for `kaehler_differential R S`.
+Note that the slash is `\textfractionsolidus`.
+-/
+@[derive [add_comm_group, module R, module S, module (S ⊗[R] S)]]
+def kaehler_differential : Type* := (kaehler_differential.ideal R S).cotangent
+
+notation `Ω[ `:100 S ` ⁄ `:0 R ` ]`:0 := kaehler_differential R S
+
+instance : nonempty Ω[S⁄R] := ⟨0⟩
+
+instance : is_scalar_tower S (S ⊗[R] S) Ω[S⁄R] :=
+ideal.cotangent.is_scalar_tower _
+
+instance kaehler_differential.is_scalar_tower' : is_scalar_tower R S Ω[S⁄R] :=
+begin
+  haveI : is_scalar_tower R S (kaehler_differential.ideal R S),
+  { constructor, intros x y z, ext1, exact smul_assoc x y z.1 },
+  exact submodule.quotient.is_scalar_tower _ _
+end
+
+/-- (Implementation) The underlying linear map of the derivation into `Ω[S⁄R]`. -/
+def kaehler_differential.D_linear_map : S →ₗ[R] Ω[S⁄R] :=
+((kaehler_differential.ideal R S).to_cotangent.restrict_scalars R).comp
+  ((tensor_product.include_right.to_linear_map - tensor_product.include_left.to_linear_map :
+    S →ₗ[R] S ⊗[R] S).cod_restrict ((kaehler_differential.ideal R S).restrict_scalars R)
+      (kaehler_differential.one_smul_sub_smul_one_mem_ideal R) : _ →ₗ[R] _)
+
+lemma kaehler_differential.D_linear_map_apply (s : S) :
+  kaehler_differential.D_linear_map R S s = (kaehler_differential.ideal R S).to_cotangent
+    ⟨1 ⊗ₜ s - s ⊗ₜ 1, kaehler_differential.one_smul_sub_smul_one_mem_ideal R s⟩ :=
+rfl
+
+/-- The universal derivation into `Ω[S⁄R]`. -/
+def kaehler_differential.D : derivation R S Ω[S⁄R] :=
+{ map_one_eq_zero' := begin
+    dsimp [kaehler_differential.D_linear_map_apply],
+    rw [ideal.to_cotangent_eq_zero, subtype.coe_mk, sub_self],
+    exact zero_mem _
+  end,
+  leibniz' := λ a b, begin
+    dsimp [kaehler_differential.D_linear_map_apply],
+    rw [← linear_map.map_smul_of_tower, ← linear_map.map_smul_of_tower, ← map_add,
+      ideal.to_cotangent_eq, pow_two],
+    convert submodule.mul_mem_mul (kaehler_differential.one_smul_sub_smul_one_mem_ideal R a : _)
+      (kaehler_differential.one_smul_sub_smul_one_mem_ideal R b : _) using 1,
+    simp only [add_subgroup_class.coe_sub, submodule.coe_add, submodule.coe_mk,
+      tensor_product.tmul_mul_tmul, mul_sub, sub_mul, mul_comm b,
+      submodule.coe_smul_of_tower, smul_sub, tensor_product.smul_tmul', smul_eq_mul, mul_one],
+    ring_nf,
+  end,
+  ..(kaehler_differential.D_linear_map R S) }
+
+lemma kaehler_differential.D_apply (s : S) :
+  kaehler_differential.D R S s = (kaehler_differential.ideal R S).to_cotangent
+    ⟨1 ⊗ₜ s - s ⊗ₜ 1, kaehler_differential.one_smul_sub_smul_one_mem_ideal R s⟩ :=
+rfl
+
+lemma kaehler_differential.span_range_derivation :
+  submodule.span S (set.range $ kaehler_differential.D R S) = ⊤ :=
+begin
+  rw _root_.eq_top_iff,
+  rintros x -,
+  obtain ⟨⟨x, hx⟩, rfl⟩ := ideal.to_cotangent_surjective _ x,
+  have : x ∈ (kaehler_differential.ideal R S).restrict_scalars S := hx,
+  rw ← kaehler_differential.submodule_span_range_eq_ideal at this,
+  suffices : ∃ hx, (kaehler_differential.ideal R S).to_cotangent ⟨x, hx⟩ ∈
+    submodule.span S (set.range $ kaehler_differential.D R S),
+  { exact this.some_spec },
+  apply submodule.span_induction this,
+  { rintros _ ⟨x, rfl⟩,
+    refine ⟨kaehler_differential.one_smul_sub_smul_one_mem_ideal R x, _⟩,
+    apply submodule.subset_span,
+    exact ⟨x, kaehler_differential.D_linear_map_apply R S x⟩ },
+  { exact ⟨zero_mem _, zero_mem _⟩ },
+  { rintros x y ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩, exact ⟨add_mem hx₁ hy₁, add_mem hx₂ hy₂⟩ },
+  { rintros r x ⟨hx₁, hx₂⟩, exact ⟨((kaehler_differential.ideal R S).restrict_scalars S).smul_mem
+      r hx₁, submodule.smul_mem _ r hx₂⟩ }
+end
+
+variables {R S}
+
+/-- The linear map from `Ω[S⁄R]`, associated with a derivation. -/
+def derivation.lift_kaehler_differential (D : derivation R S M) : Ω[S⁄R] →ₗ[S] M :=
+begin
+  refine ((kaehler_differential.ideal R S • ⊤ :
+    submodule (S ⊗[R] S) (kaehler_differential.ideal R S)).restrict_scalars S).liftq _ _,
+  { exact D.tensor_product_to.comp ((kaehler_differential.ideal R S).subtype.restrict_scalars S) },
+  { intros x hx,
+    change _ = _,
+    apply submodule.smul_induction_on hx; clear hx x,
+    { rintros x (hx : _ = _) ⟨y, hy : _ = _⟩ -,
+      dsimp,
+      rw [derivation.tensor_product_to_mul, hx, hy, zero_smul, zero_smul, zero_add] },
+    { intros x y ex ey, rw [map_add, ex, ey, zero_add] } }
+end
+
+lemma derivation.lift_kaehler_differential_apply (D : derivation R S M) (x) :
+  D.lift_kaehler_differential
+    ((kaehler_differential.ideal R S).to_cotangent x) = D.tensor_product_to x :=
+rfl
+
+lemma derivation.lift_kaehler_differential_comp (D : derivation R S M) :
+  D.lift_kaehler_differential.comp_der (kaehler_differential.D R S) = D :=
+begin
+  ext a,
+  dsimp [kaehler_differential.D_apply],
+  refine (D.lift_kaehler_differential_apply _).trans _,
+  rw [subtype.coe_mk, map_sub, derivation.tensor_product_to_tmul,
+    derivation.tensor_product_to_tmul, one_smul, D.map_one_eq_zero, smul_zero, sub_zero],
+end
+
+@[ext]
+lemma derivation.lift_kaehler_differential_unique
+  (f f' : Ω[S⁄R] →ₗ[S] M)
+  (hf : f.comp_der (kaehler_differential.D R S) =
+    f'.comp_der (kaehler_differential.D R S)) :
+  f = f' :=
+begin
+  apply linear_map.ext,
+  intro x,
+  have : x ∈ submodule.span S (set.range $ kaehler_differential.D R S),
+  { rw kaehler_differential.span_range_derivation, trivial },
+  apply submodule.span_induction this,
+  { rintros _ ⟨x, rfl⟩, exact congr_arg (λ D : derivation R S M, D x) hf },
+  { rw [map_zero, map_zero] },
+  { intros x y hx hy, rw [map_add, map_add, hx, hy] },
+  { intros a x e, rw [map_smul, map_smul, e] }
+end
+
+variables (R S)
+
+lemma derivation.lift_kaehler_differential_D :
+  (kaehler_differential.D R S).lift_kaehler_differential = linear_map.id :=
+derivation.lift_kaehler_differential_unique _ _
+  (kaehler_differential.D R S).lift_kaehler_differential_comp
+
+variables {R S}
+
+lemma kaehler_differential.D_tensor_product_to (x : kaehler_differential.ideal R S) :
+  (kaehler_differential.D R S).tensor_product_to x =
+    (kaehler_differential.ideal R S).to_cotangent x :=
+begin
+  rw [← derivation.lift_kaehler_differential_apply, derivation.lift_kaehler_differential_D],
+  refl,
+end
+
+variables (R S)
+
+lemma kaehler_differential.tensor_product_to_surjective :
+  function.surjective (kaehler_differential.D R S).tensor_product_to :=
+begin
+  intro x, obtain ⟨x, rfl⟩ := (kaehler_differential.ideal R S).to_cotangent_surjective x,
+  exact ⟨x, kaehler_differential.D_tensor_product_to x⟩
+end
+
+/-- The `S`-linear maps from `Ω[S⁄R]` to `M` are (`S`-linearly) equivalent to `R`-derivations
+from `S` to `M`.  -/
+def kaehler_differential.linear_map_equiv_derivation : (Ω[S⁄R] →ₗ[S] M) ≃ₗ[S] derivation R S M :=
+{ inv_fun := derivation.lift_kaehler_differential,
+  left_inv := λ f, derivation.lift_kaehler_differential_unique _ _
+    (derivation.lift_kaehler_differential_comp _),
+  right_inv := derivation.lift_kaehler_differential_comp,
+  ..(derivation.llcomp.flip $ kaehler_differential.D R S) }
+
+end kaehler_differential