feat(Algebra/ModuleCat): descent data

Mathlib.lean

@@ -128,6 +128,7 @@ import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.Algebra.Category.ModuleCat.Biproducts
 import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
 import Mathlib.Algebra.Category.ModuleCat.Colimits
+import Mathlib.Algebra.Category.ModuleCat.Descent
 import Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
 import Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
 import Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
@@ -5275,6 +5276,7 @@ import Mathlib.RingTheory.Radical
 import Mathlib.RingTheory.ReesAlgebra
 import Mathlib.RingTheory.Regular.IsSMulRegular
 import Mathlib.RingTheory.Regular.RegularSequence
+import Mathlib.RingTheory.RingHom.FaithfullyFlat
 import Mathlib.RingTheory.RingHom.Finite
 import Mathlib.RingTheory.RingHom.FinitePresentation
 import Mathlib.RingTheory.RingHom.FiniteType

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -92,6 +92,12 @@ instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
     (restrictScalars.{v} f).PreservesMonomorphisms where
   preserves _ h := by rwa [mono_iff_injective] at h ⊢
 
+instance {R S : Type*} [Ring R] [Ring S] (f : R →+* S) :
+    (restrictScalars f).ReflectsIsomorphisms :=
+  have : (restrictScalars f ⋙ CategoryTheory.forget (ModuleCat R)).ReflectsIsomorphisms :=
+    inferInstanceAs (CategoryTheory.forget _).ReflectsIsomorphisms
+  reflectsIsomorphisms_of_comp _ (CategoryTheory.forget _)
+
 -- Porting note: this should be automatic
 -- TODO: this instance gives diamonds if `f : S →+* S`, see `PresheafOfModules.pushforward₀`.
 -- The correct solution is probably to define explicit maps between `M` and

Mathlib/Algebra/Category/ModuleCat/Descent.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2025 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson, Jack McKoen, Christian Merten, Joël Riou, Adam Topaz
+-/
+import Mathlib.Algebra.Category.ModuleCat.Abelian
+import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
+import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
+import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
+import Mathlib.CategoryTheory.Monad.Comonadicity
+import Mathlib.RingTheory.RingHom.FaithfullyFlat
+
+/-!
+# Faithfully flat descent for modules
+
+In this file we show that extension of scalars by a faithfully flat ring homomorphism is comonadic.
+Then the general theory of descent implies that the pseudofunctor to `Cat` given by extension
+of scalars has effective descent relative to faithfully flat maps (TODO).
+
+## Notes
+
+This contribution was created as part of the AIM workshop
+"Formalizing algebraic geometry" in June 2024.
+-/
+
+universe u
+
+noncomputable section
+
+open CategoryTheory Comonad ModuleCat Limits MonoidalCategory
+
+variable {A B : Type u} [CommRing A] [CommRing B] {f : A →+* B}
+
+instance (M : ModuleCat.{u} A) [Module.Flat A M] : PreservesFiniteLimits <| tensorLeft M := by
+  have h2 := (Functor.preservesFiniteColimits_iff_forall_exact_map_and_epi (tensorLeft M)).mp
+    (inferInstanceAs <| PreservesFiniteColimits (tensorLeft M))
+  rw [Functor.preservesFiniteLimits_iff_forall_exact_map_and_mono]
+  refine fun S hS ↦ ⟨(h2 S hS).1, ?_⟩
+  have := hS.mono_f
+  rw [ModuleCat.mono_iff_injective] at this ⊢
+  exact Module.Flat.lTensor_preserves_injective_linearMap _ this
+
+lemma ModuleCat.preservesFiniteLimits_tensorLeft_of_flat (hf : f.Flat) :
+    PreservesFiniteLimits <| tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := by
+  algebraize [f]
+  change PreservesFiniteLimits <| tensorLeft (ModuleCat.of A B)
+  infer_instance
+
+lemma ModuleCat.preservesFiniteLimits_extendScalars_of_flat (hf : f.Flat) :
+    PreservesFiniteLimits (extendScalars.{_, _, u} f) := by
+  have : PreservesFiniteLimits (extendScalars.{_, _, u} f ⋙ restrictScalars.{_, _, u} f) :=
+    ModuleCat.preservesFiniteLimits_tensorLeft_of_flat hf
+  exact preservesFiniteLimits_of_reflects_of_preserves (extendScalars f) (restrictScalars f)
+
+/-- Extension of scalars along faithfully flat ring maps reflects isomorphisms. -/
+lemma ModuleCat.reflectsIsomorphisms_extendScalars_of_faithfullyFlat
+    (hf : f.FaithfullyFlat) : (extendScalars.{_, _, u} f).ReflectsIsomorphisms := by
+  refine ⟨fun {M N} g h ↦ ?_⟩
+  algebraize [f]
+  rw [ConcreteCategory.isIso_iff_bijective] at h ⊢
+  replace h : Function.Bijective (LinearMap.lTensor B g.hom) := h
+  rwa [Module.FaithfullyFlat.lTensor_bijective_iff_bijective] at h
+
+/-- Extension of scalars by a faithfully flat ring map is comonadic. -/
+def comonadicExtendScalars (hf : f.FaithfullyFlat) :
+    ComonadicLeftAdjoint (extendScalars f) := by
+  have := preservesFiniteLimits_extendScalars_of_flat hf.flat
+  have := reflectsIsomorphisms_extendScalars_of_faithfullyFlat hf
+  convert Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms
+      (extendRestrictScalarsAdj f)
+  · exact ⟨inferInstance⟩
+  · exact ⟨inferInstance⟩

Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean

@@ -147,6 +147,11 @@ lemma preservesFiniteLimits_tfae : List.TFAE
 
   tfae_finish
 
+lemma preservesFiniteLimits_iff_forall_exact_map_and_mono :
+    PreservesFiniteLimits F ↔
+      ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f) :=
+  ((Functor.preservesFiniteLimits_tfae F).out 0 3).symm
+
 /--
 If a functor `F : C ⥤ D` preserves exact sequences on the right hand side (i.e.
 if `0 ⟶ A ⟶ B ⟶ C ⟶ 0` is exact then `F(A) ⟶ F(B) ⟶ F(C) ⟶ 0` is exact),
@@ -247,6 +252,11 @@ lemma exact_tfae : List.TFAE
 
   tfae_finish
 
+lemma preservesFiniteColimits_iff_forall_exact_map_and_epi :
+    PreservesFiniteColimits F ↔
+      ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g) :=
+  ((Functor.preservesFiniteColimits_tfae F).out 0 3).symm
+
 end
 
 end Functor

Mathlib/Algebra/Ring/Equiv.lean

@@ -454,6 +454,18 @@ theorem ofBijective_apply [NonUnitalRingHomClass F R S] (f : F) (hf : Function.B
     (x : R) : ofBijective f hf x = f x :=
   rfl
 
+@[simp]
+lemma ofBijective_symm_comp (f : R →ₙ+* S) (hf : Function.Bijective f) :
+    ((RingEquiv.ofBijective f hf).symm : _ →ₙ+* _).comp f = NonUnitalRingHom.id R := by
+  ext
+  exact (RingEquiv.ofBijective f hf).injective <| RingEquiv.apply_symm_apply ..
+
+@[simp]
+lemma comp_ofBijective_symm (f : R →ₙ+* S) (hf : Function.Bijective f) :
+    f.comp ((RingEquiv.ofBijective f hf).symm : _ →ₙ+* _) = NonUnitalRingHom.id S := by
+  ext
+  exact (RingEquiv.ofBijective f hf).symm.injective <| RingEquiv.apply_symm_apply ..
+
 /-- Product of a singleton family of (non-unital non-associative semi)rings is isomorphic
 to the only member of this family. -/
 @[simps! -fullyApplied]

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -83,7 +83,7 @@ theorem IsStableUnderBaseChange.pullback_fst_appTop
     Functor.op_map, Quiver.Hom.unop_op, AffineScheme.forgetToScheme_map, Scheme.Γ_map] at this
   rw [← this, CommRingCat.hom_comp, hP'.cancel_right_isIso, ← pushoutIsoUnopPullback_inl_hom,
     CommRingCat.hom_comp, hP'.cancel_right_isIso]
-  exact hP.pushout_inl _ hP' _ _ H
+  exact hP.pushout_inl hP' _ _ H
 
 @[deprecated (since := "2024-11-23")]
 alias IsStableUnderBaseChange.pullback_fst_app_top :=

Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean

@@ -374,6 +374,11 @@ lemma lTensor_surjective_iff_surjective [Module.FaithfullyFlat R M] :
   conv_rhs => rw [← lTensor_exact_iff_exact R M]
   simp
 
+@[simp]
+lemma lTensor_bijective_iff_bijective [Module.FaithfullyFlat R M] :
+    Function.Bijective (f.lTensor M) ↔ Function.Bijective f := by
+  simp [Function.Bijective]
+
 end
 
 end arbitrary_universe

Mathlib/RingTheory/LocalProperties/Basic.lean

@@ -355,6 +355,45 @@ lemma RingHom.OfLocalizationSpanTarget.ofIsLocalization
 
 section
 
+variable {Q : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop}
+
+lemma RingHom.OfLocalizationSpanTarget.and (hP : OfLocalizationSpanTarget P)
+    (hQ : OfLocalizationSpanTarget Q) :
+    OfLocalizationSpanTarget (fun f ↦ P f ∧ Q f) := by
+  introv R hs hf
+  exact ⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩
+
+lemma RingHom.OfLocalizationSpan.and (hP : OfLocalizationSpan P) (hQ : OfLocalizationSpan Q) :
+    OfLocalizationSpan (fun f ↦ P f ∧ Q f) := by
+  introv R hs hf
+  exact ⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩
+
+lemma RingHom.LocalizationAwayPreserves.and (hP : LocalizationAwayPreserves P)
+    (hQ : LocalizationAwayPreserves Q) :
+    LocalizationAwayPreserves (fun f ↦ P f ∧ Q f) := by
+  introv R h
+  exact ⟨hP f r R' S' h.1, hQ f r R' S' h.2⟩
+
+lemma RingHom.StableUnderCompositionWithLocalizationAwayTarget.and
+    (hP : StableUnderCompositionWithLocalizationAwayTarget P)
+    (hQ : StableUnderCompositionWithLocalizationAwayTarget Q) :
+    StableUnderCompositionWithLocalizationAwayTarget (fun f ↦ P f ∧ Q f) := by
+  introv R h hf
+  exact ⟨hP T s f hf.1, hQ T s f hf.2⟩
+
+lemma RingHom.PropertyIsLocal.and (hP : PropertyIsLocal P) (hQ : PropertyIsLocal Q) :
+    PropertyIsLocal (fun f ↦ P f ∧ Q f) where
+  localizationAwayPreserves := hP.localizationAwayPreserves.and hQ.localizationAwayPreserves
+  ofLocalizationSpanTarget := hP.ofLocalizationSpanTarget.and hQ.ofLocalizationSpanTarget
+  ofLocalizationSpan := hP.ofLocalizationSpan.and hQ.ofLocalizationSpan
+  StableUnderCompositionWithLocalizationAwayTarget :=
+    hP.StableUnderCompositionWithLocalizationAwayTarget.and
+    hQ.StableUnderCompositionWithLocalizationAwayTarget
+
+end
+
+section
+
 variable (hP : RingHom.IsStableUnderBaseChange @P)
 variable {R S Rᵣ Sᵣ : Type u} [CommRing R] [CommRing S] [CommRing Rᵣ] [CommRing Sᵣ] [Algebra R Rᵣ]
   [Algebra S Sᵣ]

Mathlib/RingTheory/RingHom/FaithfullyFlat.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2025 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten, Joël Riou
+-/
+import Mathlib.RingTheory.RingHom.Flat
+
+/-!
+# Faithfully flat ring maps
+
+A ring map `f : R →+* S` is faithfully flat if `S` is faithfully flat as an `R`-algebra. This is
+the same as being flat and a surjection on prime spectra.
+-/
+
+namespace RingHom
+
+variable {R S : Type*} [CommRing R] [CommRing S] {f : R →+* S}
+
+/-- A ring map `f : R →+* S` is faithfully flat if `S` is faithfully flat as an `R`-algebra. -/
+@[algebraize Module.FaithfullyFlat]
+def FaithfullyFlat {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) : Prop :=
+  letI : Algebra R S := f.toAlgebra
+  Module.FaithfullyFlat R S
+
+lemma faithfullyFlat_algebraMap_iff [Algebra R S] :
+    (algebraMap R S).FaithfullyFlat ↔ Module.FaithfullyFlat R S := by
+  simp only [RingHom.FaithfullyFlat]
+  congr!
+  exact Algebra.algebra_ext _ _ fun _ ↦ rfl
+
+namespace FaithfullyFlat
+
+lemma flat (hf : f.FaithfullyFlat) : f.Flat := by
+  algebraize [f]
+  exact inferInstanceAs <| Module.Flat R S
+
+lemma iff_flat_and_comap_surjective :
+    f.FaithfullyFlat ↔ f.Flat ∧ Function.Surjective f.specComap := by
+  algebraize [f]
+  show (algebraMap R S).FaithfullyFlat ↔ (algebraMap R S).Flat ∧
+    Function.Surjective (algebraMap R S).specComap
+  rw [RingHom.faithfullyFlat_algebraMap_iff, RingHom.flat_algebraMap_iff]
+  exact ⟨fun h ↦ ⟨inferInstance, PrimeSpectrum.specComap_surjective_of_faithfullyFlat⟩,
+    fun ⟨h, hf⟩ ↦ .of_specComap_surjective hf⟩
+
+lemma eq_and : @FaithfullyFlat =
+      fun R S (_ : CommRing R) (_ : CommRing S) f ↦ f.Flat ∧ Function.Surjective f.specComap := by
+  ext
+  rw [iff_flat_and_comap_surjective]
+
+lemma stableUnderComposition : StableUnderComposition FaithfullyFlat := by
+  rw [eq_and]
+  refine Flat.stableUnderComposition.and ?_
+  introv R hf hg
+  rw [PrimeSpectrum.specComap_comp]
+  exact hf.comp hg
+
+lemma of_bijective (hf : Function.Bijective f) : f.FaithfullyFlat := by
+  rw [iff_flat_and_comap_surjective]
+  refine ⟨.of_bijective hf, fun p ↦ ?_⟩
+  use ((RingEquiv.ofBijective f hf).symm : _ →+* _).specComap p
+  have : ((RingEquiv.ofBijective f hf).symm : _ →+* _).comp f = RingHom.id R := by
+    ext
+    exact (RingEquiv.ofBijective f hf).injective (by simp)
+  rw [← PrimeSpectrum.specComap_comp_apply, this, PrimeSpectrum.specComap_id]
+
+lemma respectsIso : RespectsIso FaithfullyFlat :=
+  stableUnderComposition.respectsIso (fun e ↦ .of_bijective e.bijective)
+
+lemma isStableUnderBaseChange : IsStableUnderBaseChange FaithfullyFlat := by
+  refine .mk respectsIso (fun R S T _ _ _ _ _ _ ↦ show (algebraMap _ _).FaithfullyFlat from ?_)
+  rw [faithfullyFlat_algebraMap_iff] at *
+  infer_instance
+
+end RingHom.FaithfullyFlat

Mathlib/RingTheory/RingHom/Finite.lean

@@ -41,7 +41,7 @@ theorem finite_respectsIso : RespectsIso @Finite := by
 lemma finite_containsIdentities : ContainsIdentities @Finite := Finite.id
 
 theorem finite_isStableUnderBaseChange : IsStableUnderBaseChange @Finite := by
-  refine IsStableUnderBaseChange.mk _ finite_respectsIso ?_
+  refine IsStableUnderBaseChange.mk finite_respectsIso ?_
   classical
   introv h
   replace h : Module.Finite R T := by

Mathlib/RingTheory/RingHom/Flat.lean

@@ -24,7 +24,7 @@ def RingHom.Flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+
   letI : Algebra R S := f.toAlgebra
   Module.Flat R S
 
-lemma flat_algebraMap_iff {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] :
+lemma RingHom.flat_algebraMap_iff {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] :
     (algebraMap R S).Flat ↔ Module.Flat R S := by
   simp only [RingHom.Flat]
   congr!
@@ -61,7 +61,7 @@ lemma respectsIso : RespectsIso Flat := by
   exact of_bijective e.bijective
 
 lemma isStableUnderBaseChange : IsStableUnderBaseChange Flat := by
-  apply IsStableUnderBaseChange.mk _ respectsIso
+  apply IsStableUnderBaseChange.mk respectsIso
   introv h
   replace h : Module.Flat R T := by
     rw [RingHom.Flat] at h; convert h; ext; simp_rw [Algebra.smul_def]; rfl

Mathlib/RingTheory/RingHom/Integral.lean

@@ -29,7 +29,7 @@ theorem isIntegral_respectsIso : RespectsIso fun f => f.IsIntegral := by
   apply RingHom.isIntegralElem_map
 
 theorem isIntegral_isStableUnderBaseChange : IsStableUnderBaseChange fun f => f.IsIntegral := by
-  refine IsStableUnderBaseChange.mk _ isIntegral_respectsIso ?_
+  refine IsStableUnderBaseChange.mk isIntegral_respectsIso ?_
   introv h x
   refine TensorProduct.induction_on x ?_ ?_ ?_
   · apply isIntegral_zero

Mathlib/RingTheory/RingHom/Locally.lean

@@ -272,7 +272,7 @@ attribute [local instance] Algebra.TensorProduct.rightAlgebra in
 /-- If `P` is stable under base change, then so is `Locally P`. -/
 lemma locally_isStableUnderBaseChange (hPi : RespectsIso P) (hPb : IsStableUnderBaseChange P) :
     IsStableUnderBaseChange (Locally P) := by
-  apply IsStableUnderBaseChange.mk _ (locally_respectsIso hPi)
+  apply IsStableUnderBaseChange.mk (locally_respectsIso hPi)
   introv hf
   obtain ⟨s, hsone, hs⟩ := hf
   rw [locally_iff_exists hPi]

Mathlib/RingTheory/RingHom/Surjective.lean

@@ -42,7 +42,7 @@ theorem surjective_respectsIso : RespectsIso surjective := by
   exact e.surjective
 
 theorem surjective_isStableUnderBaseChange : IsStableUnderBaseChange surjective := by
-  refine IsStableUnderBaseChange.mk _ surjective_respectsIso ?_
+  refine IsStableUnderBaseChange.mk surjective_respectsIso ?_
   classical
   introv h x
   induction x with

Mathlib/RingTheory/RingHom/Unramified.lean

@@ -48,7 +48,7 @@ lemma respectsIso :
 
 lemma isStableUnderBaseChange :
     IsStableUnderBaseChange FormallyUnramified := by
-  refine .mk _ respectsIso ?_
+  refine .mk respectsIso ?_
   intros R S T _ _ _ _ _ h
   show (algebraMap _ _).FormallyUnramified
   rw [formallyUnramified_algebraMap] at h ⊢