Documentation

Mathlib.RingTheory.Etale.Kaehler

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.

source
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.

Equations
Instances For
    source
    @[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])) :
    (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R S T) a✝ = (KaehlerDifferential.mapBaseChange R S T) a✝
    source
    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 (KaehlerDifferential.map R R S T)
    source
    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 (KaehlerDifferential.map R R S T)