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.

@[inline, reducible]

noncomputable abbrev KaehlerDifferential.ideal (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Ideal (TensorProduct R S S)

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

Equations

• KaehlerDifferential.ideal R S = RingHom.ker (Algebra.TensorProduct.lmul' R)

theorem KaehlerDifferential.one_smul_sub_smul_one_mem_ideal (R : Type u) {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (a : S) : 1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ KaehlerDifferential.ideal R S

noncomputable def Derivation.tensorProductTo {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) : TensorProduct R S S →ₗ[S] M

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

Equations

• Derivation.tensorProductTo D = TensorProduct.AlgebraTensorModule.lift ((LinearMap.flip (LinearMap.lsmul S (S →ₗ[R] M))) ↑D)

theorem Derivation.tensorProductTo_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) (s : S) (t : S) : (Derivation.tensorProductTo D) (s ⊗ₜ[R] t) = s • D t

theorem Derivation.tensorProductTo_mul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) (x : TensorProduct R S S) (y : TensorProduct R S S) : (Derivation.tensorProductTo D) (x * y) = (Algebra.TensorProduct.lmul' R) x • (Derivation.tensorProductTo D) y + (Algebra.TensorProduct.lmul' R) y • (Derivation.tensorProductTo D) x

theorem KaehlerDifferential.submodule_span_range_eq_ideal (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Submodule.span S (Set.range fun (s : S) => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Submodule.restrictScalars S (KaehlerDifferential.ideal R S)

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) [CommRing R] [CommRing S] [Algebra R S] : Ideal.span (Set.range fun (s : S) => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = KaehlerDifferential.ideal R S

noncomputable def KaehlerDifferential (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Type v

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

• Ω[S⁄R] = Ideal.Cotangent (KaehlerDifferential.ideal R S)

noncomputable instance instAddCommGroupKaehlerDifferential (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : AddCommGroup (Ω[S⁄R])

Equations

• instAddCommGroupKaehlerDifferential R S = id inferInstance

noncomputable instance KaehlerDifferential.module (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Module (TensorProduct R S S) (Ω[S⁄R])

Equations

• KaehlerDifferential.module R S = Ideal.Cotangent.moduleOfTower (KaehlerDifferential.ideal R S)

def «termΩ[_⁄_]» : Lean.ParserDescr

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.

noncomputable instance instNonemptyKaehlerDifferential (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Nonempty (Ω[S⁄R])

Equations

• ⋯ = ⋯

noncomputable instance KaehlerDifferential.module' (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {R' : Type u_2} [CommRing R'] [Algebra R' S] [SMulCommClass R R' S] : Module R' (Ω[S⁄R])

Equations

• KaehlerDifferential.module' R S = Submodule.Quotient.module' (KaehlerDifferential.ideal R S • ⊤)

noncomputable instance instIsScalarTowerTensorProductToCommSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToModuleToSemiringToCommSemiringKaehlerDifferentialLeftHasSMulToMonoidToMonoidWithZeroToDistribMulActionToModuleTo_smulCommClassToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidInstAddCommGroupKaehlerDifferentialToSMulZeroClassToZeroToCommMonoidWithZeroInstCommRingToSMulWithZeroInstSemiringToMulActionWithZeroToAddCommMonoidModuleModule'Id (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : IsScalarTower S (TensorProduct R S S) (Ω[S⁄R])

Equations

• ⋯ = ⋯

noncomputable instance KaehlerDifferential.isScalarTower_of_tower (R : Type u) (S : Type v) [CommRing R] [CommRing S] [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₂ (Ω[S⁄R])

Equations

• ⋯ = ⋯

noncomputable instance KaehlerDifferential.isScalarTower' (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : IsScalarTower R (TensorProduct R S S) (Ω[S⁄R])

Equations

• ⋯ = ⋯

noncomputable def KaehlerDifferential.fromIdeal (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : ↥(KaehlerDifferential.ideal R S) →ₗ[TensorProduct R S S] Ω[S⁄R]

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

Equations

• KaehlerDifferential.fromIdeal R S = Ideal.toCotangent (KaehlerDifferential.ideal R S)

noncomputable def KaehlerDifferential.DLinearMap (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : S →ₗ[R] Ω[S⁄R]

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

Equations

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

theorem KaehlerDifferential.DLinearMap_apply (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (s : S) : (KaehlerDifferential.DLinearMap R S) s = (Ideal.toCotangent (KaehlerDifferential.ideal R S)) { val := 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, property := ⋯ }

noncomputable def KaehlerDifferential.D (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Derivation R S (Ω[S⁄R])

The universal derivation into Ω[S⁄R].

Equations

• KaehlerDifferential.D R S = { toLinearMap := KaehlerDifferential.DLinearMap R S, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

theorem KaehlerDifferential.D_apply (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (s : S) : (KaehlerDifferential.D R S) s = (Ideal.toCotangent (KaehlerDifferential.ideal R S)) { val := 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, property := ⋯ }

theorem KaehlerDifferential.span_range_derivation (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) = ⊤

noncomputable def Derivation.liftKaehlerDifferential {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) : Ω[S⁄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.

theorem Derivation.liftKaehlerDifferential_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) (x : ↥(KaehlerDifferential.ideal R S)) : (Derivation.liftKaehlerDifferential D) ((Ideal.toCotangent (KaehlerDifferential.ideal R S)) x) = (Derivation.tensorProductTo D) ↑x

theorem Derivation.liftKaehlerDifferential_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) : (LinearMap.compDer (Derivation.liftKaehlerDifferential D)) (KaehlerDifferential.D R S) = D

@[simp]

theorem Derivation.liftKaehlerDifferential_comp_D {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D' : Derivation R S M) (x : S) : (Derivation.liftKaehlerDifferential D') ((KaehlerDifferential.D R S) x) = D' x

theorem Derivation.liftKaehlerDifferential_unique {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (f : Ω[S⁄R] →ₗ[S] M) (f' : Ω[S⁄R] →ₗ[S] M) (hf : (LinearMap.compDer f) (KaehlerDifferential.D R S) = (LinearMap.compDer f') (KaehlerDifferential.D R S)) : f = f'

theorem Derivation.liftKaehlerDifferential_D (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Derivation.liftKaehlerDifferential (KaehlerDifferential.D R S) = LinearMap.id

theorem KaehlerDifferential.D_tensorProductTo {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (x : ↥(KaehlerDifferential.ideal R S)) : (Derivation.tensorProductTo (KaehlerDifferential.D R S)) ↑x = (Ideal.toCotangent (KaehlerDifferential.ideal R S)) x

theorem KaehlerDifferential.tensorProductTo_surjective (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Function.Surjective ⇑(Derivation.tensorProductTo (KaehlerDifferential.D R S))

noncomputable def KaehlerDifferential.linearMapEquivDerivation (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : (Ω[S⁄R] →ₗ[S] M) ≃ₗ[S] Derivation R 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.

@[simp]

theorem KaehlerDifferential.linearMapEquivDerivation_symm_apply (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) : (LinearEquiv.symm (KaehlerDifferential.linearMapEquivDerivation R S)) D = Derivation.liftKaehlerDifferential D

@[simp]

theorem KaehlerDifferential.linearMapEquivDerivation_apply_apply (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (m : Ω[S⁄R] →ₗ[S] M) : ∀ (a : S), ((KaehlerDifferential.linearMapEquivDerivation R S) m) a = m ((KaehlerDifferential.D R S) a)

noncomputable def KaehlerDifferential.quotientCotangentIdealRingEquiv (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸ Ideal.cotangentIdeal (KaehlerDifferential.ideal R S) ≃+* 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.

noncomputable def KaehlerDifferential.quotientCotangentIdeal (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸ Ideal.cotangentIdeal (KaehlerDifferential.ideal R S)) ≃ₐ[S] S

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

Equations

• KaehlerDifferential.quotientCotangentIdeal R S = let __src := KaehlerDifferential.quotientCotangentIdealRingEquiv R S; { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem KaehlerDifferential.End_equiv_aux (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (f : S →ₐ[R] TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) : AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.cotangentIdeal (KaehlerDifferential.ideal R S))) f = IsScalarTower.toAlgHom R S ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸ Ideal.cotangentIdeal (KaehlerDifferential.ideal R S)) ↔ AlgHom.comp (AlgHom.kerSquareLift (Algebra.TensorProduct.lmul' R)) f = AlgHom.id R S

noncomputable def smul_SSmod_SSmod (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : SMul (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2)

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

Equations

• smul_SSmod_SSmod R S = Mul.toSMul (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2)

noncomputable def isScalarTower_S_right (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : IsScalarTower S (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2)

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

Equations

• ⋯ = ⋯

noncomputable def isScalarTower_R_right (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : IsScalarTower R (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2)

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

Equations

• ⋯ = ⋯

noncomputable def isScalarTower_SS_right (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : IsScalarTower (TensorProduct R S S) (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2)

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

Equations

• ⋯ = ⋯

noncomputable def instS (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Module S ↥(Ideal.cotangentIdeal (KaehlerDifferential.ideal R S))

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

Equations

• instS R S = Submodule.module' (Ideal.cotangentIdeal (KaehlerDifferential.ideal R S))

noncomputable def instR (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Module R ↥(Ideal.cotangentIdeal (KaehlerDifferential.ideal R S))

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

Equations

• instR R S = Submodule.module' (Ideal.cotangentIdeal (KaehlerDifferential.ideal R S))

noncomputable def instSS (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Module (TensorProduct R S S) ↥(Ideal.cotangentIdeal (KaehlerDifferential.ideal R S))

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

Equations

• instSS R S = Submodule.module' (Ideal.cotangentIdeal (KaehlerDifferential.ideal R S))

noncomputable def KaehlerDifferential.endEquivDerivation' (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Derivation R S (Ω[S⁄R]) ≃ₗ[R] Derivation R S ↥(Ideal.cotangentIdeal (KaehlerDifferential.ideal R S))

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

Equations

• KaehlerDifferential.endEquivDerivation' R S = LinearEquiv.compDer (LinearEquiv.restrictScalars S (Ideal.cotangentEquivIdeal (KaehlerDifferential.ideal R S)))

noncomputable def KaehlerDifferential.endEquivAuxEquiv (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : { f : S →ₐ[R] TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2 // AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.cotangentIdeal (KaehlerDifferential.ideal R S))) f = IsScalarTower.toAlgHom R S ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸ Ideal.cotangentIdeal (KaehlerDifferential.ideal R S)) } ≃ { f : S →ₐ[R] TensorProduct R S S ⧸ RingHom.ker (Algebra.TensorProduct.lmul' R).toRingHom ^ 2 // AlgHom.comp (AlgHom.kerSquareLift (Algebra.TensorProduct.lmul' R)) f = AlgHom.id R S }

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

Equations

• KaehlerDifferential.endEquivAuxEquiv R S = Equiv.subtypeEquiv (Equiv.refl (S →ₐ[R] TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2)) ⋯

noncomputable def KaehlerDifferential.endEquiv (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Module.End S (Ω[S⁄R]) ≃ { f : S →ₐ[R] TensorProduct R S S ⧸ RingHom.ker (Algebra.TensorProduct.lmul' R).toRingHom ^ 2 // AlgHom.comp (AlgHom.kerSquareLift (Algebra.TensorProduct.lmul' R)) f = AlgHom.id R S }

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.

noncomputable def KaehlerDifferential.kerTotal (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Submodule S (S →₀ 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.

theorem KaehlerDifferential.kerTotal_mkQ_single_add (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x : S) (y : S) (z : S) : (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (Finsupp.single (x + y) z) = (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (Finsupp.single x z) + (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (Finsupp.single y z)

theorem KaehlerDifferential.kerTotal_mkQ_single_mul (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x : S) (y : S) (z : S) : (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (Finsupp.single (x * y) z) = (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (Finsupp.single y (z * x)) + (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (Finsupp.single x (z * y))

theorem KaehlerDifferential.kerTotal_mkQ_single_algebraMap (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x : R) (y : S) : (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (Finsupp.single ((algebraMap R S) x) y) = 0

theorem KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x : S) : (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (Finsupp.single 1 x) = 0

theorem KaehlerDifferential.kerTotal_mkQ_single_smul (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (r : R) (x : S) (y : S) : (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (Finsupp.single (r • x) y) = r • (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (Finsupp.single x y)

noncomputable def KaehlerDifferential.derivationQuotKerTotal (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Derivation R S ((S →₀ S) ⧸ KaehlerDifferential.kerTotal R S)

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

Equations

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

theorem KaehlerDifferential.derivationQuotKerTotal_apply (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x : S) : (KaehlerDifferential.derivationQuotKerTotal R S) x = (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (Finsupp.single x 1)

theorem KaehlerDifferential.derivationQuotKerTotal_lift_comp_total (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Derivation.liftKaehlerDifferential (KaehlerDifferential.derivationQuotKerTotal R S) ∘ₗ Finsupp.total S (Ω[S⁄R]) S ⇑(KaehlerDifferential.D R S) = Submodule.mkQ (KaehlerDifferential.kerTotal R S)

theorem KaehlerDifferential.kerTotal_eq (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : LinearMap.ker (Finsupp.total S (Ω[S⁄R]) S ⇑(KaehlerDifferential.D R S)) = KaehlerDifferential.kerTotal R S

theorem KaehlerDifferential.total_surjective (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Function.Surjective ⇑(Finsupp.total S (Ω[S⁄R]) S ⇑(KaehlerDifferential.D R S))

noncomputable def KaehlerDifferential.quotKerTotalEquiv (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : ((S →₀ S) ⧸ KaehlerDifferential.kerTotal R S) ≃ₗ[S] Ω[S⁄R]

Ω[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.

@[simp]

theorem KaehlerDifferential.quotKerTotalEquiv_apply (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : ∀ (a : (S →₀ S) ⧸ Submodule.toAddSubgroup (KaehlerDifferential.kerTotal R S)), (KaehlerDifferential.quotKerTotalEquiv R S) a = (QuotientAddGroup.lift (Submodule.toAddSubgroup (KaehlerDifferential.kerTotal R S)) (LinearMap.toAddMonoidHom (Finsupp.total S (Ω[S⁄R]) S ⇑(KaehlerDifferential.D R S))) ⋯) a

@[simp]

theorem KaehlerDifferential.quotKerTotalEquiv_symm_apply (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (a : Ω[S⁄R]) : (LinearEquiv.symm (KaehlerDifferential.quotKerTotalEquiv R S)) a = (Derivation.liftKaehlerDifferential (KaehlerDifferential.derivationQuotKerTotal R S)) a

theorem KaehlerDifferential.quotKerTotalEquiv_symm_comp_D (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (LinearMap.compDer ↑(LinearEquiv.symm (KaehlerDifferential.quotKerTotalEquiv R S))) (KaehlerDifferential.D R S) = KaehlerDifferential.derivationQuotKerTotal R S

theorem KaehlerDifferential.kerTotal_map (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] (h : Function.Surjective ⇑(algebraMap A B)) : Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (KaehlerDifferential.kerTotal R A) ⊔ Submodule.span A (Set.range fun (x : S) => Finsupp.single ((algebraMap S B) x) 1) = Submodule.restrictScalars A (KaehlerDifferential.kerTotal S B)

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) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (KaehlerDifferential.kerTotal R A ⊔ Submodule.span A (Set.range fun (x : R) => Finsupp.single ((algebraMap R A) x) 1)) = Submodule.restrictScalars A (KaehlerDifferential.kerTotal R B)

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) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] : Ω[A⁄R] →ₗ[A] Ω[B⁄S]

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

Equations

• KaehlerDifferential.map R S A B = Derivation.liftKaehlerDifferential (Derivation.compAlgebraMap A (Derivation.restrictScalars R (KaehlerDifferential.D S B)))

theorem KaehlerDifferential.map_compDer (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] : (LinearMap.compDer (KaehlerDifferential.map R S A B)) (KaehlerDifferential.D R A) = Derivation.compAlgebraMap A (Derivation.restrictScalars R (KaehlerDifferential.D S B))

@[simp]

theorem KaehlerDifferential.map_D (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] (x : A) : (KaehlerDifferential.map R S A B) ((KaehlerDifferential.D R A) x) = (KaehlerDifferential.D S B) ((algebraMap A B) x)

theorem KaehlerDifferential.ker_map (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] : LinearMap.ker (KaehlerDifferential.map R S A B) = Submodule.map (Finsupp.total A (Ω[A⁄R]) A ⇑(KaehlerDifferential.D R A)) (Submodule.comap (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (Submodule.restrictScalars A (KaehlerDifferential.kerTotal S B)))

theorem KaehlerDifferential.map_surjective_of_surjective (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Surjective ⇑(KaehlerDifferential.map R S A B)

theorem KaehlerDifferential.map_surjective (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (B : Type u_3) [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] : Function.Surjective ⇑(KaehlerDifferential.map R S B B)

noncomputable def KaehlerDifferential.mapBaseChange (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : TensorProduct A B (Ω[A⁄R]) →ₗ[B] Ω[B⁄R]

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

• KaehlerDifferential.mapBaseChange R A B = IsBaseChange.lift ⋯ (KaehlerDifferential.map R R A B)

@[simp]

theorem KaehlerDifferential.mapBaseChange_tmul (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (x : B) (y : Ω[A⁄R]) : (KaehlerDifferential.mapBaseChange R A B) (x ⊗ₜ[A] y) = x • (KaehlerDifferential.map R R A B) y

theorem KaehlerDifferential.range_mapBaseChange (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : LinearMap.range (KaehlerDifferential.mapBaseChange R A B) = LinearMap.ker (KaehlerDifferential.map R A B B)

theorem KaehlerDifferential.exact_mapBaseChange_map (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : Function.Exact ⇑(KaehlerDifferential.mapBaseChange R A B) ⇑(KaehlerDifferential.map R A B B)

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) [CommRing R] (σ : Type u_2) : Ω[MvPolynomial σ R⁄R] ≃ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R

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.

noncomputable def KaehlerDifferential.mvPolynomialBasis (R : Type u) [CommRing R] (σ : Type u_2) : Basis σ (MvPolynomial σ R) (Ω[MvPolynomial σ R⁄R])

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

Equations

• KaehlerDifferential.mvPolynomialBasis R σ = { repr := KaehlerDifferential.mvPolynomialEquiv R σ }

theorem KaehlerDifferential.mvPolynomialBasis_repr_comp_D (R : Type u) [CommRing R] (σ : Type u_2) : (LinearMap.compDer ↑(KaehlerDifferential.mvPolynomialBasis R σ).repr) (KaehlerDifferential.D R (MvPolynomial σ R)) = MvPolynomial.mkDerivation R fun (x : σ) => Finsupp.single x 1

theorem KaehlerDifferential.mvPolynomialBasis_repr_D (R : Type u) [CommRing R] (σ : Type u_2) (x : MvPolynomial σ R) : (KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) x) = (MvPolynomial.mkDerivation R fun (x : σ) => Finsupp.single x 1) x

@[simp]

theorem KaehlerDifferential.mvPolynomialBasis_repr_D_X (R : Type u) [CommRing R] (σ : Type u_2) (i : σ) : (KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)) = Finsupp.single i 1

@[simp]

theorem KaehlerDifferential.mvPolynomialBasis_repr_apply (R : Type u) [CommRing R] (σ : Type u_2) (x : MvPolynomial σ R) (i : σ) : ((KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x

theorem KaehlerDifferential.mvPolynomialBasis_repr_symm_single (R : Type u) [CommRing R] (σ : Type u_2) (i : σ) (x : MvPolynomial σ R) : (LinearEquiv.symm (KaehlerDifferential.mvPolynomialBasis R σ).repr) (Finsupp.single i x) = x • (KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)

@[simp]

theorem KaehlerDifferential.mvPolynomialBasis_apply (R : Type u) [CommRing R] (σ : Type u_2) (i : σ) : (KaehlerDifferential.mvPolynomialBasis R σ) i = (KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)

noncomputable instance instFreeMvPolynomialToCommSemiringKaehlerDifferentialInstCommRingMvPolynomialAlgebraIdToSemiringCommSemiringToAddCommMonoidInstAddCommGroupKaehlerDifferentialModule'IdToCommSemiringSmulCommClass_rightToDistribSMulToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingSmulCommClass_selfToCommMonoidToMulActionToMonoidWithZeroToSemiringToZeroToCommMonoidWithZeroToMulActionWithZero (R : Type u) [CommRing R] (σ : Type u_2) : Module.Free (MvPolynomial σ R) (Ω[MvPolynomial σ R⁄R])

Equations

• ⋯ = ⋯

theorem KaehlerDifferential.polynomial_D_apply (R : Type u) [CommRing R] (P : Polynomial R) : (KaehlerDifferential.D R (Polynomial R)) P = Polynomial.derivative P • (KaehlerDifferential.D R (Polynomial R)) Polynomial.X

noncomputable def KaehlerDifferential.polynomialEquiv (R : Type u) [CommRing R] : Ω[Polynomial R⁄R] ≃ₗ[Polynomial R] Polynomial R

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.

theorem KaehlerDifferential.polynomialEquiv_comp_D (R : Type u) [CommRing R] : (LinearEquiv.compDer (KaehlerDifferential.polynomialEquiv R)) (KaehlerDifferential.D R (Polynomial R)) = Polynomial.derivative'

@[simp]

theorem KaehlerDifferential.polynomialEquiv_D (R : Type u) [CommRing R] (P : Polynomial R) : (KaehlerDifferential.polynomialEquiv R) ((KaehlerDifferential.D R (Polynomial R)) P) = Polynomial.derivative P

@[simp]

theorem KaehlerDifferential.polynomialEquiv_symm (R : Type u) [CommRing R] (P : Polynomial R) : (LinearEquiv.symm (KaehlerDifferential.polynomialEquiv R)) P = P • (KaehlerDifferential.D R (Polynomial R)) Polynomial.X