Documentation

Mathlib.CategoryTheory.Monad.Comonadicity

Comonadicity theorems #

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

F is a comonadic left adjoint if it has a right adjoint, and:

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

Tags #

Beck, comonadicity, descent

The "main pair" for a coalgebra (A, α) is the pair of morphisms (G α, η_GA). It is always a coreflexive pair, and will be used to construct the left adjoint to the comparison functor and show it is an equivalence.

Equations
  • =
instance CategoryTheory.Comonad.ComonadicityInternal.main_pair_F_cosplit {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) (A : adj.toComonad.Coalgebra) :
F.IsCosplitPair (G.map A.a) (adj.unit.app (G.obj A.A))

The "main pair" for a coalgebra (A, α) is the pair of morphisms (G α, η_GA). It is always a G-cosplit pair, and will be used to construct the right adjoint to the comparison functor and show it is an equivalence.

Equations
  • =
def CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.toPrefunctor.1 A.A))] :
C

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

Equations
Instances For

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def CategoryTheory.Comonad.ComonadicityInternal.rightAdjointComparison {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] :
      CategoryTheory.Functor adj.toComonad.Coalgebra C

      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 equalizers, we have an adjunction to the comparison functor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F G} [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (A : adj.toComonad.Coalgebra) :
          ((CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit.app A).f = (adj.homEquiv (CategoryTheory.Limits.equalizer (G.map A.a) (adj.unit.app (G.obj A.A))) A.A).symm (CategoryTheory.Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))
          @[simp]
          theorem CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] :
          def CategoryTheory.Comonad.ComonadicityInternal.counitFork {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] :
          CategoryTheory.Limits.Fork (F.map (G.map A.a)) (F.map (adj.unit.app (G.obj A.A)))

          This is a fork which is helpful for establishing comonadicity: the morphism from this fork to the Beck equalizer is the counit for the adjunction on the comparison functor.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] :
            @[simp]
            theorem CategoryTheory.Comonad.ComonadicityInternal.unitFork_π_app {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) (B : C) (X : CategoryTheory.Limits.WalkingParallelPair) :
            (CategoryTheory.Comonad.ComonadicityInternal.unitFork adj B).app X = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun (t : CategoryTheory.Limits.WalkingParallelPair) => X = t(B (CategoryTheory.Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))).obj X)) (fun (h : X = CategoryTheory.Limits.WalkingParallelPair.zero) => adj.unit.app B) (fun (h : X = CategoryTheory.Limits.WalkingParallelPair.one) => CategoryTheory.CategoryStruct.comp (adj.unit.app B) (adj.unit.app (G.obj (F.obj B)))) X
            def CategoryTheory.Comonad.ComonadicityInternal.unitFork {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) (B : C) :
            CategoryTheory.Limits.Fork (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))

            The fork which describes the unit of the adjunction: the morphism from this fork to the the equalizer of this pair is the unit.

            Equations
            Instances For

              The unit fork is a limit provided F coreflects it.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                instance CategoryTheory.Comonad.ComonadicityInternal.instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (B : C) :
                CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))
                Equations
                • =

                If F is comonadic, it creates limits of F-cosplit pairs. This is the "boring" direction of Beck's comonadicity theorem, the converse is given in comonadicOfCreatesFSplitEqualizers.

                Equations
                Instances For

                  Dual to Monad.HasCoequalizerOfIsSplitPair.

                  Instances

                    If f, g is an F-cosplit pair, then they have an equalizer.

                    Dual to Monad.PreservesColimitOfIsSplitPair.

                    Instances

                      Dual to Monad.ReflectsColimitOfIsSplitPair.

                      Instances

                        Dual to Monad.CreatesColimitOfIsSplitPair.

                        Instances

                          Dual to Monad.PreservesColimitOfIsReflexivePair.

                          Instances

                            Coreflexive (crude) comonadicity theorem. If F has a right adjoint, C has and F preserves coreflexive equalizers and F reflects isomorphisms, then F is comonadic.

                            Equations
                            Instances For