# The module of kaehler differentials #

## Main results #

• KaehlerDifferential: The module of kaehler differentials. For an R-algebra S, we provide the notation Ω[S⁄R] for KaehlerDifferential R S. Note that the slash is \textfractionsolidus.
• KaehlerDifferential.D: The derivation into the module of kaehler differentials.
• KaehlerDifferential.span_range_derivation: The image of D spans Ω[S⁄R] as an S-module.
• KaehlerDifferential.linearMapEquivDerivation: The isomorphism Hom_R(Ω[S⁄R], M) ≃ₗ[S] Der_R(S, M).
• KaehlerDifferential.quotKerTotalEquiv: An alternative description of Ω[S⁄R] as S copies of S with kernel (KaehlerDifferential.kerTotal) generated by the relations:
1. dx + dy = d(x + y)
2. x dy + y dx = d(x * y)
3. dr = 0 for r ∈ R
• KaehlerDifferential.map: Given a map between the arrows R →+* A and S →+* B, we have an A-linear map Ω[A⁄R] → Ω[B⁄S].
• KaehlerDifferential.map_surjective: The sequence Ω[B⁄R] → Ω[B⁄A] → 0 is exact.
• KaehlerDifferential.exact_mapBaseChange_map: The sequence B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] is exact.

## Future project #

• Define the IsKaehlerDifferential predicate.
@[reducible, inline]
noncomputable abbrev KaehlerDifferential.ideal (R : Type u) (S : Type v) [] [] [Algebra R S] :

The kernel of the multiplication map S ⊗[R] S →ₐ[R] S.

Equations
Instances For
theorem KaehlerDifferential.one_smul_sub_smul_one_mem_ideal (R : Type u) {S : Type v} [] [] [Algebra R S] (a : S) :
1 ⊗ₜ[R] a - a ⊗ₜ[R] 1
noncomputable def Derivation.tensorProductTo {R : Type u} {S : Type v} [] [] [Algebra R S] {M : Type u_1} [] [Module R M] [Module S M] [] (D : Derivation R S M) :

For a R-derivation S → M, this is the map S ⊗[R] S →ₗ[S] M sending s ⊗ₜ t ↦ s • D t.

Equations
Instances For
theorem Derivation.tensorProductTo_tmul {R : Type u} {S : Type v} [] [] [Algebra R S] {M : Type u_1} [] [Module R M] [Module S M] [] (D : Derivation R S M) (s : S) (t : S) :
D.tensorProductTo (s ⊗ₜ[R] t) = s D t
theorem Derivation.tensorProductTo_mul {R : Type u} {S : Type v} [] [] [Algebra R S] {M : Type u_1} [] [Module R M] [Module S M] [] (D : Derivation R S M) (x : ) (y : ) :
D.tensorProductTo (x * y) = D.tensorProductTo y + D.tensorProductTo x
theorem KaehlerDifferential.submodule_span_range_eq_ideal (R : Type u) (S : Type v) [] [] [Algebra R S] :
Submodule.span S (Set.range fun (s : S) => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) =

The kernel of S ⊗[R] S →ₐ[R] S is generated by 1 ⊗ s - s ⊗ 1 as a S-module.

theorem KaehlerDifferential.span_range_eq_ideal (R : Type u) (S : Type v) [] [] [Algebra R S] :
Ideal.span (Set.range fun (s : S) => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) =
noncomputable def KaehlerDifferential (R : Type u) (S : Type v) [] [] [Algebra R S] :

The module of Kähler differentials (Kahler differentials, Kaehler differentials). This is implemented as I / I ^ 2 with I the kernel of the multiplication map S ⊗[R] S →ₐ[R] S. To view elements as a linear combination of the form s • D s', use KaehlerDifferential.tensorProductTo_surjective and Derivation.tensorProductTo_tmul.

We also provide the notation Ω[S⁄R] for KaehlerDifferential R S. Note that the slash is \textfractionsolidus.

Equations
Instances For
noncomputable instance instAddCommGroupKaehlerDifferential (R : Type u) (S : Type v) [] [] [Algebra R S] :
Equations
• = id inferInstance
noncomputable instance KaehlerDifferential.module (R : Type u) (S : Type v) [] [] [Algebra R S] :
Equations

The module of Kähler differentials (Kahler differentials, Kaehler differentials). This is implemented as I / I ^ 2 with I the kernel of the multiplication map S ⊗[R] S →ₐ[R] S. To view elements as a linear combination of the form s • D s', use KaehlerDifferential.tensorProductTo_surjective and Derivation.tensorProductTo_tmul.

We also provide the notation Ω[S⁄R] for KaehlerDifferential R S. Note that the slash is \textfractionsolidus.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance instNonemptyKaehlerDifferential (R : Type u) (S : Type v) [] [] [Algebra R S] :
Equations
• =
noncomputable instance KaehlerDifferential.module' (R : Type u) (S : Type v) [] [] [Algebra R S] {R' : Type u_2} [CommRing R'] [Algebra R' S] [SMulCommClass R R' S] :
Equations
noncomputable instance instIsScalarTowerTensorProductKaehlerDifferential (R : Type u) (S : Type v) [] [] [Algebra R S] :
Equations
• =
noncomputable instance KaehlerDifferential.isScalarTower_of_tower (R : Type u) (S : Type v) [] [] [Algebra R S] {R₁ : Type u_2} {R₂ : Type u_3} [CommRing R₁] [CommRing R₂] [Algebra R₁ S] [Algebra R₂ S] [SMul R₁ R₂] [SMulCommClass R R₁ S] [SMulCommClass R R₂ S] [IsScalarTower R₁ R₂ S] :
IsScalarTower R₁ R₂ (Ω[SR])
Equations
• =
noncomputable instance KaehlerDifferential.isScalarTower' (R : Type u) (S : Type v) [] [] [Algebra R S] :
Equations
• =
noncomputable def KaehlerDifferential.fromIdeal (R : Type u) (S : Type v) [] [] [Algebra R S] :

The quotient map I → Ω[S⁄R] with I being the kernel of S ⊗[R] S → S.

Equations
• = .toCotangent
Instances For
noncomputable def KaehlerDifferential.DLinearMap (R : Type u) (S : Type v) [] [] [Algebra R S] :

(Implementation) The underlying linear map of the derivation into Ω[S⁄R].

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem KaehlerDifferential.DLinearMap_apply (R : Type u) (S : Type v) [] [] [Algebra R S] (s : S) :
= .toCotangent 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1,
noncomputable def KaehlerDifferential.D (R : Type u) (S : Type v) [] [] [Algebra R S] :

The universal derivation into Ω[S⁄R].

Equations
• = { toLinearMap := , map_one_eq_zero' := , leibniz' := }
Instances For
theorem KaehlerDifferential.D_apply (R : Type u) (S : Type v) [] [] [Algebra R S] (s : S) :
() s = .toCotangent 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1,
noncomputable def Derivation.liftKaehlerDifferential {R : Type u} {S : Type v} [] [] [Algebra R S] {M : Type u_1} [] [Module R M] [Module S M] [] (D : Derivation R S M) :

The linear map from Ω[S⁄R], associated with a derivation.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Derivation.liftKaehlerDifferential_apply {R : Type u} {S : Type v} [] [] [Algebra R S] {M : Type u_1} [] [Module R M] [Module S M] [] (D : Derivation R S M) (x : ) :
D.liftKaehlerDifferential (.toCotangent x) = D.tensorProductTo x
theorem Derivation.liftKaehlerDifferential_comp {R : Type u} {S : Type v} [] [] [Algebra R S] {M : Type u_1} [] [Module R M] [Module S M] [] (D : Derivation R S M) :
D.liftKaehlerDifferential.compDer () = D
@[simp]
theorem Derivation.liftKaehlerDifferential_comp_D {R : Type u} {S : Type v} [] [] [Algebra R S] {M : Type u_1} [] [Module R M] [Module S M] [] (D' : Derivation R S M) (x : S) :
D'.liftKaehlerDifferential (() x) = D' x
theorem Derivation.liftKaehlerDifferential_unique {R : Type u} {S : Type v} [] [] [Algebra R S] {M : Type u_1} [] [Module R M] [Module S M] [] (f : Ω[SR] →ₗ[S] M) (f' : Ω[SR] →ₗ[S] M) (hf : f.compDer () = f'.compDer ()) :
f = f'
theorem Derivation.liftKaehlerDifferential_D (R : Type u) (S : Type v) [] [] [Algebra R S] :
().liftKaehlerDifferential = LinearMap.id
theorem KaehlerDifferential.D_tensorProductTo {R : Type u} {S : Type v} [] [] [Algebra R S] (x : ) :
().tensorProductTo x = .toCotangent x
theorem KaehlerDifferential.tensorProductTo_surjective (R : Type u) (S : Type v) [] [] [Algebra R S] :
Function.Surjective ().tensorProductTo
noncomputable def KaehlerDifferential.linearMapEquivDerivation (R : Type u) (S : Type v) [] [] [Algebra R S] {M : Type u_1} [] [Module R M] [Module S M] [] :

The S-linear maps from Ω[S⁄R] to M are (S-linearly) equivalent to R-derivations from S to M.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem KaehlerDifferential.linearMapEquivDerivation_symm_apply (R : Type u) (S : Type v) [] [] [Algebra R S] {M : Type u_1} [] [Module R M] [Module S M] [] (D : Derivation R S M) :
.symm D = D.liftKaehlerDifferential
@[simp]
theorem KaehlerDifferential.linearMapEquivDerivation_apply_apply (R : Type u) (S : Type v) [] [] [Algebra R S] {M : Type u_1} [] [Module R M] [Module S M] [] (m : Ω[SR] →ₗ[S] M) :
∀ (a : S), a = m (() a)
noncomputable def KaehlerDifferential.quotientCotangentIdealRingEquiv (R : Type u) (S : Type v) [] [] [Algebra R S] :
( ) .cotangentIdeal ≃+* S

The quotient ring of S ⊗ S ⧸ J ^ 2 by Ω[S⁄R] is isomorphic to S.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def KaehlerDifferential.quotientCotangentIdeal (R : Type u) (S : Type v) [] [] [Algebra R S] :
(( ) .cotangentIdeal) ≃ₐ[S] S

The quotient ring of S ⊗ S ⧸ J ^ 2 by Ω[S⁄R] is isomorphic to S as an S-algebra.

Equations
• = let __src := ; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
theorem KaehlerDifferential.End_equiv_aux (R : Type u) (S : Type v) [] [] [Algebra R S] (f : S →ₐ[R] ) :
(Ideal.Quotient.mkₐ R .cotangentIdeal).comp f = IsScalarTower.toAlgHom R S (( ) .cotangentIdeal) .kerSquareLift.comp f =
noncomputable def smul_SSmod_SSmod (R : Type u) (S : Type v) [] [] [Algebra R S] :
SMul ( ) ( )

A shortcut instance to prevent timing out. Hopefully to be removed in the future.

Equations
Instances For
noncomputable def isScalarTower_S_right (R : Type u) (S : Type v) [] [] [Algebra R S] :

A shortcut instance to prevent timing out. Hopefully to be removed in the future.

Equations
• =
Instances For
noncomputable def isScalarTower_R_right (R : Type u) (S : Type v) [] [] [Algebra R S] :

A shortcut instance to prevent timing out. Hopefully to be removed in the future.

Equations
• =
Instances For
noncomputable def isScalarTower_SS_right (R : Type u) (S : Type v) [] [] [Algebra R S] :
IsScalarTower () ( ) ( )

A shortcut instance to prevent timing out. Hopefully to be removed in the future.

Equations
• =
Instances For
noncomputable def instS (R : Type u) (S : Type v) [] [] [Algebra R S] :
Module S .cotangentIdeal

A shortcut instance to prevent timing out. Hopefully to be removed in the future.

Equations
Instances For
noncomputable def instR (R : Type u) (S : Type v) [] [] [Algebra R S] :
Module R .cotangentIdeal

A shortcut instance to prevent timing out. Hopefully to be removed in the future.

Equations
Instances For
noncomputable def instSS (R : Type u) (S : Type v) [] [] [Algebra R S] :
Module () .cotangentIdeal

A shortcut instance to prevent timing out. Hopefully to be removed in the future.

Equations
Instances For
noncomputable def KaehlerDifferential.endEquivDerivation' (R : Type u) (S : Type v) [] [] [Algebra R S] :
Derivation R S (Ω[SR]) ≃ₗ[R] Derivation R S .cotangentIdeal

Derivations into Ω[S⁄R] is equivalent to derivations into (KaehlerDifferential.ideal R S).cotangentIdeal.

Equations
Instances For
noncomputable def KaehlerDifferential.endEquivAuxEquiv (R : Type u) (S : Type v) [] [] [Algebra R S] :
{ f : S →ₐ[R] // (Ideal.Quotient.mkₐ R .cotangentIdeal).comp f = IsScalarTower.toAlgHom R S (( ) .cotangentIdeal) } { f : S →ₐ[R] RingHom.ker .toRingHom ^ 2 // .kerSquareLift.comp f = }

(Implementation) An Equiv version of KaehlerDifferential.End_equiv_aux. Used in KaehlerDifferential.endEquiv.

Equations
Instances For
noncomputable def KaehlerDifferential.endEquiv (R : Type u) (S : Type v) [] [] [Algebra R S] :
Module.End S (Ω[SR]) { f : S →ₐ[R] RingHom.ker .toRingHom ^ 2 // .kerSquareLift.comp f = }

The endomorphisms of Ω[S⁄R] corresponds to sections of the surjection S ⊗[R] S ⧸ J ^ 2 →ₐ[R] S, with J being the kernel of the multiplication map S ⊗[R] S →ₐ[R] S.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def KaehlerDifferential.kerTotal (R : Type u) (S : Type v) [] [] [Algebra R S] :

The S-submodule of S →₀ S (the direct sum of copies of S indexed by S) generated by the relations:

1. dx + dy = d(x + y)
2. x dy + y dx = d(x * y)
3. dr = 0 for r ∈ R where db is the unit in the copy of S with index b.

This is the kernel of the surjection Finsupp.total S Ω[S⁄R] S (KaehlerDifferential.D R S). See KaehlerDifferential.kerTotal_eq and KaehlerDifferential.total_surjective.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem KaehlerDifferential.kerTotal_mkQ_single_add (R : Type u) (S : Type v) [] [] [Algebra R S] (x : S) (y : S) (z : S) :
.mkQ (Finsupp.single (x + y) z) = .mkQ () + .mkQ ()
theorem KaehlerDifferential.kerTotal_mkQ_single_mul (R : Type u) (S : Type v) [] [] [Algebra R S] (x : S) (y : S) (z : S) :
.mkQ (Finsupp.single (x * y) z) = .mkQ (Finsupp.single y (z * x)) + .mkQ (Finsupp.single x (z * y))
theorem KaehlerDifferential.kerTotal_mkQ_single_algebraMap (R : Type u) (S : Type v) [] [] [Algebra R S] (x : R) (y : S) :
.mkQ (Finsupp.single (() x) y) = 0
theorem KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one (R : Type u) (S : Type v) [] [] [Algebra R S] (x : S) :
.mkQ () = 0
theorem KaehlerDifferential.kerTotal_mkQ_single_smul (R : Type u) (S : Type v) [] [] [Algebra R S] (r : R) (x : S) (y : S) :
.mkQ (Finsupp.single (r x) y) = r .mkQ ()
noncomputable def KaehlerDifferential.derivationQuotKerTotal (R : Type u) (S : Type v) [] [] [Algebra R S] :
Derivation R S ((S →₀ S) )

The (universal) derivation into (S →₀ S) ⧸ KaehlerDifferential.kerTotal R S.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem KaehlerDifferential.derivationQuotKerTotal_apply (R : Type u) (S : Type v) [] [] [Algebra R S] (x : S) :
= .mkQ ()
theorem KaehlerDifferential.derivationQuotKerTotal_lift_comp_total (R : Type u) (S : Type v) [] [] [Algebra R S] :
.liftKaehlerDifferential ∘ₗ Finsupp.total S (Ω[SR]) S () = .mkQ
theorem KaehlerDifferential.kerTotal_eq (R : Type u) (S : Type v) [] [] [Algebra R S] :
noncomputable def KaehlerDifferential.quotKerTotalEquiv (R : Type u) (S : Type v) [] [] [Algebra R S] :

Ω[S⁄R] is isomorphic to S copies of S with kernel KaehlerDifferential.kerTotal.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem KaehlerDifferential.quotKerTotalEquiv_symm_apply (R : Type u) (S : Type v) [] [] [Algebra R S] (a : Ω[SR]) :
.symm a = .liftKaehlerDifferential a
@[simp]
theorem KaehlerDifferential.quotKerTotalEquiv_apply (R : Type u) (S : Type v) [] [] [Algebra R S] :
theorem KaehlerDifferential.quotKerTotalEquiv_symm_comp_D (R : Type u) (S : Type v) [] [] [Algebra R S] :
(.symm).compDer () =
theorem KaehlerDifferential.kerTotal_map (R : Type u) (S : Type v) [] [] [Algebra R S] (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [] [] (h : ) :
Submodule.map ( ∘ₗ Finsupp.lmapDomain A A ()) Submodule.span A (Set.range fun (x : S) => Finsupp.single (() x) 1) =

Given the commutative diagram A --→ B ↑ ↑ | | R --→ S The kernel of the presentation ⊕ₓ B dx ↠ Ω_{B/S} is spanned by the image of the kernel of ⊕ₓ A dx ↠ Ω_{A/R} and all ds with s : S. See kerTotal_map' for the special case where R = S.

theorem KaehlerDifferential.kerTotal_map' (R : Type u) [] (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [Algebra R B] [Algebra A B] [] (h : ) :
Submodule.map ( ∘ₗ Finsupp.lmapDomain A A ()) ( Submodule.span A (Set.range fun (x : R) => Finsupp.single (() x) 1)) =

This is a special case of kerTotal_map where R = S. The kernel of the presentation ⊕ₓ B dx ↠ Ω_{B/R} is spanned by the image of the kernel of ⊕ₓ A dx ↠ Ω_{A/R} and all da with a : A.

noncomputable def KaehlerDifferential.map (R : Type u) (S : Type v) [] [] [Algebra R S] (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [] [] [] :

The map Ω[A⁄R] →ₗ[A] Ω[B⁄S] given a square A --→ B ↑ ↑ | | R --→ S

Equations
• = .liftKaehlerDifferential
Instances For
theorem KaehlerDifferential.map_compDer (R : Type u) (S : Type v) [] [] [Algebra R S] (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [] [] [] :
().compDer () =
@[simp]
theorem KaehlerDifferential.map_D (R : Type u) (S : Type v) [] [] [Algebra R S] (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [] [] [] (x : A) :
() (() x) = () (() x)
theorem KaehlerDifferential.ker_map (R : Type u) (S : Type v) [] [] [Algebra R S] (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [] [] [] :
theorem KaehlerDifferential.map_surjective_of_surjective (R : Type u) (S : Type v) [] [] [Algebra R S] (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [] [] [] (h : ) :
theorem KaehlerDifferential.map_surjective (R : Type u) (S : Type v) [] [] [Algebra R S] (B : Type u_3) [] [Algebra R B] [Algebra S B] [] :
noncomputable def KaehlerDifferential.mapBaseChange (R : Type u) [] (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [Algebra R B] [Algebra A B] [] :

The lift of the map Ω[A⁄R] →ₗ[A] Ω[B⁄R] to the base change along A → B. This is the first map in the exact sequence B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0.

Equations
• = .lift ()
Instances For
@[simp]
theorem KaehlerDifferential.mapBaseChange_tmul (R : Type u) [] (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [Algebra R B] [Algebra A B] [] (x : B) (y : Ω[AR]) :
(x ⊗ₜ[A] y) = x () y
theorem KaehlerDifferential.range_mapBaseChange (R : Type u) [] (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [Algebra R B] [Algebra A B] [] :
theorem KaehlerDifferential.exact_mapBaseChange_map (R : Type u) [] (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [Algebra R B] [Algebra A B] [] :
Function.Exact ()

The sequence B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0 is exact. Also see KaehlerDifferential.map_surjective.

noncomputable def KaehlerDifferential.mvPolynomialEquiv (R : Type u) [] (σ : Type u_2) :

The relative differential module of a polynomial algebra R[σ] is the free module generated by { dx | x ∈ σ }. Also see KaehlerDifferential.mvPolynomialBasis.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def KaehlerDifferential.mvPolynomialBasis (R : Type u) [] (σ : Type u_2) :
Basis σ () (Ω[R])

{ dx | x ∈ σ } forms a basis of the relative differential module of a polynomial algebra R[σ].

Equations
• = { repr := }
Instances For
theorem KaehlerDifferential.mvPolynomialBasis_repr_comp_D (R : Type u) [] (σ : Type u_2) :
(.repr).compDer () = MvPolynomial.mkDerivation R fun (x : σ) =>
theorem KaehlerDifferential.mvPolynomialBasis_repr_D (R : Type u) [] (σ : Type u_2) (x : ) :
.repr (() x) = (MvPolynomial.mkDerivation R fun (x : σ) => ) x
@[simp]
theorem KaehlerDifferential.mvPolynomialBasis_repr_D_X (R : Type u) [] (σ : Type u_2) (i : σ) :
.repr (() ()) =
@[simp]
theorem KaehlerDifferential.mvPolynomialBasis_repr_apply (R : Type u) [] (σ : Type u_2) (x : ) (i : σ) :
(.repr (() x)) i = x
theorem KaehlerDifferential.mvPolynomialBasis_repr_symm_single (R : Type u) [] (σ : Type u_2) (i : σ) (x : ) :
.repr.symm () = x () ()
@[simp]
theorem KaehlerDifferential.mvPolynomialBasis_apply (R : Type u) [] (σ : Type u_2) (i : σ) :
= () ()
noncomputable instance instFreeMvPolynomialKaehlerDifferential (R : Type u) [] (σ : Type u_2) :
Equations
• =
theorem KaehlerDifferential.polynomial_D_apply (R : Type u) [] (P : ) :
() P = Polynomial.derivative P () Polynomial.X
noncomputable def KaehlerDifferential.polynomialEquiv (R : Type u) [] :

The relative differential module of the univariate polynomial algebra R[X] is isomorphic to R[X] as an R[X]-module.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem KaehlerDifferential.polynomialEquiv_comp_D (R : Type u) [] :
.compDer () = Polynomial.derivative'
@[simp]
theorem KaehlerDifferential.polynomialEquiv_D (R : Type u) [] (P : ) :
(() P) = Polynomial.derivative P
@[simp]
theorem KaehlerDifferential.polynomialEquiv_symm (R : Type u) [] (P : ) :
.symm P = P () Polynomial.X