Documentation

Mathlib.CategoryTheory.Monad.Products

Algebras for the coproduct monad #

The functor Y ↦ X ⨿ Y forms a monad, whose category of monads is equivalent to the under category of X. Similarly, Y ↦ X ⨯ Y forms a comonad, whose category of comonads is equivalent to the over category of X.

TODO #

Show that Over.forget X : Over X ⥤ C is a comonadic left adjoint and Under.forget : Under X ⥤ C is a monadic right adjoint.

source
def CategoryTheory.prodComonad {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] :
Comonad C

X ⨯ - has a comonad structure. This is sometimes called the writer comonad.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.prodComonad_obj {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] (Y : C) :
    (prodComonad X).obj Y = (X ⨯ Y)
    source
    @[simp]
    theorem CategoryTheory.prodComonad_δ_app {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] (x✝ : C) :
    (prodComonad X).δ.app x✝ = Limits.prod.lift Limits.prod.fst (CategoryStruct.id (X ⨯ x✝))
    source
    @[simp]
    theorem CategoryTheory.prodComonad_map {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) :
    (prodComonad X).map g = Limits.prod.map (CategoryStruct.id X) g
    source
    @[simp]
    theorem CategoryTheory.prodComonad_ε_app {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] (x✝ : C) :
    (prodComonad X).ε.app x✝ = Limits.prod.snd
    source
    def CategoryTheory.coalgebraToOver {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] :
    Functor (prodComonad X).Coalgebra (Over X)

    The forward direction of the equivalence from coalgebras for the product comonad to the over category.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.coalgebraToOver_map {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] {X✝ Y✝ : (prodComonad X).Coalgebra} (f : X✝ ⟶ Y✝) :
      (coalgebraToOver X).map f = Over.homMk f.f ⋯
      source
      @[simp]
      theorem CategoryTheory.coalgebraToOver_obj {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] (A : (prodComonad X).Coalgebra) :
      (coalgebraToOver X).obj A = Over.mk (CategoryStruct.comp A.a Limits.prod.fst)
      source
      def CategoryTheory.overToCoalgebra {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] :
      Functor (Over X) (prodComonad X).Coalgebra

      The backward direction of the equivalence from coalgebras for the product comonad to the over category.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.overToCoalgebra_obj_a {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] (f : Over X) :
        ((overToCoalgebra X).obj f).a = Limits.prod.lift f.hom (CategoryStruct.id f.left)
        source
        @[simp]
        theorem CategoryTheory.overToCoalgebra_map_f {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] {X✝ Y✝ : Over X} (g : X✝ ⟶ Y✝) :
        ((overToCoalgebra X).map g).f = g.left
        source
        @[simp]
        theorem CategoryTheory.overToCoalgebra_obj_A {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] (f : Over X) :
        ((overToCoalgebra X).obj f).A = f.left
        source
        def CategoryTheory.coalgebraEquivOver {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] :
        (prodComonad X).Coalgebra ≌ Over X

        The equivalence from coalgebras for the product comonad to the over category.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.coalgebraEquivOver_counitIso {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] :
          (coalgebraEquivOver X).counitIso = NatIso.ofComponents (fun (f : Over X) => Over.isoMk (Iso.refl (((overToCoalgebra X).comp (coalgebraToOver X)).obj f).left) ⋯) ⋯
          source
          @[simp]
          theorem CategoryTheory.coalgebraEquivOver_unitIso {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] :
          (coalgebraEquivOver X).unitIso = NatIso.ofComponents (fun (A : (prodComonad X).Coalgebra) => Comonad.Coalgebra.isoMk (Iso.refl ((Functor.id (prodComonad X).Coalgebra).obj A).A) ⋯) ⋯
          source
          @[simp]
          theorem CategoryTheory.coalgebraEquivOver_functor {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] :
          (coalgebraEquivOver X).functor = coalgebraToOver X
          source
          @[simp]
          theorem CategoryTheory.coalgebraEquivOver_inverse {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] :
          (coalgebraEquivOver X).inverse = overToCoalgebra X
          source
          def CategoryTheory.coprodMonad {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] :
          Monad C

          X ⨿ - has a monad structure. This is sometimes called the either monad.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.coprodMonad_η_app {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] (x✝ : C) :
            (coprodMonad X).η.app x✝ = Limits.coprod.inr
            source
            @[simp]
            theorem CategoryTheory.coprodMonad_map {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) :
            (coprodMonad X).map g = Limits.coprod.map (CategoryStruct.id X) g
            source
            @[simp]
            theorem CategoryTheory.coprodMonad_μ_app {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] (x✝ : C) :
            (coprodMonad X).μ.app x✝ = Limits.coprod.desc Limits.coprod.inl (CategoryStruct.id (X ⨿ x✝))
            source
            @[simp]
            theorem CategoryTheory.coprodMonad_obj {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] (Y : C) :
            (coprodMonad X).obj Y = (X ⨿ Y)
            source
            def CategoryTheory.algebraToUnder {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] :
            Functor (coprodMonad X).Algebra (Under X)

            The forward direction of the equivalence from algebras for the coproduct monad to the under category.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.algebraToUnder_map {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] {X✝ Y✝ : (coprodMonad X).Algebra} (f : X✝ ⟶ Y✝) :
              (algebraToUnder X).map f = Under.homMk f.f ⋯
              source
              @[simp]
              theorem CategoryTheory.algebraToUnder_obj {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] (A : (coprodMonad X).Algebra) :
              (algebraToUnder X).obj A = Under.mk (CategoryStruct.comp Limits.coprod.inl A.a)
              source
              def CategoryTheory.underToAlgebra {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] :
              Functor (Under X) (coprodMonad X).Algebra

              The backward direction of the equivalence from algebras for the coproduct monad to the under category.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.underToAlgebra_obj_a {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] (f : Under X) :
                ((underToAlgebra X).obj f).a = Limits.coprod.desc f.hom (CategoryStruct.id f.right)
                source
                @[simp]
                theorem CategoryTheory.underToAlgebra_obj_A {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] (f : Under X) :
                ((underToAlgebra X).obj f).A = f.right
                source
                @[simp]
                theorem CategoryTheory.underToAlgebra_map_f {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] {X✝ Y✝ : Under X} (g : X✝ ⟶ Y✝) :
                ((underToAlgebra X).map g).f = g.right
                source
                def CategoryTheory.algebraEquivUnder {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] :
                (coprodMonad X).Algebra ≌ Under X

                The equivalence from algebras for the coproduct monad to the under category.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.algebraEquivUnder_functor {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] :
                  (algebraEquivUnder X).functor = algebraToUnder X
                  source
                  @[simp]
                  theorem CategoryTheory.algebraEquivUnder_inverse {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] :
                  (algebraEquivUnder X).inverse = underToAlgebra X
                  source
                  @[simp]
                  theorem CategoryTheory.algebraEquivUnder_counitIso {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] :
                  (algebraEquivUnder X).counitIso = NatIso.ofComponents (fun (f : Under X) => Under.isoMk (Iso.refl (((underToAlgebra X).comp (algebraToUnder X)).obj f).right) ⋯) ⋯
                  source
                  @[simp]
                  theorem CategoryTheory.algebraEquivUnder_unitIso {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] :
                  (algebraEquivUnder X).unitIso = NatIso.ofComponents (fun (A : (coprodMonad X).Algebra) => Monad.Algebra.isoMk (Iso.refl ((Functor.id (coprodMonad X).Algebra).obj A).A) ⋯) ⋯