feat(RingTheory): Extension.CotangentSpace commutes with base change (#35594)

From Pi1.

Author: chrisflav

Mathlib.lean

@@ -6212,6 +6212,7 @@ public import Mathlib.RingTheory.Etale.QuasiFinite
 public import Mathlib.RingTheory.Etale.StandardEtale
 public import Mathlib.RingTheory.EuclideanDomain
 public import Mathlib.RingTheory.Extension.Basic
+public import Mathlib.RingTheory.Extension.Cotangent.BaseChange
 public import Mathlib.RingTheory.Extension.Cotangent.Basic
 public import Mathlib.RingTheory.Extension.Cotangent.Basis
 public import Mathlib.RingTheory.Extension.Cotangent.Free

Mathlib/RingTheory/Extension/Basic.lean

@@ -161,6 +161,20 @@ def baseChange {T} [CommRing T] [Algebra R T] (P : Extension R S) : Extension T
     (IsScalarTower.toAlgHom _ _ _)) (LinearMap.lTensor_surjective T
     (g := (IsScalarTower.toAlgHom R P.Ring S).toLinearMap) P.algebraMap_surjective)
 
+variable (T) in
+/--
+The ring `T ⊗[R] P.Ring` underlying the extension `P.baseChange T` is a `P.Ring`-algebra
+by action on the right. This causes a (mathematical) diamond when `T = P.Ring`, so it is
+not an instance.
+-/
+@[instance_reducible]
+noncomputable def algebraBaseChange : Algebra P.Ring (P.baseChange (T := T)).Ring :=
+  TensorProduct.rightAlgebra
+
+set_option backward.isDefEq.respectTransparency false in
+attribute [local instance] algebraBaseChange in
+instance : IsScalarTower R P.Ring (P.baseChange (T := T)).Ring :=
+  .of_algebraMap_eq fun x ↦ by simp [baseChange, RingHom.algebraMap_toAlgebra]; rfl
 
 end Construction
 
@@ -242,6 +256,16 @@ def Hom.mapKer (f : P.Hom P')
   map_add' _ _ := Subtype.ext (map_add _ _ _)
   map_smul' := by simp [Algebra.smul_def, ← halg]
 
+set_option backward.isDefEq.respectTransparency false in
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+/-- The canonical hom from `P` to its base change `P.baseChange`. -/
+@[simps]
+noncomputable def toBaseChange (T : Type*) [CommRing T] [Algebra R T] :
+    P.Hom (P.baseChange (T := T)) where
+  toRingHom := TensorProduct.includeRight.toRingHom
+  toRingHom_algebraMap x := by simp [baseChange]
+  algebraMap_toRingHom x := rfl
+
 end
 
 end Hom

Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2025 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+module
+
+public import Mathlib.RingTheory.Extension.Cotangent.Basic
+public import Mathlib.RingTheory.Kaehler.TensorProduct
+
+/-!
+# 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.
+-/
+
+public section
+
+universe u
+
+open TensorProduct
+
+namespace Algebra
+
+namespace Extension
+
+variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+variable (P : Extension.{u} R S)
+variable (T : Type*) [CommRing T] [Algebra R T]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The cotangent space of an extension commutes with base change. -/
+noncomputable
+def tensorCotangentSpace (P : Extension.{u} R S) (T : Type*) [CommRing T] [Algebra R T] :
+    T ⊗[R] P.CotangentSpace ≃ₗ[T] (P.baseChange (T := T)).CotangentSpace :=
+  letI := P.algebraBaseChange T
+  letI : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
+  letI : Algebra P.Ring (T ⊗[R] S) := Algebra.compHom _ (algebraMap P.Ring S)
+  haveI : IsScalarTower R P.Ring (T ⊗[R] S) :=
+    .of_algebraMap_eq fun x ↦ by
+      rw [TensorProduct.algebraMap_apply, RingHom.algebraMap_toAlgebra,
+        Algebra.TensorProduct.tmul_one_eq_one_tmul, IsScalarTower.algebraMap_apply R P.Ring]
+      rfl
+  letI PT : Extension T (T ⊗[R] S) := P.baseChange
+  haveI : IsPushout R T P.Ring PT.Ring := by
+    convert TensorProduct.isPushout (R := R) (T := P.Ring) (S := T)
+    exact Algebra.algebra_ext _ _ fun _ ↦ rfl
+  haveI : IsScalarTower P.Ring PT.Ring (T ⊗[R] S) := .of_algebraMap_eq' rfl
+  (IsTensorProduct.assocOfMapSMul (TensorProduct.mk R T S) (isTensorProduct _ _ _)
+    (TensorProduct.mk _ _ _) (isTensorProduct _ _ _) (by simp [Algebra.smul_def])
+    (by simp [Algebra.smul_def, RingHom.algebraMap_toAlgebra])).symm ≪≫ₗ
+  (AlgebraTensorModule.cancelBaseChange _ PT.Ring PT.Ring _ _).symm.restrictScalars T ≪≫ₗ
+  (AlgebraTensorModule.congr (LinearEquiv.refl PT.Ring (T ⊗[R] S))
+    (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring PT.Ring)).restrictScalars T
+
+attribute [local instance] algebraBaseChange in
+lemma tensorCotangentSpace_tmul_tmul (t : T) (s : S) (x : Ω[P.Ring⁄R]) :
+    P.tensorCotangentSpace T (t ⊗ₜ (s ⊗ₜ x)) = t ⊗ₜ s ⊗ₜ KaehlerDifferential.map _ _ _ _ x := by
+  simp only [tensorCotangentSpace, LinearEquiv.trans_apply, LinearEquiv.restrictScalars_apply,
+    ← mk_apply s x, IsTensorProduct.assocOfMapSMul_symm_tmul]
+  simp only [mk_apply, AlgebraTensorModule.cancelBaseChange_symm_tmul,
+    AlgebraTensorModule.congr_tmul, LinearEquiv.refl_apply]
+  have this : x ∈ Submodule.span P.Ring (Set.range (KaehlerDifferential.D R P.Ring)) := by
+    rw [KaehlerDifferential.span_range_derivation]
+    trivial
+  induction this using Submodule.span_induction with
+  | zero => simp
+  | add x y _ _ hx hy => simp [tmul_add, hx, hy]
+  | mem y hy =>
+    obtain ⟨y, rfl⟩ := hy
+    simp
+  | smul a x _ hx =>
+    rw [tmul_smul, ← algebraMap_smul (P.baseChange (T := T)).Ring a, LinearEquiv.map_smul,
+      tmul_smul, hx, LinearMap.map_smul, ← algebraMap_smul (P.baseChange (T := T)).Ring a,
+      tmul_smul]
+
+set_option backward.isDefEq.respectTransparency false in
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+@[simp]
+lemma tensorCotangentSpace_tmul (t : T) (x : P.CotangentSpace) :
+    P.tensorCotangentSpace T (t ⊗ₜ x) = t • CotangentSpace.map (P.toBaseChange T) x := by
+  dsimp only [CotangentSpace] at x
+  induction x with
+  | zero => rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
+  | add x y hx hy => rw [tmul_add, LinearEquiv.map_add, LinearMap.map_add, smul_add, hx, hy]
+  | tmul s y =>
+  simp [tensorCotangentSpace_tmul_tmul, CotangentSpace.map_tmul_eq_tmul_map,
+    smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra]
+
+end Extension
+
+end Algebra

Mathlib/RingTheory/Extension/Cotangent/Basic.lean

@@ -159,6 +159,13 @@ lemma map_tmul (f : Hom P P') (x y) :
   rw [smul_tmul', ← Algebra.algebraMap_eq_smul_one]
   rfl
 
+lemma map_tmul_eq_tmul_map (f : P.Hom P') (x : S) (y : Ω[P.Ring⁄R]) :
+    letI : Algebra P.Ring P'.Ring := f.toAlgHom.toAlgebra
+    (CotangentSpace.map f) (x ⊗ₜ[P.Ring] y) =
+      (algebraMap S S') x ⊗ₜ[P'.Ring] KaehlerDifferential.map _ _ _ _ y := by
+  rw [CotangentSpace.map, LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, Function.comp_apply,
+    LinearMap.restrictScalars_apply, mk_apply, smul_tmul', Algebra.smul_def, mul_one]
+
 @[simp]
 lemma map_id :
     CotangentSpace.map (.id P) = LinearMap.id := by ext; simp
@@ -371,6 +378,11 @@ lemma h1Cotangentι_injective : Function.Injective P.h1Cotangentι := Subtype.va
 
 @[ext] lemma h1Cotangentι_ext (x y : P.H1Cotangent) (e : x.1 = y.1) : x = y := Subtype.ext e
 
+/-- The sequence `H¹(L_{S/R}) → P.Cotangent → P.CotangentSpace` is exact. -/
+lemma exact_hCotangentι_cotangentComplex : Function.Exact h1Cotangentι P.cotangentComplex := by
+  rw [LinearMap.exact_iff]
+  exact (Submodule.range_subtype _).symm
+
 /--
 The induced map on the first homology of the (naive) cotangent complex.
 -/