[Merged by Bors] - feat(RingTheory/Extension): naive cotangent complex commutes with flat base change

Mathlib/RingTheory/Extension/Basic.lean

@@ -151,7 +151,7 @@ def localization (P : Extension.{w} R S) : Extension R S' where
 
 end Localization
 
-variable {T} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
+variable {T} [CommRing T] [Algebra R T]
 
 /-- The base change of an `R`-extension of `S` to `T` gives a `T`-extension of `T ⊗[R] S`. -/
 noncomputable
@@ -161,6 +161,12 @@ 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
+lemma ker_baseChange :
+    (P.baseChange (T := T)).ker = P.ker.map Algebra.TensorProduct.includeRight.toRingHom :=
+  Algebra.TensorProduct.lTensor_ker (A := T) (IsScalarTower.toAlgHom R P.Ring S)
+    P.algebraMap_surjective
+
 variable (T) in
 /--
 The ring `T ⊗[R] P.Ring` underlying the extension `P.baseChange T` is a `P.Ring`-algebra
@@ -221,6 +227,26 @@ def Hom.toAlgHom [Algebra R S'] [IsScalarTower R R' S'] (f : Hom P P') :
 lemma Hom.toAlgHom_apply [Algebra R S'] [IsScalarTower R R' S'] (f : Hom P P') (x) :
     f.toAlgHom x = f.toRingHom x := rfl
 
+/-- A hom of extensions `P → P'` can be constructed from an algebra map
+`P.Ring →ₐ[R] P'.Ring`. -/
+@[simps]
+def Hom.ofAlgHom [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
+    (f : P.Ring →ₐ[R] P'.Ring)
+    (H : (IsScalarTower.toAlgHom R P'.Ring S').comp f =
+      (IsScalarTower.toAlgHom R S S').comp (IsScalarTower.toAlgHom R P.Ring S)) :
+    P.Hom P' where
+  toRingHom := f.toRingHom
+  toRingHom_algebraMap := f.commutes'
+  algebraMap_toRingHom x := congr($H x)
+
+@[simp]
+lemma Hom.toAlgHom_ofAlgHom [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
+    (f : P.Ring →ₐ[R] P'.Ring)
+    (H : (IsScalarTower.toAlgHom R P'.Ring S').comp f =
+      (IsScalarTower.toAlgHom R S S').comp (IsScalarTower.toAlgHom R P.Ring S)) :
+    (Hom.ofAlgHom f H).toAlgHom = f :=
+  rfl
+
 variable (P P')
 
 /-- The identity hom. -/
@@ -381,6 +407,14 @@ lemma Cotangent.val_smul' (r : P.Ring) (x : P.Cotangent) : (r • x).val = r •
 lemma Cotangent.val_smul'' (r : R) (x : P.Cotangent) : (r • x).val = r • x.val := by
   rw [← algebraMap_smul P.Ring, val_smul', algebraMap_smul]
 
+/-- `Cotangent.val` as a linear isomorphism. -/
+@[simps]
+def cotangentEquivCotangentKer : P.Cotangent ≃ₗ[P.Ring] P.ker.Cotangent where
+  toFun := Cotangent.val
+  invFun := Cotangent.of
+  map_add' x y := by simp
+  map_smul' x y := by simp
+
 /-- The quotient map from the kernel of `P → S` onto the cotangent space. -/
 noncomputable def Cotangent.mk : P.ker →ₗ[P.Ring] P.Cotangent where
   toFun x := .of (Ideal.toCotangent _ x)

Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean

@@ -5,7 +5,9 @@ Authors: Christian Merten
 -/
 module
 
+public import Mathlib.RingTheory.Ideal.CotangentBaseChange
 public import Mathlib.RingTheory.Extension.Cotangent.Basic
+public import Mathlib.Algebra.FiveLemma
 public import Mathlib.RingTheory.Kaehler.TensorProduct
 
 /-!
@@ -18,11 +20,12 @@ commute with base change.
 
 - `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`.
 
-## TODOs (@chrisflav)
-
-- Show that `P.Cotangent` commutes with flat base change.
-- Show that `P.H1Cotangent` commutes with flat base change.
 -/
 
 public section
@@ -33,10 +36,11 @@ open TensorProduct
 
 namespace Algebra
 
+variable (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
+
 namespace Extension
 
-variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
-variable (P : Extension.{u} R S)
+variable {R S} (P : Extension.{u} R S)
 variable (T : Type*) [CommRing T] [Algebra R T]
 
 set_option backward.isDefEq.respectTransparency false in
@@ -98,6 +102,115 @@ lemma tensorCotangentSpace_tmul (t : T) (x : P.CotangentSpace) :
   simp [tensorCotangentSpace_tmul_tmul, CotangentSpace.map_tmul_eq_tmul_map,
     smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra]
 
+/-- If `T` is flat over `R`, there is a `T`-linear isomorphism
+`T ⊗[R] P.Cotangent ≃ₗ[T] (P.baseChange).Cotangent`. -/
+noncomputable def tensorCotangentOfFlat [Module.Flat R T] :
+    T ⊗[R] P.Cotangent ≃ₗ[T] (P.baseChange (T := T)).Cotangent :=
+  AlgebraTensorModule.congr (.refl T T) (P.cotangentEquivCotangentKer.restrictScalars R) ≪≫ₗ
+    P.ker.tensorCotangentEquiv R T ≪≫ₗ
+    (Ideal.Cotangent.equivOfEq _ _ (P.ker_baseChange T).symm).restrictScalars T ≪≫ₗ
+    (P.baseChange (T := T)).cotangentEquivCotangentKer.symm.restrictScalars T
+
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+@[simp]
+lemma tensorCotangentOfFlat_tmul [Module.Flat R T] (t : T) (x : P.Cotangent) :
+    P.tensorCotangentOfFlat T (t ⊗ₜ x) = t • Cotangent.map (P.toBaseChange T) x := by
+  obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
+  simp only [tensorCotangentOfFlat, LinearEquiv.trans_apply, AlgebraTensorModule.congr_tmul,
+    LinearEquiv.refl_apply, LinearEquiv.restrictScalars_apply, cotangentEquivCotangentKer_apply,
+    Cotangent.val_mk, Ideal.tensorCotangentEquiv_tmul, map_smul, Cotangent.map_mk,
+    Hom.toAlgHom_apply, Ideal.Cotangent.equivOfEq_toCotangent]
+  rfl
+
+/-- The canonical map `T ⊗[R] P.H1Cotangent →ₗ[T] (P.baseChange).H1Cotangent`. -/
+@[expose]
+noncomputable
+def tensorToH1Cotangent : T ⊗[R] P.H1Cotangent →ₗ[T] (P.baseChange (T := T)).H1Cotangent :=
+  letI : Algebra S (T ⊗[R] S) := Algebra.TensorProduct.rightAlgebra
+  LinearMap.liftBaseChange T <|
+    (Extension.H1Cotangent.map (P.toBaseChange T)).restrictScalars R
+
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+@[simp]
+lemma tensorToH1Cotangent_tmul (t : T) (x : P.H1Cotangent) :
+    (P.tensorToH1Cotangent T (t ⊗ₜ x)).val = t • Cotangent.map (P.toBaseChange T) x.val :=
+  rfl
+
+/-- If `T` is `R`-flat, the canonical map `T ⊗[R] P.H1Cotangent →ₗ[T] (P.baseChange T).H1Cotangent`
+is bijective. -/
+lemma tensorToH1Cotangent_bijective_of_flat [Module.Flat R T] :
+    Function.Bijective (P.tensorToH1Cotangent T) := by
+  -- We apply the five lemma.
+  apply LinearMap.bijective_of_surjective_of_bijective_of_bijective_of_injective (M₁ := Unit)
+      (N₁ := Unit) (M₂ := Unit) (N₂ := Unit)
+    -- The row `0 → 0 → T ⊗ H¹(P) → T ⊗ P.Cotangent → T ⊗ P.CotangentSpace`.
+    0 0
+    ((P.h1Cotangentι.restrictScalars R).lTensor T)
+    ((P.cotangentComplex.restrictScalars R).lTensor T)
+    -- The row `0 → 0 → H¹(T ⊗ P) → (T ⊗ P).Cotangent → (T ⊗ P).CotangentSpace`.
+    0 0
+    (h1Cotangentι.restrictScalars R)
+    ((P.baseChange (T := T)).cotangentComplex.restrictScalars R)
+    -- The vertical maps induced by base change.
+    0 0
+    ((P.tensorToH1Cotangent T).restrictScalars R)
+    ((P.tensorCotangentOfFlat T).restrictScalars R)
+    ((P.tensorCotangentSpace T).restrictScalars R)
+  · simp
+  · simp
+  · ext
+    simp
+  · ext
+    simp [CotangentSpace.map_cotangentComplex]
+  · tauto
+  · simp only [LinearMap.exact_zero_iff_injective]
+    apply Module.Flat.lTensor_preserves_injective_linearMap
+    exact h1Cotangentι_injective
+  · apply Module.Flat.lTensor_exact
+    exact P.exact_hCotangentι_cotangentComplex
+  · tauto
+  · rw [LinearMap.exact_zero_iff_injective]
+    simp only [LinearMap.coe_restrictScalars]
+    exact h1Cotangentι_injective
+  · apply exact_hCotangentι_cotangentComplex
+  · tauto
+  · simp
+  · exact (P.tensorCotangentOfFlat T).bijective
+  · exact (P.tensorCotangentSpace T).injective
+
+/-- If `T` is flat over `R`, there is a `T`-linear isomorphism
+`T ⊗[R] P.H1Cotangent ≃ₗ[T] (P.baseChange).H1Cotangent`. -/
+@[expose]
+noncomputable def tensorH1CotangentOfFlat [Module.Flat R T] :
+    T ⊗[R] P.H1Cotangent ≃ₗ[T] (P.baseChange (T := T)).H1Cotangent :=
+  LinearEquiv.ofBijective (P.tensorToH1Cotangent T)
+    (P.tensorToH1Cotangent_bijective_of_flat T)
+
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+lemma tensorH1CotangentOfFlat_tmul [Module.Flat R T] (t : T) (x : P.H1Cotangent) :
+    P.tensorH1CotangentOfFlat T (t ⊗ₜ x) = t • H1Cotangent.map (P.toBaseChange T) x :=
+  rfl
+
 end Extension
 
+/-- Flat base change commutes with `H1Cotangent`. -/
+noncomputable def tensorH1CotangentOfFlat (T : Type*) [CommRing T] [Algebra R T] [Module.Flat R T] :
+    T ⊗[R] H1Cotangent R S ≃ₗ[T] H1Cotangent T (T ⊗[R] S) :=
+  (Generators.self R S).toExtension.tensorH1CotangentOfFlat T ≪≫ₗ
+    (Extension.H1Cotangent.equiv
+      ((Generators.self R S).baseChangeFromBaseChange T)
+      ((Generators.self R S).baseChangeToBaseChange T)).restrictScalars T ≪≫ₗ
+    ((Generators.self R S).baseChange (T := T)).equivH1Cotangent.restrictScalars T
+
+attribute [local instance] TensorProduct.rightAlgebra in
+lemma tensorH1CotangentOfFlat_tmul (T : Type*) [CommRing T] [Algebra R T] [Module.Flat R T]
+    (t : T) (x : H1Cotangent R S) :
+    tensorH1CotangentOfFlat R S T (t ⊗ₜ x) = t • H1Cotangent.map _ _ _ _ x := by
+  simp only [tensorH1CotangentOfFlat, LinearEquiv.trans_apply,
+    Extension.tensorH1CotangentOfFlat_tmul, map_smul, LinearEquiv.restrictScalars_apply,
+    Extension.H1Cotangent.equiv, LinearEquiv.coe_mk, Generators.equivH1Cotangent,
+    Generators.H1Cotangent.equiv]
+  rw [← Extension.H1Cotangent.map_comp_apply, ← Extension.H1Cotangent.map_comp_apply,
+    H1Cotangent.map, Extension.H1Cotangent.map_eq]
+
 end Algebra

Mathlib/RingTheory/Extension/Cotangent/Basic.lean

@@ -412,6 +412,12 @@ lemma H1Cotangent.map_comp
     map (g.comp f) = (map g).restrictScalars S ∘ₗ map f := by
   ext; simp [Cotangent.map_comp]
 
+omit [IsScalarTower R S S'] in
+@[simp]
+lemma H1Cotangent.map_comp_apply (f : Hom P P') (g : Hom P' P'') (x : P.H1Cotangent) :
+    map (g.comp f) x = map g (map f x) :=
+  congr($(H1Cotangent.map_comp f g) x)
+
 /-- Maps `P₁ → P₂` and `P₂ → P₁` between extensions
 induce an isomorphism between `H¹(L_P₁)` and `H¹(L_P₂)`. -/
 @[simps! apply]

Mathlib/RingTheory/Extension/Generators.lean

@@ -8,7 +8,7 @@ module
 public import Mathlib.RingTheory.Ideal.Cotangent
 public import Mathlib.RingTheory.Localization.Away.Basic
 public import Mathlib.RingTheory.MvPolynomial.Tower
-public import Mathlib.RingTheory.TensorProduct.Basic
+public import Mathlib.RingTheory.TensorProduct.MvPolynomial
 public import Mathlib.RingTheory.Extension.Basic
 
 /-!
@@ -209,13 +209,14 @@ def localizationAway : Generators R S Unit where
 
 end Localization
 
-variable {ι' : Type*} {T} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
+variable {ι' : Type*} {T} [CommRing T] [Algebra R T]
 
 /-- Given two families of generators `S[X] → T` and `R[Y] → S`,
 we may construct the family of generators `R[X, Y] → T`. -/
 @[simps val, simps -isSimp σ]
 noncomputable
-def comp (Q : Generators S T ι') (P : Generators R S ι) : Generators R T (ι' ⊕ ι) where
+def comp [Algebra S T] [IsScalarTower R S T]
+    (Q : Generators S T ι') (P : Generators R S ι) : Generators R T (ι' ⊕ ι) where
   val := Sum.elim Q.val (algebraMap S T ∘ P.val)
   σ' x := (Q.σ x).sum (fun n r ↦ rename Sum.inr (P.σ r) * monomial (n.mapDomain Sum.inl) 1)
   aeval_val_σ' s := by
@@ -231,7 +232,8 @@ variable (S) in
 gives a family of generators `S[X] → T`. -/
 @[simps val]
 noncomputable
-def extendScalars (P : Generators R T ι) : Generators S T ι where
+def extendScalars [Algebra S T] [IsScalarTower R S T] (P : Generators R T ι) :
+    Generators S T ι where
   val := P.val
   σ' x := map (algebraMap R S) (P.σ x)
   aeval_val_σ' s := by simp [@aeval_def S, ← IsScalarTower.algebraMap_eq, ← @aeval_def R]
@@ -266,6 +268,40 @@ def baseChange (T) [CommRing T] [Algebra R T] (P : Generators R S ι) :
     use (a + b)
     rw [map_add, ha, hb]
 
+variable (T) in
+set_option backward.isDefEq.respectTransparency false in
+/-- The forwards direction of the canonical isomorphism `T ⊗[R] R[Xᵢ] ≃ₐ[T] T[Xᵢ]` as
+a map of extensions. -/
+noncomputable def baseChangeFromBaseChange :
+    (P.toExtension.baseChange (T := T)).Hom (P.baseChange (T := T)).toExtension :=
+  .ofAlgHom (MvPolynomial.algebraTensorAlgEquiv R T).toAlgHom <| by
+    dsimp [Extension.baseChange]
+    ext
+    simp [RingHom.algebraMap_toAlgebra]
+
+@[simp]
+lemma baseChangeFromBaseChange_apply (x : P.toExtension.baseChange.Ring) :
+    dsimp% (P.baseChangeFromBaseChange T).toRingHom x = MvPolynomial.algebraTensorAlgEquiv R T x :=
+  rfl
+
+variable (T) in
+set_option backward.isDefEq.respectTransparency false in
+/-- The backwards direction of the canonical isomorphism `T ⊗[R] R[Xᵢ] ≃ₐ[T] T[Xᵢ]` as
+a map of extensions. -/
+noncomputable def baseChangeToBaseChange :
+    (P.baseChange (T := T)).toExtension.Hom (P.toExtension.baseChange (T := T)) :=
+  .ofAlgHom (MvPolynomial.algebraTensorAlgEquiv R T).symm.toAlgHom <| by
+    dsimp [Extension.baseChange]
+    ext
+    simp [RingHom.algebraMap_toAlgebra]
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma baseChangeToBaseChange_apply (x : (baseChange T P).toExtension.Ring) :
+    dsimp% (P.baseChangeToBaseChange T).toRingHom x =
+      (MvPolynomial.algebraTensorAlgEquiv R T).symm x :=
+  rfl
+
 /-- Extend generators by more variables. -/
 noncomputable def extend (P : Generators R S ι) (b : ι' → S) : Generators R S (ι ⊕ ι') :=
   .ofSurjective (Sum.elim P.val b) fun s ↦ by

Mathlib/RingTheory/Ideal/Cotangent.lean

@@ -223,14 +223,16 @@ lemma mapCotangent_toCotangent
     (I₁ : Ideal A) (I₂ : Ideal B) (f : A →ₐ[R] B) (h : I₁ ≤ I₂.comap f) (x : I₁) :
     Ideal.mapCotangent I₁ I₂ f h (Ideal.toCotangent I₁ x) = Ideal.toCotangent I₂ ⟨f x, h x.2⟩ := rfl
 
+namespace Cotangent
+
 section Lift
 
 variable {S : Type*} [CommRing S] [Algebra R S] {I : Ideal S}
 variable {M : Type*} [AddCommGroup M] [Module R M]
 
 /-- Lift a linear map `f : I →ₗ[R] M` that vanishes on products to a linear map on the
 cotangent space `I ⧸ I ^ 2`. -/
-def Cotangent.lift (f : I →ₗ[R] M) (hf : ∀ (x y : I), f (x * y) = 0) :
+def lift (f : I →ₗ[R] M) (hf : ∀ (x y : I), f (x * y) = 0) :
     I.Cotangent →ₗ[R] M where
   __ := QuotientAddGroup.lift _ f.toAddMonoidHom <| fun x hx ↦ by
     simp only [Submodule.mem_toAddSubgroup, AddMonoidHom.mem_ker] at hx ⊢
@@ -241,16 +243,16 @@ def Cotangent.lift (f : I →ₗ[R] M) (hf : ∀ (x y : I), f (x * y) = 0) :
     exact map_smul f _ _
 
 @[simp]
-lemma Cotangent.lift_toCotangent (f : I →ₗ[R] M) (hf : ∀ (x y : I), f (x * y) = 0) (x : I) :
+lemma lift_toCotangent (f : I →ₗ[R] M) (hf : ∀ (x y : I), f (x * y) = 0) (x : I) :
     Cotangent.lift f hf (I.toCotangent x) = f x :=
   rfl
 
 @[simp]
-lemma Cotangent.lift_comp_toCotangent (f : I →ₗ[R] M) (hf : ∀ (x y : I), f (x * y) = 0) :
+lemma lift_comp_toCotangent (f : I →ₗ[R] M) (hf : ∀ (x y : I), f (x * y) = 0) :
     Cotangent.lift f hf ∘ₗ I.toCotangent = f :=
   rfl
 
-lemma Cotangent.lift_surjective_iff (f : I →ₗ[R] M) (hf : ∀ (x y : I), f (x * y) = 0) :
+lemma lift_surjective_iff (f : I →ₗ[R] M) (hf : ∀ (x y : I), f (x * y) = 0) :
     Function.Surjective (Cotangent.lift f hf) ↔ Function.Surjective f := by
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · rw [← Cotangent.lift_comp_toCotangent f hf, LinearMap.coe_comp]
@@ -260,7 +262,34 @@ lemma Cotangent.lift_surjective_iff (f : I →ₗ[R] M) (hf : ∀ (x y : I), f (
 
 end Lift
 
-end Ideal
+/-- A linear isomorphism between cotangent spaces induced by an equality of ideals. -/
+@[expose]
+def equivOfEq (I J : Ideal R) (hIJ : I = J) :
+    I.Cotangent ≃ₗ[R] J.Cotangent where
+  __ := Cotangent.lift (J.toCotangent ∘ₗ LinearEquiv.ofEq I J hIJ) <| fun x y ↦ by
+    simp [toCotangent_eq_zero, ← hIJ, sq, mul_mem_mul]
+  invFun := Cotangent.lift (I.toCotangent ∘ₗ LinearEquiv.ofEq J I hIJ.symm) <| fun x y ↦ by
+    simp [toCotangent_eq_zero, hIJ, sq, mul_mem_mul]
+  left_inv x := by
+    subst hIJ
+    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
+    simp
+  right_inv x := by
+    subst hIJ
+    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
+    simp
+
+@[simp]
+lemma equivOfEq_toCotangent (I J : Ideal R) (hIJ : I = J) (x : I) :
+    Cotangent.equivOfEq I J hIJ (I.toCotangent x) = J.toCotangent (LinearEquiv.ofEq I J hIJ x) :=
+  rfl
+
+@[simp]
+lemma equivOfEq_symm (I J : Ideal R) (hIJ : I = J) :
+    (Cotangent.equivOfEq I J hIJ).symm = Cotangent.equivOfEq J I hIJ.symm :=
+  rfl
+
+end Ideal.Cotangent
 
 namespace IsLocalRing