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.

theorem ModuleCat.preservesFiniteLimits_tensorLeft_of_ringHomFlat {A B : Type u} [CommRing A] [CommRing B] {f : A →+* B} (hf : f.Flat) : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft ((restrictScalars f).obj (of B B)))

theorem ModuleCat.preservesFiniteLimits_extendScalars_of_flat {A B : Type u} [CommRing A] [CommRing B] {f : A →+* B} (hf : f.Flat) : CategoryTheory.Limits.PreservesFiniteLimits (extendScalars f)

theorem ModuleCat.reflectsIsomorphisms_extendScalars_of_faithfullyFlat {A B : Type u} [CommRing A] [CommRing B] {f : A →+* B} (hf : f.FaithfullyFlat) : (extendScalars f).ReflectsIsomorphisms

Extension of scalars along faithfully flat ring maps reflects isomorphisms.

def comonadicExtendScalars {A B : Type u} [CommRing A] [CommRing B] {f : A →+* B} (hf : f.FaithfullyFlat) : CategoryTheory.ComonadicLeftAdjoint (ModuleCat.extendScalars f)

Extension of scalars by a faithfully flat ring map is comonadic.

Equations

• comonadicExtendScalars hf = ⋯.mpr (CategoryTheory.Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms (ModuleCat.extendRestrictScalarsAdj f))