Skip to content

Commit bbe8850

Browse files
tillrampetillrampe
committed
Create a file that collects all important properties about the tensorproduct
1 parent 0cb626c commit bbe8850

File tree

3 files changed

+91
-26
lines changed

3 files changed

+91
-26
lines changed

‎src/Categories/Bicategory/Construction/Bimodules/Tensorproduct.agda‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Categories.Bicategory
4+
open import Categories.Bicategory.LocalCoequalizers
5+
open import Categories.Bicategory.Monad
6+
7+
--- The construction of the tensorproduct is in ---
8+
--- Categories.Bicategory.Construction.Bimodules.TensorproductOfBimodules and ---
9+
--- Categories.Bicategory.Construction.Bimodules.TensorproductOfHomomorphisms ---
10+
--- but for almost all purposes you do not want to look at the construction there; ---
11+
--- instead use the properties collected in this module. ---
12+
module Categories.Bicategory.Construction.Bimodules.Tensorproduct
13+
{o ℓ e t} {𝒞 : Bicategory o ℓ e t} {localCoeq : LocalCoequalizers 𝒞} {M₁ M₂ M₃ : Monad 𝒞}where
14+
15+
import Categories.Bicategory.Extras as Bicat
16+
open Bicat 𝒞
17+
open Shorthands
18+
open import Categories.Bicategory.Monad.Bimodule using (Bimodule)
19+
open import Categories.Bicategory.Monad.Bimodule.Homomorphism using (Bimodulehomomorphism)
20+
21+
import Categories.Bicategory.Construction.Bimodules.TensorproductOfBimodules {𝒞 = 𝒞} {localCoeq} {M₁} {M₂} {M₃} as TensorproductOfBimodules
22+
import Categories.Bicategory.Construction.Bimodules.TensorproductOfHomomorphisms {𝒞 = 𝒞} {localCoeq} {M₁} {M₂} {M₃} as TensorproductOfHomomorphisms
23+
24+
private
25+
module HomCat {X} {Y} where
26+
open import Categories.Morphism (hom X Y) public using (Epi)
27+
open import Categories.Diagram.Coequalizer (hom X Y) public using (Coequalizer; Coequalizer⇒Epi)
28+
29+
open HomCat
30+
31+
open Bimodule using (F; actionˡ)
32+
open Monad using (T)
33+
34+
abstract
35+
infixl 30 _⊗₀_ _⊗₁_
36+
37+
--- Tensorproduct of Bimodules ---
38+
_⊗₀_ : Bimodule M₂ M₃ → Bimodule M₁ M₂ → Bimodule M₁ M₃
39+
L ⊗₀ R = L⊗R
40+
where
41+
open TensorproductOfBimodules L R using (L⊗R)
42+
43+
44+
arr_⊗₀_ : (L : Bimodule M₂ M₃) (R : Bimodule M₁ M₂) → (F L ∘₁ F R) ⇒₂ F (L ⊗₀ R)
45+
arr L ⊗₀ R = Coequalizer.arr F₂⊗F₁
46+
where
47+
open TensorproductOfBimodules L R using (F₂⊗F₁)
48+
49+
epi_⊗₀_ : (L : Bimodule M₂ M₃) (R : Bimodule M₁ M₂) → Epi (arr L ⊗₀ R)
50+
epi L ⊗₀ R = Coequalizer⇒Epi F₂⊗F₁
51+
where
52+
open TensorproductOfBimodules L R using (F₂⊗F₁)
53+
54+
actionˡDef_⊗₀_ : (L : Bimodule M₂ M₃) (R : Bimodule M₁ M₂)
55+
→ (arr L ⊗₀ R) ∘ᵥ F L ▷ actionˡ R ∘ᵥ α⇒ ≈ actionˡ (L ⊗₀ R) ∘ᵥ arr L ⊗₀ R ◁ T M₁
56+
actionˡDef L ⊗₀ R = actionˡSq
57+
where
58+
open TensorproductOfBimodules.Left-Action L R using (actionˡSq)
59+
60+
--- Tensorproduct of Homomoprhisms ---
61+
_⊗₁_ : {L L' : Bimodule M₂ M₃} {R R' : Bimodule M₁ M₂}
62+
→ Bimodulehomomorphism L L' → Bimodulehomomorphism R R' → Bimodulehomomorphism (L ⊗₀ R) (L' ⊗₀ R')
63+
l ⊗₁ r = l⊗r
64+
where
65+
open TensorproductOfHomomorphisms l r using (l⊗r)

‎src/Categories/Bicategory/Construction/Bimodules/TensorproductOfBimodules.agda‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ open import Categories.Bicategory.Monad.Bimodule
77

88
module Categories.Bicategory.Construction.Bimodules.TensorproductOfBimodules
99
{o ℓ e t} {𝒞 : Bicategory o ℓ e t} {localCoeq : LocalCoequalizers 𝒞}
10-
{M₁ M₂ M₃ : Monad 𝒞} (B₂ : Bimodule M₂ M₃) (B₁ : Bimodule M₁ M₂) where
10+
{M₁ M₂ M₃ : Monad 𝒞} (L : Bimodule M₂ M₃) (R : Bimodule M₁ M₂) where
1111

1212
open import Level
1313
open import Categories.Bicategory.Monad.Bimodule.Homomorphism using (Bimodulehomomorphism)
@@ -28,15 +28,15 @@ open ComposeWithLocalCoequalizer 𝒞 localCoeq using (_coeq-◁_; _▷-coeq_)
2828
open Monad M₁ using () renaming (C to C₁; T to T₁; μ to μ₁; η to η₁)
2929
open Monad M₂ using () renaming (C to C₂; T to T₂; μ to μ₂; η to η₂)
3030
open Monad M₃ using () renaming (C to C₃; T to T₃; μ to μ₃; η to η₃)
31-
open Bimodule B₁ using ()
31+
open Bimodule R using ()
3232
renaming (F to F₁; actionˡ to actionˡ₁; actionʳ to actionʳ₁; assoc to action-assoc₁;
3333
sym-assoc to action-sym-assoc₁; assoc-actionˡ to assoc-actionˡ₁; identityˡ to identityˡ₁)
34-
open Bimodule B₂ using ()
34+
open Bimodule L using ()
3535
renaming (F to F₂; actionˡ to actionˡ₂; actionʳ to actionʳ₂; assoc to action-assoc₂;
3636
sym-assoc to action-sym-assoc₂; assoc-actionʳ to assoc-actionʳ₂; identityʳ to identityʳ₂)
3737

3838
{-
39-
To construct the tensorproduct B₂⊗B₁ we will define its underlying 1-cell
39+
To construct the tensorproduct L⊗R we will define its underlying 1-cell
4040
to be the coequalizer of the following parallel pair in hom C₁ C₃:
4141
4242
F₂ ▷ actionʳ₁
@@ -55,7 +55,7 @@ F₂⊗F₁ : Coequalizer (hom C₁ C₃) (act-to-the-left) (act-to-the-right)
5555
F₂⊗F₁ = localCoequalizers C₁ C₃ (act-to-the-left) (act-to-the-right)
5656
-- coequalizer {_} {_} {F₂ ∘₁ T₂ ∘₁ F₁} {F₂ ∘₁ F₁} (act-to-the-left) (act-to-the-right)
5757

58-
-- The underlying object of that coequalizer is the underlying 1-cell of the bimodule B₂⊗B₁ --
58+
-- The underlying object of that coequalizer is the underlying 1-cell of the bimodule L⊗R --
5959
F : C₁ ⇒₁ C₃
6060
F = Coequalizer.obj F₂⊗F₁
6161

@@ -557,8 +557,8 @@ module Identity where
557557
identityʳ = Coequalizer⇒Epi (hom C₁ C₃) F₂⊗F₁ (actionʳ ∘ᵥ (η₃ ◁ F) ∘ᵥ unitorˡ.to) id₂ identityʳ∘arr
558558
-- end abstract --
559559

560-
B₂⊗B₁ : Bimodule M₁ M₃
561-
B₂⊗B₁ = record
560+
L⊗R : Bimodule M₁ M₃
561+
L⊗R = record
562562
{ F = F
563563
; actionˡ = Left-Action.actionˡ --: F ∘₁ T₁ ⇒₂ F
564564
; actionʳ = Right-Action.actionʳ --: T₂ ∘₁ F ⇒₂ F

‎src/Categories/Bicategory/Construction/Bimodules/TensorproductOfHomomorphisms.agda‎

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@ open import Categories.Bicategory.Monad.Bimodule.Homomorphism using (Bimodulehom
88

99
module Categories.Bicategory.Construction.Bimodules.TensorproductOfHomomorphisms
1010
{o ℓ e t} {𝒞 : Bicategory o ℓ e t} {localCoeq : LocalCoequalizers 𝒞}
11-
{M₁ M₂ M₃ : Monad 𝒞} {B₂ B'₂ : Bimodule M₂ M₃} {B₁ B'₁ : Bimodule M₁ M₂}
12-
(h₂ : Bimodulehomomorphism B₂ B'₂) (h₁ : Bimodulehomomorphism B₁ B'₁) where
11+
{M₁ M₂ M₃ : Monad 𝒞} {L L' : Bimodule M₂ M₃} {R R' : Bimodule M₁ M₂}
12+
(l : Bimodulehomomorphism L L') (r : Bimodulehomomorphism R R') where
1313

1414
open import Level
1515
import Categories.Category.Construction.Bimodules
@@ -30,18 +30,18 @@ open ComposeWithLocalCoequalizer 𝒞 localCoeq using (_coeq-◁_; _▷-coeq_)
3030
open Monad M₁ using () renaming (C to C₁; T to T₁; μ to μ₁; η to η₁)
3131
open Monad M₂ using () renaming (C to C₂; T to T₂; μ to μ₂; η to η₂)
3232
open Monad M₃ using () renaming (C to C₃; T to T₃; μ to μ₃; η to η₃)
33-
open Bimodule B₁ using () renaming (F to F₁; actionʳ to actionʳ₁; actionˡ to actionˡ₁)
34-
open Bimodule B'₁ using () renaming (F to F'₁; actionʳ to actionʳ'₁; actionˡ to actionˡ'₁)
35-
open Bimodule B₂ using () renaming (F to F₂; actionʳ to actionʳ₂; actionˡ to actionˡ₂)
36-
open Bimodule B'₂ using () renaming (F to F'₂; actionʳ to actionʳ'₂; actionˡ to actionˡ'₂)
33+
open Bimodule R using () renaming (F to F₁; actionʳ to actionʳ₁; actionˡ to actionˡ₁)
34+
open Bimodule R' using () renaming (F to F'₁; actionʳ to actionʳ'₁; actionˡ to actionˡ'₁)
35+
open Bimodule L using () renaming (F to F₂; actionʳ to actionʳ₂; actionˡ to actionˡ₂)
36+
open Bimodule L' using () renaming (F to F'₂; actionʳ to actionʳ'₂; actionˡ to actionˡ'₂)
3737
import Categories.Bicategory.Construction.Bimodules.TensorproductOfBimodules {𝒞 = 𝒞} {localCoeq} {M₁} {M₂} {M₃} as TensorproductOfBimodules
38-
open TensorproductOfBimodules B₂ B₁ using (B₂⊗B₁; F₂⊗F₁; act-to-the-left; act-to-the-right)
39-
open TensorproductOfBimodules B'₂ B'₁ using ()
40-
renaming (B₂⊗B₁ to B'₂⊗B'₁; F₂⊗F₁ to F'₂⊗F'₁; act-to-the-left to act-to-the-left'; act-to-the-right to act-to-the-right')
41-
open Bimodule B₂⊗B₁ using (F; actionˡ; actionʳ)
42-
open Bimodule B'₂⊗B'₁ using () renaming (F to F'; actionˡ to actionˡ'; actionʳ to actionʳ')
43-
open Bimodulehomomorphism h₁ using () renaming (α to α₁; linearˡ to linearˡ₁; linearʳ to linearʳ₁)
44-
open Bimodulehomomorphism h₂ using () renaming (α to α₂; linearˡ to linearˡ₂; linearʳ to linearʳ₂)
38+
open TensorproductOfBimodules L R using (L⊗R; F₂⊗F₁; act-to-the-left; act-to-the-right)
39+
open TensorproductOfBimodules L' R' using ()
40+
renaming (L⊗R to L'⊗R'; F₂⊗F₁ to F'₂⊗F'₁; act-to-the-left to act-to-the-left'; act-to-the-right to act-to-the-right')
41+
open Bimodule L⊗R using (F; actionˡ; actionʳ)
42+
open Bimodule L'⊗R' using () renaming (F to F'; actionˡ to actionˡ'; actionʳ to actionʳ')
43+
open Bimodulehomomorphism r using () renaming (α to α₁; linearˡ to linearˡ₁; linearʳ to linearʳ₁)
44+
open Bimodulehomomorphism l using () renaming (α to α₂; linearˡ to linearˡ₂; linearʳ to linearʳ₂)
4545

4646
open Definitions (hom C₁ C₃) -- for Commutative Squares
4747

@@ -86,8 +86,8 @@ sq₂ = begin
8686
where
8787
open CoeqProperties (hom C₁ C₃)
8888

89-
open TensorproductOfBimodules.Left-Action B₂ B₁ using (F∘T₁Coequalizer; F₂▷actionˡ₁; actionˡSq)
90-
open TensorproductOfBimodules.Left-Action B'₂ B'₁ using ()
89+
open TensorproductOfBimodules.Left-Action L R using (F∘T₁Coequalizer; F₂▷actionˡ₁; actionˡSq)
90+
open TensorproductOfBimodules.Left-Action L' R' using ()
9191
renaming (F₂▷actionˡ₁ to F'₂▷actionˡ'₁; actionˡSq to actionˡ'Sq)
9292

9393
linearˡ-square : F'₂▷actionˡ'₁ ∘ᵥ (α₂ ⊚₁ α₁) ◁ T₁ ≈ (α₂ ⊚₁ α₁) ∘ᵥ F₂▷actionˡ₁
@@ -130,8 +130,8 @@ linearˡ = Coequalizer⇒Epi (hom C₁ C₃) F∘T₁Coequalizer
130130
linearˡ∘arr
131131

132132

133-
open TensorproductOfBimodules.Right-Action B₂ B₁ using (T₃∘FCoequalizer; actionʳ₂◁F₁; actionʳSq)
134-
open TensorproductOfBimodules.Right-Action B'₂ B'₁ using () renaming (actionʳ₂◁F₁ to actionʳ'₂◁F'₁; actionʳSq to actionʳ'Sq)
133+
open TensorproductOfBimodules.Right-Action L R using (T₃∘FCoequalizer; actionʳ₂◁F₁; actionʳSq)
134+
open TensorproductOfBimodules.Right-Action L' R' using () renaming (actionʳ₂◁F₁ to actionʳ'₂◁F'₁; actionʳSq to actionʳ'Sq)
135135

136136
linearʳ-square : actionʳ'₂◁F'₁ ∘ᵥ T₃ ▷ (α₂ ⊚₁ α₁) ≈ (α₂ ⊚₁ α₁) ∘ᵥ actionʳ₂◁F₁
137137
linearʳ-square = begin
@@ -171,8 +171,8 @@ linearʳ = Coequalizer⇒Epi (hom C₁ C₃) T₃∘FCoequalizer
171171
(actionʳ' ∘ᵥ T₃ ▷ α) (α ∘ᵥ actionʳ)
172172
linearʳ∘arr
173173

174-
h₂⊗h₁ : Bimodulehomomorphism B₂⊗B₁ B'₂⊗B'₁
175-
h₂⊗h₁ = record
174+
l⊗r : Bimodulehomomorphism L⊗R L'⊗R'
175+
l⊗r = record
176176
{ α = α
177177
; linearˡ = linearˡ
178178
; linearʳ = linearʳ

0 commit comments

Comments
 (0)