Base change of cotangent spaces

Given an R-algebra S, an ideal I of S and a flat R-algebra T, we show that the base change T ⊗[R] I/I² of the cotangent space of I is naturally isomorphic to the cotangent space of the extended ideal I · (T ⊗[R] S).

Main definitions

• Ideal.tensorCotangentHom: The canonical map T ⊗[R] I/I² → (I · (T ⊗[R] S))/(I · (T ⊗[R] S))².
• Ideal.tensorCotangentEquiv: When T is R-flat, tensorCotangentHom is an isomorphism.

def Ideal.tensorCotangentHom (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] (I : Ideal S) : TensorProduct R T I.Cotangent →ₗ[T] (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent

The canonical map from the base change of the cotangent space T ⊗[R] I/I² to the cotangent space (I · (T ⊗[R] S))/(I · (T ⊗[R] S))² of the extended ideal. This map is always surjective (tensorCotangentHom_surjective) and injective if T is R-flat (tensorCotangentHom_injective_of_flat).

Equations

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

theorem Ideal.tensorCotangentHom_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] (I : Ideal S) (t : T) (x : ↥I) : (tensorCotangentHom R T I) (t ⊗ₜ[R] I.toCotangent x) = t • (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent ⟨1 ⊗ₜ[R] ↑x, ⋯⟩

theorem Ideal.tensorCotangentHom_surjective (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] (I : Ideal S) : Function.Surjective ⇑(tensorCotangentHom R T I)

theorem Ideal.tensorCotangentHom_injective_of_flat (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] (I : Ideal S) [Module.Flat R T] : Function.Injective ⇑(tensorCotangentHom R T I)

If T is a flat R-module, the canonical map tensorCotangentHom R T I is injective.

noncomputable def Ideal.tensorCotangentEquiv (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] (I : Ideal S) [Module.Flat R T] : TensorProduct R T I.Cotangent ≃ₗ[T] (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent

If T is a flat R-module, the base change of the cotangent space of I is linearly equivalent to the cotangent space of the extended ideal I · (T ⊗[R] S).

Equations

• Ideal.tensorCotangentEquiv R T I = LinearEquiv.ofBijective (Ideal.tensorCotangentHom R T I) ⋯

theorem Ideal.tensorCotangentEquiv_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] (I : Ideal S) [Module.Flat R T] (t : T) (x : ↥I) : (tensorCotangentEquiv R T I) (t ⊗ₜ[R] I.toCotangent x) = t • (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent ⟨1 ⊗ₜ[R] ↑x, ⋯⟩