Eilenberg-Moore adjunction (#772)

* Define IsMonad. * HomFunctor. * bind as a natural transformation. * Functor algebras (WIP). * Functor algebras. * Eilenberg-Moore category. * FreeEMAlgebra -| ForgetEMAlgebra. * Shorten long lines. * Fix long lines; remove comment. * Remove comment.
agda · May 3, 2022 · 5e558a7 · 5e558a7
1 parent 0be116c
commit 5e558a7
Show file tree

Hide file tree

Showing 2 changed files with 74 additions and 3 deletions.
diff --git a/Cubical/Categories/Constructions/FullSubcategory.agda b/Cubical/Categories/Constructions/FullSubcategory.agda
@@ -12,8 +12,6 @@ private
   variable
     ℓC ℓC' ℓP : Level
 
---open Category
-
 module _ (C : Category ℓC ℓC') (P : Category.ob C → Type ℓP) where
   private
     module C = Category C

diff --git a/Cubical/Categories/Instances/EilenbergMoore.agda b/Cubical/Categories/Instances/EilenbergMoore.agda
@@ -8,11 +8,12 @@ open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_)
 open import Cubical.Foundations.Univalence
 
 open import Cubical.Categories.Category
-open import Cubical.Categories.Functor
+open import Cubical.Categories.Functor renaming (𝟙⟨_⟩ to funcId)
 open import Cubical.Categories.NaturalTransformation.Base
 open import Cubical.Categories.Monad.Base
 open import Cubical.Categories.Instances.FunctorAlgebras
 open import Cubical.Categories.Constructions.FullSubcategory
+open import Cubical.Categories.Adjoint
 
 private
   variable
@@ -75,3 +76,75 @@ module _ {C : Category ℓC ℓC'} (monadM : Monad C) where
   strHom (F-hom FreeEMAlgebra {x} {y} φ) = sym (N-hom μ φ)
   F-id FreeEMAlgebra = AlgebraHom≡ M (F-id M)
   F-seq FreeEMAlgebra {x} {y} {z} φ ψ = AlgebraHom≡ M (F-seq M φ ψ)
+
+  ForgetFreeEMAlgebra : funcComp ForgetEMAlgebra FreeEMAlgebra ≡ M
+  ForgetFreeEMAlgebra = Functor≡ (λ x → refl) (λ f → refl)
+
+  emCounit : NatTrans (funcComp FreeEMAlgebra ForgetEMAlgebra) (funcId EMCategory)
+  carrierHom (N-ob emCounit (algebra A α , isEMA)) = α
+  strHom (N-ob emCounit (algebra A α , isEMA)) = str-μ isEMA
+  N-hom emCounit {algebra A α , isEMA} {algebra B β , isEMB} (algebraHom f isalgF) =
+    AlgebraHom≡ M (sym (isalgF))
+
+  open NaturalBijection
+  open _⊣_
+  open _≅_
+
+  emBijection : ∀ a emB →
+    (EMCategory [ FreeEMAlgebra ⟅ a ⟆ , emB ]) ≅ (C [ a , ForgetEMAlgebra ⟅ emB ⟆ ])
+  fun (emBijection a (algebra b β , isEMB)) (algebraHom f isalgF) = f C.∘ N-ob η a
+  carrierHom (inv (emBijection a (algebra b β , isEMB)) f) = β C.∘ F-hom M f
+  strHom (inv (emBijection a (algebra b β , isEMB)) f) =
+    (N-ob μ a C.⋆ (F-hom M f C.⋆ β))
+      ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
+    ((N-ob μ a C.⋆ F-hom M f) C.⋆ β)
+      ≡⟨ cong (C._⋆ β) (sym (N-hom μ f)) ⟩
+    ((F-hom M (F-hom M f) C.⋆ N-ob μ b) C.⋆ β)
+      ≡⟨ C.⋆Assoc _ _ _ ⟩
+    (F-hom M (F-hom M f) C.⋆ (N-ob μ b C.⋆ β))
+      ≡⟨ cong (F-hom M (F-hom M f) C.⋆_) (str-μ isEMB) ⟩
+    (F-hom M (F-hom M f) C.⋆ (F-hom M β C.⋆ β))
+      ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
+    ((F-hom M (F-hom M f) C.⋆ F-hom M β) C.⋆ β)
+      ≡⟨ cong (C._⋆ β) (sym (F-seq M _ _)) ⟩
+    (F-hom M (F-hom M f C.⋆ β) C.⋆ β) ∎
+  rightInv (emBijection a (algebra b β , isEMB)) f =
+    (N-ob η a C.⋆ (F-hom M f C.⋆ β))
+      ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
+    ((N-ob η a C.⋆ F-hom M f) C.⋆ β)
+      ≡⟨ cong (C._⋆ β) (sym (N-hom η f)) ⟩
+    ((f C.⋆ N-ob η b) C.⋆ β)
+      ≡⟨ C.⋆Assoc _ _ _ ⟩
+    (f C.⋆ (N-ob η b C.⋆ β))
+      ≡⟨ cong (f C.⋆_) (str-η isEMB) ⟩
+    (f C.⋆ C.id)
+      ≡⟨ C.⋆IdR _ ⟩
+    f ∎
+  leftInv (emBijection a (algebra b β , isEMB)) (algebraHom f isalgF) = AlgebraHom≡ M (
+    (F-hom M (N-ob η a C.⋆ f) C.⋆ β)
+      ≡⟨ cong (C._⋆ β) (F-seq M _ _) ⟩
+    ((F-hom M (N-ob η a) C.⋆ F-hom M f) C.⋆ β)
+      ≡⟨ C.⋆Assoc _ _ _ ⟩
+    (F-hom M (N-ob η a) C.⋆ (F-hom M f C.⋆ β))
+      ≡⟨ cong (F-hom M (N-ob η a) C.⋆_) (sym isalgF) ⟩
+    (F-hom M (N-ob η a) C.⋆ (N-ob μ a C.⋆ f))
+      ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
+    ((F-hom M (N-ob η a) C.⋆ N-ob μ a) C.⋆ f)
+      ≡⟨ cong (C._⋆ f) (funExt⁻ (congP (λ i → N-ob) idr-μ) a) ⟩
+    (C.id C.⋆ f)
+      ≡⟨ C.⋆IdL f ⟩
+    f ∎
+    )
+
+  emAdjunction : FreeEMAlgebra ⊣ ForgetEMAlgebra
+  adjIso emAdjunction {a} {algebra b β , isEMB} = emBijection a (algebra b β , isEMB)
+  adjNatInD emAdjunction {a} {algebra b β , isEMB} {algebra c γ , isEMC}
+    (algebraHom f isalgF) (algebraHom g isalgG) =
+    sym (C.⋆Assoc _ _ _)
+  adjNatInC emAdjunction {a} {b} {algebra c γ , isEMC} f g = AlgebraHom≡ M (
+    (F-hom M (g C.⋆ f) C.⋆ γ)
+      ≡⟨ cong (C._⋆ γ) (F-seq M _ _) ⟩
+    ((F-hom M g C.⋆ F-hom M f) C.⋆ γ)
+      ≡⟨ C.⋆Assoc _ _ _ ⟩
+    (F-hom M g C.⋆ (F-hom M f C.⋆ γ)) ∎
+    )