Kaehler2.lean

/-
Copyright © 2020 Nicolò Cavalleri. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Nicolò Cavalleri, Andrew Yang
-/
import Mathlib.RingTheory.Derivation.ToSquareZero
import Mathlib.RingTheory.Ideal.Cotangent
import Mathlib.RingTheory.IsTensorProduct

#align_import ring_theory.kaehler from "leanprover-community/mathlib"@"b608348ffaeb7f557f2fd46876037abafd326ff3"

/-!
# The module of kaehler differentials

## Main results

- `KaehlerDifferential`: The module of kaehler differentials. For an `R`-algebra `S`, we provide
  the notation `Ω[S⁄R]` for `KaehlerDifferential R S`.
  Note that the slash is `\textfractionsolidus`.
- `KaehlerDifferential.D`: The derivation into the module of kaehler differentials.
- `KaehlerDifferential.span_range_derivation`: The image of `D` spans `Ω[S⁄R]` as an `S`-module.
- `KaehlerDifferential.linearMapEquivDerivation`:
  The isomorphism `Hom_R(Ω[S⁄R], M) ≃ₗ[S] Der_R(S, M)`.
- `KaehlerDifferential.quotKerTotalEquiv`: An alternative description of `Ω[S⁄R]` as `S` copies
  of `S` with kernel (`KaehlerDifferential.kerTotal`) generated by the relations:
  1. `dx + dy = d(x + y)`
  2. `x dy + y dx = d(x * y)`
  3. `dr = 0` for `r ∈ R`
- `KaehlerDifferential.map`: Given a map between the arrows `R → A` and `S → B`, we have an
  `A`-linear map `Ω[A⁄R] → Ω[B⁄S]`.

## Future project

- Define the `IsKaehlerDifferential` predicate.
-/

section KaehlerDifferential

open scoped TensorProduct
open Algebra

universe u v

variable (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]

/-- The kernel of the multiplication map `S ⊗[R] S →ₐ[R] S`. -/
abbrev KaehlerDifferential.ideal : Ideal (S ⊗[R] S) :=
  RingHom.ker (TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S)
#align kaehler_differential.ideal KaehlerDifferential.ideal

variable {S}

theorem KaehlerDifferential.one_smul_sub_smul_one_mem_ideal (a : S) :
    (1 : S) ⊗ₜ[R] a - a ⊗ₜ[R] (1 : S) ∈ KaehlerDifferential.ideal R S := by simp [RingHom.mem_ker]
#align kaehler_differential.one_smul_sub_smul_one_mem_ideal KaehlerDifferential.one_smul_sub_smul_one_mem_ideal

variable {R}

variable {M : Type _} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]

/-- For a `R`-derivation `S → M`, this is the map `S ⊗[R] S →ₗ[S] M` sending `s ⊗ₜ t ↦ s • D t`. -/
def Derivation.tensorProductTo (D : Derivation R S M) : S ⊗[R] S →ₗ[S] M :=
  TensorProduct.AlgebraTensorModule.lift ((LinearMap.lsmul S (S →ₗ[R] M)).flip D.toLinearMap)
#align derivation.tensor_product_to Derivation.tensorProductTo

theorem Derivation.tensorProductTo_tmul (D : Derivation R S M) (s t : S) :
    D.tensorProductTo (s ⊗ₜ t) = s • D t := rfl
#align derivation.tensor_product_to_tmul Derivation.tensorProductTo_tmul

theorem Derivation.tensorProductTo_mul (D : Derivation R S M) (x y : S ⊗[R] S) :
    D.tensorProductTo (x * y) =
      TensorProduct.lmul' R x • D.tensorProductTo y +
        TensorProduct.lmul' R y • D.tensorProductTo x := by
  refine TensorProduct.induction_on x ?_ ?_ ?_
  · rw [MulZeroClass.zero_mul, map_zero, map_zero, zero_smul, smul_zero, add_zero]
  swap
  · intro x₁ y₁ h₁ h₂
    rw [add_mul, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]
  intro x₁ x₂
  refine TensorProduct.induction_on y ?_ ?_ ?_
  · rw [MulZeroClass.mul_zero, map_zero, map_zero, zero_smul, smul_zero, add_zero]
  swap
  · intro x₁ y₁ h₁ h₂
    rw [mul_add, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]
  intro x y
  simp only [TensorProduct.tmul_mul_tmul, Derivation.tensorProductTo,
    TensorProduct.AlgebraTensorModule.lift_apply, TensorProduct.lift.tmul',
    TensorProduct.lmul'_apply_tmul]
  dsimp
  rw [D.leibniz]
  simp only [smul_smul, smul_add, mul_comm (x * y) x₁, mul_right_comm x₁ x₂, ← mul_assoc]
#align derivation.tensor_product_to_mul Derivation.tensorProductTo_mul

variable (R S)

/-- The kernel of `S ⊗[R] S →ₐ[R] S` is generated by `1 ⊗ s - s ⊗ 1` as a `S`-module. -/
theorem KaehlerDifferential.submodule_span_range_eq_ideal :
    Submodule.span S (Set.range fun s : S => (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)) =
      (KaehlerDifferential.ideal R S).restrictScalars S := by
  apply le_antisymm
  · rw [Submodule.span_le]
    rintro _ ⟨s, rfl⟩
    exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _
  · rintro x (hx : _ = _)
    have : x - TensorProduct.lmul' R x ⊗ₜ[R] (1 : S) = x := by
      rw [hx, TensorProduct.zero_tmul, sub_zero]
    rw [← this]
    clear this hx
    refine TensorProduct.induction_on x ?_ ?_ ?_
    · rw [map_zero, TensorProduct.zero_tmul, sub_zero]; exact zero_mem _
    · intro x y
      have : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] (1 : S) = x • ((1 : S) ⊗ₜ y - y ⊗ₜ (1 : S)) := by
        simp_rw [smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
      rw [TensorProduct.lmul'_apply_tmul, this]
      refine Submodule.smul_mem _ x ?_
      apply Submodule.subset_span
      exact Set.mem_range_self y
    · intro x y hx hy
      rw [map_add, TensorProduct.add_tmul, ← sub_add_sub_comm]
      exact add_mem hx hy
#align kaehler_differential.submodule_span_range_eq_ideal KaehlerDifferential.submodule_span_range_eq_ideal

theorem KaehlerDifferential.span_range_eq_ideal :
    Ideal.span (Set.range fun s : S => (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)) =
      KaehlerDifferential.ideal R S := by
  apply le_antisymm
  · rw [Ideal.span_le]
    rintro _ ⟨s, rfl⟩
    exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _
  · change (KaehlerDifferential.ideal R S).restrictScalars S ≤ (Ideal.span _).restrictScalars S
    rw [← KaehlerDifferential.submodule_span_range_eq_ideal, Ideal.span]
    conv_rhs => rw [← Submodule.span_span_of_tower S]
    exact Submodule.subset_span
#align kaehler_differential.span_range_eq_ideal KaehlerDifferential.span_range_eq_ideal

/-- 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
`KaehlerDifferential.tensorProductTo_surjective` and `Derivation.tensorProductTo_tmul`.

We also provide the notation `Ω[S⁄R]` for `KaehlerDifferential R S`.
Note that the slash is `\textfractionsolidus`.
-/
def KaehlerDifferential : Type _ :=
  (KaehlerDifferential.ideal R S).Cotangent
#align kaehler_differential KaehlerDifferential

instance : AddCommGroup (KaehlerDifferential R S) := by
  unfold KaehlerDifferential
  infer_instance

instance KaehlerDifferential.module : Module (S ⊗[R] S) (KaehlerDifferential R S) :=
  Ideal.Cotangent.moduleOfTower _
#align kaehler_differential.module KaehlerDifferential.module

notation:100 "Ω[" S "⁄" R "]" => KaehlerDifferential R S

instance : Nonempty (Ω[S⁄R]) := ⟨0⟩

instance KaehlerDifferential.module' {R' : Type _} [CommRing R'] [Algebra R' S] :
    Module R' (Ω[S⁄R]) :=
  (Module.compHom (KaehlerDifferential.ideal R S).Cotangent (algebraMap R' S) : _)
#align kaehler_differential.module' KaehlerDifferential.module'

instance : IsScalarTower S (S ⊗[R] S) (Ω[S⁄R]) :=
  Ideal.Cotangent.isScalarTower _

instance KaehlerDifferential.isScalarTower_of_tower {R₁ R₂ : Type _} [CommRing R₁] [CommRing R₂]
    [Algebra R₁ S] [Algebra R₂ S] [Algebra R₁ R₂] [IsScalarTower R₁ R₂ S] :
    IsScalarTower R₁ R₂ (Ω[S⁄R]) := by
  convert RestrictScalars.isScalarTower R₁ R₂ (Ω[S⁄R]) using 1
  ext (x m)
  show algebraMap R₁ S x • m = algebraMap R₂ S (algebraMap R₁ R₂ x) • m
  rw [← IsScalarTower.algebraMap_apply]
#align kaehler_differential.is_scalar_tower_of_tower KaehlerDifferential.isScalarTower_of_tower

instance KaehlerDifferential.isScalarTower' : IsScalarTower R (S ⊗[R] S) (Ω[S⁄R]) := by
  convert RestrictScalars.isScalarTower R (S ⊗[R] S) (Ω[S⁄R]) using 1
  ext (x m)
  show algebraMap R S x • m = algebraMap R (S ⊗[R] S) x • m
  simp_rw [IsScalarTower.algebraMap_apply R S (S ⊗[R] S), IsScalarTower.algebraMap_smul]
#align kaehler_differential.is_scalar_tower' KaehlerDifferential.isScalarTower'

/-- The quotient map `I → Ω[S⁄R]` with `I` being the kernel of `S ⊗[R] S → S`. -/
def KaehlerDifferential.fromIdeal : KaehlerDifferential.ideal R S →ₗ[S ⊗[R] S] Ω[S⁄R] :=
  (KaehlerDifferential.ideal R S).toCotangent
#align kaehler_differential.from_ideal KaehlerDifferential.fromIdeal

/-- (Implementation) The underlying linear map of the derivation into `Ω[S⁄R]`. -/
def KaehlerDifferential.DLinearMap : S →ₗ[R] Ω[S⁄R] :=
  ((KaehlerDifferential.fromIdeal R S).restrictScalars R).comp
    ((TensorProduct.includeRight.toLinearMap - TensorProduct.includeLeft.toLinearMap :
            S →ₗ[R] S ⊗[R] S).codRestrict
        ((KaehlerDifferential.ideal R S).restrictScalars R)
        (KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R) :
      _ →ₗ[R] _)
set_option linter.uppercaseLean3 false in
#align kaehler_differential.D_linear_map KaehlerDifferential.DLinearMap

theorem KaehlerDifferential.DLinearMap_apply (s : S) :
    KaehlerDifferential.DLinearMap R S s =
      (KaehlerDifferential.ideal R S).toCotangent
        ⟨1 ⊗ₜ s - s ⊗ₜ 1, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R s⟩ := rfl
set_option linter.uppercaseLean3 false in
#align kaehler_differential.D_linear_map_apply KaehlerDifferential.DLinearMap_apply

--      set_option pp.all true in
/-- The universal derivation into `Ω[S⁄R]`. -/
def KaehlerDifferential.D : Derivation R S (Ω[S⁄R]) :=
  { KaehlerDifferential.DLinearMap R S with
    map_one_eq_zero' := by sorry
    leibniz' := fun a b => by
      have : LinearMap.CompatibleSMul { x // x ∈ ideal R S } (Ω[S⁄R]) S (S ⊗[R] S) := inferInstance
      dsimp [KaehlerDifferential.DLinearMap_apply, - Ideal.toCotangent_apply]
/-
                  [Meta.synthInstance] [0.212955s] ✅ AddCommMonoid { x // x ∈ KaehlerDifferential.ideal R S } ▶
-/
      have foo := @LinearMap.map_smul_of_tower (M₂ := Ω[S⁄R])
      set_option trace.profiler true in
      --set_option trace.Meta.isDefEq true in
      rw [← foo]
      sorry }