From 71628923b303930904ab7a5357b587f1915235cf Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Mon, 1 Dec 2025 19:59:43 +0100 Subject: [PATCH 1/5] descent --- Mathlib.lean | 1 + .../Category/ModuleCat/ChangeOfRings.lean | 6 ++ .../Algebra/Category/ModuleCat/Descent.lean | 72 +++++++++++++++++++ .../Homology/ShortComplex/ExactFunctor.lean | 10 +++ .../RingTheory/Flat/FaithfullyFlat/Basic.lean | 5 ++ 5 files changed, 94 insertions(+) create mode 100644 Mathlib/Algebra/Category/ModuleCat/Descent.lean diff --git a/Mathlib.lean b/Mathlib.lean index 32ce3b5f405e6c..5f3fbf6e6fc222 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -153,6 +153,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 cb898e4e7dc8ff..ae2846c15f924a 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..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 c41ef43328f08e..0600a49ebfd334 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 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), @@ -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 0 3).symm + end end Functor diff --git a/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean b/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean index 0c7940b45beca4..25b8eb85bb5409 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 From 798bc9aa00db342c3ad0c6affaa44177d00f1773 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Mon, 1 Dec 2025 20:11:03 +0100 Subject: [PATCH 2/5] module system --- Mathlib/Algebra/Category/ModuleCat/Descent.lean | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean index 67a4dae1dd40dd..e5560dcb00ee4b 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Descent.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean @@ -3,12 +3,14 @@ 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 +module + +public import Mathlib.Algebra.Category.ModuleCat.Abelian +public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings +public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed +public import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor +public import Mathlib.CategoryTheory.Monad.Comonadicity +public import Mathlib.RingTheory.RingHom.FaithfullyFlat /-! # Faithfully flat descent for modules @@ -23,6 +25,8 @@ This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024. -/ +@[expose] public section + universe u noncomputable section From 9342a274564209fdc211d2d138d63d15689568b1 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Mon, 8 Dec 2025 17:15:56 +0100 Subject: [PATCH 3/5] wip --- Mathlib/Algebra/Category/ModuleCat/Descent.lean | 15 +++++++++++++++ .../Homology/ShortComplex/ExactFunctor.lean | 4 ++-- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean index e5560dcb00ee4b..be0dbd0b03121f 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Descent.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean @@ -44,6 +44,21 @@ instance (M : ModuleCat.{u} A) [Module.Flat A M] : PreservesFiniteLimits <| tens rw [ModuleCat.mono_iff_injective] at this ⊢ exact Module.Flat.lTensor_preserves_injective_linearMap _ this +lemma foo (M : ModuleCat.{u} A) : Module.Flat A M ↔ PreservesFiniteLimits (tensorLeft M) := by + refine ⟨fun _ ↦ ?_, fun h ↦ ?_⟩ + · 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 + · constructor + intro P _ _ _ N hN + -- rw [← ModuleCat.mono_iff_injective] + sorry + + lemma ModuleCat.preservesFiniteLimits_tensorLeft_of_flat (hf : f.Flat) : PreservesFiniteLimits <| tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := by algebraize [f] diff --git a/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean b/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean index 0600a49ebfd334..96cd7c1a6d7ab5 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean @@ -150,7 +150,7 @@ lemma preservesFiniteLimits_tfae : List.TFAE 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 + (Functor.preservesFiniteLimits_tfae F).out 3 0 /-- If a functor `F : C ⥤ D` preserves exact sequences on the right-hand side (i.e. @@ -247,7 +247,7 @@ lemma exact_tfae : List.TFAE 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 + (Functor.preservesFiniteColimits_tfae F).out 3 0 end From 2a695fda3b2a6e5bba7151bc8006383ebd910b38 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Thu, 15 Jan 2026 21:46:29 +0100 Subject: [PATCH 4/5] review comments --- .../Algebra/Category/ModuleCat/Descent.lean | 28 +------------------ Mathlib/RingTheory/Flat/CategoryTheory.lean | 14 +++++++++- 2 files changed, 14 insertions(+), 28 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean index be0dbd0b03121f..043e92ac3e291e 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Descent.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean @@ -5,11 +5,9 @@ Authors: Dagur Asgeirsson, Jack McKoen, Christian Merten, Joël Riou, Adam Topaz -/ module -public import Mathlib.Algebra.Category.ModuleCat.Abelian public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings -public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed -public import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor public import Mathlib.CategoryTheory.Monad.Comonadicity +public import Mathlib.RingTheory.Flat.CategoryTheory public import Mathlib.RingTheory.RingHom.FaithfullyFlat /-! @@ -35,30 +33,6 @@ 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 foo (M : ModuleCat.{u} A) : Module.Flat A M ↔ PreservesFiniteLimits (tensorLeft M) := by - refine ⟨fun _ ↦ ?_, fun h ↦ ?_⟩ - · 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 - · constructor - intro P _ _ _ N hN - -- rw [← ModuleCat.mono_iff_injective] - sorry - - lemma ModuleCat.preservesFiniteLimits_tensorLeft_of_flat (hf : f.Flat) : PreservesFiniteLimits <| tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := by algebraize [f] diff --git a/Mathlib/RingTheory/Flat/CategoryTheory.lean b/Mathlib/RingTheory/Flat/CategoryTheory.lean index e59ebf3e4d4971..ec6ce5505291ce 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 From de46ae9ed3de33af7f9f862123516cb7cd9dc86f Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Mon, 19 Jan 2026 13:25:16 +0100 Subject: [PATCH 5/5] rename --- Mathlib/Algebra/Category/ModuleCat/Descent.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean index 043e92ac3e291e..43d8e542761853 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Descent.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean @@ -33,7 +33,7 @@ open CategoryTheory Comonad ModuleCat Limits MonoidalCategory variable {A B : Type u} [CommRing A] [CommRing B] {f : A →+* B} -lemma ModuleCat.preservesFiniteLimits_tensorLeft_of_flat (hf : f.Flat) : +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) @@ -42,7 +42,7 @@ lemma ModuleCat.preservesFiniteLimits_tensorLeft_of_flat (hf : f.Flat) : 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 + 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. -/