feat(RingTheory/Derivation): define Differential and DifferentialAlgebra typeclasses (#14699)

Define a typeclass `Differential` of `CommRing`s with a chosen `Derivation`, a notation for that derivation, and a `DifferentialAlgebra` for `Algerba`s on differential rings whose `algebraMap` commutes with the derivation.



Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>

Author: Command-Master

Mathlib.lean

@@ -3753,6 +3753,7 @@ import Mathlib.RingTheory.DedekindDomain.PID
 import Mathlib.RingTheory.DedekindDomain.SInteger
 import Mathlib.RingTheory.DedekindDomain.SelmerGroup
 import Mathlib.RingTheory.Derivation.Basic
+import Mathlib.RingTheory.Derivation.DifferentialRing
 import Mathlib.RingTheory.Derivation.Lie
 import Mathlib.RingTheory.Derivation.ToSquareZero
 import Mathlib.RingTheory.DiscreteValuationRing.Basic

Mathlib/RingTheory/Derivation/Basic.lean

@@ -474,5 +474,4 @@ end
 
 end
 
-
 end Derivation

Mathlib/RingTheory/Derivation/DifferentialRing.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2024 Daniel Weber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Weber
+-/
+import Mathlib.RingTheory.Derivation.Basic
+
+/-!
+# Differential and Algebras
+
+This file defines derivations from a commutative ring to itself as a typeclass, which lets us
+use the x′ notation for the derivative of x.
+-/
+
+/-- A derivation from a ring to itself, as a typeclass. -/
+class Differential (R : Type*) [CommRing R] where
+  /-- The `Derivation` assosiated with the ring. -/
+  deriv : Derivation ℤ R R
+
+@[inherit_doc]
+scoped[Differential] postfix:max "′" => Differential.deriv
+
+open scoped Differential
+
+open Lean PrettyPrinter Delaborator SubExpr in
+/--
+A delaborator for the x′ notation. This is required because it's not direct function application,
+so the default delaborator doesn't work.
+-/
+@[delab app.DFunLike.coe]
+def delabDeriv : Delab := do
+  let e ← getExpr
+  guard <| e.isAppOfArity' ``DFunLike.coe 6
+  guard <| (e.getArg!' 4).isAppOf' ``Differential.deriv
+  let arg ← withAppArg delab
+  `($arg′)
+
+/--
+A differential algebra is an `Algebra` where the derivation commutes with `algebraMap`.
+-/
+class DifferentialAlgebra (A B : Type*) [CommRing A] [CommRing B] [Algebra A B]
+    [Differential A] [Differential B] : Prop where
+  deriv_algebraMap : ∀ a : A, (algebraMap A B a)′ = algebraMap A B a′
+
+export DifferentialAlgebra (deriv_algebraMap)
+
+@[norm_cast]
+lemma algebraMap.coe_deriv {A : Type*} {B : Type*} [CommRing A] [CommRing B] [Algebra A B]
+    [Differential A] [Differential B] [DifferentialAlgebra A B] (a : A) :
+    (a′ : A) = (a : B)′ :=
+  (DifferentialAlgebra.deriv_algebraMap _).symm
+
+/--
+A differential ring `A` and an algebra over it `B` share constants if all
+constants in B are in the range of `algberaMap A B`.
+-/
+class Differential.ContainConstants (A B : Type*) [CommRing A] [CommRing B]
+    [Algebra A B] [Differential B] : Prop where
+  /-- If the derivative of x is 0, then it's in the range of `algberaMap A B`. -/
+  protected mem_range_of_deriv_eq_zero {x : B} (h : x′ = 0) : x ∈ (algebraMap A B).range
+
+lemma mem_range_of_deriv_eq_zero (A : Type*) {B : Type*} [CommRing A] [CommRing B] [Algebra A B]
+    [Differential B] [Differential.ContainConstants A B] {x : B} (h : x′ = 0) :
+    x ∈ (algebraMap A B).range :=
+  Differential.ContainConstants.mem_range_of_deriv_eq_zero h
+
+instance (A : Type*) [CommRing A] [Differential A] : DifferentialAlgebra A A where
+  deriv_algebraMap _ := rfl
+
+instance (A : Type*) [CommRing A] [Differential A] : Differential.ContainConstants A A where
+  mem_range_of_deriv_eq_zero {x} _ := ⟨x, rfl⟩
+
+/-- Transfer a `Differential` instance accross a `RingEquiv`. -/
+@[reducible]
+def Differential.equiv {R R₂ : Type*} [CommRing R] [CommRing R₂] [Differential R₂]
+    (h : R ≃+* R₂) : Differential R :=
+  ⟨Derivation.mk' (h.symm.toAddMonoidHom.toIntLinearMap ∘ₗ
+    Differential.deriv.toLinearMap ∘ₗ h.toAddMonoidHom.toIntLinearMap) (by simp)⟩
+
+/--
+Transfer a `DifferentialAlgebra` instance accross a `AlgEquiv`.
+-/
+lemma DifferentialAlgebra.equiv {A : Type*} [CommRing A] [Differential A]
+    {R R₂ : Type*} [CommRing R] [CommRing R₂] [Differential R₂] [Algebra A R]
+    [Algebra A R₂] [DifferentialAlgebra A R₂] (h : R ≃ₐ[A] R₂) :
+    letI := Differential.equiv h.toRingEquiv
+    DifferentialAlgebra A R :=
+  letI := Differential.equiv h.toRingEquiv
+  ⟨fun a ↦ by
+    change (LinearMap.comp ..) _ = _
+    simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.toAddMonoidHom_eq_coe,
+      RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom, LinearMap.coe_comp,
+      AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.coe_coe, RingHom.coe_coe, Derivation.coeFn_coe,
+      Function.comp_apply, AlgEquiv.commutes, deriv_algebraMap]
+    apply h.symm.commutes⟩