feat(ring_theory/derivation): A presentation of the Kähler differential module (#17011)

We add an alternative description of `Ω[S⁄R]`, presenting it as `S` copies of `S` with kernel generated by the relations:
1. `dx + dy = d(x + y)`
2. `x dy + y dx = d(x * y)`
3. `dr = 0` for `r ∈ R` 



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

Author: erdOne

src/ring_theory/derivation.lean

@@ -31,12 +31,19 @@ This file defines derivation. A derivation `D` from the `R`-algebra `A` to the `
 - `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)`.
+- `kaehler_differential.quot_ker_total_equiv`: An alternative description of `Ω[S⁄R]` as `S` copies
+  of `S` with kernel (`kaehler_differential.ker_total`) generated by the relations:
+  1. `dx + dy = d(x + y)`
+  2. `x dy + y dx = d(x * y)`
+  3. `dr = 0` for `r ∈ R`
 - `kaehler_differential.map`: Given a map between the arrows `R → A` and `S → B`, we have an
   `A`-linear map `Ω[A⁄R] → Ω[B⁄S]`.
 
 ## Future project
 
-Generalize this into bimodules.
+- Generalize derivations into bimodules.
+- Define a `is_kaehler_differential` predicate.
+
 -/
 
 open algebra
@@ -717,6 +724,10 @@ begin
     derivation.tensor_product_to_tmul, one_smul, D.map_one_eq_zero, smul_zero, sub_zero],
 end
 
+@[simp] lemma derivation.lift_kaehler_differential_comp_D (D' : derivation R S M) (x : S) :
+  D'.lift_kaehler_differential (kaehler_differential.D R S x) = D' x :=
+derivation.congr_fun D'.lift_kaehler_differential_comp x
+
 @[ext]
 lemma derivation.lift_kaehler_differential_unique
   (f f' : Ω[S⁄R] →ₗ[S] M)
@@ -847,6 +858,169 @@ def kaehler_differential.End_equiv :
   (kaehler_differential.ideal R S).cotangent_ideal_square).trans $
   kaehler_differential.End_equiv_aux_equiv R S
 
+section presentation
+
+open kaehler_differential (D)
+open finsupp (single)
+
+/-- The `S`-submodule of `S →₀ S` (the direct sum of copies of `S` indexed by `S`) generated by
+the relations:
+1. `dx + dy = d(x + y)`
+2. `x dy + y dx = d(x * y)`
+3. `dr = 0` for `r ∈ R`
+where `db` is the unit in the copy of `S` with index `b`.
+
+This is the kernel of the surjection `finsupp.total S Ω[S⁄R] S (kaehler_differential.D R S)`.
+See `kaehler_differential.ker_total_eq` and `kaehler_differential.total_surjective`.
+-/
+noncomputable
+def kaehler_differential.ker_total : submodule S (S →₀ S) :=
+submodule.span S
+  ((set.range (λ (x : S × S), single x.1 1 + single x.2 1 - single (x.1 + x.2) 1)) ∪
+  (set.range (λ (x : S × S), single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1)) ∪
+  (set.range (λ x : R, single (algebra_map R S x) 1)))
+
+local notation x `𝖣` y := (kaehler_differential.ker_total R S).mkq (single y x)
+
+lemma kaehler_differential.ker_total_mkq_single_add (x y z) :
+  (z 𝖣 (x + y)) = (z 𝖣 x) + (z 𝖣 y) :=
+begin
+  rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub, submodule.mkq_apply,
+    submodule.quotient.mk_eq_zero],
+  simp_rw [← finsupp.smul_single_one _ z, ← smul_add, ← smul_sub],
+  exact submodule.smul_mem _ _ (submodule.subset_span (or.inl $ or.inl $ ⟨⟨_, _⟩, rfl⟩)),
+end
+
+lemma kaehler_differential.ker_total_mkq_single_mul (x y z) :
+  (z 𝖣 (x * y)) = ((z * x) 𝖣 y) + ((z * y) 𝖣 x) :=
+begin
+  rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub, submodule.mkq_apply,
+    submodule.quotient.mk_eq_zero],
+  simp_rw [← finsupp.smul_single_one _ z, ← @smul_eq_mul _ _ z,
+    ← finsupp.smul_single, ← smul_add, ← smul_sub],
+  exact submodule.smul_mem _ _ (submodule.subset_span (or.inl $ or.inr $ ⟨⟨_, _⟩, rfl⟩)),
+end
+
+lemma kaehler_differential.ker_total_mkq_single_algebra_map (x y) :
+  (y 𝖣 (algebra_map R S x)) = 0 :=
+begin
+  rw [submodule.mkq_apply, submodule.quotient.mk_eq_zero, ← finsupp.smul_single_one _ y],
+  exact submodule.smul_mem _ _ (submodule.subset_span (or.inr $ ⟨_, rfl⟩)),
+end
+
+lemma kaehler_differential.ker_total_mkq_single_algebra_map_one (x) :
+  (x 𝖣 1) = 0 :=
+begin
+  rw [← (algebra_map R S).map_one, kaehler_differential.ker_total_mkq_single_algebra_map],
+end
+
+lemma kaehler_differential.ker_total_mkq_single_smul (r : R) (x y) :
+  (y 𝖣 (r • x)) = r • (y 𝖣 x) :=
+begin
+  rw [algebra.smul_def, kaehler_differential.ker_total_mkq_single_mul,
+    kaehler_differential.ker_total_mkq_single_algebra_map, add_zero,
+    ← linear_map.map_smul_of_tower, finsupp.smul_single, mul_comm, algebra.smul_def],
+end
+
+/-- The (universal) derivation into `(S →₀ S) ⧸ kaehler_differential.ker_total R S`. -/
+noncomputable
+def kaehler_differential.derivation_quot_ker_total :
+  derivation R S ((S →₀ S) ⧸ kaehler_differential.ker_total R S) :=
+{ to_fun := λ x, 1 𝖣 x,
+  map_add' := λ x y, kaehler_differential.ker_total_mkq_single_add _ _ _ _ _,
+  map_smul' := λ r s, kaehler_differential.ker_total_mkq_single_smul _ _ _ _ _,
+  map_one_eq_zero' := kaehler_differential.ker_total_mkq_single_algebra_map_one _ _ _,
+  leibniz' := λ a b, (kaehler_differential.ker_total_mkq_single_mul _ _ _ _ _).trans
+    (by { simp_rw [← finsupp.smul_single_one _ (1 * _ : S)], dsimp, simp }) }
+
+lemma kaehler_differential.derivation_quot_ker_total_apply (x) :
+  kaehler_differential.derivation_quot_ker_total R S x = (1 𝖣 x) := rfl
+
+lemma kaehler_differential.derivation_quot_ker_total_lift_comp_total :
+  (kaehler_differential.derivation_quot_ker_total R S).lift_kaehler_differential.comp
+    (finsupp.total S Ω[S⁄R] S (kaehler_differential.D R S)) = submodule.mkq _ :=
+begin
+  apply finsupp.lhom_ext,
+  intros a b,
+  conv_rhs { rw [← finsupp.smul_single_one a b, linear_map.map_smul] },
+  simp [kaehler_differential.derivation_quot_ker_total_apply],
+end
+
+lemma kaehler_differential.ker_total_eq :
+  (finsupp.total S Ω[S⁄R] S (kaehler_differential.D R S)).ker =
+    kaehler_differential.ker_total R S :=
+begin
+  apply le_antisymm,
+  { conv_rhs { rw ← (kaehler_differential.ker_total R S).ker_mkq },
+    rw ← kaehler_differential.derivation_quot_ker_total_lift_comp_total,
+    exact linear_map.ker_le_ker_comp _ _ },
+  { rw [kaehler_differential.ker_total, submodule.span_le],
+    rintros _ ((⟨⟨x, y⟩, rfl⟩|⟨⟨x, y⟩, rfl⟩)|⟨x, rfl⟩); dsimp; simp [linear_map.mem_ker] },
+end
+
+lemma kaehler_differential.total_surjective :
+  function.surjective (finsupp.total S Ω[S⁄R] S (kaehler_differential.D R S)) :=
+begin
+  rw [← linear_map.range_eq_top, finsupp.range_total, kaehler_differential.span_range_derivation],
+end
+
+/-- `Ω[S⁄R]` is isomorphic to `S` copies of `S` with kernel `kaehler_differential.ker_total`. -/
+@[simps] noncomputable
+def kaehler_differential.quot_ker_total_equiv :
+  ((S →₀ S) ⧸ kaehler_differential.ker_total R S) ≃ₗ[S] Ω[S⁄R] :=
+{ inv_fun := (kaehler_differential.derivation_quot_ker_total R S).lift_kaehler_differential,
+  left_inv := begin
+    intro x,
+    obtain ⟨x, rfl⟩ := submodule.mkq_surjective _ x,
+    exact linear_map.congr_fun
+      (kaehler_differential.derivation_quot_ker_total_lift_comp_total R S : _) x,
+  end,
+  right_inv := begin
+    intro x,
+    obtain ⟨x, rfl⟩ := kaehler_differential.total_surjective R S x,
+    erw linear_map.congr_fun
+      (kaehler_differential.derivation_quot_ker_total_lift_comp_total R S : _) x,
+    refl
+  end,
+  ..(kaehler_differential.ker_total R S).liftq
+    (finsupp.total S Ω[S⁄R] S (kaehler_differential.D R S))
+    (kaehler_differential.ker_total_eq R S).ge }
+
+lemma kaehler_differential.quot_ker_total_equiv_symm_comp_D :
+  (kaehler_differential.quot_ker_total_equiv R S).symm.to_linear_map.comp_der
+    (kaehler_differential.D R S) = kaehler_differential.derivation_quot_ker_total R S :=
+by convert
+  (kaehler_differential.derivation_quot_ker_total R S).lift_kaehler_differential_comp using 0
+
+variables (A B : Type*) [comm_ring A] [comm_ring B] [algebra R A] [algebra S B] [algebra R B]
+variables [algebra A B] [is_scalar_tower R S B] [is_scalar_tower R A B]
+
+-- The map `(A →₀ A) →ₗ[A] (B →₀ B)`
+local notation `finsupp_map` := ((finsupp.map_range.linear_map (algebra.of_id A B).to_linear_map)
+  .comp (finsupp.lmap_domain A A (algebra_map A B)))
+
+lemma kaehler_differential.ker_total_map (h : function.surjective (algebra_map A B)) :
+  (kaehler_differential.ker_total R A).map finsupp_map ⊔
+    submodule.span A (set.range (λ x : S, single (algebra_map S B x) (1 : B))) =
+    (kaehler_differential.ker_total S B).restrict_scalars _  :=
+begin
+  rw [kaehler_differential.ker_total, submodule.map_span, kaehler_differential.ker_total,
+    ← submodule.span_eq_restrict_scalars _ _ _ _ h],
+  simp_rw [set.image_union, submodule.span_union, ← set.image_univ, set.image_image,
+    set.image_univ, map_sub, map_add],
+  simp only [linear_map.comp_apply, finsupp.map_range.linear_map_apply, finsupp.map_range_single,
+    finsupp.lmap_domain_apply, finsupp.map_domain_single, alg_hom.to_linear_map_apply,
+    algebra.of_id_apply, ← is_scalar_tower.algebra_map_apply, map_one, map_add, map_mul],
+  simp_rw [sup_assoc, ← (h.prod_map h).range_comp],
+  congr' 3,
+  rw [sup_eq_right],
+  apply submodule.span_mono,
+  simp_rw is_scalar_tower.algebra_map_apply R S B,
+  exact set.range_comp_subset_range (algebra_map R S) (λ x, single (algebra_map S B x) (1 : B))
+end
+
+end presentation
+
 section exact_sequence
 
 local attribute [irreducible] kaehler_differential