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.

• deriv : Derivation ℤ R R

  The Derivation associated with the ring.

def Differential.«term_′» : Lean.TrailingParserDescr

The Derivation associated with the ring.

Equations

• Differential.«term_′» = Lean.ParserDescr.trailingNode `Differential.«term_′» 1024 1024 (Lean.ParserDescr.symbol "′")

def delabDeriv : Lean.PrettyPrinter.Delaborator.Delab

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] : Prop

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

• deriv_algebraMap : ∀ (a : A), ((algebraMap A B) a)′ = (algebraMap A B) a′

theorem DifferentialAlgebra.deriv_algebraMap {A : Type u_1} {B : Type u_2} : ∀ {inst : CommRing A} {inst_1 : CommRing B} {inst_2 : Algebra A B} {inst_3 : Differential A} {inst_4 : 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] : Prop

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′ = 0 → x ∈ (algebraMap A B).range

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

theorem Differential.ContainConstants.mem_range_of_deriv_eq_zero {A : Type u_1} {B : Type u_2} : ∀ {inst : CommRing A} {inst_1 : CommRing B} {inst_2 : Algebra A B} {inst_3 : Differential B} [self : Differential.ContainConstants A B] {x : B}, 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

instance instDifferentialAlgebra (A : Type u_1) [CommRing A] [Differential A] : DifferentialAlgebra A A

Equations

• ⋯ = ⋯

instance instContainConstants (A : Type u_1) [CommRing A] [Differential A] : Differential.ContainConstants A A

Equations

• ⋯ = ⋯

@[reducible]

def Differential.equiv {R : Type u_1} {R₂ : Type u_2} [CommRing R] [CommRing R₂] [Differential R₂] (h : R ≃+* R₂) : Differential R

Transfer a Differential instance across a RingEquiv.

Equations

• Differential.equiv h = { deriv := Derivation.mk' (h.symm.toAddMonoidHom.toIntLinearMap ∘ₗ ↑Differential.deriv ∘ₗ h.toAddMonoidHom.toIntLinearMap) ⋯ }

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₂) : DifferentialAlgebra A R

Transfer a DifferentialAlgebra instance across a AlgEquiv.