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
@[simp]
theorem CategoryTheory.prodComonad_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] {Y : C} {Z : C} (g : Y ⟶ Z) :
(CategoryTheory.prodComonad X).toFunctor.toPrefunctor.map g = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) g
source
@[simp]
theorem CategoryTheory.prodComonad_δ_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (Y : C) :
(CategoryTheory.Comonad.δ (CategoryTheory.prodComonad X)).app Y = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (X ⨯ Y))
source
@[simp]
theorem CategoryTheory.prodComonad_ε_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (Y : C) :
(CategoryTheory.Comonad.ε (CategoryTheory.prodComonad X)).app Y = CategoryTheory.Limits.prod.snd
source
@[simp]
theorem CategoryTheory.prodComonad_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (Y : C) :
(CategoryTheory.prodComonad X).toFunctor.toPrefunctor.obj Y = (X ⨯ Y)
source
def CategoryTheory.prodComonad {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
CategoryTheory.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.coalgebraToOver_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
    ∀ {X_1 Y : CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X)} (f : X_1 ⟶ Y), (CategoryTheory.coalgebraToOver X).toPrefunctor.map f = CategoryTheory.Over.homMk f.f
    source
    @[simp]
    theorem CategoryTheory.coalgebraToOver_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (A : CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X)) :
    (CategoryTheory.coalgebraToOver X).toPrefunctor.obj A = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp A.a CategoryTheory.Limits.prod.fst)
    source
    def CategoryTheory.coalgebraToOver {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
    CategoryTheory.Functor (CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X)) (CategoryTheory.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.overToCoalgebra_obj_A {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (f : CategoryTheory.Over X) :
      ((CategoryTheory.overToCoalgebra X).toPrefunctor.obj f).A = f.left
      source
      @[simp]
      theorem CategoryTheory.overToCoalgebra_obj_a {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (f : CategoryTheory.Over X) :
      ((CategoryTheory.overToCoalgebra X).toPrefunctor.obj f).a = CategoryTheory.Limits.prod.lift f.hom (CategoryTheory.CategoryStruct.id f.left)
      source
      @[simp]
      theorem CategoryTheory.overToCoalgebra_map_f {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
      ∀ {X_1 Y : CategoryTheory.Over X} (g : X_1 ⟶ Y), ((CategoryTheory.overToCoalgebra X).toPrefunctor.map g).f = g.left
      source
      def CategoryTheory.overToCoalgebra {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
      CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X))

      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.coalgebraEquivOver_functor {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
        (CategoryTheory.coalgebraEquivOver X).functor = CategoryTheory.coalgebraToOver X
        source
        @[simp]
        theorem CategoryTheory.coalgebraEquivOver_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
        (CategoryTheory.coalgebraEquivOver X).counitIso = CategoryTheory.NatIso.ofComponents fun (f : CategoryTheory.Over X) => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.overToCoalgebra X) (CategoryTheory.coalgebraToOver X)).toPrefunctor.obj f).left)
        source
        @[simp]
        theorem CategoryTheory.coalgebraEquivOver_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
        (CategoryTheory.coalgebraEquivOver X).unitIso = CategoryTheory.NatIso.ofComponents fun (A : CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X)) => CategoryTheory.Comonad.Coalgebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X))).toPrefunctor.obj A).A)
        source
        @[simp]
        theorem CategoryTheory.coalgebraEquivOver_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
        (CategoryTheory.coalgebraEquivOver X).inverse = CategoryTheory.overToCoalgebra X
        source
        def CategoryTheory.coalgebraEquivOver {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
        CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X) ≌ CategoryTheory.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.coprodMonad_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (Y : C) :
          (CategoryTheory.coprodMonad X).toFunctor.toPrefunctor.obj Y = (X ⨿ Y)
          source
          @[simp]
          theorem CategoryTheory.coprodMonad_μ_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (Y : C) :
          (CategoryTheory.Monad.μ (CategoryTheory.coprodMonad X)).app Y = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.id (X ⨿ Y))
          source
          @[simp]
          theorem CategoryTheory.coprodMonad_η_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (Y : C) :
          (CategoryTheory.Monad.η (CategoryTheory.coprodMonad X)).app Y = CategoryTheory.Limits.coprod.inr
          source
          @[simp]
          theorem CategoryTheory.coprodMonad_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] {Y : C} {Z : C} (g : Y ⟶ Z) :
          (CategoryTheory.coprodMonad X).toFunctor.toPrefunctor.map g = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) g
          source
          def CategoryTheory.coprodMonad {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
          CategoryTheory.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.algebraToUnder_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (A : CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X)) :
            (CategoryTheory.algebraToUnder X).toPrefunctor.obj A = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl A.a)
            source
            @[simp]
            theorem CategoryTheory.algebraToUnder_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
            ∀ {X_1 Y : CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X)} (f : X_1 ⟶ Y), (CategoryTheory.algebraToUnder X).toPrefunctor.map f = CategoryTheory.Under.homMk f.f
            source
            def CategoryTheory.algebraToUnder {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
            CategoryTheory.Functor (CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X)) (CategoryTheory.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.underToAlgebra_obj_A {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (f : CategoryTheory.Under X) :
              ((CategoryTheory.underToAlgebra X).toPrefunctor.obj f).A = f.right
              source
              @[simp]
              theorem CategoryTheory.underToAlgebra_obj_a {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (f : CategoryTheory.Under X) :
              ((CategoryTheory.underToAlgebra X).toPrefunctor.obj f).a = CategoryTheory.Limits.coprod.desc f.hom (CategoryTheory.CategoryStruct.id f.right)
              source
              @[simp]
              theorem CategoryTheory.underToAlgebra_map_f {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
              ∀ {X_1 Y : CategoryTheory.Under X} (g : X_1 ⟶ Y), ((CategoryTheory.underToAlgebra X).toPrefunctor.map g).f = g.right
              source
              def CategoryTheory.underToAlgebra {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
              CategoryTheory.Functor (CategoryTheory.Under X) (CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X))

              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.algebraEquivUnder_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
                (CategoryTheory.algebraEquivUnder X).counitIso = CategoryTheory.NatIso.ofComponents fun (f : CategoryTheory.Under X) => CategoryTheory.Under.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.underToAlgebra X) (CategoryTheory.algebraToUnder X)).toPrefunctor.obj f).right)
                source
                @[simp]
                theorem CategoryTheory.algebraEquivUnder_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
                (CategoryTheory.algebraEquivUnder X).inverse = CategoryTheory.underToAlgebra X
                source
                @[simp]
                theorem CategoryTheory.algebraEquivUnder_functor {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
                (CategoryTheory.algebraEquivUnder X).functor = CategoryTheory.algebraToUnder X
                source
                @[simp]
                theorem CategoryTheory.algebraEquivUnder_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
                (CategoryTheory.algebraEquivUnder X).unitIso = CategoryTheory.NatIso.ofComponents fun (A : CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X)) => CategoryTheory.Monad.Algebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X))).toPrefunctor.obj A).A)
                source
                def CategoryTheory.algebraEquivUnder {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
                CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X) ≌ CategoryTheory.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