[Merged by Bors] - feat(RingTheory/Smooth): calculate H¹(L) via formally smooth extensions

Mathlib/RingTheory/Extension.lean

@@ -115,6 +115,9 @@ def self : Extension R S where
   σ := _root_.id
   algebraMap_σ _ := rfl
 
+/-- The kernel of an extension. -/
+abbrev ker : Ideal P.Ring := RingHom.ker (algebraMap P.Ring S)
+
 section Localization
 
 variable (M : Submonoid S) {S' : Type*} [CommRing S'] [Algebra S S'] [IsLocalization M S']
@@ -232,10 +235,30 @@ end
 
 end Hom
 
-section Cotangent
+section Infinitesimal
 
-/-- The kernel of an extension. -/
-abbrev ker : Ideal P.Ring := RingHom.ker (algebraMap P.Ring S)
+/-- Given an `R`-algebra extension `0 → I → P → S → 0` of `S`,
+the infinitesimal extension associated to it is `0 → I/I² → P/I² → S → 0`. -/
+noncomputable
+def infinitesimal (P : Extension R S) : Extension R S where
+  Ring := P.Ring ⧸ P.ker ^ 2
+  σ := Ideal.Quotient.mk _ ∘ P.σ
+  algebraMap_σ x := by dsimp; exact P.algebraMap_σ x
+
+/-- The canonical map `P → P/I²` as maps between extensions. -/
+noncomputable
+def toInfinitesimal (P : Extension R S) : P.Hom P.infinitesimal where
+  toRingHom := Ideal.Quotient.mk _
+  toRingHom_algebraMap _ := rfl
+  algebraMap_toRingHom _ := rfl
+
+lemma ker_infinitesimal (P : Extension R S) :
+    P.infinitesimal.ker = P.ker.cotangentIdeal :=
+  AlgHom.ker_kerSquareLift _
+
+end Infinitesimal
+
+section Cotangent
 
 /-- The cotangent space of an extension.
 This is a type synonym so that `P.Ring` can act on it through the action of `S` without creating

Mathlib/RingTheory/Ideal/Cotangent.lean

@@ -120,18 +120,31 @@ theorem cotangentIdeal_square (I : Ideal R) : I.cotangentIdeal ^ 2 = ⊥ := by
     rw [sub_zero, pow_two]; exact Ideal.mul_mem_mul hx hy
   · intro x y hx hy; exact add_mem hx hy
 
-theorem to_quotient_square_range :
+lemma mk_mem_cotangentIdeal {I : Ideal R} {x : R} :
+    Quotient.mk (I ^ 2) x ∈ I.cotangentIdeal ↔ x ∈ I := by
+  refine ⟨fun ⟨y, hy, e⟩ ↦ ?_,  fun h ↦ ⟨x, h, rfl⟩⟩
+  simpa using sub_mem hy (Ideal.pow_le_self two_ne_zero
+    ((Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mp e))
+
+lemma comap_cotangentIdeal (I : Ideal R) :
+    I.cotangentIdeal.comap (Quotient.mk (I ^ 2)) = I :=
+  Ideal.ext fun _ ↦ mk_mem_cotangentIdeal
+
+theorem range_cotangentToQuotientSquare :
     LinearMap.range I.cotangentToQuotientSquare = I.cotangentIdeal.restrictScalars R := by
   trans LinearMap.range (I.cotangentToQuotientSquare.comp I.toCotangent)
   · rw [LinearMap.range_comp, I.toCotangent_range, Submodule.map_top]
   · rw [to_quotient_square_comp_toCotangent, LinearMap.range_comp, I.range_subtype]; ext; rfl
 
+@[deprecated (since := "2025-01-04")]
+alias to_quotient_square_range := range_cotangentToQuotientSquare
+
 /-- The equivalence of the two definitions of `I / I ^ 2`, either as the quotient of `I` or the
 ideal of `R / I ^ 2`. -/
 noncomputable def cotangentEquivIdeal : I.Cotangent ≃ₗ[R] I.cotangentIdeal := by
   refine
   { LinearMap.codRestrict (I.cotangentIdeal.restrictScalars R) I.cotangentToQuotientSquare
-      fun x => by { rw [← to_quotient_square_range]; exact LinearMap.mem_range_self _ _ },
+      fun x => by rw [← range_cotangentToQuotientSquare]; exact LinearMap.mem_range_self _ _,
     Equiv.ofBijective _ ⟨?_, ?_⟩ with }
   · rintro x y e
     replace e := congr_arg Subtype.val e

Mathlib/RingTheory/Kaehler/CotangentComplex.lean

@@ -350,6 +350,23 @@ lemma H1Cotangent.map_comp
     map (g.comp f) = (map g).restrictScalars S ∘ₗ map f := by
   ext; simp [Cotangent.map_comp]
 
+/-- Maps `P₁ → P₂` and `P₂ → P₁` between extensions
+induce an isomorphism between `H¹(L_P₁)` and `H¹(L_P₂)`. -/
+@[simps! apply]
+noncomputable
+def H1Cotangent.equiv {P₁ P₂ : Extension R S} (f₁ : P₁.Hom P₂) (f₂ : P₂.Hom P₁) :
+    P₁.H1Cotangent ≃ₗ[S] P₂.H1Cotangent where
+  __ := map f₁
+  invFun := map f₂
+  left_inv x :=
+    show (map f₂ ∘ₗ map f₁) x = LinearMap.id x by
+    rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ (f₂.comp f₁),
+      Extension.H1Cotangent.map_comp]; rfl
+  right_inv x :=
+    show (map f₁ ∘ₗ map f₂) x = LinearMap.id x by
+    rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ (f₁.comp f₂),
+      Extension.H1Cotangent.map_comp]; rfl
+
 end Extension
 
 namespace Generators
@@ -423,19 +440,9 @@ open Extension.H1Cotangent in
 @[simps! apply]
 noncomputable
 def Generators.H1Cotangent.equiv (P : Generators R S) (P' : Generators R S) :
-    P.toExtension.H1Cotangent ≃ₗ[S] P'.toExtension.H1Cotangent where
-  __ := map (Generators.defaultHom P P').toExtensionHom
-  invFun := map (Generators.defaultHom P' P).toExtensionHom
-  left_inv x :=
-    show ((map (defaultHom P' P).toExtensionHom) ∘ₗ
-      (map (defaultHom P P').toExtensionHom)) x = LinearMap.id x by
-    rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ ((defaultHom P' P).toExtensionHom.comp
-      (defaultHom P P').toExtensionHom), Extension.H1Cotangent.map_comp]; rfl
-  right_inv x :=
-    show ((map (defaultHom P P').toExtensionHom) ∘ₗ
-      (map (defaultHom P' P).toExtensionHom)) x = LinearMap.id x by
-    rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ ((defaultHom P P').toExtensionHom.comp
-      (defaultHom P' P).toExtensionHom), Extension.H1Cotangent.map_comp]; rfl
+    P.toExtension.H1Cotangent ≃ₗ[S] P'.toExtension.H1Cotangent :=
+  Extension.H1Cotangent.equiv
+    (Generators.defaultHom P P').toExtensionHom (Generators.defaultHom P' P).toExtensionHom
 
 variable {S' : Type*} [CommRing S'] [Algebra R S']
 variable {T : Type w} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]

Mathlib/RingTheory/Smooth/Kaehler.lean

@@ -31,6 +31,8 @@ import Mathlib.Tactic.StacksAttribute
   then `S` is formally smooth iff `Ω[S/R]` is projective and `I/I² → S ⊗[P] Ω[P⁄R]` is injective.
 - `Algebra.FormallySmooth.iff_subsingleton_and_projective`:
   An algebra is formally smooth if and only if `H¹(L_{R/S}) = 0` and `Ω_{S/R}` is projective.
+- `Algebra.Extension.equivH1CotangentOfFormallySmooth`:
+  Any formally smooth extension can be used to calculate `H¹(L_{S/R})`.
 
 ## Future projects
 
@@ -472,3 +474,99 @@ theorem Algebra.FormallySmooth.iff_subsingleton_and_projective :
 
 instance [Algebra.FormallySmooth R S] : Subsingleton (Algebra.H1Cotangent R S) :=
   (Algebra.FormallySmooth.iff_subsingleton_and_projective.mp ‹_›).1
+
+namespace Algebra.Extension
+
+lemma CotangentSpace.map_toInfinitesimal_bijective (P : Extension.{u} R S) :
+    Function.Bijective (CotangentSpace.map P.toInfinitesimal) := by
+  suffices CotangentSpace.map P.toInfinitesimal =
+      (tensorKaehlerQuotKerSqEquiv _ _ _).symm.toLinearMap by
+    rw [this]; exact(tensorKaehlerQuotKerSqEquiv _ _ _).symm.bijective
+  letI : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ _))
+  have : IsScalarTower P.Ring P.infinitesimal.Ring S := .of_algebraMap_eq' rfl
+  apply LinearMap.restrictScalars_injective P.Ring
+  ext x a
+  dsimp
+  simp only [map_tmul, id.map_eq_id, RingHom.id_apply, Hom.toAlgHom_apply]
+  exact (tensorKaehlerQuotKerSqEquiv_symm_tmul_D _ _).symm
+
+lemma Cotangent.map_toInfinitesimal_bijective (P : Extension.{u} R S) :
+    Function.Bijective (Cotangent.map P.toInfinitesimal) := by
+  constructor
+  · rw [injective_iff_map_eq_zero]
+    intro x hx
+    obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
+    have hx : x.1 ∈ P.ker ^ 2 := by
+      apply_fun Cotangent.val at hx
+      simp only [map_mk, Hom.toAlgHom_apply, val_mk, val_zero, Ideal.toCotangent_eq_zero,
+        Extension.ker_infinitesimal] at hx
+      rw [Ideal.cotangentIdeal_square] at hx
+      simpa only [toInfinitesimal, Ideal.mem_bot, infinitesimal,
+        Ideal.Quotient.eq_zero_iff_mem] using hx
+    ext
+    simpa [Ideal.toCotangent_eq_zero]
+  · intro x
+    obtain ⟨⟨x, hx⟩, rfl⟩ := Cotangent.mk_surjective x
+    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
+    rw [ker_infinitesimal, Ideal.mk_mem_cotangentIdeal] at hx
+    exact ⟨.mk ⟨x, hx⟩, rfl⟩
+
+lemma H1Cotangent.map_toInfinitesimal_bijective (P : Extension.{u} R S) :
+    Function.Bijective (H1Cotangent.map P.toInfinitesimal) := by
+  constructor
+  · intro x y e
+    ext1
+    exact (Cotangent.map_toInfinitesimal_bijective P).1 (congr_arg Subtype.val e)
+  · intro ⟨x, hx⟩
+    obtain ⟨x, rfl⟩ := (Cotangent.map_toInfinitesimal_bijective P).2 x
+    refine ⟨⟨x, ?_⟩, rfl⟩
+    simpa [← CotangentSpace.map_cotangentComplex,
+      map_eq_zero_iff _ (CotangentSpace.map_toInfinitesimal_bijective P).injective] using hx
+
+/--
+Given extensions `0 → I₁ → P₁ → S → 0` and `0 → I₂ → P₂ → S → 0` with `P₁` formally smooth,
+this is an arbitrarily chosen map `P₁/I₁² → P₂/I₂²` of extensions.
+-/
+noncomputable
+def homInfinitesimal (P₁ P₂ : Extension R S) [FormallySmooth R P₁.Ring] :
+    P₁.infinitesimal.Hom P₂.infinitesimal :=
+  letI lift : P₁.Ring →ₐ[R] P₂.infinitesimal.Ring := FormallySmooth.liftOfSurjective
+    (IsScalarTower.toAlgHom R P₁.Ring S)
+    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring S)
+    P₂.infinitesimal.algebraMap_surjective
+    ⟨2, show P₂.infinitesimal.ker ^ 2 = ⊥ by
+      rw [ker_infinitesimal]; exact Ideal.cotangentIdeal_square _⟩
+  { toRingHom := (Ideal.Quotient.liftₐ (P₁.ker ^ 2) lift (by
+        show P₁.ker ^ 2 ≤ RingHom.ker lift
+        rw [pow_two, Ideal.mul_le]
+        have : ∀ r ∈ P₁.ker, lift r ∈ P₂.infinitesimal.ker :=
+          fun r hr ↦ (FormallySmooth.liftOfSurjective_apply _
+            (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring S) _ _ r).trans hr
+        intro r hr s hs
+        rw [RingHom.mem_ker, map_mul, ← Ideal.mem_bot, ← P₂.ker.cotangentIdeal_square,
+          ← ker_infinitesimal, pow_two]
+        exact Ideal.mul_mem_mul (this r hr) (this s hs))).toRingHom
+    toRingHom_algebraMap := by simp
+    algebraMap_toRingHom x := by
+      obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
+      exact FormallySmooth.liftOfSurjective_apply _
+            (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring S) _ _ x }
+
+/-- Formally smooth extensions have isomorphic `H¹(L_P)`. -/
+noncomputable
+def H1Cotangent.equivOfFormallySmooth (P₁ P₂ : Extension R S)
+    [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] :
+    P₁.H1Cotangent ≃ₗ[S] P₂.H1Cotangent :=
+  .ofBijective _ (H1Cotangent.map_toInfinitesimal_bijective P₁) ≪≫ₗ
+    H1Cotangent.equiv (Extension.homInfinitesimal _ _) (Extension.homInfinitesimal _ _)
+    ≪≫ₗ .symm (.ofBijective _ (H1Cotangent.map_toInfinitesimal_bijective P₂))
+
+/-- Any formally smooth extension can be used to calculate `H¹(L_{S/R})`. -/
+noncomputable
+def equivH1CotangentOfFormallySmooth (P : Extension R S) [FormallySmooth R P.Ring] :
+    P.H1Cotangent ≃ₗ[S] H1Cotangent R S :=
+  have : FormallySmooth R (Generators.self R S).toExtension.Ring :=
+    inferInstanceAs (FormallySmooth R (MvPolynomial _ _))
+  H1Cotangent.equivOfFormallySmooth _ _
+
+end Algebra.Extension