Documentation

Mathlib.CategoryTheory.Monad.Monadicity

Monadicity theorems #

We prove monadicity theorems which can establish a given functor is monadic. In particular, we show three versions of Beck's monadicity theorem, and the reflexive (crude) monadicity theorem:

G is a monadic right adjoint if it has a left adjoint, and:

This file has been adapted to Mathlib.CategoryTheory.Monad.Comonadicity. Please try to keep them in sync.

Tags #

Beck, monadicity, descent

instance CategoryTheory.Monad.MonadicityInternal.main_pair_reflexive {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) (A : adj.toMonad.Algebra) :
CategoryTheory.IsReflexivePair (F.map A.a) (adj.counit.app (F.obj A.A))

The "main pair" for an algebra (A, α) is the pair of morphisms (F α, ε_FA). It is always a reflexive pair, and will be used to construct the left adjoint to the comparison functor and show it is an equivalence.

instance CategoryTheory.Monad.MonadicityInternal.main_pair_G_split {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) (A : adj.toMonad.Algebra) :
G.IsSplitPair (F.map A.a) (adj.counit.app (F.obj A.A))

The "main pair" for an algebra (A, α) is the pair of morphisms (F α, ε_FA). It is always a G-split pair, and will be used to construct the left adjoint to the comparison functor and show it is an equivalence.

The object function for the left adjoint to the comparison functor.

Equations
Instances For

    We have a bijection of homsets which will be used to construct the left adjoint to the comparison functor.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison {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) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] :
      CategoryTheory.Functor adj.toMonad.Algebra D

      Construct the adjunction to the comparison functor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Provided we have the appropriate coequalizers, we have an adjunction to the comparison functor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit {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) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] :
          (CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).counit = { app := fun (Y : D) => (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))) Y).symm (adj.homEquiv (G.obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G.obj Y)), , naturality := }
          theorem CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux {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} [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (A : adj.toMonad.Algebra) :
          ((CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).unit.app A).f = (adj.homEquiv A.A (CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A)))) (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
          def CategoryTheory.Monad.MonadicityInternal.unitCofork {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} (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] :
          CategoryTheory.Limits.Cofork (G.map (F.map A.a)) (G.map (adj.counit.app (F.obj A.A)))

          This is a cofork which is helpful for establishing monadicity: the morphism from the Beck coequalizer to this cofork is the unit for the adjunction on the comparison functor.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Monad.MonadicityInternal.unitCofork_pt {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} (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] :
            (CategoryTheory.Monad.MonadicityInternal.unitCofork A).pt = G.obj (CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A)))
            @[simp]
            theorem CategoryTheory.Monad.MonadicityInternal.unitCofork_π {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} (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] :
            (CategoryTheory.Monad.MonadicityInternal.unitCofork A) = G.map (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
            def CategoryTheory.Monad.MonadicityInternal.counitCofork {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) (B : D) :
            CategoryTheory.Limits.Cofork (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B)))

            The cofork which describes the counit of the adjunction: the morphism from the coequalizer of this pair to this morphism is the counit.

            Equations
            Instances For

              The counit cofork is a colimit provided G reflects it.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                instance CategoryTheory.Monad.MonadicityInternal.instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA {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) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (B : D) :
                CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
                Instances

                  Reflexive (crude) monadicity theorem. If G has a right adjoint, D has and G preserves reflexive coequalizers and G reflects isomorphisms, then G is monadic.

                  Equations
                  Instances For