Kähler differentials over a formally unramified base

For a scalar tower R → S → A, formal unramifiedness of S/R identifies Ω[A⁄R] with Ω[A⁄S]. Thus differentials, and their Fitting ideals, do not depend on which of these two base rings is used. In particular this applies to changing affine base charts along an open immersion.

References

• The Stacks Project, Tag 00RS: the transitivity sequence for differentials.

theorem KaehlerDifferential.map_bijective_of_formallyUnramified_base (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra.FormallyUnramified R S] : Function.Bijective ⇑(map R S A A)

Enlarging the base through a formally unramified algebra makes the canonical map on Kähler differentials bijective.

noncomputable def KaehlerDifferential.equivOfFormallyUnramifiedBase (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra.FormallyUnramified R S] : Ω[A⁄R] ≃ₗ[A] Ω[A⁄S]

The canonical identification Ω[A⁄R] ≃ₗ[A] Ω[A⁄S] when S/R is formally unramified.

@[simp]

theorem KaehlerDifferential.equivOfFormallyUnramifiedBase_apply (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra.FormallyUnramified R S] (x : Ω[A⁄R]) : (equivOfFormallyUnramifiedBase R S A) x = (map R S A A) x

The base comparison is the canonical map on Kähler differentials.

@[simp]

theorem KaehlerDifferential.equivOfFormallyUnramifiedBase_symm_D (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra.FormallyUnramified R S] (a : A) : (equivOfFormallyUnramifiedBase R S A).symm ((D S A) a) = (D R A) a

The inverse base comparison preserves the differential of a function.