Documentation

Mathlib.RingTheory.Derivation.DifferentialRing

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.

class Differential (R : Type u_1) [CommRing R] :
Type u_1

A derivation from a ring to itself, as a typeclass.

Instances

    A delaborator for the x′ notation. This is required because it's not direct function application, so the default delaborator doesn't work.

    Equations
    • One or more equations did not get rendered due to their size.
    class DifferentialAlgebra (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Differential A] [Differential B] :

    A differential algebra is an Algebra where the derivation commutes with algebraMap.

    Instances
    theorem DifferentialAlgebra.deriv_algebraMap {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Differential A] [Differential B] [self : DifferentialAlgebra A B] (a : A) :
    ((algebraMap A B) a) = (algebraMap A B) a
    theorem algebraMap.coe_deriv {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Differential A] [Differential B] [DifferentialAlgebra A B] (a : A) :
    a = (↑a)
    class Differential.ContainConstants (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Differential B] :

    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.

    • mem_range_of_deriv_eq_zero : ∀ {x : B}, x = 0x (algebraMap A B).range

      If the derivative of x is 0, then it's in the range of algberaMap A B.

    Instances
    theorem Differential.ContainConstants.mem_range_of_deriv_eq_zero {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Differential B] [self : Differential.ContainConstants A B] {x : B} (h : x = 0) :
    x (algebraMap A B).range

    If the derivative of x is 0, then it's in the range of algberaMap A B.

    theorem mem_range_of_deriv_eq_zero (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Differential B] [Differential.ContainConstants A B] {x : B} (h : x = 0) :
    x (algebraMap A B).range
    Equations
    • =
    @[reducible]
    def Differential.equiv {R : Type u_1} {R₂ : Type u_2} [CommRing R] [CommRing R₂] [Differential R₂] (h : R ≃+* R₂) :

    Transfer a Differential instance across a RingEquiv.

    Equations
    theorem DifferentialAlgebra.equiv {A : Type u_1} [CommRing A] [Differential A] {R : Type u_2} {R₂ : Type u_3} [CommRing R] [CommRing R₂] [Differential R₂] [Algebra A R] [Algebra A R₂] [DifferentialAlgebra A R₂] (h : R ≃ₐ[A] R₂) :

    Transfer a DifferentialAlgebra instance across a AlgEquiv.