diff --git a/Mathlib.lean b/Mathlib.lean
index 7da2ef28a9dbbf..aef15fa9894685 100644
--- a/Mathlib.lean
+++ b/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
diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
index d0bf4dd5bae4ab..a8e53362943179 100644
--- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
+++ b/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
diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean
new file mode 100644
index 00000000000000..67a4dae1dd40dd
--- /dev/null
+++ b/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⟩
diff --git a/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean b/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean
index 06141d6538e482..8c7c167112388c 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean
+++ b/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
diff --git a/Mathlib/Algebra/Ring/Equiv.lean b/Mathlib/Algebra/Ring/Equiv.lean
index cab85052362661..ac7fd9b16fda86 100644
--- a/Mathlib/Algebra/Ring/Equiv.lean
+++ b/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]
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
index 0cb356bd847ca4..e0585bd799331b 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
+++ b/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 :=
diff --git a/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean b/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
index 74a56aadc38d4c..966c677be6ed26 100644
--- a/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
+++ b/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
diff --git a/Mathlib/RingTheory/LocalProperties/Basic.lean b/Mathlib/RingTheory/LocalProperties/Basic.lean
index 6cfd1fc4831360..b0749f7956f8d8 100644
--- a/Mathlib/RingTheory/LocalProperties/Basic.lean
+++ b/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ᵣ]
diff --git a/Mathlib/RingTheory/RingHom/FaithfullyFlat.lean b/Mathlib/RingTheory/RingHom/FaithfullyFlat.lean
new file mode 100644
index 00000000000000..6340f943b3a559
--- /dev/null
+++ b/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
diff --git a/Mathlib/RingTheory/RingHom/Finite.lean b/Mathlib/RingTheory/RingHom/Finite.lean
index 3286a56d35bb24..c47a16a49c844b 100644
--- a/Mathlib/RingTheory/RingHom/Finite.lean
+++ b/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
diff --git a/Mathlib/RingTheory/RingHom/Flat.lean b/Mathlib/RingTheory/RingHom/Flat.lean
index ae742aa4674fc8..b4f888074c9b2a 100644
--- a/Mathlib/RingTheory/RingHom/Flat.lean
+++ b/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
diff --git a/Mathlib/RingTheory/RingHom/Integral.lean b/Mathlib/RingTheory/RingHom/Integral.lean
index a938ac44a00cbf..0822781dc03f4c 100644
--- a/Mathlib/RingTheory/RingHom/Integral.lean
+++ b/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
diff --git a/Mathlib/RingTheory/RingHom/Locally.lean b/Mathlib/RingTheory/RingHom/Locally.lean
index f84f17bcf4d46f..f1edbe094e293a 100644
--- a/Mathlib/RingTheory/RingHom/Locally.lean
+++ b/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]
diff --git a/Mathlib/RingTheory/RingHom/Surjective.lean b/Mathlib/RingTheory/RingHom/Surjective.lean
index f81c8c1d9032bd..6158b94c50ed03 100644
--- a/Mathlib/RingTheory/RingHom/Surjective.lean
+++ b/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
diff --git a/Mathlib/RingTheory/RingHom/Unramified.lean b/Mathlib/RingTheory/RingHom/Unramified.lean
index 1016996901edb0..5f0952a47462eb 100644
--- a/Mathlib/RingTheory/RingHom/Unramified.lean
+++ b/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 ⊢
diff --git a/Mathlib/RingTheory/RingHomProperties.lean b/Mathlib/RingTheory/RingHomProperties.lean
index dc7809bdc84400..ae7717b5ea7daa 100644
--- a/Mathlib/RingTheory/RingHomProperties.lean
+++ b/Mathlib/RingTheory/RingHomProperties.lean
@@ -30,10 +30,11 @@ open CategoryTheory Opposite CategoryTheory.Limits
 
 namespace RingHom
 
-variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S), Prop)
+variable {P Q : ∀ {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S), Prop}
 
 section RespectsIso
 
+variable (P) in
 /-- A property `RespectsIso` if it still holds when composed with an isomorphism -/
 def RespectsIso : Prop :=
   (∀ {R S T : Type u} [CommRing R] [CommRing S] [CommRing T],
@@ -41,8 +42,6 @@ def RespectsIso : Prop :=
     ∀ {R S T : Type u} [CommRing R] [CommRing S] [CommRing T],
       ∀ (f : S →+* T) (e : R ≃+* S) (_ : P f), P (f.comp e.toRingHom)
 
-variable {P}
-
 theorem RespectsIso.cancel_left_isIso (hP : RespectsIso @P) {R S T : CommRingCat} (f : R ⟶ S)
     (g : S ⟶ T) [IsIso f] : P (g.hom.comp f.hom) ↔ P g.hom :=
   ⟨fun H => by
@@ -87,18 +86,25 @@ theorem RespectsIso.isLocalization_away_iff (hP : RingHom.RespectsIso @P) {R S :
 @[deprecated (since := "2025-03-01")]
 alias RespectsIso.is_localization_away_iff := RespectsIso.isLocalization_away_iff
 
+lemma RespectsIso.and (hP : RespectsIso P) (hQ : RespectsIso Q) :
+    RespectsIso (fun f ↦ P f ∧ Q f) := by
+  refine ⟨?_, ?_⟩
+  · introv hf
+    exact ⟨hP.1 f e hf.1, hQ.1 f e hf.2⟩
+  · introv hf
+    exact ⟨hP.2 f e hf.1, hQ.2 f e hf.2⟩
+
 end RespectsIso
 
 section StableUnderComposition
 
+variable (P) in
 /-- A property is `StableUnderComposition` if the composition of two such morphisms
 still falls in the class. -/
 def StableUnderComposition : Prop :=
   ∀ ⦃R S T⦄ [CommRing R] [CommRing S] [CommRing T],
     ∀ (f : R →+* S) (g : S →+* T) (_ : P f) (_ : P g), P (g.comp f)
 
-variable {P}
-
 theorem StableUnderComposition.respectsIso (hP : RingHom.StableUnderComposition @P)
     (hP' : ∀ {R S : Type u} [CommRing R] [CommRing S] (e : R ≃+* S), P e.toRingHom) :
     RingHom.RespectsIso @P := by
@@ -110,10 +116,16 @@ theorem StableUnderComposition.respectsIso (hP : RingHom.StableUnderComposition
     apply hP
     exacts [hP' e, H]
 
+lemma StableUnderComposition.and (hP : StableUnderComposition P) (hQ : StableUnderComposition Q) :
+    StableUnderComposition (fun f ↦ P f ∧ Q f) := by
+  introv R hf hg
+  exact ⟨hP f g hf.1 hg.1, hQ f g hf.2 hg.2⟩
+
 end StableUnderComposition
 
 section IsStableUnderBaseChange
 
+variable (P) in
 /-- A morphism property `P` is `IsStableUnderBaseChange` if `P(S →+* A)` implies
 `P(B →+* A ⊗[S] B)`. -/
 def IsStableUnderBaseChange : Prop :=
@@ -169,16 +181,21 @@ theorem IsStableUnderBaseChange.pushout_inl (hP : RingHom.IsStableUnderBaseChang
   apply hP R T S (TensorProduct R S T)
   exact H
 
+lemma IsStableUnderBaseChange.and (hP : IsStableUnderBaseChange P)
+    (hQ : IsStableUnderBaseChange Q) :
+    IsStableUnderBaseChange (fun f ↦ P f ∧ Q f) := by
+  introv R _ h
+  exact ⟨hP R S R' S' h.1, hQ R S R' S' h.2⟩
+
 end IsStableUnderBaseChange
 
 section ToMorphismProperty
 
+variable (P) in
 /-- The categorical `MorphismProperty` associated to a property of ring homs expressed
 non-categorical terms. -/
 def toMorphismProperty : MorphismProperty CommRingCat := fun _ _ f ↦ P f.hom
 
-variable {P}
-
 lemma toMorphismProperty_respectsIso_iff :
     RespectsIso P ↔ (toMorphismProperty P).RespectsIso := by
   refine ⟨fun h ↦ MorphismProperty.RespectsIso.mk _ ?_ ?_, fun h ↦ ⟨?_, ?_⟩⟩