Mathlib Map

Theorems · Theorem · category theory

Module.Flat.iff_preservesFiniteLimits_tensorLeft

∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R),
  Module.Flat R ↑M ↔ CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft M)
Defined in
Mathlib.RingTheory.Flat.CategoryTheory
Cited by
1 results in Mathlib
Foundations
Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Module.Flat.iff_preservesFiniteLimits_tensorRight · cited by 0Flat.iff_preservesFiniteL…CommRing · cited by 17173CommRingCategoryTheory.ShortComplex · cited by 1850CategoryTheory.ShortCompl…ModuleCat · cited by 1429ModuleCatModuleCat.carrier · cited by 997ModuleCat.carrierCategoryTheory.ShortComplex.Exact · cited by 292ShortComplex.ExactModule.Flat · cited by 279Module.FlatCategoryTheory.ShortComplex.ShortExact · cited by 232ShortComplex.ShortExactCategoryTheory.ShortComplex.map · cited by 188ShortComplex.mapList.TFAE.out · cited by 177TFAE.outCategoryTheory.MonoidalCategory.tensorLeft · cited by 170MonoidalCategory.tensorLe…CategoryTheory.Limits.PreservesFiniteLimits · cited by 121Limits.PreservesFiniteLim…CategoryTheory.Limits.PreservesFiniteColimits · cited by 102Limits.PreservesFiniteCol…CategoryTheory.Functor.PreservesHomology · cited by 42Functor.PreservesHomologyCategoryTheory.Functor.exact_tfae · cited by 3Functor.exact_tfaeModule.Flat.iff_lTensor_preserves_shortComplex_exact · cited by 1Flat.iff_lTensor_preserve…Flat.iff_preservesFiniteLimit…CITED BYCITES

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.