Documentation Verification Report

FreydMitchell

📁 Source: Mathlib/CategoryTheory/Abelian/FreydMitchell.lean

Statistics

Metric	Count
Definitions `EmbeddingRing`, `functor`, `instRingEmbeddingRing`	3
Theorems `instFaithfulModuleCatEmbeddingRingFunctor`, `instFullModuleCatEmbeddingRingFunctor`, `instNonemptyAsSmall`, `instPreservesFiniteColimitsModuleCatEmbeddingRingFunctor`, `instPreservesFiniteLimitsModuleCatEmbeddingRingFunctor`, `freyd_mitchell`	6
Total	9

CategoryTheory.Abelian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`freyd_mitchell` 📖	mathematical	—	`CategoryTheory.Functor.Full` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Functor.Faithful` `CategoryTheory.Limits.PreservesFiniteLimits` `CategoryTheory.Limits.PreservesFiniteColimits`	—	`FreydMitchell.instFullModuleCatEmbeddingRingFunctor` `FreydMitchell.instFaithfulModuleCatEmbeddingRingFunctor` `FreydMitchell.instPreservesFiniteLimitsModuleCatEmbeddingRingFunctor` `FreydMitchell.instPreservesFiniteColimitsModuleCatEmbeddingRingFunctor`

CategoryTheory.Abelian.FreydMitchell

Definitions

Name	Category	Theorems
`EmbeddingRing` 📖	CompOp	4 math math: `instFaithfulModuleCatEmbeddingRingFunctor`, `instPreservesFiniteLimitsModuleCatEmbeddingRingFunctor`, `instPreservesFiniteColimitsModuleCatEmbeddingRingFunctor`, `instFullModuleCatEmbeddingRingFunctor`
`functor` 📖	CompOp	4 math math: `instFaithfulModuleCatEmbeddingRingFunctor`, `instPreservesFiniteLimitsModuleCatEmbeddingRingFunctor`, `instPreservesFiniteColimitsModuleCatEmbeddingRingFunctor`, `instFullModuleCatEmbeddingRingFunctor`
`instRingEmbeddingRing` 📖	CompOp	4 math math: `instFaithfulModuleCatEmbeddingRingFunctor`, `instPreservesFiniteLimitsModuleCatEmbeddingRingFunctor`, `instPreservesFiniteColimitsModuleCatEmbeddingRingFunctor`, `instFullModuleCatEmbeddingRingFunctor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulModuleCatEmbeddingRingFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `ModuleCat` `EmbeddingRing` `instRingEmbeddingRing` `ModuleCat.moduleCategory` `functor`	—	`functor.eq_1` `CategoryTheory.Equivalence.faithful_functor` `CategoryTheory.Functor.rightOp_faithful` `CategoryTheory.instFaithfulIndYoneda` `CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.faithful_embedding` `instNonemptyAsSmall` `CategoryTheory.Functor.Faithful.comp`
`instFullModuleCatEmbeddingRingFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Full` `ModuleCat` `EmbeddingRing` `instRingEmbeddingRing` `ModuleCat.moduleCategory` `functor`	—	`functor.eq_1` `CategoryTheory.Equivalence.full_functor` `CategoryTheory.Functor.rightOp_full` `CategoryTheory.instFullIndYoneda` `CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding` `instNonemptyAsSmall` `CategoryTheory.Functor.Full.comp`
`instNonemptyAsSmall` 📖	mathematical	—	`CategoryTheory.AsSmall`	—	`CategoryTheory.Abelian.hasZeroObject`
`instPreservesFiniteColimitsModuleCatEmbeddingRingFunctor` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteColimits` `ModuleCat` `EmbeddingRing` `instRingEmbeddingRing` `ModuleCat.moduleCategory` `functor`	—	`functor.eq_1` `CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits` `CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.preservesFiniteColimits_rightOp` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.instPreservesLimitsIndYoneda` `CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteColimits_embedding` `CategoryTheory.Limits.comp_preservesFiniteColimits`
`instPreservesFiniteLimitsModuleCatEmbeddingRingFunctor` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `ModuleCat` `EmbeddingRing` `instRingEmbeddingRing` `ModuleCat.moduleCategory` `functor`	—	`functor.eq_1` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint` `CategoryTheory.Functor.isRightAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.preservesFiniteLimits_rightOp` `CategoryTheory.instPreservesFiniteColimitsIndYoneda` `CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteLimits_embedding` `CategoryTheory.Limits.comp_preservesFiniteLimits`

---

← Back to Index