feat(category_theory/monad): monadic adjunctions (#1176)

* feat(category_theory/limits): equivalences create limits

* equivalence lemma

* feat(category_theory/monad): monadic adjunctions

* move file

* fix

* add @[simp]

* use right_adjoint_preserves_limits

* fix

* fix

* undo weird changes in topology files

* formatting

* do colimits too

* missing proofs

* convert monad to a typeclass decorating a functor

* changing name

* cleaning up

* oops

* minor

Author: kim-em

src/category_theory/adjunction/basic.lean

@@ -37,6 +37,11 @@ class is_right_adjoint (right : D ⥤ C) :=
 (left : C ⥤ D)
 (adj : left ⊣ right)
 
+def left_adjoint (R : D ⥤ C) [is_right_adjoint R] : C ⥤ D :=
+is_right_adjoint.left R
+def right_adjoint (L : C ⥤ D) [is_left_adjoint L] : D ⥤ C :=
+is_left_adjoint.right L
+
 namespace adjunction
 
 restate_axiom hom_equiv_unit'
@@ -113,6 +118,10 @@ by { rw [←assoc], dsimp, simp }
 
 end
 
+end adjunction
+
+namespace adjunction
+
 structure core_hom_equiv (F : C ⥤ D) (G : D ⥤ C) :=
 (hom_equiv : Π (X Y), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
 (hom_equiv_naturality_left_symm' : Π {X' X Y} (f : X' ⟶ X) (g : X ⟶ G.obj Y),

src/category_theory/adjunction/fully_faithful.lean

@@ -0,0 +1,70 @@
+-- Copyright (c) 2019 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import category_theory.adjunction.basic
+import category_theory.yoneda
+
+open category_theory
+
+namespace category_theory
+universes v₁ v₂ u₁ u₂
+
+open category
+open opposite
+
+variables {C : Type u₁} [𝒞 : category.{v₁} C]
+variables {D : Type u₂} [𝒟 : category.{v₂} D]
+include 𝒞 𝒟
+variables {L : C ⥤ D} {R : D ⥤ C} (h : L ⊣ R)
+
+-- Lemma 4.5.13 from Riehl
+-- Proof in https://stacks.math.columbia.edu/tag/0036
+-- or at https://math.stackexchange.com/a/2727177
+instance unit_is_iso_of_L_fully_faithful [full L] [faithful L] : is_iso (adjunction.unit h) :=
+@nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ (adjunction.unit h) $ λ X,
+@yoneda.is_iso _ _ _ _ ((adjunction.unit h).app X)
+{ inv := { app := λ Y f, L.preimage ((h.hom_equiv (unop Y) (L.obj X)).symm f) },
+  inv_hom_id' :=
+  begin
+    ext1, ext1, dsimp,
+    simp only [adjunction.hom_equiv_counit, preimage_comp, preimage_map, category.assoc],
+    rw ←h.unit_naturality,
+    simp,
+  end,
+  hom_inv_id' :=
+  begin
+    ext1, ext1, dsimp,
+    apply L.injectivity,
+    simp,
+  end }.
+
+instance counit_is_iso_of_R_fully_faithful [full R] [faithful R] : is_iso (adjunction.counit h) :=
+@nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ (adjunction.counit h) $ λ X,
+@is_iso_of_op _ _ _ _ _ $
+@coyoneda.is_iso _ _ _ _ ((adjunction.counit h).app X).op
+{ inv := { app := λ Y f, R.preimage ((h.hom_equiv (R.obj X) Y) f) },
+  inv_hom_id' :=
+  begin
+    ext1, ext1, dsimp,
+    simp only [adjunction.hom_equiv_unit, preimage_comp, preimage_map],
+    rw ←h.counit_naturality,
+    simp,
+  end,
+  hom_inv_id' :=
+  begin
+    ext1, ext1, dsimp,
+    apply R.injectivity,
+    simp,
+  end }
+
+-- TODO also prove the converses?
+-- def L_full_of_unit_is_iso [is_iso (adjunction.unit h)] : full L := sorry
+-- def L_faithful_of_unit_is_iso [is_iso (adjunction.unit h)] : faithful L := sorry
+-- def R_full_of_counit_is_iso [is_iso (adjunction.counit h)] : full R := sorry
+-- def R_faithful_of_counit_is_iso [is_iso (adjunction.counit h)] : faithful R := sorry
+
+-- TODO also do the statements from Riehl 4.5.13 for full and faithful separately?
+
+
+end category_theory

src/category_theory/monad/adjunction.lean

@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2019 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.monad.algebra
+import category_theory.adjunction.fully_faithful
+
+namespace category_theory
+open category
+
+universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+
+variables {C : Type u₁} [𝒞 : category.{v₁} C] {D : Type u₂} [𝒟 : category.{v₂} D]
+include 𝒞 𝒟
+variables (R : D ⥤ C)
+
+namespace adjunction
+
+instance monad (R : D ⥤ C) [is_right_adjoint R] : monad.{v₁} ((left_adjoint R) ⋙ R) :=
+let L := left_adjoint R in
+let h := (is_right_adjoint.adj R) in
+{ η := h.unit,
+  μ := whisker_right (whisker_left L h.counit) R,
+  assoc' := λ X, by { dsimp, erw [←R.map_comp, h.counit.naturality, R.map_comp], refl },
+  right_unit' := λ X, by { dsimp, rw [←R.map_comp], simp }, }
+
+@[simp] lemma monad_η_app [is_right_adjoint R] (X) : (η_ ((left_adjoint R) ⋙ R)).app X = (is_right_adjoint.adj R).unit.app X := rfl
+@[simp] lemma monad_μ_app [is_right_adjoint R] (X) : (μ_ ((left_adjoint R) ⋙ R)).app X = R.map ((is_right_adjoint.adj R).counit.app ((left_adjoint R).obj X)) := rfl
+
+end adjunction
+
+namespace monad
+
+def comparison [is_right_adjoint R] : D ⥤ algebra ((left_adjoint R) ⋙ R) :=
+let h := (is_right_adjoint.adj R) in
+{ obj := λ X,
+  { A := R.obj X,
+    a := R.map (h.counit.app X),
+    assoc' := by { dsimp, conv { to_rhs, erw [←R.map_comp, h.counit.naturality, R.map_comp], }, refl } },
+  map := λ X Y f,
+  { f := R.map f,
+    h' := begin dsimp, erw [←R.map_comp, h.counit.naturality, R.map_comp, functor.id_map], refl, end } }.
+
+@[simp] lemma comparison_map_f [is_right_adjoint R] {X Y} (f : X ⟶ Y) : ((comparison R).map f).f = R.map f := rfl
+@[simp] lemma comparison_obj_a [is_right_adjoint R] (X) : ((comparison R).obj X).a = R.map ((is_right_adjoint.adj R).counit.app X) := rfl
+
+def comparison_forget [is_right_adjoint R] : comparison R ⋙ forget ((left_adjoint R) ⋙ R) ≅ R :=
+{ hom := { app := λ X, 𝟙 _, },
+  inv := { app := λ X, 𝟙 _, } }
+
+end monad
+
+class reflective (R : D ⥤ C) extends is_right_adjoint R, full R, faithful R.
+
+instance μ_iso_of_reflective [reflective R] : is_iso (μ_ ((left_adjoint R) ⋙ R)) :=
+by { dsimp [adjunction.monad], apply_instance }
+
+class monadic_right_adjoint (R : D ⥤ C) extends is_right_adjoint R :=
+(eqv : is_equivalence (monad.comparison R))
+
+attribute [instance] monadic_right_adjoint.eqv
+
+-- PROJECT prove Beck's monadicity theorem, e.g. from Section 5.5 of Riehl
+
+namespace reflective
+
+lemma comparison_ess_surj_aux [reflective R] (X : monad.algebra ((left_adjoint R) ⋙ R)) :
+  ((is_right_adjoint.adj R).unit).app (R.obj ((left_adjoint R).obj (X.A))) = R.map ((left_adjoint R).map ((is_right_adjoint.adj R).unit.app X.A)) :=
+begin
+ -- both are left inverses to μ_X.
+ apply (cancel_mono ((μ_ ((left_adjoint R) ⋙ R)).app _)).1,
+ { dsimp, erw [adjunction.right_triangle_components, ←R.map_comp], simp, },
+ { apply is_iso.mono_of_iso _,
+   apply nat_iso.is_iso_app_of_is_iso }
+end
+
+instance [reflective R] (X : monad.algebra ((left_adjoint R) ⋙ R)) :
+  is_iso ((is_right_adjoint.adj R).unit.app X.A) :=
+let L := left_adjoint R in
+let h := (is_right_adjoint.adj R) in
+{ inv := X.a,
+  hom_inv_id' := X.unit,
+  inv_hom_id' :=
+  begin
+    dsimp,
+    erw [h.unit.naturality, comparison_ess_surj_aux,
+          ←R.map_comp, ←L.map_comp, X.unit, L.map_id, R.map_id],
+    refl
+  end }
+
+instance comparison_ess_surj [reflective R]: ess_surj (monad.comparison R) :=
+let L := left_adjoint R in
+let h := (is_right_adjoint.adj R) in
+{ obj_preimage := λ X, L.obj X.A,
+  iso' := λ X,
+  { hom :=
+    { f := (as_iso (h.unit.app X.A)).inv,
+      h' :=
+      begin
+        dsimp,
+        apply (cancel_epi (R.map (L.map ((h.unit).app (X.A))))).1,
+        rw [is_iso.hom_inv_id_assoc, ←category.assoc, ←R.map_comp,adjunction.left_triangle_components],
+        erw [functor.map_id, category.id_comp],
+        apply (cancel_epi ((h.unit).app (X.A))).1,
+        rw is_iso.hom_inv_id,
+        exact X.unit,
+      end },
+    inv :=
+    { f := (as_iso (h.unit.app X.A)).hom,
+      h' :=
+      begin
+        dsimp,
+        erw [←R.map_comp, adjunction.left_triangle_components, R.map_id],
+        apply (cancel_epi ((h.unit).app (X.A))).1,
+        conv { to_rhs, erw [←category.assoc, X.unit] },
+        erw [comp_id, id_comp],
+      end },
+    hom_inv_id' := by { ext, exact (as_iso (h.unit.app X.A)).inv_hom_id, },
+    inv_hom_id' := by { ext, exact (as_iso (h.unit.app X.A)).hom_inv_id, }, } }
+
+instance comparison_full [full R] [is_right_adjoint R] : full (monad.comparison R) :=
+{ preimage := λ X Y f, R.preimage f.f }
+instance comparison_faithful [faithful R] [is_right_adjoint R] : faithful (monad.comparison R) :=
+{ injectivity' := λ X Y f g w, by { have w' := (congr_arg monad.algebra.hom.f w), exact R.injectivity w' } }
+
+end reflective
+
+-- Proposition 5.3.3 of Riehl
+instance monadic_of_reflective [reflective R] : monadic_right_adjoint R :=
+{ eqv := equivalence.equivalence_of_fully_faithfully_ess_surj _ }
+
+end category_theory

src/category_theory/monad/algebra.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2019 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.monad.basic
+import category_theory.adjunction.basic
+
+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]
+include 𝒞
+
+namespace monad
+
+structure algebra (T : C ⥤ C) [monad.{v₁} T] : Type (max u₁ v₁) :=
+(A : C)
+(a : T.obj A ⟶ A)
+(unit' : (η_ T).app A ≫ a = 𝟙 A . obviously)
+(assoc' : ((μ_ T).app A ≫ a) = (T.map a ≫ a) . obviously)
+
+restate_axiom algebra.unit'
+restate_axiom algebra.assoc'
+
+namespace algebra
+variables {T : C ⥤ C} [monad.{v₁} T]
+
+structure hom (A B : algebra T) :=
+(f : A.A ⟶ B.A)
+(h' : T.map f ≫ B.a = A.a ≫ f . obviously)
+
+restate_axiom hom.h'
+attribute [simp] hom.h
+
+namespace hom
+@[extensionality] lemma ext {A B : algebra T} (f g : hom A B) (w : f.f = g.f) : f = g :=
+by { cases f, cases g, congr, assumption }
+
+def id (A : algebra T) : hom A A :=
+{ f := 𝟙 A.A }
+
+@[simp] lemma id_f (A : algebra T) : (id A).f = 𝟙 A.A := rfl
+
+def comp {P Q R : algebra T} (f : hom P Q) (g : hom Q R) : hom P R :=
+{ f := f.f ≫ g.f,
+  h' := by rw [functor.map_comp, category.assoc, g.h, ←category.assoc, f.h, category.assoc] }
+
+@[simp] lemma comp_f {P Q R : algebra T} (f : hom P Q) (g : hom Q R) : (comp f g).f = f.f ≫ g.f := rfl
+end hom
+
+instance EilenbergMoore : category (algebra T) :=
+{ hom := hom,
+  id := hom.id,
+  comp := @hom.comp _ _ _ _ }
+
+@[simp] lemma id_f (P : algebra T) : hom.f (𝟙 P) = 𝟙 P.A := rfl
+@[simp] lemma comp_f {P Q R : algebra T} (f : P ⟶ Q) (g : Q ⟶ R) : (f ≫ g).f = f.f ≫ g.f := rfl
+
+end algebra
+
+variables (T : C ⥤ C) [monad.{v₁} T]
+
+def forget : algebra T ⥤ C :=
+{ obj := λ A, A.A,
+  map := λ A B f, f.f }
+
+@[simp] lemma forget_map {X Y : algebra T} (f : X ⟶ Y) : (forget T).map f = f.f := rfl
+
+def free : C ⥤ algebra T :=
+{ obj := λ X,
+  { A := T.obj X,
+    a := (μ_ T).app X,
+    assoc' := (monad.assoc T _).symm },
+  map := λ X Y f,
+  { f := T.map f,
+    h' := by erw (μ_ T).naturality } }
+
+@[simp] lemma free_obj_a (X) : ((free T).obj X).a = (μ_ T).app X := rfl
+@[simp] lemma free_map_f {X Y : C} (f : X ⟶ Y) : ((free T).map f).f = T.map f := rfl
+
+def adj : free T ⊣ forget T :=
+adjunction.mk_of_hom_equiv
+{ hom_equiv := λ X Y,
+  { to_fun := λ f, (η_ T).app X ≫ f.f,
+    inv_fun := λ f,
+    { f := T.map f ≫ Y.a,
+      h' :=
+      begin
+        dsimp, simp,
+        conv { to_rhs, rw [←category.assoc, ←(μ_ T).naturality, category.assoc], erw algebra.assoc },
+        refl,
+      end },
+    left_inv := λ f,
+    begin
+      ext1, dsimp,
+      simp only [free_obj_a, functor.map_comp, algebra.hom.h, category.assoc],
+      erw [←category.assoc, monad.right_unit, id_comp],
+    end,
+    right_inv := λ f,
+    begin
+      dsimp,
+      erw [←category.assoc, ←(η_ T).naturality, functor.id_map,
+            category.assoc, Y.unit, comp_id],
+    end }}
+
+end monad
+
+end category_theory

src/category_theory/monad/basic.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2019 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.functor_category
+
+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]
+include 𝒞
+
+class monad (T : C ⥤ C) :=
+(η : functor.id _ ⟶ T)
+(μ : T ⋙ T ⟶ T)
+(assoc' : ∀ X : C, T.map (nat_trans.app μ X) ≫ μ.app _ = μ.app (T.obj X) ≫ μ.app _ . obviously)
+(left_unit' : ∀ X : C, η.app (T.obj X) ≫ μ.app _ = 𝟙 _  . obviously)
+(right_unit' : ∀ X : C, T.map (η.app X) ≫ μ.app _ = 𝟙 _  . obviously)
+
+restate_axiom monad.assoc'
+restate_axiom monad.left_unit'
+restate_axiom monad.right_unit'
+attribute [simp] monad.left_unit monad.right_unit
+
+notation `η_` := monad.η
+notation `μ_` := monad.μ
+
+end category_theory

src/category_theory/monad/default.lean

@@ -0,0 +1 @@
+import category_theory.monad.limits