Descent

📁 Source: Mathlib/Algebra/Category/ModuleCat/Descent.lean

Statistics

Metric	Count
Definitions comonadicExtendScalars	1
Theorems preservesFiniteLimits_extendScalars_of_flat, preservesFiniteLimits_tensorLeft_of_ringHomFlat, reflectsIsomorphisms_extendScalars_of_faithfullyFlat	3
Total	4

ModuleCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesFiniteLimits_extendScalars_of_flat 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits ModuleCat CommRing.toRing moduleCategory extendScalars	—	preservesFiniteLimits_tensorLeft_of_ringHomFlat CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms instReflectsIsomorphismsRestrictScalars CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint instIsRightAdjointRestrictScalars
preservesFiniteLimits_tensorLeft_of_ringHomFlat 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits ModuleCat CommRing.toRing moduleCategory CategoryTheory.MonoidalCategory.tensorLeft monoidalCategory CategoryTheory.Functor.obj restrictScalars of Ring.toAddCommGroup Semiring.toModule Ring.toSemiring	—	Module.Flat.instPreservesFiniteLimitsModuleCatTensorLeftOfCarrier
reflectsIsomorphisms_extendScalars_of_faithfullyFlat 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms ModuleCat CommRing.toRing moduleCategory extendScalars	—	CategoryTheory.ConcreteCategory.isIso_iff_bijective instReflectsIsomorphismsForgetLinearMapIdCarrier Module.FaithfullyFlat.lTensor_bijective_iff_bijective

(root)

Definitions

Name	Category	Theorems
comonadicExtendScalars 📖	CompOp	—

---

← Back to Index