CategoryTheory

📁 Source: Mathlib/RingTheory/Flat/CategoryTheory.lean

Statistics

Metric	Count
Definitions	0
Theorems iff_lTensor_preserves_shortComplex_exact, iff_preservesFiniteLimits_tensorLeft, iff_rTensor_preserves_shortComplex_exact, instPreservesFiniteLimitsModuleCatTensorLeftOfCarrier, lTensor_shortComplex_exact, rTensor_shortComplex_exact	6
Total	6

Module.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_lTensor_preserves_shortComplex_exact 📖	mathematical	—	Module.Flat ModuleCat.carrier CommRing.toRing CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule CategoryTheory.ShortComplex.Exact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.map CategoryTheory.MonoidalCategory.tensorLeft ModuleCat.monoidalCategory CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.tensoringLeft_additive ModuleCat.instMonoidalPreadditive	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.tensoringLeft_additive ModuleCat.instMonoidalPreadditive lTensor_shortComplex_exact iff_lTensor_exact ModuleCat.hom_ext DFunLike.ext Function.Exact.apply_apply_eq_zero CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact
iff_preservesFiniteLimits_tensorLeft 📖	mathematical	—	Module.Flat ModuleCat.carrier CommRing.toRing CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule CategoryTheory.Limits.PreservesFiniteLimits ModuleCat ModuleCat.moduleCategory CategoryTheory.MonoidalCategory.tensorLeft ModuleCat.monoidalCategory	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.tensoringLeft_additive ModuleCat.instMonoidalPreadditive iff_lTensor_preserves_shortComplex_exact List.TFAE.out CategoryTheory.Functor.exact_tfae CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.instPreservesColimitsTensorLeft
iff_rTensor_preserves_shortComplex_exact 📖	mathematical	—	Module.Flat ModuleCat.carrier CommRing.toRing CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule CategoryTheory.ShortComplex.Exact ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.map CategoryTheory.MonoidalCategory.tensorRight ModuleCat.monoidalCategory CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.tensoringRight_additive ModuleCat.instMonoidalPreadditive	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.tensoringRight_additive ModuleCat.instMonoidalPreadditive rTensor_shortComplex_exact iff_rTensor_exact ModuleCat.hom_ext DFunLike.ext Function.Exact.apply_apply_eq_zero CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact
instPreservesFiniteLimitsModuleCatTensorLeftOfCarrier 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.MonoidalCategory.tensorLeft ModuleCat.monoidalCategory	—	iff_preservesFiniteLimits_tensorLeft
lTensor_shortComplex_exact 📖	mathematical	CategoryTheory.ShortComplex.Exact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive	CategoryTheory.ShortComplex.map CategoryTheory.MonoidalCategory.tensorLeft ModuleCat.monoidalCategory CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.tensoringLeft_additive ModuleCat.instMonoidalPreadditive	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.tensoringLeft_additive ModuleCat.instMonoidalPreadditive CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact lTensor_exact
rTensor_shortComplex_exact 📖	mathematical	CategoryTheory.ShortComplex.Exact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive	CategoryTheory.ShortComplex.map CategoryTheory.MonoidalCategory.tensorRight ModuleCat.monoidalCategory CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.tensoringRight_additive ModuleCat.instMonoidalPreadditive	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.tensoringRight_additive ModuleCat.instMonoidalPreadditive CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact rTensor_exact

---

← Back to Index