18 Category theory; homological algebra

DefinitionBeck's monadicity theorem#

Beck's monadicity theorem: if G has a left adjoint and creates coequalizers of G-split pairs, then it is monadic. This is the converse of createsGSplitCoequalizersOfMonadic.

CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers.{v₁, u₁, u₂} {C : Type u₁} {D : Type u₂}
  [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G)
  [CategoryTheory.Monad.CreatesColimitOfIsSplitPair G] : CategoryTheory.MonadicRightAdjoint G
Sources
MathlibCategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers
Uses 4
Statement usesAdjunction · Isomorphism · Monad · Small category

TheoremMitchell's embedding theorem#

The Freyd-Mitchell embedding theorem. See also FreydMitchell.functor for a functor which has the relevant instances.

CategoryTheory.Abelian.freyd_mitchell.{v, u} (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Abelian C] :
  ∃ R x F,
    F.Full ∧
      F.Faithful ∧
        CategoryTheory.Limits.PreservesFiniteLimits F ∧
          CategoryTheory.Limits.PreservesFiniteColimits F
Sources
MathlibCategoryTheory.Abelian.freyd_mitchell
Uses 8
Statement usesAbelian category · Finite set · Small category · The category of modules over a ring
Proof usesAdjunction · Isomorphism · Linear map · Yoneda embedding

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.