The differential module and etale algebras

Main results

• KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale: The canonical isomorphism T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R] for T a formally etale S-algebra.
• Algebra.tensorH1CotangentOfIsLocalization: The canonical isomorphism T ⊗[S] H¹(L_{S⁄R}) ≃ₗ[T] H¹(L_{T⁄R}) for T a localization of S.

noncomputable def KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.FormallyEtale S T] : TensorProduct S T Ω[S⁄R] ≃ₗ[T] Ω[T⁄R]

The canonical isomorphism T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R] for T a formally etale S-algebra. Also see S ⊗[R] Ω[A⁄R] ≃ₗ[S] Ω[S ⊗[R] A⁄S] at KaehlerDifferential.tensorKaehlerEquiv.

@[simp]

theorem KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_apply (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.FormallyEtale S T] (a✝ : TensorProduct S T Ω[S⁄R]) : (tensorKaehlerEquivOfFormallyEtale R S T) a✝ = (mapBaseChange R S T) a✝

theorem KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.FormallyEtale S T] (s : S) : (tensorKaehlerEquivOfFormallyEtale R S T).symm ((D R T) ((algebraMap S T) s)) = 1 ⊗ₜ[S] (D R S) s

theorem KaehlerDifferential.isBaseChange_of_formallyEtale (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.FormallyEtale S T] : IsBaseChange T (map R R S T)

instance KaehlerDifferential.isLocalizedModule_map (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (M : Submonoid S) [IsLocalization M T] : IsLocalizedModule M (map R R S T)

Suppose we have a morphism of extensions of R-algebras

0 → J → Q → T → 0
    ↑   ↑   ↑
0 → I → P → S → 0

noncomputable def Algebra.Extension.tensorCotangentSpace {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {P : Extension R S} {Q : Extension R T} (f : P.Hom Q) (H : f.toRingHom.FormallyEtale) : TensorProduct S T P.CotangentSpace ≃ₗ[T] Q.CotangentSpace

If P → Q is formally etale, then T ⊗ₛ (S ⊗ₚ Ω[P/R]) ≃ T ⊗_Q Ω[Q/R].

noncomputable def Algebra.Extension.tensorCotangentInvFun {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] {P : Extension R S} {Q : Extension R T} (f : P.Hom Q) [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom) (H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))) : Q.Cotangent →+ TensorProduct S T P.Cotangent

(Implementation) If J ≃ Q ⊗ₚ I (e.g. when T = Q ⊗ₚ S and P → Q is flat), then T ⊗ₛ I/I² ≃ J/J². This is the inverse.

theorem Algebra.Extension.tensorCotangentInvFun_smul_mk {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] {P : Extension R S} {Q : Extension R T} (f : P.Hom Q) [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom) (H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))) (x : Q.Ring) (y : ↥P.ker) : (tensorCotangentInvFun f halg H) (x • Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) = x • 1 ⊗ₜ[S] Cotangent.mk y

noncomputable def Algebra.Extension.tensorCotangent {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] {P : Extension R S} {Q : Extension R T} (f : P.Hom Q) [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom) (H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))) : TensorProduct S T P.Cotangent ≃ₗ[T] Q.Cotangent

If J ≃ Q ⊗ₚ I (e.g. when T = Q ⊗ₚ S and P → Q is flat), then T ⊗ₛ I/I² ≃ J/J².

noncomputable def Algebra.Extension.tensorH1Cotangent {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {P : Extension R S} {Q : Extension R T} (f : P.Hom Q) [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom) [Module.Flat S T] (H₁ : f.toRingHom.FormallyEtale) (H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))) : TensorProduct S T P.H1Cotangent ≃ₗ[T] Q.H1Cotangent

If J ≃ Q ⊗ₚ I, S → T is flat and P → Q is formally etale, then T ⊗ H¹(L_P) ≃ H¹(L_Q).

noncomputable def Algebra.tensorH1CotangentOfIsLocalization (R : Type u) {S : Type u} (T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (M : Submonoid S) [IsLocalization M T] : TensorProduct S T (H1Cotangent R S) ≃ₗ[T] H1Cotangent R T

let p be a submonoid of an R-algebra S. Then Sₚ ⊗ H¹(L_{S/R}) ≃ H¹(L_{Sₚ/R}).

theorem Algebra.tensorH1CotangentOfIsLocalization_toLinearMap (R : Type u) {S : Type u} (T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (M : Submonoid S) [IsLocalization M T] : ↑(tensorH1CotangentOfIsLocalization R T M) = LinearMap.liftBaseChange T (H1Cotangent.map R R S T)

instance Algebra.H1Cotangent.isLocalizedModule (R : Type u) {S : Type u} (T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (M : Submonoid S) [IsLocalization M T] : IsLocalizedModule M (map R R S T)