Kaehler differential module under base change #

Main results #

KaehlerDifferential.tensorKaehlerEquiv: (S ⊗[R] Ω[A⁄R]) ≃ₗ[S] Ω[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].

Equations

KaehlerDifferential.mulActionBaseChange R S A = Equiv.mulAction A (TensorProduct.comm R S (Ω[A⁄R])).toEquiv

Instances For

source

@[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)

source

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

source

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 : TensorProduct R S (Ω[A⁄R])) (y : TensorProduct R S (Ω[A⁄R])) :

a • (x + y) = a • x + a • y

source

@[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].

Equations

KaehlerDifferential.moduleBaseChange R S A = Module.mk ⋯ ⋯

Instances For

source

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]))

Equations

⋯ = ⋯

source

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]))

Equations

⋯ = ⋯

source

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]))

Equations

⋯ = ⋯

source

@[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].

Equations

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

Instances For

source

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]))

Equations

⋯ = ⋯

source

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]))

Equations

⋯ = ⋯

source

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 (KaehlerDifferential.map R S A B))) (b • x) = b • (LinearMap.liftBaseChange S (↑R (KaehlerDifferential.map R S A B))) x

source

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.

Equations

KaehlerDifferential.derivationTensorProduct R S A B = { toLinearMap := ⋯.lift ((TensorProduct.mk R S (Ω[A⁄R])) 1 ∘ₗ ↑(KaehlerDifferential.D R A)), map_one_eq_zero' := ⋯, leibniz' := ⋯ }

Instances For

source

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) :

(KaehlerDifferential.derivationTensorProduct R S A B) ((algebraMap A B) x) = 1 ⊗ₜ[R] (KaehlerDifferential.D R A) x

source

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 (KaehlerDifferential.derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (KaehlerDifferential.map R S A B)) = LinearMap.id

source

@[simp]

theorem KaehlerDifferential.tensorKaehlerEquiv_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]) :

(KaehlerDifferential.tensorKaehlerEquiv R S A B).symm a = (KaehlerDifferential.derivationTensorProduct R S A B).liftKaehlerDifferential a

source

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 R S (Ω[A⁄R]) ≃ₗ[S] Ω[B⁄S]

The canonical isomorphism (S ⊗[R] Ω[A⁄R]) ≃ₗ[S] Ω[B⁄S] for B = S ⊗[R] A.

Equations

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

Instances For

source

@[simp]

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]) :

(KaehlerDifferential.tensorKaehlerEquiv R S A B) (a ⊗ₜ[R] b) = a • (KaehlerDifferential.map R S A B) b

source

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 (KaehlerDifferential.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.

source

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 (KaehlerDifferential.map R S A B))

Equations

⋯ = ⋯

source

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 (KaehlerDifferential.map R S A B))

Equations

⋯ = ⋯

Documentation

Mathlib.RingTheory.Kaehler.TensorProduct

Kaehler differential module under base change #

Main results #