Documentation

LeanPool.Stafford38.AlgebraicAnalysis.DifferentialOperators.FormallyEtaleDerivations

Derivations through formally étale algebras #

The base-change equivalence for Kähler differentials extends derivations uniquely. Localizations and separable field extensions use this common construction.

source
noncomputable def AlgebraicAnalysis.DifferentialOperators.FormallyEtaleDerivations.extendDerivation (k A B : Type u) [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] [Algebra.FormallyEtale A B] (D : Derivation k A B) :
Derivation k B B

Extend a k-derivation through a formally étale algebra A → B, by the formally-etale base-change equivalence for Kähler differentials.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AlgebraicAnalysis.DifferentialOperators.FormallyEtaleDerivations.extendDerivation_compAlgebraMap (k A B : Type u) [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] [Algebra.FormallyEtale A B] (D : Derivation k A B) :
    Derivation.compAlgebraMap A (extendDerivation k A B D) = D
    source
    theorem AlgebraicAnalysis.DifferentialOperators.FormallyEtaleDerivations.derivation_ext_of_compAlgebraMap_eq (k A B : Type u) [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] [Algebra.FormallyEtale A B] {D₁ D₂ : Derivation k B B} (h : Derivation.compAlgebraMap A D₁ = Derivation.compAlgebraMap A D₂) :
    D₁ = D₂

    A derivation of a formally étale algebra is uniquely determined by its restriction to the original algebra.