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.
• Algebra.Extension.tensorCotangentOfFlat: If T is flat over R, there is a T-linear isomorphism T ⊗[R] P.Cotangent ≃ₗ[T] (P.baseChange).Cotangent.
• Algebra.Extension.tensorH1CotangentOfFlat: If T is flat over R, there is a T-linear isomorphism T ⊗[R] P.H1Cotangent ≃ₗ[T] (P.baseChange).H1Cotangent.
• Algebra.tensorH1CotangentOfFlat: Flat base change commutes with H1Cotangent.

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

noncomputable def Algebra.Extension.tensorCotangentOfFlat {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] [Module.Flat R T] : TensorProduct R T P.Cotangent ≃ₗ[T] P.baseChange.Cotangent

If T is flat over R, there is a T-linear isomorphism T ⊗[R] P.Cotangent ≃ₗ[T] (P.baseChange).Cotangent.

Equations

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

@[simp]

theorem Algebra.Extension.tensorCotangentOfFlat_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] [Module.Flat R T] (t : T) (x : P.Cotangent) : (P.tensorCotangentOfFlat T) (t ⊗ₜ[R] x) = t • (Cotangent.map (toBaseChange T)) x

noncomputable def Algebra.Extension.tensorToH1Cotangent {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] : TensorProduct R T P.H1Cotangent →ₗ[T] P.baseChange.H1Cotangent

The canonical map T ⊗[R] P.H1Cotangent →ₗ[T] (P.baseChange).H1Cotangent.

Equations

• P.tensorToH1Cotangent T = LinearMap.liftBaseChange T (↑R (Algebra.Extension.H1Cotangent.map (Algebra.Extension.toBaseChange T)))

@[simp]

theorem Algebra.Extension.tensorToH1Cotangent_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.H1Cotangent) : ↑((P.tensorToH1Cotangent T) (t ⊗ₜ[R] x)) = t • (Cotangent.map (toBaseChange T)) ↑x

theorem Algebra.Extension.tensorToH1Cotangent_bijective_of_flat {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] [Module.Flat R T] : Function.Bijective ⇑(P.tensorToH1Cotangent T)

If T is R-flat, the canonical map T ⊗[R] P.H1Cotangent →ₗ[T] (P.baseChange T).H1Cotangent is bijective.

noncomputable def Algebra.Extension.tensorH1CotangentOfFlat {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] [Module.Flat R T] : TensorProduct R T P.H1Cotangent ≃ₗ[T] P.baseChange.H1Cotangent

If T is flat over R, there is a T-linear isomorphism T ⊗[R] P.H1Cotangent ≃ₗ[T] (P.baseChange).H1Cotangent.

Equations

• P.tensorH1CotangentOfFlat T = LinearEquiv.ofBijective (P.tensorToH1Cotangent T) ⋯

theorem Algebra.Extension.tensorH1CotangentOfFlat_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] [Module.Flat R T] (t : T) (x : P.H1Cotangent) : (P.tensorH1CotangentOfFlat T) (t ⊗ₜ[R] x) = t • (H1Cotangent.map (toBaseChange T)) x

noncomputable def Algebra.tensorH1CotangentOfFlat (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] [Module.Flat R T] : TensorProduct R T (H1Cotangent R S) ≃ₗ[T] H1Cotangent T (TensorProduct R T S)

Flat base change commutes with H1Cotangent.

Equations

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

theorem Algebra.tensorH1CotangentOfFlat_tmul (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] [Module.Flat R T] (t : T) (x : H1Cotangent R S) : (tensorH1CotangentOfFlat R S T) (t ⊗ₜ[R] x) = t • (H1Cotangent.map R T S (TensorProduct R T S)) x