Skip to content

Properties of the 1-Category of Bimodules #481

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
JacquesCarette merged 2 commits into from
Jul 10, 2025
Merged

Properties of the 1-Category of Bimodules #481

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
386b672
Rewrite the import commands and open the relevant (bi)categories insi…
tillrampe Jul 7, 2025
22ef11c
Put import commands at the beginning, leaving the open commands where…
tillrampe Jul 10, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
65 changes: 31 additions & 34 deletions src/Categories/Category/Construction/Bimodules/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,35 +7,32 @@ open import Categories.Bicategory.Monad
module Categories.Category.Construction.Bimodules.Properties
{o ℓ e t} {𝒞 : Bicategory o ℓ e t} {M₁ M₂ : Monad 𝒞} where

open import Agda.Primitive

import Categories.Category.Construction.Bimodules
open import Categories.Category

Bimodules : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e
Bimodules = Categories.Category.Construction.Bimodules.Bimodules M₁ M₂
open import Categories.Bicategory.Monad.Bimodule using (Bimodule)
open import Categories.Bicategory.Monad.Bimodule.Homomorphism using (Bimodulehomomorphism)
import Categories.Morphism as Mor
import Categories.Morphism.Reasoning.Iso as IsoReasoning
open import Categories.Category.Construction.Bimodules M₁ M₂ using (Bimodules)
open import Categories.Category using (Category)
import Categories.Bicategory.Extras as Bicat

private
module Cat {o₁ ℓ₁ e₁} {C : Categories.Category.Category o₁ ℓ₁ e₁} where
open Categories.Category.Category C using (Obj; _⇒_) public
open import Categories.Morphism C using (IsIso; _≅_) public
open import Categories.Morphism.Reasoning.Iso C using (conjugate-from) public
module Bimodules where
open Category Bimodules public
open Mor Bimodules using (IsIso; _≅_) public

open Cat


import Categories.Bicategory.Extras as Bicat
open Bicat 𝒞 using (hom; _⇒₂_; _≈_; _∘ᵥ_; _◁_; _▷_; _◁ᵢ_; _▷ᵢ_)
module 𝒞 where
open Bicat 𝒞 public

open import Categories.Bicategory.Monad.Bimodule {𝒞 = 𝒞}
open import Categories.Bicategory.Monad.Bimodule.Homomorphism {𝒞 = 𝒞}
module HomCat {A B : 𝒞.Obj} where
open Mor (𝒞.hom A B) using (IsIso; _≅_) public
open IsoReasoning (𝒞.hom A B) using (conjugate-from) public

module Bimodulehom-isIso {B₁ B₂ : Obj {C = Bimodules}} (f : _⇒_ {C = Bimodules} B₁ B₂) where
module Bimodule-Isomorphism {B₁ B₂ : Bimodules.Obj} (f : B₁ Bimodules.⇒ B₂) where
open Monad using (C; T)
open Bimodule using (F; actionˡ; actionʳ)
open Bimodulehomomorphism f using (α; linearˡ; linearʳ)

αisIso⇒fisIso : IsIso {C = hom (C M₁) (C M₂)} α → IsIso {C = Bimodules} f
αisIso⇒fisIso : HomCat.IsIso α → Bimodules.IsIso f
αisIso⇒fisIso αisIso = record
{ inv = record
{ α = α⁻¹
Expand All @@ -44,32 +41,32 @@ module Bimodulehom-isIso {B₁ B₂ : Obj {C = Bimodules}} (f : _⇒_ {C = Bimod
}
; iso = record
-- Cannot be delta reduced because of size issues
{ isoˡ = IsIso.isoˡ αisIso
; isoʳ = IsIso.isoʳ αisIso
{ isoˡ = HomCat.IsIso.isoˡ αisIso
; isoʳ = HomCat.IsIso.isoʳ αisIso
}
}
where
open hom.HomReasoning
open 𝒞.hom.HomReasoning

α⁻¹ : F B₂ ⇒₂ F B₁
α⁻¹ = IsIso.inv αisIso
α⁻¹ : F B₂ 𝒞.⇒₂ F B₁
α⁻¹ = HomCat.IsIso.inv αisIso

αIso : F B₁ ≅ F B₂
αIso : F B₁ HomCat.≅ F B₂
αIso = record
{ from = α
; to = α⁻¹
; iso = IsIso.iso αisIso
; iso = HomCat.IsIso.iso αisIso
}

linearˡ⁻¹ : actionˡ B₁ ∘ᵥ α⁻¹ ◁ T M₁ ≈ α⁻¹ ∘ᵥ actionˡ B₂
linearˡ⁻¹ = ⟺ (conjugate-from (αIso ◁ᵢ T M₁) αIso linearˡ)
linearˡ⁻¹ : actionˡ B₁ 𝒞.∘ᵥ α⁻¹ 𝒞.◁ T M₁ 𝒞.≈ α⁻¹ 𝒞.∘ᵥ actionˡ B₂
linearˡ⁻¹ = ⟺ (HomCat.conjugate-from (αIso 𝒞.◁ᵢ T M₁) αIso linearˡ)

linearʳ⁻¹ : actionʳ B₁ ∘ᵥ T M₂ ▷ α⁻¹ ≈ α⁻¹ ∘ᵥ actionʳ B₂
linearʳ⁻¹ = ⟺ (conjugate-from (T M₂ ▷ᵢ αIso) αIso linearʳ)
linearʳ⁻¹ : actionʳ B₁ 𝒞.∘ᵥ T M₂ 𝒞.▷ α⁻¹ 𝒞.≈ α⁻¹ 𝒞.∘ᵥ actionʳ B₂
linearʳ⁻¹ = ⟺ (HomCat.conjugate-from (T M₂ 𝒞.▷ᵢ αIso) αIso linearʳ)

αisIso⇒Iso : IsIso {C = hom (C M₁) (C M₂)} α → B₁ ≅ B₂
αisIso⇒Iso : HomCat.IsIso α → B₁ Bimodules.≅ B₂
αisIso⇒Iso αisIso = record
{ from = f
; to = IsIso.inv (αisIso⇒fisIso αisIso)
; iso = IsIso.iso (αisIso⇒fisIso αisIso)
; to = Bimodules.IsIso.inv (αisIso⇒fisIso αisIso)
; iso = Bimodules.IsIso.iso (αisIso⇒fisIso αisIso)
}
Loading