From ffe8409a56231da69b77662503c2946423bccd82 Mon Sep 17 00:00:00 2001 From: Timotej Tomandl <27767427+formrre@users.noreply.github.com> Date: Wed, 25 Oct 2023 15:59:12 +0100 Subject: [PATCH 1/5] wip: Isbell duality --- src/IsbellDuality/IsbellDuality.lagda.md | 48 ++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 src/IsbellDuality/IsbellDuality.lagda.md diff --git a/src/IsbellDuality/IsbellDuality.lagda.md b/src/IsbellDuality/IsbellDuality.lagda.md new file mode 100644 index 000000000..605f868cb --- /dev/null +++ b/src/IsbellDuality/IsbellDuality.lagda.md @@ -0,0 +1,48 @@ + + +```agda +module IsbellDuality.IsbellDuality where + +open import Cat.Functor.Base +open import Cat.Functor.Kan.Nerve +open import Cat.Functor.Hom + +CoPSh : ∀ κ {o ℓ} → Precategory o ℓ → Precategory _ _ +CoPSh κ C = Cat[ C , Sets κ ] ^op + +module _ {o κ} (C : Precategory o κ) where + -- coyoneda embedding + z : Functor C (CoPSh κ C) + z = Functor.op (よ (C ^op)) + +open import Cat.Diagram.Colimit.Base +open import Cat.Diagram.Limit.Base + +module _ {o}{l}{x} {y} {C : Precategory o l} where + + + open import Cat.Diagram.Duals + + is-complete-is-cocomplete-op : is-complete x y C -> is-cocomplete x y (C ^op) + is-complete-is-cocomplete-op isCompl F = Co-limit→Colimit _ (isCompl _) + +module _ {o ℓ} (C : Precategory o ℓ) where + + open import Cat.Instances.Functor.Limits + open import Cat.Instances.Sets.Complete + + CoPSh-cocomplete : ∀ κ → is-cocomplete κ κ (CoPSh κ C) + CoPSh-cocomplete κ = is-complete-is-cocomplete-op {C = Cat[ C , Sets κ ]} (Functor-cat-is-complete (Sets-is-complete {o = κ})) + +Spec : ∀ κ (C : Precategory κ κ) → Functor (CoPSh κ C) (PSh κ C) +Spec κ C = Nerve (z _) + +-- agda refused to figure out implicits quickly so we help it +IsbellDuality : ∀ κ {C : Precategory κ κ} -> _ ⊣ Spec _ C +IsbellDuality κ {C} = Realisation⊣Nerve {C = C} {D = CoPSh κ C} (z C) (CoPSh-cocomplete _ _) +``` From 4f76d29fca245f1b9aaa4afb3d8492d09797147d Mon Sep 17 00:00:00 2001 From: Timotej Tomandl <27767427+formrre@users.noreply.github.com> Date: Fri, 27 Oct 2023 18:30:21 +0100 Subject: [PATCH 2/5] wip: move Isbell duality to Cat.Functor.Kan --- .../IsbellDuality.lagda.md => Cat/Functor/Kan/Isbell.lagda.md} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename src/{IsbellDuality/IsbellDuality.lagda.md => Cat/Functor/Kan/Isbell.lagda.md} (97%) diff --git a/src/IsbellDuality/IsbellDuality.lagda.md b/src/Cat/Functor/Kan/Isbell.lagda.md similarity index 97% rename from src/IsbellDuality/IsbellDuality.lagda.md rename to src/Cat/Functor/Kan/Isbell.lagda.md index 605f868cb..76b49107e 100644 --- a/src/IsbellDuality/IsbellDuality.lagda.md +++ b/src/Cat/Functor/Kan/Isbell.lagda.md @@ -6,7 +6,7 @@ open import Cat.Functor.Adjoint --> ```agda -module IsbellDuality.IsbellDuality where +module Cat.Functor.Kan.Isbell where open import Cat.Functor.Base open import Cat.Functor.Kan.Nerve From 4972e322f3e29a6e3f77cd7afb20e59854de04e1 Mon Sep 17 00:00:00 2001 From: Timotej Tomandl <27767427+formrre@users.noreply.github.com> Date: Mon, 18 Dec 2023 14:16:05 +0000 Subject: [PATCH 3/5] wip: Isbell duality, prose start --- src/Cat/Functor/Kan/Isbell.lagda.md | 37 +++++++++++++++++++++++++++-- src/index.lagda.md | 1 + 2 files changed, 36 insertions(+), 2 deletions(-) diff --git a/src/Cat/Functor/Kan/Isbell.lagda.md b/src/Cat/Functor/Kan/Isbell.lagda.md index 76b49107e..80b2bf53b 100644 --- a/src/Cat/Functor/Kan/Isbell.lagda.md +++ b/src/Cat/Functor/Kan/Isbell.lagda.md @@ -1,3 +1,8 @@ +--- +description: | + We use the construction of Realisation Nerve adjunction to obtain an adjunction between Presheaves and Copresheaves +--- + +# Copresheaves +First we define co-presheaves, where presheaves are the functorial category from a category $\cC ^{op}$ to $\Sets$, +co-presheaves are the opposite of the functor category from $\cC$ to $\Sets$. +```agda CoPSh : ∀ κ {o ℓ} → Precategory o ℓ → Precategory _ _ CoPSh κ C = Cat[ C , Sets κ ] ^op +``` +Co-presheaves come with their own variant of Yoneda embedding, the co-Yoneda embedding $\mathbb{z}$. +The co-Yoneda is just the opposite of the Yoneda embedding on the opposite category. +```agda module _ {o κ} (C : Precategory o κ) where - -- coyoneda embedding z : Functor C (CoPSh κ C) z = Functor.op (よ (C ^op)) - +``` + +We will require the fact that the opposite of a complete category is cocomplete, this is a direct consequence of duality for diagrams +```agda module _ {o}{l}{x} {y} {C : Precategory o l} where @@ -30,7 +53,11 @@ module _ {o}{l}{x} {y} {C : Precategory o l} where is-complete-is-cocomplete-op : is-complete x y C -> is-cocomplete x y (C ^op) is-complete-is-cocomplete-op isCompl F = Co-limit→Colimit _ (isCompl _) +``` +Next we prove that Copresheaves are co-complete this is a direct consequence of opposites swapping completeness for cocompletess, +together with completeness of the functor category and Sets +```agda module _ {o ℓ} (C : Precategory o ℓ) where open import Cat.Instances.Functor.Limits @@ -38,10 +65,16 @@ module _ {o ℓ} (C : Precategory o ℓ) where CoPSh-cocomplete : ∀ κ → is-cocomplete κ κ (CoPSh κ C) CoPSh-cocomplete κ = is-complete-is-cocomplete-op {C = Cat[ C , Sets κ ]} (Functor-cat-is-complete (Sets-is-complete {o = κ})) +``` +As a next step we define half of the adjunction going from Co-presheaves to presheaves. This is the nerve of the Co-yoneda embedding +```agda Spec : ∀ κ (C : Precategory κ κ) → Functor (CoPSh κ C) (PSh κ C) Spec κ C = Nerve (z _) +``` +Now the Isbell duality is just the abstract non-sense wrapping the Realisation⊣Nerve duality for co-presheaves as they are co-complete +```agda -- agda refused to figure out implicits quickly so we help it IsbellDuality : ∀ κ {C : Precategory κ κ} -> _ ⊣ Spec _ C IsbellDuality κ {C} = Realisation⊣Nerve {C = C} {D = CoPSh κ C} (z C) (CoPSh-cocomplete _ _) diff --git a/src/index.lagda.md b/src/index.lagda.md index 79192d81c..606607558 100644 --- a/src/index.lagda.md +++ b/src/index.lagda.md @@ -440,6 +440,7 @@ open import Cat.Functor.Kan.Adjoint -- Adjoints are Kan extensions open import Cat.Functor.Kan.Pointwise -- Pointwise Kan extensions open import Cat.Functor.Kan.Unique -- Uniqueness of Kan extensions open import Cat.Functor.Kan.Representable -- Kan extensions as Hom isomorphisms +open import Cat.Functor.Kan.Isbell -- Isbell duality between Presheaves and Copresheaves ``` Properties of Hom-functors, and (direct) consequences of the Yoneda From 5349e6ad844e4ea112b00b0521eaa661a6ed5137 Mon Sep 17 00:00:00 2001 From: Timotej Tomandl <27767427+formrre@users.noreply.github.com> Date: Mon, 18 Dec 2023 14:35:57 +0000 Subject: [PATCH 4/5] wip: Second pass of Isbell duality prose --- src/Cat/Functor/Kan/Isbell.lagda.md | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/Cat/Functor/Kan/Isbell.lagda.md b/src/Cat/Functor/Kan/Isbell.lagda.md index 80b2bf53b..7637690d8 100644 --- a/src/Cat/Functor/Kan/Isbell.lagda.md +++ b/src/Cat/Functor/Kan/Isbell.lagda.md @@ -21,8 +21,8 @@ open import Cat.Functor.Kan.Nerve open import Cat.Functor.Hom ``` --> - -# Copresheaves +# Isbell duality +## Copresheaves First we define co-presheaves, where presheaves are the functorial category from a category $\cC ^{op}$ to $\Sets$, co-presheaves are the opposite of the functor category from $\cC$ to $\Sets$. ```agda @@ -31,7 +31,7 @@ CoPSh κ C = Cat[ C , Sets κ ] ^op ``` Co-presheaves come with their own variant of Yoneda embedding, the co-Yoneda embedding $\mathbb{z}$. -The co-Yoneda is just the opposite of the Yoneda embedding on the opposite category. +The co-Yoneda embedding is just the opposite of the Yoneda embedding on the opposite category. ```agda module _ {o κ} (C : Precategory o κ) where z : Functor C (CoPSh κ C) @@ -48,7 +48,6 @@ We will require the fact that the opposite of a complete category is cocomplete, ```agda module _ {o}{l}{x} {y} {C : Precategory o l} where - open import Cat.Diagram.Duals is-complete-is-cocomplete-op : is-complete x y C -> is-cocomplete x y (C ^op) @@ -67,15 +66,23 @@ module _ {o ℓ} (C : Precategory o ℓ) where CoPSh-cocomplete κ = is-complete-is-cocomplete-op {C = Cat[ C , Sets κ ]} (Functor-cat-is-complete (Sets-is-complete {o = κ})) ``` +## Isbell duality itself + As a next step we define half of the adjunction going from Co-presheaves to presheaves. This is the nerve of the Co-yoneda embedding ```agda Spec : ∀ κ (C : Precategory κ κ) → Functor (CoPSh κ C) (PSh κ C) Spec κ C = Nerve (z _) ``` -Now the Isbell duality is just the abstract non-sense wrapping the Realisation⊣Nerve duality for co-presheaves as they are co-complete +Now the Isbell duality is just a wrapping of the abstract non-sense coming from the Realisation⊣Nerve duality for co-presheaves as they are co-complete ```agda -- agda refused to figure out implicits quickly so we help it IsbellDuality : ∀ κ {C : Precategory κ κ} -> _ ⊣ Spec _ C IsbellDuality κ {C} = Realisation⊣Nerve {C = C} {D = CoPSh κ C} (z C) (CoPSh-cocomplete _ _) ``` + + From 0ac02612bdcdbb26f1471e0eed5102f81eb86c28 Mon Sep 17 00:00:00 2001 From: Timotej Tomandl <27767427+formrre@users.noreply.github.com> Date: Mon, 18 Dec 2023 14:52:39 +0000 Subject: [PATCH 5/5] wip: Isbell duality, sort imports and full stops --- src/Cat/Functor/Kan/Isbell.lagda.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Cat/Functor/Kan/Isbell.lagda.md b/src/Cat/Functor/Kan/Isbell.lagda.md index 7637690d8..ebe6daa95 100644 --- a/src/Cat/Functor/Kan/Isbell.lagda.md +++ b/src/Cat/Functor/Kan/Isbell.lagda.md @@ -5,8 +5,8 @@ description: | @@ -44,7 +44,7 @@ open import Cat.Diagram.Limit.Base ``` --> -We will require the fact that the opposite of a complete category is cocomplete, this is a direct consequence of duality for diagrams +We will require the fact that the opposite of a complete category is cocomplete, this is a direct consequence of duality for diagrams. ```agda module _ {o}{l}{x} {y} {C : Precategory o l} where @@ -55,7 +55,7 @@ module _ {o}{l}{x} {y} {C : Precategory o l} where ``` Next we prove that Copresheaves are co-complete this is a direct consequence of opposites swapping completeness for cocompletess, -together with completeness of the functor category and Sets +together with completeness of the functor category and Sets. ```agda module _ {o ℓ} (C : Precategory o ℓ) where @@ -68,13 +68,13 @@ module _ {o ℓ} (C : Precategory o ℓ) where ## Isbell duality itself -As a next step we define half of the adjunction going from Co-presheaves to presheaves. This is the nerve of the Co-yoneda embedding +As a next step we define half of the adjunction going from Co-presheaves to presheaves. This is the nerve of the Co-yoneda embedding. ```agda Spec : ∀ κ (C : Precategory κ κ) → Functor (CoPSh κ C) (PSh κ C) Spec κ C = Nerve (z _) ``` -Now the Isbell duality is just a wrapping of the abstract non-sense coming from the Realisation⊣Nerve duality for co-presheaves as they are co-complete +Now the Isbell duality is just a wrapping of the abstract non-sense coming from the Realisation⊣Nerve duality for co-presheaves as they are co-complete. ```agda -- agda refused to figure out implicits quickly so we help it IsbellDuality : ∀ κ {C : Precategory κ κ} -> _ ⊣ Spec _ C