diff --git a/Mathlib.lean b/Mathlib.lean
index 3f1f162bf242c1..94cdf2e57c76e2 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -151,6 +151,7 @@ public import Mathlib.Algebra.Category.ModuleCat.Basic
 public import Mathlib.Algebra.Category.ModuleCat.Biproducts
 public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
 public import Mathlib.Algebra.Category.ModuleCat.Colimits
+public import Mathlib.Algebra.Category.ModuleCat.Descent
 public import Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
 public import Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
 public import Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
index 4a77cd2fefb2ec..4f0faedb0d7f9d 100644
--- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -97,6 +97,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
diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean
new file mode 100644
index 00000000000000..43d8e542761853
--- /dev/null
+++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean
@@ -0,0 +1,65 @@
+/-
+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
+-/
+module
+
+public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
+public import Mathlib.CategoryTheory.Monad.Comonadicity
+public import Mathlib.RingTheory.Flat.CategoryTheory
+public 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.
+-/
+
+@[expose] public section
+
+universe u
+
+noncomputable section
+
+open CategoryTheory Comonad ModuleCat Limits MonoidalCategory
+
+variable {A B : Type u} [CommRing A] [CommRing B] {f : A →+* B}
+
+lemma ModuleCat.preservesFiniteLimits_tensorLeft_of_ringHomFlat (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_ringHomFlat 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⟩
diff --git a/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean b/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean
index 6d15b96a32d2ad..596dc52ac3bdb5 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean
+++ b/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean
@@ -147,6 +147,11 @@ lemma preservesFiniteLimits_tfae : List.TFAE
     (S.map F).exact_and_mono_f_iff_f_is_kernel |>.2 ⟨KernelFork.mapIsLimit _ hS.fIsKernel F⟩
   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 3 0
+
 /--
 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),
@@ -239,6 +244,11 @@ lemma exact_tfae : List.TFAE
   | ⟨h1, h2⟩, _, h => h.map F
   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 3 0
+
 end
 
 end Functor
diff --git a/Mathlib/RingTheory/Flat/CategoryTheory.lean b/Mathlib/RingTheory/Flat/CategoryTheory.lean
index ab9aed87114484..fb02cb5dded16f 100644
--- a/Mathlib/RingTheory/Flat/CategoryTheory.lean
+++ b/Mathlib/RingTheory/Flat/CategoryTheory.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.RingTheory.Flat.Basic
 public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
-public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
+public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
 
 /-!
 # Tensoring with a flat module is an exact functor
@@ -70,4 +70,16 @@ lemma iff_rTensor_preserves_shortComplex_exact :
         (ModuleCat.hom_ext (DFunLike.ext _ _ h.apply_apply_eq_zero)))
           (moduleCat_exact_iff_function_exact _ |>.2 h)⟩
 
+open Limits
+
+lemma iff_preservesFiniteLimits_tensorLeft :
+    Flat R M ↔ PreservesFiniteLimits (tensorLeft M) := by
+  rw [Module.Flat.iff_lTensor_preserves_shortComplex_exact,
+    ((Functor.exact_tfae <| tensorLeft M).out 1 3 :)]
+  simp [show PreservesFiniteColimits (tensorLeft M) from inferInstance]
+
+instance [Module.Flat R M] : PreservesFiniteLimits <| tensorLeft M := by
+  rw [← iff_preservesFiniteLimits_tensorLeft]
+  infer_instance
+
 end Module.Flat
diff --git a/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean b/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
index 9ffa4fc1303529..61116bb52e910e 100644
--- a/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
+++ b/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
@@ -394,6 +394,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