Kähler differential module under base change

Main results

• KaehlerDifferential.tensorKaehlerEquivBase: (S ⊗[R] Ω[A⁄R]) ≃ₗ[S] Ω[B⁄S] for B = S ⊗[R] A.
• KaehlerDifferential.tensorKaehlerEquiv: (B ⊗[A] Ω[A⁄R]) ≃ₗ[B] Ω[B⁄S] for B = S ⊗[R] A.
• KaehlerDifferential.isLocalizedModule_of_isLocalizedModule: Ω[Aₚ/Rₚ] is the localization of Ω[A/R] at p.

@[reducible, inline]

noncomputable abbrev KaehlerDifferential.mulActionBaseChange (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] : MulAction A (TensorProduct R S Ω[A⁄R])

(Implementation). A-action on S ⊗[R] Ω[A⁄R].

@[simp]

theorem KaehlerDifferential.mulActionBaseChange_smul_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] (a : A) (s : S) (x : Ω[A⁄R]) : a • s ⊗ₜ[R] x = s ⊗ₜ[R] (a • x)

theorem KaehlerDifferential.mulActionBaseChange_smul_zero (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] (a : A) : a • 0 = 0

theorem KaehlerDifferential.mulActionBaseChange_smul_add (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] (a : A) (x y : TensorProduct R S Ω[A⁄R]) : a • (x + y) = a • x + a • y

@[reducible, inline]

noncomputable abbrev KaehlerDifferential.moduleBaseChange (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] : Module A (TensorProduct R S Ω[A⁄R])

(Implementation). A-module structure on S ⊗[R] Ω[A⁄R].

instance KaehlerDifferential.instIsScalarTowerTensorProduct (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] : IsScalarTower R A (TensorProduct R S Ω[A⁄R])

instance KaehlerDifferential.instSMulCommClassTensorProduct (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] : SMulCommClass S A (TensorProduct R S Ω[A⁄R])

instance KaehlerDifferential.instSMulCommClassTensorProduct_1 (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] : SMulCommClass A S (TensorProduct R S Ω[A⁄R])

@[reducible]

noncomputable def KaehlerDifferential.moduleBaseChange' (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] : Module B (TensorProduct R S Ω[A⁄R])

(Implementation). B = S ⊗[R] A-module structure on S ⊗[R] Ω[A⁄R].

instance KaehlerDifferential.instIsScalarTowerTensorProduct_1 (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] : IsScalarTower A B (TensorProduct R S Ω[A⁄R])

instance KaehlerDifferential.instIsScalarTowerTensorProduct_2 (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] : IsScalarTower S B (TensorProduct R S Ω[A⁄R])

theorem KaehlerDifferential.map_liftBaseChange_smul (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [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 : Algebra.IsPushout R S A B] (b : B) (x : TensorProduct R S Ω[A⁄R]) : (LinearMap.liftBaseChange S (↑R (map R S A B))) (b • x) = b • (LinearMap.liftBaseChange S (↑R (map R S A B))) x

noncomputable def KaehlerDifferential.derivationTensorProduct (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [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 : Algebra.IsPushout R S A B] : Derivation S B (TensorProduct R S Ω[A⁄R])

(Implementation). The S-derivation B = S ⊗[R] A to S ⊗[R] Ω[A⁄R] sending a ⊗ b to a ⊗ d b.

theorem KaehlerDifferential.derivationTensorProduct_algebraMap (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] (x : A) : (derivationTensorProduct R S A B) ((algebraMap A B) x) = 1 ⊗ₜ[R] (D R A) x

theorem KaehlerDifferential.tensorKaehlerEquiv_left_inv (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] : ↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B)) = LinearMap.id

noncomputable def KaehlerDifferential.tensorKaehlerEquivBase (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [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 : Algebra.IsPushout R S A B] : TensorProduct R S Ω[A⁄R] ≃ₗ[S] Ω[B⁄S]

The canonical isomorphism (S ⊗[R] Ω[A⁄R]) ≃ₗ[S] Ω[B⁄S] for B = S ⊗[R] A. Also see KaehlerDifferential.tensorKaehlerEquiv for the version with B ⊗[A] Ω[A⁄R].

@[simp]

theorem KaehlerDifferential.tensorKaehlerEquivBase_symm_apply (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [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 : Algebra.IsPushout R S A B] (a : Ω[B⁄S]) : (tensorKaehlerEquivBase R S A B).symm a = (derivationTensorProduct R S A B).liftKaehlerDifferential a

@[simp]

theorem KaehlerDifferential.tensorKaehlerEquivBase_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] (a : S) (b : Ω[A⁄R]) : (tensorKaehlerEquivBase R S A B) (a ⊗ₜ[R] b) = a • (map R S A B) b

@[deprecated KaehlerDifferential.tensorKaehlerEquivBase_tmul (since := "2026-01-01")]

theorem KaehlerDifferential.tensorKaehlerEquiv_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] (a : S) (b : Ω[A⁄R]) : (tensorKaehlerEquivBase R S A B) (a ⊗ₜ[R] b) = a • (map R S A B) b

Alias of KaehlerDifferential.tensorKaehlerEquivBase_tmul.

theorem KaehlerDifferential.isBaseChange (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [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 : Algebra.IsPushout R S A B] : IsBaseChange S (↑R (map R S A B))

If B is the tensor product of S and A over R, then Ω[B⁄S] is the base change of Ω[A⁄R] along R → S.

instance KaehlerDifferential.isLocalizedModule (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] (p : Submonoid R) [IsLocalization p S] [IsLocalization (Algebra.algebraMapSubmonoid A p) B] : IsLocalizedModule p (↑R (map R S A B))

instance KaehlerDifferential.isLocalizedModule_of_isLocalizedModule (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] (p : Submonoid R) [IsLocalization p S] [IsLocalizedModule p (IsScalarTower.toAlgHom R A B).toLinearMap] : IsLocalizedModule p (↑R (map R S A B))

noncomputable def KaehlerDifferential.tensorKaehlerEquiv (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [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 : Algebra.IsPushout R S A B] : TensorProduct A B Ω[A⁄R] ≃ₗ[B] Ω[B⁄S]

The canonical isomorphism (B ⊗[A] Ω[A⁄R]) ≃ₗ[B] Ω[B⁄S] for B = S ⊗[R] A. Also see KaehlerDifferential.tensorKaehlerEquivBase for the version with S ⊗[R] Ω[A⁄R].

@[simp]

theorem KaehlerDifferential.tensorKaehlerEquiv_tmul_D (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] (b : B) (a : A) : (tensorKaehlerEquiv R S A B) (b ⊗ₜ[A] (D R A) a) = b • (D S B) ((algebraMap A B) a)

@[simp]

theorem KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] (s : S) (a : A) : (tensorKaehlerEquiv R S A (TensorProduct R S A)).symm ((D S (TensorProduct R S A)) (s ⊗ₜ[R] a)) = (algebraMap S (TensorProduct R S A)) s ⊗ₜ[A] (D R A) a

@[simp]

theorem KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul' (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] (s : S) (a : A) : (tensorKaehlerEquiv R S A (TensorProduct R A S)).symm ((D S (TensorProduct R A S)) (a ⊗ₜ[R] s)) = (algebraMap S (TensorProduct R A S)) s ⊗ₜ[A] (D R A) a