Derivations through localizations

The differentials of a localization are obtained by formally-etale base change. This file records the resulting extension operation and its specialization to the partial derivations of a polynomial ring.

noncomputable def AlgebraicAnalysis.DifferentialOperators.LocalizedPolynomialDerivations.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] (S : Submonoid A) [IsLocalization S B] (D : Derivation k A B) : Derivation k B B

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

Equations

• AlgebraicAnalysis.DifferentialOperators.LocalizedPolynomialDerivations.extendDerivation k A B S D = AlgebraicAnalysis.DifferentialOperators.FormallyEtaleDerivations.extendDerivation k A B D

@[simp]

theorem AlgebraicAnalysis.DifferentialOperators.LocalizedPolynomialDerivations.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] (S : Submonoid A) [IsLocalization S B] (D : Derivation k A B) : Derivation.compAlgebraMap A (extendDerivation k A B S D) = D

theorem AlgebraicAnalysis.DifferentialOperators.LocalizedPolynomialDerivations.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] (S : Submonoid A) [IsLocalization S B] {D₁ D₂ : Derivation k B B} (h : Derivation.compAlgebraMap A D₁ = Derivation.compAlgebraMap A D₂) : D₁ = D₂

A derivation of a localization is uniquely determined by its restriction to the original algebra.

@[reducible, inline]

abbrev AlgebraicAnalysis.DifferentialOperators.LocalizedPolynomialDerivations.PolynomialRing {k : Type u} {n : ℕ} [Field k] : Type u

The polynomial ring in n coordinate variables over k.

Equations

• AlgebraicAnalysis.DifferentialOperators.LocalizedPolynomialDerivations.PolynomialRing = MvPolynomial (Fin n) k

noncomputable def AlgebraicAnalysis.DifferentialOperators.LocalizedPolynomialDerivations.localizedPderiv {k : Type u} {n : ℕ} [Field k] (S : Submonoid PolynomialRing) (B : Type u) [CommRing B] [Algebra PolynomialRing B] [Algebra k B] [IsScalarTower k PolynomialRing B] [IsLocalization S B] (i : Fin n) : Derivation k B B

The ith polynomial partial derivative, transported to a localization.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicAnalysis.DifferentialOperators.LocalizedPolynomialDerivations.localizedPderiv_compAlgebraMap {k : Type u} {n : ℕ} [Field k] (S : Submonoid PolynomialRing) (B : Type u) [CommRing B] [Algebra PolynomialRing B] [Algebra k B] [IsScalarTower k PolynomialRing B] [IsLocalization S B] (i : Fin n) : Derivation.compAlgebraMap (MvPolynomial (Fin n) k) (localizedPderiv S B i) = (Algebra.linearMap (MvPolynomial (Fin n) k) B).compDer (MvPolynomial.pderiv i)

theorem AlgebraicAnalysis.DifferentialOperators.LocalizedPolynomialDerivations.localizedPderiv_apply_algebraMap_X {k : Type u} {n : ℕ} [Field k] (S : Submonoid PolynomialRing) (B : Type u) [CommRing B] [Algebra PolynomialRing B] [Algebra k B] [IsScalarTower k PolynomialRing B] [IsLocalization S B] (i j : Fin n) : (localizedPderiv S B i) ((algebraMap PolynomialRing B) (MvPolynomial.X j)) = if i = j then 1 else 0

theorem AlgebraicAnalysis.DifferentialOperators.LocalizedPolynomialDerivations.localizedPderiv_comm {k : Type u} {n : ℕ} [Field k] (S : Submonoid PolynomialRing) (B : Type u) [CommRing B] [Algebra PolynomialRing B] [Algebra k B] [IsScalarTower k PolynomialRing B] [IsLocalization S B] (i j : Fin n) : ↑(localizedPderiv S B i) ∘ₗ ↑(localizedPderiv S B j) = ↑(localizedPderiv S B j) ∘ₗ ↑(localizedPderiv S B i)