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} [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.prodComonad_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (Y : C) :
    (CategoryTheory.prodComonad X).obj Y = (X ⨯ Y)
    source
    @[simp]
    theorem CategoryTheory.prodComonad_δ_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
    ∀ (x : C), (CategoryTheory.prodComonad X).δ.app x = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (X ⨯ x))
    source
    @[simp]
    theorem CategoryTheory.prodComonad_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
    ∀ {x x_1 : C} (g : x ⟶ x_1), (CategoryTheory.prodComonad X).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] :
    ∀ (x : C), (CategoryTheory.prodComonad X).ε.app x = CategoryTheory.Limits.prod.snd
    source
    def CategoryTheory.coalgebraToOver {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
    CategoryTheory.Functor (CategoryTheory.prodComonad X).Coalgebra (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.coalgebraToOver_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
      ∀ {X_1 Y : (CategoryTheory.prodComonad X).Coalgebra} (f : X_1 ⟶ Y), (CategoryTheory.coalgebraToOver X).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.prodComonad X).Coalgebra) :
      (CategoryTheory.coalgebraToOver X).obj A = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp A.a CategoryTheory.Limits.prod.fst)
      source
      def CategoryTheory.overToCoalgebra {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
      CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (f : CategoryTheory.Over X) :
        ((CategoryTheory.overToCoalgebra X).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).map g).f = g.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).obj f).A = f.left
        source
        def CategoryTheory.coalgebraEquivOver {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :
        (CategoryTheory.prodComonad X).Coalgebra ≌ 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.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.overToCoalgebra X).comp (CategoryTheory.coalgebraToOver X)).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.prodComonad X).Coalgebra) => CategoryTheory.Comonad.Coalgebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.prodComonad X).Coalgebra).obj A).A) ⋯) ⋯
          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_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.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.coprodMonad_η_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
            ∀ (x : C), (CategoryTheory.coprodMonad X).η.app x = CategoryTheory.Limits.coprod.inr
            source
            @[simp]
            theorem CategoryTheory.coprodMonad_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
            ∀ {x x_1 : C} (g : x ⟶ x_1), (CategoryTheory.coprodMonad X).map g = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) g
            source
            @[simp]
            theorem CategoryTheory.coprodMonad_μ_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
            ∀ (x : C), (CategoryTheory.coprodMonad X).μ.app x = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.id (X ⨿ x))
            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).obj Y = (X ⨿ Y)
            source
            def CategoryTheory.algebraToUnder {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
            CategoryTheory.Functor (CategoryTheory.coprodMonad X).Algebra (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.algebraToUnder_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
              ∀ {X_1 Y : (CategoryTheory.coprodMonad X).Algebra} (f : X_1 ⟶ Y), (CategoryTheory.algebraToUnder X).map f = CategoryTheory.Under.homMk f.f ⋯
              source
              @[simp]
              theorem CategoryTheory.algebraToUnder_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (A : (CategoryTheory.coprodMonad X).Algebra) :
              (CategoryTheory.algebraToUnder X).obj A = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl A.a)
              source
              def CategoryTheory.underToAlgebra {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
              CategoryTheory.Functor (CategoryTheory.Under X) (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (f : CategoryTheory.Under X) :
                ((CategoryTheory.underToAlgebra X).obj f).a = CategoryTheory.Limits.coprod.desc f.hom (CategoryTheory.CategoryStruct.id 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).obj f).A = 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).map g).f = g.right
                source
                def CategoryTheory.algebraEquivUnder {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] :
                (CategoryTheory.coprodMonad X).Algebra ≌ 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
                  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_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_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.underToAlgebra X).comp (CategoryTheory.algebraToUnder X)).obj f).right) ⋯) ⋯
                  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.coprodMonad X).Algebra) => CategoryTheory.Monad.Algebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.coprodMonad X).Algebra).obj A).A) ⋯) ⋯