Base change for the naive cotangent complex

This file shows that the cotangent space and first homology of the naive cotangent complex commute with base change.

Main results

• Algebra.Extension.tensorCotangentSpace: If T is an R-algebra, there is a T-linear isomorphism T ⊗[R] P.CotangentSpace ≃ₗ[T] (P.baseChange).CotangentSpace.

TODOs (@chrisflav)

• Show that P.Cotangent commutes with flat base change.
• Show that P.H1Cotangent commutes with flat base change.

noncomputable def Algebra.Extension.tensorCotangentSpace {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) (T : Type u_4) [CommRing T] [Algebra R T] : TensorProduct R T P.CotangentSpace ≃ₗ[T] P.baseChange.CotangentSpace

The cotangent space of an extension commutes with base change.

Equations

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

theorem Algebra.Extension.tensorCotangentSpace_tmul_tmul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) (T : Type u_3) [CommRing T] [Algebra R T] (t : T) (s : S) (x : Ω[P.Ring⁄R]) : (P.tensorCotangentSpace T) (t ⊗ₜ[R] (s ⊗ₜ[P.Ring] x)) = t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring] (KaehlerDifferential.map R T P.Ring P.baseChange.Ring) x

@[simp]

theorem Algebra.Extension.tensorCotangentSpace_tmul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) (T : Type u_3) [CommRing T] [Algebra R T] (t : T) (x : P.CotangentSpace) : (P.tensorCotangentSpace T) (t ⊗ₜ[R] x) = t • (CotangentSpace.map (toBaseChange T)) x