Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(category_theory/monad/*): Add category of bundled (co)monads; pr…
…ove equivalence of monads with monoid objects (#3762) This PR constructs bundled monads, and proves the "usual" equivalence between the category of monads and the category of monoid objects in the endomorphism category. It also includes a definition of morphisms of unbundled monads, and proves some necessary small lemmas in the following two files: 1. `category_theory.functor_category` 2. `category_theory.monoidal.internal` Given any isomorphism in `Cat`, we construct a corresponding equivalence of categories in `Cat.equiv_of_iso`. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
- Loading branch information
Showing
5 changed files
with
337 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,112 @@ | ||
/- | ||
Copyright (c) 2020 Adam Topaz. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Adam Topaz | ||
-/ | ||
import category_theory.monad.basic | ||
import category_theory.eq_to_hom | ||
|
||
/-! | ||
# Bundled Monads | ||
We define bundled (co)monads as a structure consisting of a functor `func : C ⥤ C` endowed with | ||
a term of type `(co)monad func`. See `category_theory.monad.basic` for the definition. | ||
The type of bundled (co)monads on a category `C` is denoted `(Co)Monad C`. | ||
We also define morphisms of bundled (co)monads as morphisms of their underlying (co)monads | ||
in the sense of `category_theory.(co)monad_hom`. We construct a category instance on `(Co)Monad C`. | ||
-/ | ||
|
||
namespace category_theory | ||
open category | ||
|
||
universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation | ||
|
||
variables (C : Type u) [category.{v} C] | ||
|
||
/-- Bundled monads. -/ | ||
structure Monad := | ||
(func : C ⥤ C) | ||
(str : monad func . tactic.apply_instance) | ||
|
||
/-- Bundled comonads -/ | ||
structure Comonad := | ||
(func : C ⥤ C) | ||
(str : comonad func . tactic.apply_instance) | ||
|
||
namespace Monad | ||
|
||
/-- The initial monad. TODO: Prove it's initial. -/ | ||
def initial : Monad C := { func := 𝟭 _ } | ||
|
||
variable {C} | ||
|
||
instance : inhabited (Monad C) := ⟨initial C⟩ | ||
|
||
instance {M : Monad C} : monad M.func := M.str | ||
|
||
/-- Morphisms of bundled monads. -/ | ||
def hom (M N : Monad C) := monad_hom M.func N.func | ||
|
||
namespace hom | ||
instance {M : Monad C} : inhabited (hom M M) := ⟨monad_hom.id _⟩ | ||
end hom | ||
|
||
instance : category (Monad C) := | ||
{ hom := hom, | ||
id := λ _, monad_hom.id _, | ||
comp := λ _ _ _, monad_hom.comp } | ||
|
||
/-- The forgetful functor from `Monad C` to `C ⥤ C`. -/ | ||
def forget : Monad C ⥤ (C ⥤ C) := | ||
{ obj := func, | ||
map := λ _ _ f, f.to_nat_trans } | ||
|
||
@[simp] | ||
lemma comp_to_nat_trans {M N L : Monad C} (f : M ⟶ N) (g : N ⟶ L) : | ||
(f ≫ g).to_nat_trans = nat_trans.vcomp f.to_nat_trans g.to_nat_trans := rfl | ||
|
||
@[simp] lemma assoc_func_app {M : Monad C} {X : C} : | ||
M.func.map ((μ_ M.func).app X) ≫ (μ_ M.func).app X = | ||
(μ_ M.func).app (M.func.obj X) ≫ (μ_ M.func).app X := by apply monad.assoc | ||
|
||
end Monad | ||
|
||
namespace Comonad | ||
|
||
/-- The terminal comonad. TODO: Prove it's terminal. -/ | ||
def terminal : Comonad C := { func := 𝟭 _ } | ||
|
||
variable {C} | ||
|
||
instance : inhabited (Comonad C) := ⟨terminal C⟩ | ||
|
||
instance {M : Comonad C} : comonad M.func := M.str | ||
|
||
/-- Morphisms of bundled comonads. -/ | ||
def hom (M N : Comonad C) := comonad_hom M.func N.func | ||
|
||
namespace hom | ||
instance {M : Comonad C} : inhabited (hom M M) := ⟨comonad_hom.id _⟩ | ||
end hom | ||
|
||
instance : category (Comonad C) := | ||
{ hom := hom, | ||
id := λ _, comonad_hom.id _, | ||
comp := λ _ _ _, comonad_hom.comp } | ||
|
||
/-- The forgetful functor from `CoMonad C` to `C ⥤ C`. -/ | ||
def forget : Comonad C ⥤ (C ⥤ C) := | ||
{ obj := func, | ||
map := λ _ _ f, f.to_nat_trans } | ||
|
||
@[simp] | ||
lemma comp_to_nat_trans {M N L : Comonad C} (f : M ⟶ N) (g : N ⟶ L) : | ||
(f ≫ g).to_nat_trans = nat_trans.vcomp f.to_nat_trans g.to_nat_trans := rfl | ||
|
||
@[simp] lemma coassoc_func_app {M : Comonad C} {X : C} : | ||
(δ_ M.func).app X ≫ M.func.map ((δ_ M.func).app X) = | ||
(δ_ M.func).app X ≫ (δ_ M.func).app (M.func.obj X) := by apply comonad.coassoc | ||
|
||
end Comonad | ||
end category_theory |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,117 @@ | ||
/- | ||
Copyright (c) 2020 Adam Topaz. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Adam Topaz | ||
-/ | ||
import category_theory.monad.bundled | ||
import category_theory.monoidal.End | ||
import category_theory.monoidal.internal | ||
import category_theory.category.Cat | ||
|
||
/-! | ||
# The equivalence between `Monad C` and `Mon_ (C ⥤ C)`. | ||
A monad "is just" a monoid in the category of endofunctors. | ||
# Definitions/Theorems | ||
1. `to_Mon` associates a monoid object in `C ⥤ C` to any monad on `C`. | ||
2. `Monad_to_Mon` is the functorial version of `to_Mon`. | ||
3. `of_Mon` associates a monad on `C` to any monoid object in `C ⥤ C`. | ||
4. `Monad_Mon_equiv` is the equivalence between `Monad C` and `Mon_ (C ⥤ C)`. | ||
-/ | ||
|
||
namespace category_theory | ||
open category | ||
|
||
universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation | ||
variables {C : Type u} [category.{v} C] | ||
|
||
namespace Monad | ||
local attribute [instance, reducible] endofunctor_monoidal_category | ||
|
||
/-- To every `Monad C` we associated a monoid object in `C ⥤ C`.-/ | ||
@[simps] | ||
def to_Mon : Monad C → Mon_ (C ⥤ C) := λ M, | ||
{ X := M.func, | ||
one := η_ _, | ||
mul := μ_ _ } | ||
|
||
variable (C) | ||
/-- Passing from `Monad C` to `Mon_ (C ⥤ C)` is functorial. -/ | ||
@[simps] | ||
def Monad_to_Mon : Monad C ⥤ Mon_ (C ⥤ C) := | ||
{ obj := to_Mon, | ||
map := λ _ _ f, { hom := f.to_nat_trans } } | ||
variable {C} | ||
|
||
/-- To every monoid object in `C ⥤ C` we associate a `Monad C`. -/ | ||
@[simps] | ||
def of_Mon : Mon_ (C ⥤ C) → Monad C := λ M, | ||
{ func := M.X, | ||
str := | ||
{ η := M.one, | ||
μ := M.mul, | ||
assoc' := begin | ||
intro X, | ||
rw [←nat_trans.hcomp_id_app, ←nat_trans.comp_app], | ||
simp, | ||
end, | ||
left_unit' := begin | ||
intro X, | ||
rw [←nat_trans.id_hcomp_app, ←nat_trans.comp_app, M.mul_one], | ||
refl, | ||
end, | ||
right_unit' := begin | ||
intro X, | ||
rw [←nat_trans.hcomp_id_app, ←nat_trans.comp_app, M.one_mul], | ||
refl, | ||
end } } | ||
|
||
variable (C) | ||
/-- Passing from `Mon_ (C ⥤ C)` to `Monad C` is functorial. -/ | ||
@[simps] | ||
def Mon_to_Monad : Mon_ (C ⥤ C) ⥤ Monad C := | ||
{ obj := of_Mon, | ||
map := λ _ _ f, | ||
{ app_η' := begin | ||
intro X, | ||
erw [←nat_trans.comp_app, f.one_hom], | ||
refl, | ||
end, | ||
app_μ' := begin | ||
intro X, | ||
erw [←nat_trans.comp_app, f.mul_hom], | ||
finish, | ||
end, | ||
..f.hom } } | ||
variable {C} | ||
|
||
/-- Isomorphism of functors used in `Monad_Mon_equiv` -/ | ||
@[simps] | ||
def of_to_mon_end_iso : Mon_to_Monad C ⋙ Monad_to_Mon C ≅ 𝟭 _ := | ||
{ hom := { app := λ _, { hom := 𝟙 _ } }, | ||
inv := { app := λ _, { hom := 𝟙 _ } } } | ||
|
||
/-- Isomorphism of functors used in `Monad_Mon_equiv` -/ | ||
@[simps] | ||
def to_of_mon_end_iso : Monad_to_Mon C ⋙ Mon_to_Monad C ≅ 𝟭 _ := | ||
{ hom := { app := λ _, { app := λ _, 𝟙 _ } }, | ||
inv := { app := λ _, { app := λ _, 𝟙 _ } } } | ||
|
||
variable (C) | ||
/-- Oh, monads are just monoids in the category of endofunctors (equivalence of categories). -/ | ||
@[simps] | ||
def Monad_Mon_equiv : (Monad C) ≌ (Mon_ (C ⥤ C)) := | ||
{ functor := Monad_to_Mon _, | ||
inverse := Mon_to_Monad _, | ||
unit_iso := to_of_mon_end_iso.symm, | ||
counit_iso := of_to_mon_end_iso } | ||
|
||
-- Sanity check | ||
example (A : Monad C) {X : C} : ((Monad_Mon_equiv C).unit_iso.app A).hom.app X = 𝟙 _ := rfl | ||
|
||
end Monad | ||
end category_theory |