Skip to content

Commit e9f1d62

Browse files
JacquesCaretteJacquesCarette
authored
Merge pull request #478 from tillrampe/bimodule
Bimodule
2 parents 566e17b + 97839e2 commit e9f1d62

File tree

2 files changed

+183
-0
lines changed

2 files changed

+183
-0
lines changed

‎src/Categories/Bicategory/Monad/Bimodule.agda‎

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Categories.Bicategory
4+
5+
module Categories.Bicategory.Monad.Bimodule {o ℓ e t} {𝒞 : Bicategory o ℓ e t} where
6+
7+
open import Level
8+
open import Categories.Bicategory.Monad using (Monad)
9+
import Categories.Bicategory.Extras as Bicat
10+
open Bicat 𝒞
11+
open Shorthands
12+
import Categories.Morphism.Reasoning as MR
13+
14+
private
15+
module MR' {A B : Obj} where
16+
open MR (hom A B) using (pullˡ; elimʳ; assoc²βγ) public
17+
18+
record Bimodule (M₁ M₂ : Monad 𝒞) : Set (o ⊔ ℓ ⊔ e) where
19+
open Monad using (C; T; μ; η)
20+
field
21+
F : C M₁ ⇒₁ C M₂
22+
actionˡ : F ∘₁ T M₁ ⇒₂ F
23+
actionʳ : T M₂ ∘₁ F ⇒₂ F
24+
25+
assoc : actionʳ ∘ᵥ (T M₂ ▷ actionˡ) ∘ᵥ α⇒ ≈ actionˡ ∘ᵥ (actionʳ ◁ T M₁)
26+
sym-assoc : actionˡ ∘ᵥ (actionʳ ◁ T M₁) ∘ᵥ α⇐ ≈ actionʳ ∘ᵥ (T M₂ ▷ actionˡ)
27+
28+
assoc-actionˡ : actionˡ ∘ᵥ (F ▷ μ M₁) ∘ᵥ α⇒ ≈ actionˡ ∘ᵥ (actionˡ ◁ T M₁)
29+
sym-assoc-actionˡ : actionˡ ∘ᵥ (actionˡ ◁ T M₁) ∘ᵥ α⇐ ≈ actionˡ ∘ᵥ (F ▷ μ M₁)
30+
assoc-actionʳ : actionʳ ∘ᵥ (μ M₂ ◁ F) ∘ᵥ α⇐ ≈ actionʳ ∘ᵥ (T M₂ ▷ actionʳ)
31+
sym-assoc-actionʳ : actionʳ ∘ᵥ (T M₂ ▷ actionʳ) ∘ᵥ α⇒ ≈ actionʳ ∘ᵥ (μ M₂ ◁ F)
32+
33+
identityˡ : actionˡ ∘ᵥ (F ▷ η M₁) ∘ᵥ unitorʳ.to ≈ id₂
34+
identityʳ : actionʳ ∘ᵥ (η M₂ ◁ F) ∘ᵥ unitorˡ.to ≈ id₂
35+
36+
-- This helper definition lets us specify only one of each associativity laws
37+
-- and have the symmetric one derived.
38+
record BIMODHelper (M₁ M₂ : Monad 𝒞) : Set (o ⊔ ℓ ⊔ e) where
39+
open Monad using (C; T; μ; η)
40+
field
41+
F : C M₁ ⇒₁ C M₂
42+
actionˡ : F ∘₁ T M₁ ⇒₂ F
43+
actionʳ : T M₂ ∘₁ F ⇒₂ F
44+
45+
assoc : actionʳ ∘ᵥ (T M₂ ▷ actionˡ) ∘ᵥ α⇒ ≈ actionˡ ∘ᵥ (actionʳ ◁ T M₁)
46+
47+
assoc-actionˡ : actionˡ ∘ᵥ (F ▷ μ M₁) ∘ᵥ α⇒ ≈ actionˡ ∘ᵥ (actionˡ ◁ T M₁)
48+
assoc-actionʳ : actionʳ ∘ᵥ (μ M₂ ◁ F) ∘ᵥ α⇐ ≈ actionʳ ∘ᵥ (T M₂ ▷ actionʳ)
49+
50+
identityˡ : actionˡ ∘ᵥ (F ▷ η M₁) ∘ᵥ unitorʳ.to ≈ id₂
51+
identityʳ : actionʳ ∘ᵥ (η M₂ ◁ F) ∘ᵥ unitorˡ.to ≈ id₂
52+
53+
bimodHelper : ∀ {M₁ M₂ : Monad 𝒞} → BIMODHelper M₁ M₂ → Bimodule M₁ M₂
54+
bimodHelper {M₁} {M₂} B = record
55+
{ F = F
56+
; actionˡ = actionˡ
57+
; actionʳ = actionʳ
58+
; assoc = assoc
59+
; sym-assoc = sym-assoc
60+
; assoc-actionˡ = assoc-actionˡ
61+
; sym-assoc-actionˡ = sym-assoc-actionˡ
62+
; assoc-actionʳ = assoc-actionʳ
63+
; sym-assoc-actionʳ = sym-assoc-actionʳ
64+
; identityˡ = identityˡ
65+
; identityʳ = identityʳ
66+
}
67+
where
68+
open Monad using (T; μ)
69+
open BIMODHelper B
70+
open hom.HomReasoning
71+
open MR'
72+
73+
sym-assoc : actionˡ ∘ᵥ (actionʳ ◁ T M₁) ∘ᵥ α⇐ ≈ actionʳ ∘ᵥ (T M₂ ▷ actionˡ)
74+
sym-assoc = begin
75+
actionˡ ∘ᵥ (actionʳ ◁ T M₁) ∘ᵥ α⇐ ≈⟨ pullˡ (⟺ assoc) ⟩
76+
(actionʳ ∘ᵥ (T M₂ ▷ actionˡ) ∘ᵥ α⇒) ∘ᵥ α⇐ ≈⟨ assoc²βγ ⟩
77+
(actionʳ ∘ᵥ (T M₂ ▷ actionˡ)) ∘ᵥ α⇒ ∘ᵥ α⇐ ≈⟨ elimʳ associator.isoʳ ⟩
78+
actionʳ ∘ᵥ (T M₂ ▷ actionˡ) ∎
79+
80+
sym-assoc-actionˡ : actionˡ ∘ᵥ (actionˡ ◁ T M₁) ∘ᵥ α⇐ ≈ actionˡ ∘ᵥ (F ▷ μ M₁)
81+
sym-assoc-actionˡ = begin
82+
actionˡ ∘ᵥ (actionˡ ◁ T M₁) ∘ᵥ α⇐ ≈⟨ pullˡ (⟺ assoc-actionˡ) ⟩
83+
(actionˡ ∘ᵥ (F ▷ μ M₁) ∘ᵥ α⇒) ∘ᵥ α⇐ ≈⟨ assoc²βγ ⟩
84+
(actionˡ ∘ᵥ (F ▷ μ M₁)) ∘ᵥ α⇒ ∘ᵥ α⇐ ≈⟨ elimʳ associator.isoʳ ⟩
85+
actionˡ ∘ᵥ (F ▷ μ M₁) ∎
86+
87+
sym-assoc-actionʳ : actionʳ ∘ᵥ (T M₂ ▷ actionʳ) ∘ᵥ α⇒ ≈ actionʳ ∘ᵥ (μ M₂ ◁ F)
88+
sym-assoc-actionʳ = begin
89+
actionʳ ∘ᵥ (T M₂ ▷ actionʳ) ∘ᵥ α⇒ ≈⟨ pullˡ (⟺ assoc-actionʳ) ⟩
90+
(actionʳ ∘ᵥ (μ M₂ ◁ F) ∘ᵥ α⇐) ∘ᵥ α⇒ ≈⟨ assoc²βγ ⟩
91+
(actionʳ ∘ᵥ (μ M₂ ◁ F)) ∘ᵥ α⇐ ∘ᵥ α⇒ ≈⟨ elimʳ associator.isoˡ ⟩
92+
actionʳ ∘ᵥ (μ M₂ ◁ F) ∎
93+
94+
id-bimodule : (M : Monad 𝒞) → Bimodule M M
95+
id-bimodule M = record
96+
{ F = T
97+
; actionˡ = μ
98+
; actionʳ = μ
99+
; assoc = assoc
100+
; sym-assoc = sym-assoc
101+
; assoc-actionˡ = assoc
102+
; sym-assoc-actionˡ = sym-assoc
103+
; assoc-actionʳ = sym-assoc
104+
; sym-assoc-actionʳ = assoc
105+
; identityˡ = identityˡ
106+
; identityʳ = identityʳ
107+
}
108+
where
109+
open Monad M

‎src/Categories/Bicategory/Monad/Bimodule/Homomorphism.agda‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Categories.Bicategory
4+
open import Categories.Bicategory.Monad using (Monad)
5+
6+
module Categories.Bicategory.Monad.Bimodule.Homomorphism {o ℓ e t} {𝒞 : Bicategory o ℓ e t} {M₁ M₂ : Monad 𝒞} where
7+
8+
open import Level
9+
open import Categories.Bicategory.Monad.Bimodule using (Bimodule)
10+
import Categories.Bicategory.Extras as Bicat
11+
open Bicat 𝒞
12+
import Categories.Morphism.Reasoning as MR
13+
14+
private
15+
module MR' {A B : Obj} where
16+
open MR (hom A B) public
17+
18+
record Bimodulehomomorphism (B₁ B₂ : Bimodule M₁ M₂) : Set (ℓ ⊔ e) where
19+
open Monad using (T)
20+
open Bimodule using (F; actionˡ; actionʳ)
21+
field
22+
α : F B₁ ⇒₂ F B₂
23+
linearˡ : actionˡ B₂ ∘ᵥ (α ◁ T M₁) ≈ α ∘ᵥ actionˡ B₁
24+
linearʳ : actionʳ B₂ ∘ᵥ (T M₂ ▷ α) ≈ α ∘ᵥ actionʳ B₁
25+
26+
id-bimodule-hom : {B : Bimodule M₁ M₂} → Bimodulehomomorphism B B
27+
id-bimodule-hom {B} = record
28+
{ α = id₂
29+
; linearˡ = id-linearˡ
30+
; linearʳ = id-linearʳ
31+
}
32+
where
33+
open Monad using (C; T)
34+
open Bimodule B using (actionˡ; actionʳ)
35+
open hom.HomReasoning
36+
open MR'
37+
38+
id-linearˡ : actionˡ ∘ᵥ (id₂ ◁ T M₁) ≈ id₂ ∘ᵥ actionˡ
39+
id-linearˡ = begin
40+
actionˡ ∘ᵥ (id₂ ◁ T M₁) ≈⟨ elimʳ ▷id₂ ⟩
41+
actionˡ ≈⟨ ⟺ identity₂ˡ ⟩
42+
id₂ ∘ᵥ actionˡ ∎
43+
44+
id-linearʳ : actionʳ ∘ᵥ (T M₂ ▷ id₂) ≈ id₂ ∘ᵥ actionʳ
45+
id-linearʳ = begin
46+
actionʳ ∘ᵥ (T M₂ ▷ id₂) ≈⟨ elimʳ ▷id₂ ⟩
47+
actionʳ ≈⟨ ⟺ identity₂ˡ ⟩
48+
id₂ ∘ᵥ actionʳ ∎
49+
50+
bimodule-hom-∘ : {B₁ B₂ B₃ : Bimodule M₁ M₂}
51+
→ Bimodulehomomorphism B₂ B₃ → Bimodulehomomorphism B₁ B₂ → Bimodulehomomorphism B₁ B₃
52+
bimodule-hom-∘ {B₁} {B₂} {B₃} g f = record
53+
{ α = α g ∘ᵥ α f
54+
; linearˡ = g∘f-linearˡ
55+
; linearʳ = g∘f-linearʳ
56+
}
57+
where
58+
open Monad using (C; T)
59+
open Bimodule using (F; actionˡ; actionʳ)
60+
open Bimodulehomomorphism using (α; linearˡ; linearʳ)
61+
open hom.HomReasoning
62+
open MR'
63+
64+
g∘f-linearˡ : actionˡ B₃ ∘ᵥ (α g ∘ᵥ α f) ◁ T M₁ ≈ (α g ∘ᵥ α f) ∘ᵥ actionˡ B₁
65+
g∘f-linearˡ = begin
66+
actionˡ B₃ ∘ᵥ (α g ∘ᵥ α f) ◁ T M₁ ≈⟨ refl⟩∘⟨ ⟺ ∘ᵥ-distr-◁ ⟩
67+
actionˡ B₃ ∘ᵥ (α g ◁ T M₁) ∘ᵥ (α f ◁ T M₁) ≈⟨ glue′ (linearˡ g) (linearˡ f) ⟩
68+
(α g ∘ᵥ α f) ∘ᵥ actionˡ B₁ ∎
69+
70+
g∘f-linearʳ : actionʳ B₃ ∘ᵥ T M₂ ▷ (α g ∘ᵥ α f) ≈ (α g ∘ᵥ α f) ∘ᵥ actionʳ B₁
71+
g∘f-linearʳ = begin
72+
actionʳ B₃ ∘ᵥ T M₂ ▷ (α g ∘ᵥ α f) ≈⟨ refl⟩∘⟨ (⟺ ∘ᵥ-distr-▷) ⟩
73+
actionʳ B₃ ∘ᵥ (T M₂ ▷ α g) ∘ᵥ (T M₂ ▷ α f) ≈⟨ glue′ (linearʳ g) (linearʳ f) ⟩
74+
(α g ∘ᵥ α f) ∘ᵥ actionʳ B₁ ∎

0 commit comments

Comments
 (0)