diff --git a/CODINGSTYLE.md b/CODINGSTYLE.md index b02c0b2eb0..6e0d1a3f12 100644 --- a/CODINGSTYLE.md +++ b/CODINGSTYLE.md @@ -284,7 +284,7 @@ the `agda-unimath` library: need to sort them by hand. - The library doesn't use - [variables](https://agda.readthedocs.io/en/v2.6.3/language/generalization-of-declared-variables.html) + [variables](https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html) at the moment. All variables are declared either as parameters of an anonymous module or in the type specification of a construction. diff --git a/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md index e2bc34c8a3..0eb4646cc4 100644 --- a/MIXFIX-OPERATORS.md +++ b/MIXFIX-OPERATORS.md @@ -2,7 +2,7 @@ This document outlines our choices of conventions for setting precedence levels and associativity of -[mixfix operators in Agda](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html), +[mixfix operators in Agda](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html), and provides guidelines for this. ## Mixfix operators in Agda @@ -16,7 +16,7 @@ and mixfix operators in Agda is to make the code more readable by using commonly accepted notation for widely used operators. Mixfix operators can each be assigned a -[precedence level](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html#precedence). +[precedence level](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html#precedence). This can in principle be any signed fractional value, although we prefer them to be non-negative integral values. The higher this value is, the higher precedence the operator has, meaning it is evaluated before operators with lower @@ -32,7 +32,7 @@ is parsed as `x +ℕ (y *ℕ z)`. In addition to a precedence level, every mixfix operator can be defined to be either left or right -[associative](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html#associativity). +[associative](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html#associativity). It can be beneficial to define associativity of operators, to avoid excessively parenthesized expressions. The parenthization should, however, never be omitted when this can make the code more ambiguous or harder to read. diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index d53f0377e8..c93bad90f1 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -13,6 +13,7 @@ ```agda module category-theory where +open import category-theory.adjunctions-large-categories public open import category-theory.adjunctions-large-precategories public open import category-theory.anafunctors-categories public open import category-theory.anafunctors-precategories public @@ -48,6 +49,7 @@ open import category-theory.function-precategories public open import category-theory.functors-categories public open import category-theory.functors-from-small-to-large-categories public open import category-theory.functors-from-small-to-large-precategories public +open import category-theory.functors-large-categories public open import category-theory.functors-large-precategories public open import category-theory.functors-precategories public open import category-theory.groupoids public @@ -78,6 +80,7 @@ open import category-theory.natural-isomorphisms-maps-precategories public open import category-theory.natural-numbers-object-precategories public open import category-theory.natural-transformations-functors-categories public open import category-theory.natural-transformations-functors-from-small-to-large-precategories public +open import category-theory.natural-transformations-functors-large-categories public open import category-theory.natural-transformations-functors-large-precategories public open import category-theory.natural-transformations-functors-precategories public open import category-theory.natural-transformations-maps-categories public diff --git a/src/category-theory/adjunctions-large-categories.lagda.md b/src/category-theory/adjunctions-large-categories.lagda.md new file mode 100644 index 0000000000..227d94a5f6 --- /dev/null +++ b/src/category-theory/adjunctions-large-categories.lagda.md @@ -0,0 +1,505 @@ +# Adjunctions between large categories + +```agda +module category-theory.adjunctions-large-categories where +``` + +
Imports + +```agda +open import category-theory.adjunctions-large-precategories +open import category-theory.functors-large-categories +open import category-theory.large-categories +open import category-theory.natural-transformations-functors-large-categories + +open import foundation.commuting-squares-of-maps +open import foundation.equivalences +open import foundation.identity-types +open import foundation.universe-levels +``` + +
+ +## Idea + +Let `C` and `D` be two [large categories](category-theory.large-categories.md). +Two [functors](category-theory.functors-large-categories.md) `F : C → D` and +`G : D → C` constitute an **adjoint pair** if + +- for each pair of objects `X` in `C` and `Y` in `D`, there is an + [equivalence](foundation-core.equivalences.md) + `ϕ X Y : hom X (G Y) ≃ hom (F X) Y` such that +- for every pair of morhpisms `f : X₂ → X₁` and `g : Y₁ → Y₂` the following + square commutes: + +```text + ϕ X₁ Y₁ + hom X₁ (G Y₁) --------> hom (F X₁) Y₁ + | | + G g ∘ _ ∘ f | | g ∘ _ ∘ F f + | | + v v + hom X₂ (G Y₂) --------> hom (F X₂) Y₂ + ϕ X₂ Y₂ +``` + +In this case we say that `F` is **left adjoint** to `G` and `G` is **right +adjoint** to `F` and write this as `F ⊣ G`. + +## Definition + +### The predicate of being an adjoint pair of functors + +```agda +module _ + {αC αD γF γG : Level → Level} + {βC βD : Level → Level → Level} + (C : Large-Category αC βC) + (D : Large-Category αD βD) + (F : functor-Large-Category γF C D) + (G : functor-Large-Category γG D C) + where + + family-of-equivalences-adjoint-pair-Large-Category : UUω + family-of-equivalences-adjoint-pair-Large-Category = + family-of-equivalences-adjoint-pair-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + + naturality-family-of-equivalences-adjoint-pair-Large-Category : + family-of-equivalences-adjoint-pair-Large-Category → UUω + naturality-family-of-equivalences-adjoint-pair-Large-Category = + naturality-family-of-equivalences-adjoint-pair-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + + is-adjoint-pair-Large-Category : UUω + is-adjoint-pair-Large-Category = + is-adjoint-pair-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + + equiv-is-adjoint-pair-Large-Category : + is-adjoint-pair-Large-Category → + family-of-equivalences-adjoint-pair-Large-Category + equiv-is-adjoint-pair-Large-Category = + equiv-is-adjoint-pair-Large-Precategory + + naturality-equiv-is-adjoint-pair-Large-Category : + (H : is-adjoint-pair-Large-Category) → + naturality-family-of-equivalences-adjoint-pair-Large-Category + ( equiv-is-adjoint-pair-Large-Precategory H) + naturality-equiv-is-adjoint-pair-Large-Category = + naturality-equiv-is-adjoint-pair-Large-Precategory + + map-equiv-is-adjoint-pair-Large-Category : + (H : is-adjoint-pair-Large-Category) {l1 l2 : Level} + (X : obj-Large-Category C l1) (Y : obj-Large-Category D l2) → + hom-Large-Category C X (obj-functor-Large-Category D C G Y) → + hom-Large-Category D (obj-functor-Large-Category C D F X) Y + map-equiv-is-adjoint-pair-Large-Category = + map-equiv-is-adjoint-pair-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + + inv-equiv-is-adjoint-pair-Large-Category : + (H : is-adjoint-pair-Large-Category) {l1 l2 : Level} + (X : obj-Large-Category C l1) (Y : obj-Large-Category D l2) → + hom-Large-Category D (obj-functor-Large-Category C D F X) Y ≃ + hom-Large-Category C X (obj-functor-Large-Category D C G Y) + inv-equiv-is-adjoint-pair-Large-Category = + inv-equiv-is-adjoint-pair-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + + map-inv-equiv-is-adjoint-pair-Large-Category : + (H : is-adjoint-pair-Large-Category) {l1 l2 : Level} + (X : obj-Large-Category C l1) (Y : obj-Large-Category D l2) → + hom-Large-Category D (obj-functor-Large-Category C D F X) Y → + hom-Large-Category C X (obj-functor-Large-Category D C G Y) + map-inv-equiv-is-adjoint-pair-Large-Category = + map-inv-equiv-is-adjoint-pair-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + + naturality-inv-equiv-is-adjoint-pair-Large-Category : + ( H : is-adjoint-pair-Large-Category) + { l1 l2 l3 l4 : Level} + { X1 : obj-Large-Category C l1} + { X2 : obj-Large-Category C l2} + { Y1 : obj-Large-Category D l3} + { Y2 : obj-Large-Category D l4} + ( f : hom-Large-Category C X2 X1) + ( g : hom-Large-Category D Y1 Y2) → + coherence-square-maps + ( map-inv-equiv-is-adjoint-pair-Large-Category H X1 Y1) + ( λ h → + comp-hom-Large-Category D + ( comp-hom-Large-Category D g h) + ( hom-functor-Large-Category C D F f)) + ( λ h → + comp-hom-Large-Category C + ( comp-hom-Large-Category C (hom-functor-Large-Category D C G g) h) + ( f)) + ( map-inv-equiv-is-adjoint-pair-Large-Category H X2 Y2) + naturality-inv-equiv-is-adjoint-pair-Large-Category = + naturality-inv-equiv-is-adjoint-pair-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) +``` + +### The predicate of being a left adjoint + +```agda +module _ + {αC αD γF γG : Level → Level} + {βC βD : Level → Level → Level} + {C : Large-Category αC βC} + {D : Large-Category αD βD} + (G : functor-Large-Category γG D C) + (F : functor-Large-Category γF C D) + where + + is-left-adjoint-functor-Large-Category : UUω + is-left-adjoint-functor-Large-Category = + is-adjoint-pair-Large-Category C D F G +``` + +### The predicate of being a right adjoint + +```agda +module _ + {αC αD γF γG : Level → Level} + {βC βD : Level → Level → Level} + {C : Large-Category αC βC} + {D : Large-Category αD βD} + (F : functor-Large-Category γF C D) + (G : functor-Large-Category γG D C) + where + + is-right-adjoint-functor-Large-Category : UUω + is-right-adjoint-functor-Large-Category = + is-adjoint-pair-Large-Category C D F G +``` + +### Adjunctions of large precategories + +```agda +module _ + {αC αD : Level → Level} + {βC βD : Level → Level → Level} + (γ δ : Level → Level) + (C : Large-Category αC βC) + (D : Large-Category αD βD) + where + + Adjunction-Large-Category : UUω + Adjunction-Large-Category = + Adjunction-Large-Precategory γ δ + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + +module _ + {αC αD : Level → Level} + {βC βD : Level → Level → Level} + {γ δ : Level → Level} + (C : Large-Category αC βC) + (D : Large-Category αD βD) + (F : Adjunction-Large-Category γ δ C D) + where + + left-adjoint-Adjunction-Large-Category : + functor-Large-Category γ C D + left-adjoint-Adjunction-Large-Category = + left-adjoint-Adjunction-Large-Precategory F + + right-adjoint-Adjunction-Large-Category : + functor-Large-Category δ D C + right-adjoint-Adjunction-Large-Category = + right-adjoint-Adjunction-Large-Precategory F + + is-adjoint-pair-Adjunction-Large-Category : + is-adjoint-pair-Large-Category C D + ( left-adjoint-Adjunction-Large-Category) + ( right-adjoint-Adjunction-Large-Category) + is-adjoint-pair-Adjunction-Large-Category = + is-adjoint-pair-Adjunction-Large-Precategory F + + obj-left-adjoint-Adjunction-Large-Category : + {l : Level} → obj-Large-Category C l → obj-Large-Category D (γ l) + obj-left-adjoint-Adjunction-Large-Category = + obj-left-adjoint-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + hom-left-adjoint-Adjunction-Large-Category : + {l1 l2 : Level} + {X : obj-Large-Category C l1} + {Y : obj-Large-Category C l2} → + hom-Large-Category C X Y → + hom-Large-Category D + ( obj-left-adjoint-Adjunction-Large-Category X) + ( obj-left-adjoint-Adjunction-Large-Category Y) + hom-left-adjoint-Adjunction-Large-Category = + hom-left-adjoint-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + preserves-id-left-adjoint-Adjunction-Large-Category : + {l1 : Level} + (X : obj-Large-Category C l1) → + hom-left-adjoint-Adjunction-Large-Category + ( id-hom-Large-Category C {X = X}) ＝ + id-hom-Large-Category D + preserves-id-left-adjoint-Adjunction-Large-Category = + preserves-id-left-adjoint-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + obj-right-adjoint-Adjunction-Large-Category : + {l1 : Level} → obj-Large-Category D l1 → obj-Large-Category C (δ l1) + obj-right-adjoint-Adjunction-Large-Category = + obj-right-adjoint-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + hom-right-adjoint-Adjunction-Large-Category : + {l1 l2 : Level} + {X : obj-Large-Category D l1} + {Y : obj-Large-Category D l2} → + hom-Large-Category D X Y → + hom-Large-Category C + ( obj-right-adjoint-Adjunction-Large-Category X) + ( obj-right-adjoint-Adjunction-Large-Category Y) + hom-right-adjoint-Adjunction-Large-Category = + hom-right-adjoint-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + preserves-id-right-adjoint-Adjunction-Large-Category : + {l : Level} + (Y : obj-Large-Category D l) → + hom-right-adjoint-Adjunction-Large-Category + ( id-hom-Large-Category D {X = Y}) ＝ + id-hom-Large-Category C + preserves-id-right-adjoint-Adjunction-Large-Category = + preserves-id-right-adjoint-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + equiv-is-adjoint-pair-Adjunction-Large-Category : + family-of-equivalences-adjoint-pair-Large-Category C D + ( left-adjoint-Adjunction-Large-Category) + ( right-adjoint-Adjunction-Large-Category) + equiv-is-adjoint-pair-Adjunction-Large-Category = + equiv-is-adjoint-pair-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + map-equiv-is-adjoint-pair-Adjunction-Large-Category : + {l1 l2 : Level} + (X : obj-Large-Category C l1) + (Y : obj-Large-Category D l2) → + hom-Large-Category C + ( X) + ( obj-right-adjoint-Adjunction-Large-Category Y) → + hom-Large-Category D + ( obj-left-adjoint-Adjunction-Large-Category X) + ( Y) + map-equiv-is-adjoint-pair-Adjunction-Large-Category = + map-equiv-is-adjoint-pair-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + naturality-equiv-is-adjoint-pair-Adjunction-Large-Category : + naturality-family-of-equivalences-adjoint-pair-Large-Category C D + ( left-adjoint-Adjunction-Large-Category) + ( right-adjoint-Adjunction-Large-Category) + ( equiv-is-adjoint-pair-Adjunction-Large-Category) + naturality-equiv-is-adjoint-pair-Adjunction-Large-Category = + naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + inv-equiv-is-adjoint-pair-Adjunction-Large-Category : + {l1 l2 : Level} + (X : obj-Large-Category C l1) + (Y : obj-Large-Category D l2) → + hom-Large-Category D + ( obj-left-adjoint-Adjunction-Large-Category X) + ( Y) ≃ + hom-Large-Category C + ( X) + ( obj-right-adjoint-Adjunction-Large-Category Y) + inv-equiv-is-adjoint-pair-Adjunction-Large-Category = + inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + map-inv-equiv-is-adjoint-pair-Adjunction-Large-Category : + {l1 l2 : Level} + (X : obj-Large-Category C l1) + (Y : obj-Large-Category D l2) → + hom-Large-Category D + ( obj-left-adjoint-Adjunction-Large-Category X) + ( Y) → + hom-Large-Category C + ( X) + ( obj-right-adjoint-Adjunction-Large-Category Y) + map-inv-equiv-is-adjoint-pair-Adjunction-Large-Category = + map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Category : + {l1 l2 l3 l4 : Level} + {X1 : obj-Large-Category C l1} + {X2 : obj-Large-Category C l2} + {Y1 : obj-Large-Category D l3} + {Y2 : obj-Large-Category D l4} + (f : hom-Large-Category C X2 X1) + (g : hom-Large-Category D Y1 Y2) → + coherence-square-maps + ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Category X1 Y1) + ( λ h → + comp-hom-Large-Category D + ( comp-hom-Large-Category D g h) + ( hom-left-adjoint-Adjunction-Large-Category f)) + ( λ h → + comp-hom-Large-Category C + ( comp-hom-Large-Category C + ( hom-right-adjoint-Adjunction-Large-Category g) + ( h)) + ( f)) + ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Category X2 Y2) + naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Category = + naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) +``` + +### The unit of an adjunction + +Given an adjoint pair `F ⊣ G`, we construct a natural transformation +`η : id → G ∘ F` called the **unit** of the adjunction. + +```agda +module _ + {αC αD : Level → Level} {βC βD : Level → Level → Level} {γ δ : Level → Level} + (C : Large-Category αC βC) (D : Large-Category αD βD) + (F : Adjunction-Large-Category γ δ C D) + where + + hom-unit-Adjunction-Large-Category : + family-of-morphisms-functor-Large-Category C C + ( id-functor-Large-Category C) + ( comp-functor-Large-Category C D C + ( right-adjoint-Adjunction-Large-Category C D F) + ( left-adjoint-Adjunction-Large-Category C D F)) + hom-unit-Adjunction-Large-Category = + hom-unit-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + naturality-unit-Adjunction-Large-Category : + naturality-family-of-morphisms-functor-Large-Category C C + ( id-functor-Large-Category C) + ( comp-functor-Large-Category C D C + ( right-adjoint-Adjunction-Large-Category C D F) + ( left-adjoint-Adjunction-Large-Category C D F)) + ( hom-unit-Adjunction-Large-Category) + naturality-unit-Adjunction-Large-Category = + naturality-unit-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + unit-Adjunction-Large-Category : + natural-transformation-Large-Category C C + ( id-functor-Large-Category C) + ( comp-functor-Large-Category C D C + ( right-adjoint-Adjunction-Large-Category C D F) + ( left-adjoint-Adjunction-Large-Category C D F)) + unit-Adjunction-Large-Category = + unit-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) +``` + +### The counit of an adjunction + +Given an adjoint pair `F ⊣ G`, we construct a natural transformation +`ε : F ∘ G → id` called the **counit** of the adjunction. + +```agda +module _ + {αC αD : Level → Level} {βC βD : Level → Level → Level} {γ δ : Level → Level} + (C : Large-Category αC βC) (D : Large-Category αD βD) + (F : Adjunction-Large-Category γ δ C D) + where + + hom-counit-Adjunction-Large-Category : + family-of-morphisms-functor-Large-Category D D + ( comp-functor-Large-Category D C D + ( left-adjoint-Adjunction-Large-Category C D F) + ( right-adjoint-Adjunction-Large-Category C D F)) + ( id-functor-Large-Category D) + hom-counit-Adjunction-Large-Category = + hom-counit-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + naturality-counit-Adjunction-Large-Category : + naturality-family-of-morphisms-functor-Large-Category D D + ( comp-functor-Large-Category D C D + ( left-adjoint-Adjunction-Large-Category C D F) + ( right-adjoint-Adjunction-Large-Category C D F)) + ( id-functor-Large-Category D) + ( hom-counit-Adjunction-Large-Category) + naturality-counit-Adjunction-Large-Category = + naturality-counit-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + counit-Adjunction-Large-Category : + natural-transformation-Large-Category D D + ( comp-functor-Large-Category D C D + ( left-adjoint-Adjunction-Large-Category C D F) + ( right-adjoint-Adjunction-Large-Category C D F)) + ( id-functor-Large-Category D) + counit-Adjunction-Large-Category = + counit-Adjunction-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) +``` diff --git a/src/category-theory/adjunctions-large-precategories.lagda.md b/src/category-theory/adjunctions-large-precategories.lagda.md index b2e769fb1d..0429b48e51 100644 --- a/src/category-theory/adjunctions-large-precategories.lagda.md +++ b/src/category-theory/adjunctions-large-precategories.lagda.md @@ -34,13 +34,13 @@ Let `C` and `D` be two square commutes: ```text - ϕ X₁ Y₁ - hom X₁ (G Y₁) --------> hom (F X₁) Y₁ - | | -G g ∘ _ ∘ f | | g ∘ _ ∘ F f - | | - v v - hom X₂ (G Y₂) --------> hom (F X₂) Y₂ + ϕ X₁ Y₁ + hom X₁ (G Y₁) --------> hom (F X₁) Y₁ + | | + G g ∘ _ ∘ f | | g ∘ _ ∘ F f + | | + v v + hom X₂ (G Y₂) --------> hom (F X₂) Y₂ ϕ X₂ Y₂ ``` @@ -49,65 +49,71 @@ adjoint** to `F` and write this as `F ⊣ G`. ## Definition +### The predicate of being an adjoint pair of functors + ```agda module _ {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} - {C : Large-Precategory αC βC} - {D : Large-Precategory αD βD} - (F : functor-Large-Precategory C D γF) - (G : functor-Large-Precategory D C γG) + (C : Large-Precategory αC βC) + (D : Large-Precategory αD βD) + (F : functor-Large-Precategory γF C D) + (G : functor-Large-Precategory γG D C) where + family-of-equivalences-adjoint-pair-Large-Precategory : UUω + family-of-equivalences-adjoint-pair-Large-Precategory = + {l1 l2 : Level} (X : obj-Large-Precategory C l1) + (Y : obj-Large-Precategory D l2) → + hom-Large-Precategory C X (obj-functor-Large-Precategory G Y) ≃ + hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y + + naturality-family-of-equivalences-adjoint-pair-Large-Precategory : + family-of-equivalences-adjoint-pair-Large-Precategory → UUω + naturality-family-of-equivalences-adjoint-pair-Large-Precategory e = + { l1 l2 l3 l4 : Level} + { X1 : obj-Large-Precategory C l1} + { X2 : obj-Large-Precategory C l2} + { Y1 : obj-Large-Precategory D l3} + { Y2 : obj-Large-Precategory D l4} + ( f : hom-Large-Precategory C X2 X1) + ( g : hom-Large-Precategory D Y1 Y2) → + coherence-square-maps + ( map-equiv (e X1 Y1)) + ( λ h → + comp-hom-Large-Precategory C + ( comp-hom-Large-Precategory C + ( hom-functor-Large-Precategory G g) + ( h)) + ( f)) + ( λ h → + comp-hom-Large-Precategory D + ( comp-hom-Large-Precategory D g h) + ( hom-functor-Large-Precategory F f)) + ( map-equiv (e X2 Y2)) + record is-adjoint-pair-Large-Precategory : UUω where field equiv-is-adjoint-pair-Large-Precategory : - {l1 l2 : Level} (X : obj-Large-Precategory C l1) - (Y : obj-Large-Precategory D l2) → - ( hom-Large-Precategory C - ( X) - ( obj-functor-Large-Precategory G Y)) ≃ - ( hom-Large-Precategory D - ( obj-functor-Large-Precategory F X) - ( Y)) + family-of-equivalences-adjoint-pair-Large-Precategory naturality-equiv-is-adjoint-pair-Large-Precategory : - { l1 l2 l3 l4 : Level} - { X1 : obj-Large-Precategory C l1} - { X2 : obj-Large-Precategory C l2} - { Y1 : obj-Large-Precategory D l3} - { Y2 : obj-Large-Precategory D l4} - ( f : hom-Large-Precategory C X2 X1) - ( g : hom-Large-Precategory D Y1 Y2) → - coherence-square-maps - ( map-equiv (equiv-is-adjoint-pair-Large-Precategory X1 Y1)) - ( λ h → - comp-hom-Large-Precategory C - ( comp-hom-Large-Precategory C - ( hom-functor-Large-Precategory G g) - ( h)) - ( f)) - ( λ h → - comp-hom-Large-Precategory D - ( comp-hom-Large-Precategory D g h) - ( hom-functor-Large-Precategory F f)) - ( map-equiv (equiv-is-adjoint-pair-Large-Precategory X2 Y2)) + naturality-family-of-equivalences-adjoint-pair-Large-Precategory + equiv-is-adjoint-pair-Large-Precategory open is-adjoint-pair-Large-Precategory public map-equiv-is-adjoint-pair-Large-Precategory : (H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → - ( hom-Large-Precategory C X (obj-functor-Large-Precategory G Y)) → - ( hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y) + hom-Large-Precategory C X (obj-functor-Large-Precategory G Y) → + hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y map-equiv-is-adjoint-pair-Large-Precategory H X Y = map-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y) inv-equiv-is-adjoint-pair-Large-Precategory : - (H : is-adjoint-pair-Large-Precategory) - {l1 l2 : Level} - (X : obj-Large-Precategory C l1) - (Y : obj-Large-Precategory D l2) → + (H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level} + (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y ≃ hom-Large-Precategory C X (obj-functor-Large-Precategory G Y) inv-equiv-is-adjoint-pair-Large-Precategory H X Y = @@ -115,8 +121,7 @@ module _ map-inv-equiv-is-adjoint-pair-Large-Precategory : (H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level} - (X : obj-Large-Precategory C l1) - (Y : obj-Large-Precategory D l2) → + (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y → hom-Large-Precategory C X (obj-functor-Large-Precategory G Y) map-inv-equiv-is-adjoint-pair-Large-Precategory H X Y = @@ -158,160 +163,161 @@ module _ ( hom-functor-Large-Precategory F f)) ( equiv-is-adjoint-pair-Large-Precategory H X2 Y2) ( naturality-equiv-is-adjoint-pair-Large-Precategory H f g) +``` + +### The predicate of being a left adjoint +```agda module _ {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} - {C : Large-Precategory αC βC} - {D : Large-Precategory αD βD} - (G : functor-Large-Precategory D C γG) - (F : functor-Large-Precategory C D γF) + (C : Large-Precategory αC βC) + (D : Large-Precategory αD βD) + (G : functor-Large-Precategory γG D C) + (F : functor-Large-Precategory γF C D) where is-left-adjoint-functor-Large-Precategory : UUω is-left-adjoint-functor-Large-Precategory = - is-adjoint-pair-Large-Precategory F G + is-adjoint-pair-Large-Precategory C D F G +``` + +### The predicate of being a right adjoint +```agda module _ {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} - {C : Large-Precategory αC βC} - {D : Large-Precategory αD βD} - (F : functor-Large-Precategory C D γF) - (G : functor-Large-Precategory D C γG) + (C : Large-Precategory αC βC) + (D : Large-Precategory αD βD) + (F : functor-Large-Precategory γF C D) + (G : functor-Large-Precategory γG D C) where is-right-adjoint-functor-Large-Precategory : UUω is-right-adjoint-functor-Large-Precategory = - is-adjoint-pair-Large-Precategory F G + is-adjoint-pair-Large-Precategory C D F G +``` + +### Adjunctions of large precategories +```agda module _ {αC αD : Level → Level} {βC βD : Level → Level → Level} + (γ δ : Level → Level) (C : Large-Precategory αC βC) (D : Large-Precategory αD βD) where record Adjunction-Large-Precategory : UUω where field - level-left-adjoint-Adjunction-Large-Precategory : - Level → Level left-adjoint-Adjunction-Large-Precategory : - functor-Large-Precategory C D - level-left-adjoint-Adjunction-Large-Precategory - level-right-adjoint-Adjunction-Large-Precategory : - Level → Level + functor-Large-Precategory γ C D right-adjoint-Adjunction-Large-Precategory : - functor-Large-Precategory D C - level-right-adjoint-Adjunction-Large-Precategory + functor-Large-Precategory δ D C is-adjoint-pair-Adjunction-Large-Precategory : - is-adjoint-pair-Large-Precategory + is-adjoint-pair-Large-Precategory C D left-adjoint-Adjunction-Large-Precategory right-adjoint-Adjunction-Large-Precategory open Adjunction-Large-Precategory public +module _ + {αC αD : Level → Level} + {βC βD : Level → Level → Level} + {γ δ : Level → Level} + (C : Large-Precategory αC βC) + (D : Large-Precategory αD βD) + (FG : Adjunction-Large-Precategory γ δ C D) + where + obj-left-adjoint-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) {l : Level} → - obj-Large-Precategory C l → - obj-Large-Precategory D - ( level-left-adjoint-Adjunction-Large-Precategory FG l) - obj-left-adjoint-Adjunction-Large-Precategory FG = + {l : Level} → obj-Large-Precategory C l → obj-Large-Precategory D (γ l) + obj-left-adjoint-Adjunction-Large-Precategory = obj-functor-Large-Precategory ( left-adjoint-Adjunction-Large-Precategory FG) hom-left-adjoint-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) {l1 l2 : Level} {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2} → hom-Large-Precategory C X Y → hom-Large-Precategory D - ( obj-left-adjoint-Adjunction-Large-Precategory FG X) - ( obj-left-adjoint-Adjunction-Large-Precategory FG Y) - hom-left-adjoint-Adjunction-Large-Precategory FG = + ( obj-left-adjoint-Adjunction-Large-Precategory X) + ( obj-left-adjoint-Adjunction-Large-Precategory Y) + hom-left-adjoint-Adjunction-Large-Precategory = hom-functor-Large-Precategory ( left-adjoint-Adjunction-Large-Precategory FG) preserves-id-left-adjoint-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) - {l1 : Level} - (X : obj-Large-Precategory C l1) → - hom-left-adjoint-Adjunction-Large-Precategory FG + {l1 : Level} (X : obj-Large-Precategory C l1) → + hom-left-adjoint-Adjunction-Large-Precategory ( id-hom-Large-Precategory C {X = X}) ＝ id-hom-Large-Precategory D - preserves-id-left-adjoint-Adjunction-Large-Precategory FG X = + preserves-id-left-adjoint-Adjunction-Large-Precategory X = preserves-id-functor-Large-Precategory ( left-adjoint-Adjunction-Large-Precategory FG) obj-right-adjoint-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) - {l1 : Level} → - obj-Large-Precategory D l1 → - obj-Large-Precategory C - ( level-right-adjoint-Adjunction-Large-Precategory FG l1) - obj-right-adjoint-Adjunction-Large-Precategory FG = + {l1 : Level} → obj-Large-Precategory D l1 → obj-Large-Precategory C (δ l1) + obj-right-adjoint-Adjunction-Large-Precategory = obj-functor-Large-Precategory ( right-adjoint-Adjunction-Large-Precategory FG) hom-right-adjoint-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) {l1 l2 : Level} {X : obj-Large-Precategory D l1} {Y : obj-Large-Precategory D l2} → hom-Large-Precategory D X Y → hom-Large-Precategory C - ( obj-right-adjoint-Adjunction-Large-Precategory FG X) - ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) - hom-right-adjoint-Adjunction-Large-Precategory FG = + ( obj-right-adjoint-Adjunction-Large-Precategory X) + ( obj-right-adjoint-Adjunction-Large-Precategory Y) + hom-right-adjoint-Adjunction-Large-Precategory = hom-functor-Large-Precategory ( right-adjoint-Adjunction-Large-Precategory FG) preserves-id-right-adjoint-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) {l : Level} (Y : obj-Large-Precategory D l) → - hom-right-adjoint-Adjunction-Large-Precategory FG + hom-right-adjoint-Adjunction-Large-Precategory ( id-hom-Large-Precategory D {X = Y}) ＝ id-hom-Large-Precategory C - preserves-id-right-adjoint-Adjunction-Large-Precategory FG Y = + preserves-id-right-adjoint-Adjunction-Large-Precategory Y = preserves-id-functor-Large-Precategory ( right-adjoint-Adjunction-Large-Precategory FG) equiv-is-adjoint-pair-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory C ( X) - ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) ≃ + ( obj-right-adjoint-Adjunction-Large-Precategory Y) ≃ hom-Large-Precategory D - ( obj-left-adjoint-Adjunction-Large-Precategory FG X) + ( obj-left-adjoint-Adjunction-Large-Precategory X) ( Y) - equiv-is-adjoint-pair-Adjunction-Large-Precategory FG = + equiv-is-adjoint-pair-Adjunction-Large-Precategory = equiv-is-adjoint-pair-Large-Precategory ( is-adjoint-pair-Adjunction-Large-Precategory FG) map-equiv-is-adjoint-pair-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory C ( X) - ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) → + ( obj-right-adjoint-Adjunction-Large-Precategory Y) → hom-Large-Precategory D - ( obj-left-adjoint-Adjunction-Large-Precategory FG X) + ( obj-left-adjoint-Adjunction-Large-Precategory X) ( Y) - map-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG = - map-equiv-is-adjoint-pair-Large-Precategory + map-equiv-is-adjoint-pair-Adjunction-Large-Precategory = + map-equiv-is-adjoint-pair-Large-Precategory C D ( left-adjoint-Adjunction-Large-Precategory FG) ( right-adjoint-Adjunction-Large-Precategory FG) ( is-adjoint-pair-Adjunction-Large-Precategory FG) naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) {l1 l2 l3 l4 : Level} {X1 : obj-Large-Precategory C l1} {X2 : obj-Large-Precategory C l2} @@ -320,52 +326,49 @@ module _ (f : hom-Large-Precategory C X2 X1) (g : hom-Large-Precategory D Y1 Y2) → coherence-square-maps - ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X1 Y1) + ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory X1 Y1) ( λ h → comp-hom-Large-Precategory C ( comp-hom-Large-Precategory C - ( hom-right-adjoint-Adjunction-Large-Precategory FG g) + ( hom-right-adjoint-Adjunction-Large-Precategory g) ( h)) ( f)) ( λ h → comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D g h) - ( hom-left-adjoint-Adjunction-Large-Precategory FG f)) - ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X2 Y2) - naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG = + ( hom-left-adjoint-Adjunction-Large-Precategory f)) + ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory X2 Y2) + naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory = naturality-equiv-is-adjoint-pair-Large-Precategory ( is-adjoint-pair-Adjunction-Large-Precategory FG) inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory D - ( obj-left-adjoint-Adjunction-Large-Precategory FG X) + ( obj-left-adjoint-Adjunction-Large-Precategory X) ( Y) ≃ hom-Large-Precategory C ( X) - ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) - inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y = - inv-equiv (equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y) + ( obj-right-adjoint-Adjunction-Large-Precategory Y) + inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory X Y = + inv-equiv (equiv-is-adjoint-pair-Adjunction-Large-Precategory X Y) map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory D - ( obj-left-adjoint-Adjunction-Large-Precategory FG X) + ( obj-left-adjoint-Adjunction-Large-Precategory X) ( Y) → hom-Large-Precategory C ( X) - ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) - map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y = - map-inv-equiv (equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y) + ( obj-right-adjoint-Adjunction-Large-Precategory Y) + map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory X Y = + map-inv-equiv (equiv-is-adjoint-pair-Adjunction-Large-Precategory X Y) naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory) {l1 l2 l3 l4 : Level} {X1 : obj-Large-Precategory C l1} {X2 : obj-Large-Precategory C l2} @@ -374,62 +377,74 @@ module _ (f : hom-Large-Precategory C X2 X1) (g : hom-Large-Precategory D Y1 Y2) → coherence-square-maps - ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X1 Y1) + ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory X1 Y1) ( λ h → comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D g h) - ( hom-left-adjoint-Adjunction-Large-Precategory FG f)) + ( hom-left-adjoint-Adjunction-Large-Precategory f)) ( λ h → comp-hom-Large-Precategory C ( comp-hom-Large-Precategory C - ( hom-right-adjoint-Adjunction-Large-Precategory FG g) + ( hom-right-adjoint-Adjunction-Large-Precategory g) ( h)) ( f)) - ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X2 Y2) - naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG = - naturality-inv-equiv-is-adjoint-pair-Large-Precategory + ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory X2 Y2) + naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory = + naturality-inv-equiv-is-adjoint-pair-Large-Precategory C D ( left-adjoint-Adjunction-Large-Precategory FG) ( right-adjoint-Adjunction-Large-Precategory FG) ( is-adjoint-pair-Adjunction-Large-Precategory FG) ``` -## Properties - -### Unit of adjunction +### The unit of an adjunction -Given an adjoint pair `F ⊣ G`, we can construct a natural transformation -`η : id → G ∘ F` called the unit of the adjunction. +Given an adjoint pair `F ⊣ G`, we construct a natural transformation +`η : id → G ∘ F` called the **unit** of the adjunction. ```agda module _ - {αC αD : Level → Level} {βC βD : Level → Level → Level} + {αC αD : Level → Level} {βC βD : Level → Level → Level} {γ δ : Level → Level} (C : Large-Precategory αC βC) (D : Large-Precategory αD βD) + (FG : Adjunction-Large-Precategory γ δ C D) where - unit-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory C D) → - natural-transformation-Large-Precategory - ( id-functor-Large-Precategory) - ( comp-functor-Large-Precategory + hom-unit-Adjunction-Large-Precategory : + family-of-morphisms-functor-Large-Precategory C C + ( id-functor-Large-Precategory C) + ( comp-functor-Large-Precategory C D C ( right-adjoint-Adjunction-Large-Precategory FG) ( left-adjoint-Adjunction-Large-Precategory FG)) - hom-family-natural-transformation-Large-Precategory - ( unit-Adjunction-Large-Precategory FG) - ( X) = + hom-unit-Adjunction-Large-Precategory X = map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG X ( obj-left-adjoint-Adjunction-Large-Precategory C D FG X) ( id-hom-Large-Precategory D) - coherence-square-natural-transformation-Large-Precategory - ( unit-Adjunction-Large-Precategory FG) {X = X} {Y} f = + + naturality-unit-Adjunction-Large-Precategory : + naturality-family-of-morphisms-functor-Large-Precategory C C + ( id-functor-Large-Precategory C) + ( comp-functor-Large-Precategory C D C + ( right-adjoint-Adjunction-Large-Precategory FG) + ( left-adjoint-Adjunction-Large-Precategory FG)) + ( hom-unit-Adjunction-Large-Precategory) + naturality-unit-Adjunction-Large-Precategory {X = X} {Y} f = inv ( ( inv ( left-unit-law-comp-hom-Large-Precategory C - ( comp-hom-Large-Precategory C (η Y) f))) ∙ + ( comp-hom-Large-Precategory C + ( hom-unit-Adjunction-Large-Precategory + ( Y)) + ( f)))) ∙ ( ap ( comp-hom-Large-Precategory' C - ( comp-hom-Large-Precategory C (η Y) f)) + ( comp-hom-Large-Precategory C + ( hom-unit-Adjunction-Large-Precategory + ( Y)) + ( f))) ( inv - ( preserves-id-right-adjoint-Adjunction-Large-Precategory C D FG + ( preserves-id-right-adjoint-Adjunction-Large-Precategory + ( C) + ( D) + ( FG) ( obj-left-adjoint-Adjunction-Large-Precategory C D FG Y)))) ∙ ( inv ( associative-comp-hom-Large-Precategory C @@ -457,10 +472,10 @@ module _ ( id-hom-Large-Precategory D) ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f))) ∙ ( left-unit-law-comp-hom-Large-Precategory D - ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)) ∙ + ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)) ∙ ( inv - ( right-unit-law-comp-hom-Large-Precategory D - ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f))) ∙ + ( right-unit-law-comp-hom-Large-Precategory D + ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f))) ∙ ( inv ( right-unit-law-comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D @@ -483,44 +498,61 @@ module _ ( comp-hom-Large-Precategory C ( hom-right-adjoint-Adjunction-Large-Precategory C D FG ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)) - ( η X))))) - where - η : - {l : Level} (X : obj-Large-Precategory C l) → - hom-Large-Precategory C X - ( obj-right-adjoint-Adjunction-Large-Precategory C D FG - ( obj-left-adjoint-Adjunction-Large-Precategory C D FG X)) - η = - hom-family-natural-transformation-Large-Precategory - ( unit-Adjunction-Large-Precategory FG) + ( hom-unit-Adjunction-Large-Precategory + ( X)))))) + + unit-Adjunction-Large-Precategory : + natural-transformation-Large-Precategory C C + ( id-functor-Large-Precategory C) + ( comp-functor-Large-Precategory C D C + ( right-adjoint-Adjunction-Large-Precategory FG) + ( left-adjoint-Adjunction-Large-Precategory FG)) + hom-natural-transformation-Large-Precategory + unit-Adjunction-Large-Precategory = + hom-unit-Adjunction-Large-Precategory + naturality-natural-transformation-Large-Precategory + unit-Adjunction-Large-Precategory = + naturality-unit-Adjunction-Large-Precategory ``` -### Counit of adjunction +### The counit of an adjunction -Given an adjoint pair `F ⊣ G`, we can construct a natural transformation -`ε : F ∘ G → id` called the counit of the adjunction. +Given an adjoint pair `F ⊣ G`, we construct a natural transformation +`ε : F ∘ G → id` called the **counit** of the adjunction. ```agda - counit-Adjunction-Large-Precategory : - (FG : Adjunction-Large-Precategory C D) → - natural-transformation-Large-Precategory - ( comp-functor-Large-Precategory +module _ + {αC αD : Level → Level} {βC βD : Level → Level → Level} {γ δ : Level → Level} + (C : Large-Precategory αC βC) (D : Large-Precategory αD βD) + (FG : Adjunction-Large-Precategory γ δ C D) + where + + hom-counit-Adjunction-Large-Precategory : + family-of-morphisms-functor-Large-Precategory D D + ( comp-functor-Large-Precategory D C D ( left-adjoint-Adjunction-Large-Precategory FG) ( right-adjoint-Adjunction-Large-Precategory FG)) - ( id-functor-Large-Precategory) - hom-family-natural-transformation-Large-Precategory - ( counit-Adjunction-Large-Precategory FG) Y = + ( id-functor-Large-Precategory D) + hom-counit-Adjunction-Large-Precategory Y = map-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG ( obj-right-adjoint-Adjunction-Large-Precategory C D FG Y) ( Y) ( id-hom-Large-Precategory C) - coherence-square-natural-transformation-Large-Precategory - (counit-Adjunction-Large-Precategory FG) {X = X} {Y = Y} f = + + naturality-counit-Adjunction-Large-Precategory : + naturality-family-of-morphisms-functor-Large-Precategory D D + ( comp-functor-Large-Precategory D C D + ( left-adjoint-Adjunction-Large-Precategory FG) + ( right-adjoint-Adjunction-Large-Precategory FG)) + ( id-functor-Large-Precategory D) + ( hom-counit-Adjunction-Large-Precategory) + naturality-counit-Adjunction-Large-Precategory {X = X} {Y = Y} f = inv ( ( inv ( left-unit-law-comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D - ( ε Y) + ( hom-counit-Adjunction-Large-Precategory + ( Y)) ( hom-left-adjoint-Adjunction-Large-Precategory C D FG ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f))))) ∙ ( inv @@ -548,7 +580,7 @@ Given an adjoint pair `F ⊣ G`, we can construct a natural transformation ( hom-right-adjoint-Adjunction-Large-Precategory C D FG ( id-hom-Large-Precategory D))) ∙ ( preserves-id-right-adjoint-Adjunction-Large-Precategory - C D FG Y))) ∙ + C D FG Y))) ∙ ( left-unit-law-comp-hom-Large-Precategory C ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f)) ∙ ( ( inv @@ -560,25 +592,35 @@ Given an adjoint pair `F ⊣ G`, we can construct a natural transformation ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f) ( id-hom-Large-Precategory C)))))) ∙ ( naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG - ( id-hom-Large-Precategory C) + ( id-hom-Large-Precategory C) ( f) ( id-hom-Large-Precategory C)) ∙ ( ap ( comp-hom-Large-Precategory ( D) - ( comp-hom-Large-Precategory D f (ε X))) - ( preserves-id-left-adjoint-Adjunction-Large-Precategory C D FG + ( comp-hom-Large-Precategory D f + ( hom-counit-Adjunction-Large-Precategory + ( X)))) + ( preserves-id-left-adjoint-Adjunction-Large-Precategory + ( C) + ( D) + ( FG) ( obj-right-adjoint-Adjunction-Large-Precategory C D FG X))) ∙ ( right-unit-law-comp-hom-Large-Precategory D - ( comp-hom-Large-Precategory D f (ε X))))) - where - ε : - {l : Level} (Y : obj-Large-Precategory D l) → - hom-Large-Precategory D - ( obj-left-adjoint-Adjunction-Large-Precategory C D FG - ( obj-right-adjoint-Adjunction-Large-Precategory C D FG Y)) - ( Y) - ε = - hom-family-natural-transformation-Large-Precategory - ( counit-Adjunction-Large-Precategory FG) + ( comp-hom-Large-Precategory D f + ( hom-counit-Adjunction-Large-Precategory + ( X)))))) + + counit-Adjunction-Large-Precategory : + natural-transformation-Large-Precategory D D + ( comp-functor-Large-Precategory D C D + ( left-adjoint-Adjunction-Large-Precategory FG) + ( right-adjoint-Adjunction-Large-Precategory FG)) + ( id-functor-Large-Precategory D) + hom-natural-transformation-Large-Precategory + counit-Adjunction-Large-Precategory = + hom-counit-Adjunction-Large-Precategory + naturality-natural-transformation-Large-Precategory + counit-Adjunction-Large-Precategory = + naturality-counit-Adjunction-Large-Precategory ``` diff --git a/src/category-theory/equivalences-of-large-precategories.lagda.md b/src/category-theory/equivalences-of-large-precategories.lagda.md index 49d202d59b..c6dd8e5fb5 100644 --- a/src/category-theory/equivalences-of-large-precategories.lagda.md +++ b/src/category-theory/equivalences-of-large-precategories.lagda.md @@ -18,10 +18,14 @@ open import foundation.universe-levels ## Idea -The large precategories `C` and `D` are equivalent if there are functors -`F : C → D` and `G : D → C` such that - -- `G ∘ F` is naturally isomorphic to the identity functor on `C`, +Two [large precategories](category-theory.large-precategories.md) `C` and `D` +are said to be **equivalent** if there are +[functors](category-theory.functors-large-precategories.md) `F : C → D` and +`G : D → C` such that + +- `G ∘ F` is + [naturally isomorphic](category-theory.natural-isomorphisms-functors-large-precategories.md) + to the identity functor on `C`, - `F ∘ G` is naturally isomorphic to the identity functor on `D`. ## Definition @@ -33,24 +37,24 @@ module _ where record - equivalence-Large-Precategory (γ-there γ-back : Level → Level) : UUω where + equivalence-Large-Precategory (γ γ' : Level → Level) : UUω where constructor make-equivalence-Large-Precategory field functor-equivalence-Large-Precategory : - functor-Large-Precategory C D γ-there + functor-Large-Precategory γ C D functor-inv-equivalence-Large-Precategory : - functor-Large-Precategory D C γ-back + functor-Large-Precategory γ' D C is-section-functor-inv-equivalence-Large-Precategory : natural-isomorphism-Large-Precategory - ( comp-functor-Large-Precategory + ( comp-functor-Large-Precategory D C D functor-equivalence-Large-Precategory functor-inv-equivalence-Large-Precategory) - ( id-functor-Large-Precategory) + ( id-functor-Large-Precategory D) is-retraction-functor-inv-equivalence-Large-Precategory : natural-isomorphism-Large-Precategory - ( comp-functor-Large-Precategory + ( comp-functor-Large-Precategory C D C functor-inv-equivalence-Large-Precategory functor-equivalence-Large-Precategory) - ( id-functor-Large-Precategory) + ( id-functor-Large-Precategory C) ``` diff --git a/src/category-theory/functors-large-categories.lagda.md b/src/category-theory/functors-large-categories.lagda.md new file mode 100644 index 0000000000..eda64ca996 --- /dev/null +++ b/src/category-theory/functors-large-categories.lagda.md @@ -0,0 +1,122 @@ +# Functors between large categories + +```agda +module category-theory.functors-large-categories where +``` + +
Imports + +```agda +open import category-theory.functors-large-precategories +open import category-theory.large-categories + +open import foundation.action-on-identifications-functions +open import foundation.function-types +open import foundation.identity-types +open import foundation.universe-levels +``` + +
+ +## Idea + +A **functor** from a [large category](category-theory.large-categories.md) `C` +to a large category `D` is just a +[functor](category-theory.functors-large-precategories.md) between the +underlying [large precategories](category-theory.large-precategories.md) of `C` +and `D`. In other words, functors of large categories consist of: + +- a map `F₀ : C → D` on objects, +- a map `F₁ : hom x y → hom (F₀ x) (F₀ y)` on morphisms, such that the following + identities hold: +- `F id_x = id_(F x)`, +- `F (g ∘ f) = F g ∘ F f`. + +## Definition + +```agda +module _ + {αC αD : Level → Level} {βC βD : Level → Level → Level} (γ : Level → Level) + (C : Large-Category αC βC) (D : Large-Category αD βD) + where + + functor-Large-Category : UUω + functor-Large-Category = + functor-Large-Precategory γ + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + +module _ + {αC αD : Level → Level} {βC βD : Level → Level → Level} {γ : Level → Level} + (C : Large-Category αC βC) (D : Large-Category αD βD) + (F : functor-Large-Category γ C D) + where + + obj-functor-Large-Category : + {l1 : Level} → obj-Large-Category C l1 → obj-Large-Category D (γ l1) + obj-functor-Large-Category = + obj-functor-Large-Precategory F + + hom-functor-Large-Category : + {l1 l2 : Level} + {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2} → + hom-Large-Category C X Y → + hom-Large-Category D + ( obj-functor-Large-Category X) + ( obj-functor-Large-Category Y) + hom-functor-Large-Category = + hom-functor-Large-Precategory F + + preserves-id-functor-Large-Category : + {l1 : Level} {X : obj-Large-Category C l1} → + hom-functor-Large-Category (id-hom-Large-Category C {X = X}) ＝ + id-hom-Large-Category D + preserves-id-functor-Large-Category = + preserves-id-functor-Large-Precategory F + + preserves-comp-functor-Large-Category : + {l1 l2 l3 : Level} + {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2} + {Z : obj-Large-Category C l3} + (g : hom-Large-Category C Y Z) (f : hom-Large-Category C X Y) → + hom-functor-Large-Category (comp-hom-Large-Category C g f) ＝ + comp-hom-Large-Category D + ( hom-functor-Large-Category g) + ( hom-functor-Large-Category f) + preserves-comp-functor-Large-Category = + preserves-comp-functor-Large-Precategory F +``` + +### The identity functor + +There is an identity functor on any large category. + +```agda +id-functor-Large-Category : + {αC : Level → Level} {βC : Level → Level → Level} → + (C : Large-Category αC βC) → + functor-Large-Category id C C +id-functor-Large-Category C = + id-functor-Large-Precategory (large-precategory-Large-Category C) +``` + +### Composition of functors + +Any two compatible functors can be composed to a new functor. + +```agda +comp-functor-Large-Category : + {αC αD αE γG γF : Level → Level} + {βC βD βE : Level → Level → Level} → + (C : Large-Category αC βC) + (D : Large-Category αD βD) + (E : Large-Category αE βE) → + functor-Large-Category γG D E → + functor-Large-Category γF C D → + functor-Large-Category (λ l → γG (γF l)) C E +comp-functor-Large-Category C D E = + comp-functor-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( large-precategory-Large-Category E) +``` diff --git a/src/category-theory/functors-large-precategories.lagda.md b/src/category-theory/functors-large-precategories.lagda.md index 8684f83fc0..ced47bee15 100644 --- a/src/category-theory/functors-large-precategories.lagda.md +++ b/src/category-theory/functors-large-precategories.lagda.md @@ -32,11 +32,11 @@ A **functor** from a [large precategory](category-theory.large-precategories.md) ```agda module _ - {αC αD : Level → Level} {βC βD : Level → Level → Level} + {αC αD : Level → Level} {βC βD : Level → Level → Level} (γ : Level → Level) (C : Large-Precategory αC βC) (D : Large-Precategory αD βD) where - record functor-Large-Precategory (γ : Level → Level) : UUω + record functor-Large-Precategory : UUω where constructor make-functor field @@ -72,52 +72,97 @@ module _ open functor-Large-Precategory public ``` -## Examples - ### The identity functor -There is an identity functor on any large precategory. - ```agda id-functor-Large-Precategory : {αC : Level → Level} {βC : Level → Level → Level} → - {C : Large-Precategory αC βC} → - functor-Large-Precategory C C (λ l → l) -obj-functor-Large-Precategory id-functor-Large-Precategory = id -hom-functor-Large-Precategory id-functor-Large-Precategory = id -preserves-comp-functor-Large-Precategory id-functor-Large-Precategory g f = refl -preserves-id-functor-Large-Precategory id-functor-Large-Precategory = refl + (C : Large-Precategory αC βC) → + functor-Large-Precategory id C C +obj-functor-Large-Precategory + ( id-functor-Large-Precategory C) = + id +hom-functor-Large-Precategory + ( id-functor-Large-Precategory C) = + id +preserves-comp-functor-Large-Precategory + ( id-functor-Large-Precategory C) g f = + refl +preserves-id-functor-Large-Precategory + ( id-functor-Large-Precategory C) = + refl ``` ### Composition of functors -Any two compatible functors can be composed to a new functor. - ```agda -comp-functor-Large-Precategory : +module _ {αC αD αE γG γF : Level → Level} - {βC βD βE : Level → Level → Level} → - {C : Large-Precategory αC βC} - {D : Large-Precategory αD βD} - {E : Large-Precategory αE βE} → - functor-Large-Precategory D E γG → - functor-Large-Precategory C D γF → - functor-Large-Precategory C E (γG ∘ γF) -obj-functor-Large-Precategory (comp-functor-Large-Precategory G F) = - obj-functor-Large-Precategory G ∘ obj-functor-Large-Precategory F -hom-functor-Large-Precategory (comp-functor-Large-Precategory G F) = - hom-functor-Large-Precategory G ∘ hom-functor-Large-Precategory F -preserves-comp-functor-Large-Precategory - ( comp-functor-Large-Precategory G F) g f = - ( ap - ( hom-functor-Large-Precategory G) - ( preserves-comp-functor-Large-Precategory F g f)) ∙ - ( preserves-comp-functor-Large-Precategory G - ( hom-functor-Large-Precategory F g) - ( hom-functor-Large-Precategory F f)) -preserves-id-functor-Large-Precategory (comp-functor-Large-Precategory G F) = - ( ap - ( hom-functor-Large-Precategory G) - ( preserves-id-functor-Large-Precategory F)) ∙ - ( preserves-id-functor-Large-Precategory G) + {βC βD βE : Level → Level → Level} + (C : Large-Precategory αC βC) + (D : Large-Precategory αD βD) + (E : Large-Precategory αE βE) + (G : functor-Large-Precategory γG D E) + (F : functor-Large-Precategory γF C D) + where + + obj-comp-functor-Large-Precategory : + {l1 : Level} → + obj-Large-Precategory C l1 → obj-Large-Precategory E (γG (γF l1)) + obj-comp-functor-Large-Precategory = + obj-functor-Large-Precategory G ∘ obj-functor-Large-Precategory F + + hom-comp-functor-Large-Precategory : + {l1 l2 : Level} + {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2} → + hom-Large-Precategory C X Y → + hom-Large-Precategory E + ( obj-comp-functor-Large-Precategory X) + ( obj-comp-functor-Large-Precategory Y) + hom-comp-functor-Large-Precategory = + hom-functor-Large-Precategory G ∘ hom-functor-Large-Precategory F + + preserves-comp-comp-functor-Large-Precategory : + {l1 l2 l3 : Level} + {X : obj-Large-Precategory C l1} + {Y : obj-Large-Precategory C l2} + {Z : obj-Large-Precategory C l3} + (g : hom-Large-Precategory C Y Z) (f : hom-Large-Precategory C X Y) → + hom-comp-functor-Large-Precategory + ( comp-hom-Large-Precategory C g f) ＝ + comp-hom-Large-Precategory E + ( hom-comp-functor-Large-Precategory g) + ( hom-comp-functor-Large-Precategory f) + preserves-comp-comp-functor-Large-Precategory g f = + ( ap + ( hom-functor-Large-Precategory G) + ( preserves-comp-functor-Large-Precategory F g f)) ∙ + ( preserves-comp-functor-Large-Precategory G + ( hom-functor-Large-Precategory F g) + ( hom-functor-Large-Precategory F f)) + + preserves-id-comp-functor-Large-Precategory : + {l1 : Level} {X : obj-Large-Precategory C l1} → + hom-comp-functor-Large-Precategory (id-hom-Large-Precategory C {X = X}) ＝ + id-hom-Large-Precategory E + preserves-id-comp-functor-Large-Precategory = + ( ap + ( hom-functor-Large-Precategory G) + ( preserves-id-functor-Large-Precategory F)) ∙ + ( preserves-id-functor-Large-Precategory G) + + comp-functor-Large-Precategory : + functor-Large-Precategory (γG ∘ γF) C E + obj-functor-Large-Precategory + comp-functor-Large-Precategory = + obj-comp-functor-Large-Precategory + hom-functor-Large-Precategory + comp-functor-Large-Precategory = + hom-comp-functor-Large-Precategory + preserves-comp-functor-Large-Precategory + comp-functor-Large-Precategory = + preserves-comp-comp-functor-Large-Precategory + preserves-id-functor-Large-Precategory + comp-functor-Large-Precategory = + preserves-id-comp-functor-Large-Precategory ``` diff --git a/src/category-theory/homotopies-natural-transformations-large-precategories.lagda.md b/src/category-theory/homotopies-natural-transformations-large-precategories.lagda.md index 5432c73da3..1359d2abd4 100644 --- a/src/category-theory/homotopies-natural-transformations-large-precategories.lagda.md +++ b/src/category-theory/homotopies-natural-transformations-large-precategories.lagda.md @@ -36,17 +36,17 @@ the type of homotopies of natural transformations. ```agda module _ {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} - {C : Large-Precategory αC βC} {D : Large-Precategory αD βD} - {F : functor-Large-Precategory C D γF} - {G : functor-Large-Precategory C D γG} + (C : Large-Precategory αC βC) (D : Large-Precategory αD βD) + {F : functor-Large-Precategory γF C D} + {G : functor-Large-Precategory γG C D} where htpy-natural-transformation-Large-Precategory : - (α β : natural-transformation-Large-Precategory F G) → UUω - htpy-natural-transformation-Large-Precategory α β = + (σ τ : natural-transformation-Large-Precategory C D F G) → UUω + htpy-natural-transformation-Large-Precategory σ τ = { l : Level} (X : obj-Large-Precategory C l) → - ( hom-family-natural-transformation-Large-Precategory α X) ＝ - ( hom-family-natural-transformation-Large-Precategory β X) + ( hom-natural-transformation-Large-Precategory σ X) ＝ + ( hom-natural-transformation-Large-Precategory τ X) ``` ### The reflexivity homotopy @@ -54,14 +54,14 @@ module _ ```agda module _ {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} - {C : Large-Precategory αC βC} {D : Large-Precategory αD βD} - {F : functor-Large-Precategory C D γF} - {G : functor-Large-Precategory C D γG} + (C : Large-Precategory αC βC) (D : Large-Precategory αD βD) + {F : functor-Large-Precategory γF C D} + {G : functor-Large-Precategory γG C D} where refl-htpy-natural-transformation-Large-Precategory : - (α : natural-transformation-Large-Precategory F G) → - htpy-natural-transformation-Large-Precategory α α + (α : natural-transformation-Large-Precategory C D F G) → + htpy-natural-transformation-Large-Precategory C D α α refl-htpy-natural-transformation-Large-Precategory α = refl-htpy ``` @@ -71,28 +71,35 @@ A homotopy from `α` to `β` can be concatenated with a homotopy from `β` to ` to form a homotopy from `α` to `γ`. The concatenation is associative. ```agda +module _ + {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} + (C : Large-Precategory αC βC) (D : Large-Precategory αD βD) + {F : functor-Large-Precategory γF C D} + {G : functor-Large-Precategory γG C D} + where + concat-htpy-natural-transformation-Large-Precategory : - (α β γ : natural-transformation-Large-Precategory F G) → - htpy-natural-transformation-Large-Precategory α β → - htpy-natural-transformation-Large-Precategory β γ → - htpy-natural-transformation-Large-Precategory α γ - concat-htpy-natural-transformation-Large-Precategory α β γ H K = H ∙h K + (σ τ υ : natural-transformation-Large-Precategory C D F G) → + htpy-natural-transformation-Large-Precategory C D σ τ → + htpy-natural-transformation-Large-Precategory C D τ υ → + htpy-natural-transformation-Large-Precategory C D σ υ + concat-htpy-natural-transformation-Large-Precategory σ τ υ H K = H ∙h K associative-concat-htpy-natural-transformation-Large-Precategory : - (α β γ δ : natural-transformation-Large-Precategory F G) - (H : htpy-natural-transformation-Large-Precategory α β) - (K : htpy-natural-transformation-Large-Precategory β γ) - (L : htpy-natural-transformation-Large-Precategory γ δ) → + (σ τ υ ϕ : natural-transformation-Large-Precategory C D F G) + (H : htpy-natural-transformation-Large-Precategory C D σ τ) + (K : htpy-natural-transformation-Large-Precategory C D τ υ) + (L : htpy-natural-transformation-Large-Precategory C D υ ϕ) → {l : Level} (X : obj-Large-Precategory C l) → - ( concat-htpy-natural-transformation-Large-Precategory α γ δ - ( concat-htpy-natural-transformation-Large-Precategory α β γ H K) + ( concat-htpy-natural-transformation-Large-Precategory σ υ ϕ + ( concat-htpy-natural-transformation-Large-Precategory σ τ υ H K) ( L) ( X)) ＝ - ( concat-htpy-natural-transformation-Large-Precategory α β δ + ( concat-htpy-natural-transformation-Large-Precategory σ τ ϕ ( H) - ( concat-htpy-natural-transformation-Large-Precategory β γ δ K L) + ( concat-htpy-natural-transformation-Large-Precategory τ υ ϕ K L) ( X)) associative-concat-htpy-natural-transformation-Large-Precategory - α β γ δ H K L = + σ τ υ ϕ H K L = assoc-htpy H K L ``` diff --git a/src/category-theory/natural-isomorphisms-functors-large-precategories.lagda.md b/src/category-theory/natural-isomorphisms-functors-large-precategories.lagda.md index c0e4563f67..edaf9fc991 100644 --- a/src/category-theory/natural-isomorphisms-functors-large-precategories.lagda.md +++ b/src/category-theory/natural-isomorphisms-functors-large-precategories.lagda.md @@ -7,6 +7,7 @@ module category-theory.natural-isomorphisms-functors-large-precategories where
Imports ```agda +open import category-theory.commuting-squares-of-morphisms-in-large-precategories open import category-theory.functors-large-precategories open import category-theory.isomorphisms-in-large-precategories open import category-theory.large-precategories @@ -35,8 +36,8 @@ module _ {βC βD : Level → Level → Level} {C : Large-Precategory αC βC} {D : Large-Precategory αD βD} - (F : functor-Large-Precategory C D γF) - (G : functor-Large-Precategory C D γG) + (F : functor-Large-Precategory γF C D) + (G : functor-Large-Precategory γG C D) where iso-family-functor-Large-Precategory : UUω @@ -51,31 +52,31 @@ module _ where constructor make-natural-isomorphism field - components-natural-isomorphism-Large-Precategory : + iso-natural-isomorphism-Large-Precategory : iso-family-functor-Large-Precategory - coherence-square-natural-isomorphism-Large-Precategory : + naturality-natural-isomorphism-Large-Precategory : { l1 l2 : Level} { X : obj-Large-Precategory C l1} { Y : obj-Large-Precategory C l2} ( f : hom-Large-Precategory C X Y) → - coherence-square-Large-Precategory D - ( hom-iso-Large-Precategory D - ( components-natural-isomorphism-Large-Precategory X)) + coherence-square-hom-Large-Precategory D ( hom-functor-Large-Precategory F f) - ( hom-functor-Large-Precategory G f) ( hom-iso-Large-Precategory D - ( components-natural-isomorphism-Large-Precategory Y)) + ( iso-natural-isomorphism-Large-Precategory X)) + ( hom-iso-Large-Precategory D + ( iso-natural-isomorphism-Large-Precategory Y)) + ( hom-functor-Large-Precategory G f) open natural-isomorphism-Large-Precategory public natural-transformation-natural-isomorphism-Large-Precategory : natural-isomorphism-Large-Precategory → - natural-transformation-Large-Precategory F G - hom-family-natural-transformation-Large-Precategory + natural-transformation-Large-Precategory C D F G + hom-natural-transformation-Large-Precategory ( natural-transformation-natural-isomorphism-Large-Precategory γ) X = hom-iso-Large-Precategory D - ( components-natural-isomorphism-Large-Precategory γ X) - coherence-square-natural-transformation-Large-Precategory - (natural-transformation-natural-isomorphism-Large-Precategory γ) = - coherence-square-natural-isomorphism-Large-Precategory γ + ( iso-natural-isomorphism-Large-Precategory γ X) + naturality-natural-transformation-Large-Precategory + ( natural-transformation-natural-isomorphism-Large-Precategory γ) = + naturality-natural-isomorphism-Large-Precategory γ ``` diff --git a/src/category-theory/natural-transformations-functors-large-categories.lagda.md b/src/category-theory/natural-transformations-functors-large-categories.lagda.md new file mode 100644 index 0000000000..6c83b81689 --- /dev/null +++ b/src/category-theory/natural-transformations-functors-large-categories.lagda.md @@ -0,0 +1,175 @@ +# Natural transformations between functors between large categories + +```agda +module category-theory.natural-transformations-functors-large-categories where +``` + +
Imports + +```agda +open import category-theory.functors-large-categories +open import category-theory.large-categories +open import category-theory.natural-transformations-functors-large-precategories + +open import foundation.action-on-identifications-functions +open import foundation.identity-types +open import foundation.universe-levels +``` + +
+ +## Idea + +Given [large categories](category-theory.large-categories.md) `C` and `D`, a +**natural transformation** from a +[functor](category-theory.functors-large-categories.md) `F : C → D` to +`G : C → D` consists of : + +- a family of morphisms `γ : (x : C) → hom (F x) (G x)` such that the following + **naturality condition** holds: +- `(G f) ∘ (γ x) = (γ y) ∘ (F f)`, for all `f : hom x y`. + +## Definition + +```agda +module _ + {αC αD γF γG : Level → Level} + {βC βD : Level → Level → Level} + (C : Large-Category αC βC) + (D : Large-Category αD βD) + (F : functor-Large-Category γF C D) + (G : functor-Large-Category γG C D) + where + + family-of-morphisms-functor-Large-Category : UUω + family-of-morphisms-functor-Large-Category = + family-of-morphisms-functor-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + + naturality-family-of-morphisms-functor-Large-Category : + family-of-morphisms-functor-Large-Category → UUω + naturality-family-of-morphisms-functor-Large-Category = + naturality-family-of-morphisms-functor-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + + natural-transformation-Large-Category : UUω + natural-transformation-Large-Category = + natural-transformation-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + + hom-natural-transformation-Large-Category : + natural-transformation-Large-Category → + family-of-morphisms-functor-Large-Category + hom-natural-transformation-Large-Category = + hom-natural-transformation-Large-Precategory + + naturality-natural-transformation-Large-Category : + (τ : natural-transformation-Large-Category) → + naturality-family-of-morphisms-functor-Large-Category + (hom-natural-transformation-Large-Category τ) + naturality-natural-transformation-Large-Category = + naturality-natural-transformation-Large-Precategory +``` + +## Properties + +### The identity natural transformation + +Every functor comes equipped with an identity natural transformation. + +```agda +module _ + { αC αD γF : Level → Level} + { βC βD : Level → Level → Level} + ( C : Large-Category αC βC) + ( D : Large-Category αD βD) + ( F : functor-Large-Category γF C D) + where + + hom-id-natural-transformation-Large-Category : + family-of-morphisms-functor-Large-Category C D F F + hom-id-natural-transformation-Large-Category = + hom-id-natural-transformation-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + naturality-id-natural-transformation-Large-Category : + naturality-family-of-morphisms-functor-Large-Category C D F F + hom-id-natural-transformation-Large-Category + naturality-id-natural-transformation-Large-Category = + naturality-id-natural-transformation-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + + id-natural-transformation-Large-Category : + natural-transformation-Large-Category C D F F + id-natural-transformation-Large-Category = + id-natural-transformation-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) +``` + +### Composition of natural transformations + +```agda +module _ + {αC αD γF γG γH : Level → Level} + {βC βD : Level → Level → Level} + (C : Large-Category αC βC) + (D : Large-Category αD βD) + (F : functor-Large-Category γF C D) + (G : functor-Large-Category γG C D) + (H : functor-Large-Category γH C D) + (τ : natural-transformation-Large-Category C D G H) + (σ : natural-transformation-Large-Category C D F G) + where + + hom-comp-natural-transformation-Large-Category : + family-of-morphisms-functor-Large-Category C D F H + hom-comp-natural-transformation-Large-Category = + hom-comp-natural-transformation-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + ( H) + ( τ) + ( σ) + + naturality-comp-natural-transformation-Large-Category : + naturality-family-of-morphisms-functor-Large-Category C D F H + hom-comp-natural-transformation-Large-Category + naturality-comp-natural-transformation-Large-Category = + naturality-comp-natural-transformation-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + ( H) + ( τ) + ( σ) + + comp-natural-transformation-Large-Category : + natural-transformation-Large-Category C D F H + comp-natural-transformation-Large-Category = + comp-natural-transformation-Large-Precategory + ( large-precategory-Large-Category C) + ( large-precategory-Large-Category D) + ( F) + ( G) + ( H) + ( τ) + ( σ) +``` diff --git a/src/category-theory/natural-transformations-functors-large-precategories.lagda.md b/src/category-theory/natural-transformations-functors-large-precategories.lagda.md index 422d77fda3..40e89cd14c 100644 --- a/src/category-theory/natural-transformations-functors-large-precategories.lagda.md +++ b/src/category-theory/natural-transformations-functors-large-precategories.lagda.md @@ -7,6 +7,7 @@ module category-theory.natural-transformations-functors-large-precategories wher
Imports ```agda +open import category-theory.commuting-squares-of-morphisms-in-large-precategories open import category-theory.functors-large-precategories open import category-theory.large-precategories @@ -31,55 +32,43 @@ a **natural transformation** from a ## Definition ```agda -coherence-square-Large-Precategory : - {αC : Level → Level} - {βC : Level → Level → Level} - (C : Large-Precategory αC βC) - {l1 l2 l3 l4 : Level} - {A : obj-Large-Precategory C l1} - {B : obj-Large-Precategory C l2} - {X : obj-Large-Precategory C l3} - {Y : obj-Large-Precategory C l4} - (top : hom-Large-Precategory C A B) - (left : hom-Large-Precategory C A X) - (right : hom-Large-Precategory C B Y) - (bottom : hom-Large-Precategory C X Y) → - UU (βC l1 l4) -coherence-square-Large-Precategory C top left right bottom = - comp-hom-Large-Precategory C right top ＝ - comp-hom-Large-Precategory C bottom left - module _ {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} - {C : Large-Precategory αC βC} - {D : Large-Precategory αD βD} - (F : functor-Large-Precategory C D γF) - (G : functor-Large-Precategory C D γG) + (C : Large-Precategory αC βC) + (D : Large-Precategory αD βD) + (F : functor-Large-Precategory γF C D) + (G : functor-Large-Precategory γG C D) where - hom-family-functor-Large-Precategory : UUω - hom-family-functor-Large-Precategory = + family-of-morphisms-functor-Large-Precategory : UUω + family-of-morphisms-functor-Large-Precategory = {l : Level} (X : obj-Large-Precategory C l) → hom-Large-Precategory D ( obj-functor-Large-Precategory F X) ( obj-functor-Large-Precategory G X) + naturality-family-of-morphisms-functor-Large-Precategory : + family-of-morphisms-functor-Large-Precategory → UUω + naturality-family-of-morphisms-functor-Large-Precategory τ = + {l1 l2 : Level} {X : obj-Large-Precategory C l1} + {Y : obj-Large-Precategory C l2} + (f : hom-Large-Precategory C X Y) → + coherence-square-hom-Large-Precategory D + ( hom-functor-Large-Precategory F f) + ( τ X) + ( τ Y) + ( hom-functor-Large-Precategory G f) + record natural-transformation-Large-Precategory : UUω where constructor make-natural-transformation field - hom-family-natural-transformation-Large-Precategory : - hom-family-functor-Large-Precategory - coherence-square-natural-transformation-Large-Precategory : - {l1 l2 : Level} {X : obj-Large-Precategory C l1} - {Y : obj-Large-Precategory C l2} - (f : hom-Large-Precategory C X Y) → - coherence-square-Large-Precategory D - ( hom-family-natural-transformation-Large-Precategory X) - ( hom-functor-Large-Precategory F f) - ( hom-functor-Large-Precategory G f) - ( hom-family-natural-transformation-Large-Precategory Y) + hom-natural-transformation-Large-Precategory : + family-of-morphisms-functor-Large-Precategory + naturality-natural-transformation-Large-Precategory : + naturality-family-of-morphisms-functor-Large-Precategory + hom-natural-transformation-Large-Precategory open natural-transformation-Large-Precategory public ``` @@ -94,23 +83,34 @@ Every functor comes equipped with an identity natural transformation. module _ { αC αD γF : Level → Level} { βC βD : Level → Level → Level} - { C : Large-Precategory αC βC} - { D : Large-Precategory αD βD} + ( C : Large-Precategory αC βC) + ( D : Large-Precategory αD βD) + ( F : functor-Large-Precategory γF C D) where + hom-id-natural-transformation-Large-Precategory : + family-of-morphisms-functor-Large-Precategory C D F F + hom-id-natural-transformation-Large-Precategory X = + id-hom-Large-Precategory D + + naturality-id-natural-transformation-Large-Precategory : + naturality-family-of-morphisms-functor-Large-Precategory C D F F + hom-id-natural-transformation-Large-Precategory + naturality-id-natural-transformation-Large-Precategory f = + ( right-unit-law-comp-hom-Large-Precategory D + ( hom-functor-Large-Precategory F f)) ∙ + ( inv + ( left-unit-law-comp-hom-Large-Precategory D + ( hom-functor-Large-Precategory F f))) + id-natural-transformation-Large-Precategory : - ( F : functor-Large-Precategory C D γF) → - natural-transformation-Large-Precategory F F - hom-family-natural-transformation-Large-Precategory - ( id-natural-transformation-Large-Precategory F) X = - id-hom-Large-Precategory D - coherence-square-natural-transformation-Large-Precategory - ( id-natural-transformation-Large-Precategory F) f = - ( right-unit-law-comp-hom-Large-Precategory D - ( hom-functor-Large-Precategory F f)) ∙ - ( inv - ( left-unit-law-comp-hom-Large-Precategory D - ( hom-functor-Large-Precategory F f))) + natural-transformation-Large-Precategory C D F F + hom-natural-transformation-Large-Precategory + id-natural-transformation-Large-Precategory = + hom-id-natural-transformation-Large-Precategory + naturality-natural-transformation-Large-Precategory + id-natural-transformation-Large-Precategory = + naturality-id-natural-transformation-Large-Precategory ``` ### Composition of natural transformations @@ -119,46 +119,57 @@ module _ module _ {αC αD γF γG γH : Level → Level} {βC βD : Level → Level → Level} - {C : Large-Precategory αC βC} - {D : Large-Precategory αD βD} - (F : functor-Large-Precategory C D γF) - (G : functor-Large-Precategory C D γG) - (H : functor-Large-Precategory C D γH) + (C : Large-Precategory αC βC) + (D : Large-Precategory αD βD) + (F : functor-Large-Precategory γF C D) + (G : functor-Large-Precategory γG C D) + (H : functor-Large-Precategory γH C D) + (τ : natural-transformation-Large-Precategory C D G H) + (σ : natural-transformation-Large-Precategory C D F G) where - comp-natural-transformation-Large-Precategory : - natural-transformation-Large-Precategory G H → - natural-transformation-Large-Precategory F G → - natural-transformation-Large-Precategory F H - hom-family-natural-transformation-Large-Precategory - ( comp-natural-transformation-Large-Precategory b a) X = - comp-hom-Large-Precategory D - ( hom-family-natural-transformation-Large-Precategory b X) - ( hom-family-natural-transformation-Large-Precategory a X) - coherence-square-natural-transformation-Large-Precategory - ( comp-natural-transformation-Large-Precategory b a) {X = X} {Y} f = - ( inv + hom-comp-natural-transformation-Large-Precategory : + family-of-morphisms-functor-Large-Precategory C D F H + hom-comp-natural-transformation-Large-Precategory X = + comp-hom-Large-Precategory D + ( hom-natural-transformation-Large-Precategory τ X) + ( hom-natural-transformation-Large-Precategory σ X) + + naturality-comp-natural-transformation-Large-Precategory : + naturality-family-of-morphisms-functor-Large-Precategory C D F H + hom-comp-natural-transformation-Large-Precategory + naturality-comp-natural-transformation-Large-Precategory {X = X} {Y} f = + inv ( associative-comp-hom-Large-Precategory D ( hom-functor-Large-Precategory H f) - ( hom-family-natural-transformation-Large-Precategory b X) - ( hom-family-natural-transformation-Large-Precategory a X))) ∙ + ( hom-natural-transformation-Large-Precategory τ X) + ( hom-natural-transformation-Large-Precategory σ X)) ∙ ( ap ( comp-hom-Large-Precategory' D - ( hom-family-natural-transformation-Large-Precategory a X)) - ( coherence-square-natural-transformation-Large-Precategory b f)) ∙ + ( hom-natural-transformation-Large-Precategory σ X)) + ( naturality-natural-transformation-Large-Precategory τ f)) ∙ ( associative-comp-hom-Large-Precategory D - ( hom-family-natural-transformation-Large-Precategory b Y) + ( hom-natural-transformation-Large-Precategory τ Y) ( hom-functor-Large-Precategory G f) - ( hom-family-natural-transformation-Large-Precategory a X)) ∙ + ( hom-natural-transformation-Large-Precategory σ X)) ∙ ( ap ( comp-hom-Large-Precategory D - ( hom-family-natural-transformation-Large-Precategory b Y)) - ( coherence-square-natural-transformation-Large-Precategory a f)) ∙ + ( hom-natural-transformation-Large-Precategory τ Y)) + ( naturality-natural-transformation-Large-Precategory σ f)) ∙ ( inv - ( associative-comp-hom-Large-Precategory D - ( hom-family-natural-transformation-Large-Precategory b Y) - ( hom-family-natural-transformation-Large-Precategory a Y) + (associative-comp-hom-Large-Precategory D + ( hom-natural-transformation-Large-Precategory τ Y) + ( hom-natural-transformation-Large-Precategory σ Y) ( hom-functor-Large-Precategory F f))) + + comp-natural-transformation-Large-Precategory : + natural-transformation-Large-Precategory C D F H + hom-natural-transformation-Large-Precategory + comp-natural-transformation-Large-Precategory = + hom-comp-natural-transformation-Large-Precategory + naturality-natural-transformation-Large-Precategory + comp-natural-transformation-Large-Precategory = + naturality-comp-natural-transformation-Large-Precategory ``` ## See also diff --git a/src/category-theory/representable-functors-large-precategories.lagda.md b/src/category-theory/representable-functors-large-precategories.lagda.md index 582cf13b69..338e1aa28e 100644 --- a/src/category-theory/representable-functors-large-precategories.lagda.md +++ b/src/category-theory/representable-functors-large-precategories.lagda.md @@ -13,7 +13,10 @@ open import category-theory.natural-transformations-functors-large-precategories open import foundation.category-of-sets open import foundation.function-extensionality +open import foundation.function-types open import foundation.homotopies +open import foundation.identity-types +open import foundation.sets open import foundation.universe-levels ``` @@ -38,20 +41,60 @@ associativity and the left unit law for the precategory `C`. ## Definition ```agda -representable-functor-Large-Precategory : +module _ {α : Level → Level} {β : Level → Level → Level} - (C : Large-Precategory α β) {l : Level} (c : obj-Large-Precategory C l) → - functor-Large-Precategory C (Set-Large-Precategory) (β l) -obj-functor-Large-Precategory (representable-functor-Large-Precategory C c) = - hom-set-Large-Precategory C c -hom-functor-Large-Precategory (representable-functor-Large-Precategory C c) g = - postcomp-hom-Large-Precategory C c g -preserves-comp-functor-Large-Precategory - ( representable-functor-Large-Precategory C c) h g = - eq-htpy (associative-comp-hom-Large-Precategory C h g) -preserves-id-functor-Large-Precategory - ( representable-functor-Large-Precategory C c) = - eq-htpy (left-unit-law-comp-hom-Large-Precategory C) + (C : Large-Precategory α β) {l1 : Level} (c : obj-Large-Precategory C l1) + where + + obj-representable-functor-Large-Precategory : + {l2 : Level} (x : obj-Large-Precategory C l2) → Set (β l1 l2) + obj-representable-functor-Large-Precategory = + hom-set-Large-Precategory C c + + hom-representable-functor-Large-Precategory : + {l2 l3 : Level} + {X : obj-Large-Precategory C l2} {Y : obj-Large-Precategory C l3} → + hom-Large-Precategory C X Y → + type-hom-Set + ( obj-representable-functor-Large-Precategory X) + ( obj-representable-functor-Large-Precategory Y) + hom-representable-functor-Large-Precategory = + postcomp-hom-Large-Precategory C c + + preserves-comp-representable-functor-Large-Precategory : + {l2 l3 l4 : Level} + {X : obj-Large-Precategory C l2} + {Y : obj-Large-Precategory C l3} + {Z : obj-Large-Precategory C l4} + (g : hom-Large-Precategory C Y Z) + (f : hom-Large-Precategory C X Y) → + hom-representable-functor-Large-Precategory + ( comp-hom-Large-Precategory C g f) ＝ + hom-representable-functor-Large-Precategory g ∘ + hom-representable-functor-Large-Precategory f + preserves-comp-representable-functor-Large-Precategory g f = + eq-htpy (associative-comp-hom-Large-Precategory C g f) + + preserves-id-representable-functor-Large-Precategory : + {l2 : Level} {X : obj-Large-Precategory C l2} → + hom-representable-functor-Large-Precategory + ( id-hom-Large-Precategory C {X = X}) ＝ + id + preserves-id-representable-functor-Large-Precategory = + eq-htpy (left-unit-law-comp-hom-Large-Precategory C) + + representable-functor-Large-Precategory : + functor-Large-Precategory (β l1) C (Set-Large-Precategory) + obj-functor-Large-Precategory representable-functor-Large-Precategory = + obj-representable-functor-Large-Precategory + hom-functor-Large-Precategory representable-functor-Large-Precategory = + hom-representable-functor-Large-Precategory + preserves-comp-functor-Large-Precategory + representable-functor-Large-Precategory = + preserves-comp-representable-functor-Large-Precategory + preserves-id-functor-Large-Precategory + representable-functor-Large-Precategory = + preserves-id-representable-functor-Large-Precategory ``` ## Natural transformations between representable functors @@ -62,18 +105,37 @@ from the functor represented by `c` to the functor represented by `b`. Its components `hom c x → hom b x` are defined by precomposition with `f`. ```agda -representable-natural-transformation-Large-Precategory : +module _ {α : Level → Level} {β : Level → Level → Level} (C : Large-Precategory α β) {l1 l2 : Level} (b : obj-Large-Precategory C l1) (c : obj-Large-Precategory C l2) - (f : hom-Large-Precategory C b c) → - natural-transformation-Large-Precategory - ( representable-functor-Large-Precategory C c) - ( representable-functor-Large-Precategory C b) -hom-family-natural-transformation-Large-Precategory - ( representable-natural-transformation-Large-Precategory C b c f) = - precomp-hom-Large-Precategory C f -coherence-square-natural-transformation-Large-Precategory - ( representable-natural-transformation-Large-Precategory C b c f) h = - eq-htpy (inv-htpy (λ g → associative-comp-hom-Large-Precategory C h g f)) + (f : hom-Large-Precategory C b c) + where + + hom-representable-natural-transformation-Large-Precategory : + family-of-morphisms-functor-Large-Precategory C Set-Large-Precategory + ( representable-functor-Large-Precategory C c) + ( representable-functor-Large-Precategory C b) + hom-representable-natural-transformation-Large-Precategory = + precomp-hom-Large-Precategory C f + + naturality-representable-natural-transformation-Large-Precategory : + naturality-family-of-morphisms-functor-Large-Precategory C + ( Set-Large-Precategory) + ( representable-functor-Large-Precategory C c) + ( representable-functor-Large-Precategory C b) + ( hom-representable-natural-transformation-Large-Precategory) + naturality-representable-natural-transformation-Large-Precategory h = + inv (eq-htpy (λ g → associative-comp-hom-Large-Precategory C h g f)) + + representable-natural-transformation-Large-Precategory : + natural-transformation-Large-Precategory C Set-Large-Precategory + ( representable-functor-Large-Precategory C c) + ( representable-functor-Large-Precategory C b) + hom-natural-transformation-Large-Precategory + representable-natural-transformation-Large-Precategory = + hom-representable-natural-transformation-Large-Precategory + naturality-natural-transformation-Large-Precategory + representable-natural-transformation-Large-Precategory = + naturality-representable-natural-transformation-Large-Precategory ``` diff --git a/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md b/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md index 7e5920c717..78637d596c 100644 --- a/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md +++ b/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md @@ -21,11 +21,11 @@ open import foundation.subtypes open import foundation.universe-levels open import group-theory.abelian-groups +open import group-theory.category-of-abelian-groups open import group-theory.groups open import group-theory.homomorphisms-groups open import group-theory.homomorphisms-monoids open import group-theory.monoids -open import group-theory.precategory-of-abelian-groups open import group-theory.semigroups open import group-theory.submonoids @@ -307,10 +307,9 @@ module _ ```agda group-of-units-commutative-ring-functor-Large-Precategory : - functor-Large-Precategory + functor-Large-Precategory id ( Commutative-Ring-Large-Precategory) ( Ab-Large-Precategory) - ( id) obj-functor-Large-Precategory group-of-units-commutative-ring-functor-Large-Precategory = abelian-group-of-units-Commutative-Ring diff --git a/src/foundation/embeddings.lagda.md b/src/foundation/embeddings.lagda.md index 8d29fe181e..d452d631f4 100644 --- a/src/foundation/embeddings.lagda.md +++ b/src/foundation/embeddings.lagda.md @@ -14,6 +14,7 @@ open import foundation.commuting-squares-of-maps open import foundation.cones-over-cospans open import foundation.dependent-pair-types open import foundation.equivalences +open import foundation.fibers-of-maps open import foundation.functoriality-cartesian-product-types open import foundation.fundamental-theorem-of-identity-types open import foundation.identity-types @@ -21,6 +22,7 @@ open import foundation.truncated-maps open import foundation.universe-levels open import foundation-core.cartesian-product-types +open import foundation-core.contractible-types open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies @@ -351,3 +353,39 @@ module _ ( is-equiv-map-inv-is-equiv L) ( M) ``` + +### A map is an embedding if and only if it has contractible fibers at values + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + is-emb-is-contr-fibers-values' : + ((a : A) → is-contr (fiber' f (f a))) → is-emb f + is-emb-is-contr-fibers-values' c a = + fundamental-theorem-id (c a) (λ x → ap f {a} {x}) + + is-emb-is-contr-fibers-values : + ((a : A) → is-contr (fiber f (f a))) → is-emb f + is-emb-is-contr-fibers-values c = + is-emb-is-contr-fibers-values' + ( λ a → + is-contr-equiv' + ( fiber f (f a)) + ( equiv-fiber f (f a)) + ( c a)) + + is-contr-fibers-values-is-emb' : + is-emb f → ((a : A) → is-contr (fiber' f (f a))) + is-contr-fibers-values-is-emb' e a = + fundamental-theorem-id' (λ x → ap f {a} {x}) (e a) + + is-contr-fibers-values-is-emb : + is-emb f → ((a : A) → is-contr (fiber f (f a))) + is-contr-fibers-values-is-emb e a = + is-contr-equiv + ( fiber' f (f a)) + ( equiv-fiber f (f a)) + ( is-contr-fibers-values-is-emb' e a) +``` diff --git a/src/foundation/epimorphisms.lagda.md b/src/foundation/epimorphisms.lagda.md index 701132c370..9db0964a3c 100644 --- a/src/foundation/epimorphisms.lagda.md +++ b/src/foundation/epimorphisms.lagda.md @@ -7,10 +7,26 @@ module foundation.epimorphisms where
Imports ```agda +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.propositional-maps +open import foundation.sections open import foundation.universe-levels +open import foundation-core.commuting-squares-of-maps open import foundation-core.embeddings +open import foundation-core.equivalences +open import foundation-core.fibers-of-maps open import foundation-core.function-types +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.propositions + +open import synthetic-homotopy-theory.cocones-under-spans +open import synthetic-homotopy-theory.codiagonals-of-maps +open import synthetic-homotopy-theory.pushouts +open import synthetic-homotopy-theory.universal-property-pushouts ```
@@ -28,13 +44,100 @@ is an [embedding](foundation-core.embeddings.md) for every type `X`. ## Definitions +### Epimorphisms with respect to a specified universe + ```agda module _ - {l1 l2 : Level} (l : Level) {A : UU l1} {B : UU l2} + {l1 l2 : Level} {A : UU l1} {B : UU l2} where + is-epimorphism-Level : (l : Level) → (A → B) → UU (l1 ⊔ l2 ⊔ lsuc l) + is-epimorphism-Level l f = (X : UU l) → is-emb (precomp f X) +``` + +### Epimorphisms + +```agda is-epimorphism : (A → B) → UUω - is-epimorphism f = {l : Level} (X : UU l) → is-emb (precomp f X) + is-epimorphism f = {l : Level} → is-epimorphism-Level l f +``` + +## Properties + +### The codiagonal of an epimorphism is an equivalence + +If the map `f : A → B` is epi, then the commutative square + +```text + f + A → B + f ↓ ↓ id + B → B + id +``` + +is a pushout square. + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (X : UU l3) + where + + equiv-fibers-precomp-cocone : + Σ (B → X) (λ g → fiber (precomp f X) (g ∘ f)) ≃ cocone f f X + equiv-fibers-precomp-cocone = + equiv-tot ( λ g → + ( equiv-tot (λ h → equiv-funext) ∘e + ( equiv-fiber (precomp f X) (g ∘ f)))) + + diagonal-into-fibers-precomp : + (B → X) → Σ (B → X) (λ g → fiber (precomp f X) (g ∘ f)) + diagonal-into-fibers-precomp = map-section-family (λ g → g , refl) + + is-equiv-diagonal-into-fibers-precomp-is-epimorphism : + is-epimorphism f → is-equiv diagonal-into-fibers-precomp + is-equiv-diagonal-into-fibers-precomp-is-epimorphism e = + is-equiv-map-section-family + ( λ g → (g , refl)) + ( λ g → + is-proof-irrelevant-is-prop + ( is-prop-map-is-emb (e X) (g ∘ f)) + ( g , refl)) + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + universal-property-pushout-is-epimorphism : + is-epimorphism f → + {l : Level} → universal-property-pushout l f f (cocone-codiagonal-map f) + universal-property-pushout-is-epimorphism e X = + is-equiv-comp + ( map-equiv (equiv-fibers-precomp-cocone f X)) + ( diagonal-into-fibers-precomp f X) + ( is-equiv-diagonal-into-fibers-precomp-is-epimorphism f X e) + ( is-equiv-map-equiv (equiv-fibers-precomp-cocone f X)) +``` + +If the map `f : A → B` is epi, then its codiagonal is an equivalence. + +```agda + is-equiv-codiagonal-map-is-epimorphism : + is-epimorphism f → is-equiv (codiagonal-map f) + is-equiv-codiagonal-map-is-epimorphism e = + is-equiv-up-pushout-up-pushout f f + ( cocone-pushout f f) + ( cocone-codiagonal-map f) + ( codiagonal-map f) + ( compute-inl-codiagonal-map f , + compute-inr-codiagonal-map f , + compute-glue-codiagonal-map f) + ( up-pushout f f) + ( universal-property-pushout-is-epimorphism e) + + is-pushout-is-epimorphism : + is-epimorphism f → is-pushout f f (cocone-codiagonal-map f) + is-pushout-is-epimorphism = is-equiv-codiagonal-map-is-epimorphism ``` ## See also diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md index f4931ecfea..917c06bbea 100644 --- a/src/group-theory.lagda.md +++ b/src/group-theory.lagda.md @@ -13,6 +13,7 @@ open import group-theory.cartesian-products-concrete-groups public open import group-theory.cartesian-products-groups public open import group-theory.cartesian-products-monoids public open import group-theory.cartesian-products-semigroups public +open import group-theory.category-of-abelian-groups public open import group-theory.category-of-concrete-groups public open import group-theory.category-of-groups public open import group-theory.category-of-semigroups public @@ -130,7 +131,6 @@ open import group-theory.perfect-subgroups public open import group-theory.powers-of-elements-commutative-monoids public open import group-theory.powers-of-elements-groups public open import group-theory.powers-of-elements-monoids public -open import group-theory.precategory-of-abelian-groups public open import group-theory.precategory-of-commutative-monoids public open import group-theory.precategory-of-concrete-groups public open import group-theory.precategory-of-group-actions public diff --git a/src/group-theory/category-of-abelian-groups.lagda.md b/src/group-theory/category-of-abelian-groups.lagda.md new file mode 100644 index 0000000000..34a9f54fbd --- /dev/null +++ b/src/group-theory/category-of-abelian-groups.lagda.md @@ -0,0 +1,52 @@ +# The category of abelian groups + +```agda +module group-theory.category-of-abelian-groups where +``` + +
Imports + +```agda +open import category-theory.categories +open import category-theory.full-large-subcategories +open import category-theory.large-categories +open import category-theory.large-precategories +open import category-theory.precategories + +open import foundation.universe-levels + +open import group-theory.abelian-groups +open import group-theory.category-of-groups +``` + +
+ +## Idea + +The **category of abelian groups** is the +[full large subcategory](category-theory.full-large-subcategories.md) of the +[category of groups](group-theory.category-of-groups.md) consisting of +[groups](group-theory.groups.md) of which the group operation is +[commutative](group-theory.abelian-groups.md). + +## Definitions + +### The category of abelian groups + +```agda +Ab-Large-Category : Large-Category lsuc _⊔_ +Ab-Large-Category = + large-category-Full-Large-Subcategory + ( Group-Large-Category) + ( is-abelian-group-Prop) + +Ab-Large-Precategory : Large-Precategory lsuc _⊔_ +Ab-Large-Precategory = + large-precategory-Large-Category Ab-Large-Category + +Ab-Category : (l : Level) → Category (lsuc l) l +Ab-Category = category-Large-Category Ab-Large-Category + +Ab-Precategory : (l : Level) → Precategory (lsuc l) l +Ab-Precategory = precategory-Large-Category Ab-Large-Category +``` diff --git a/src/group-theory/cores-monoids.lagda.md b/src/group-theory/cores-monoids.lagda.md index aaa7e1a7d3..7a6109893d 100644 --- a/src/group-theory/cores-monoids.lagda.md +++ b/src/group-theory/cores-monoids.lagda.md @@ -226,7 +226,7 @@ module _ ```agda core-monoid-functor-Large-Precategory : - functor-Large-Precategory Monoid-Large-Precategory Group-Large-Precategory id + functor-Large-Precategory id Monoid-Large-Precategory Group-Large-Precategory obj-functor-Large-Precategory core-monoid-functor-Large-Precategory = core-Monoid diff --git a/src/group-theory/precategory-of-abelian-groups.lagda.md b/src/group-theory/precategory-of-abelian-groups.lagda.md deleted file mode 100644 index 60d38dbcce..0000000000 --- a/src/group-theory/precategory-of-abelian-groups.lagda.md +++ /dev/null @@ -1,60 +0,0 @@ -# The precategory of abelian groups - -```agda -module group-theory.precategory-of-abelian-groups where -``` - -
Imports - -```agda -open import category-theory.large-precategories -open import category-theory.precategories - -open import foundation.universe-levels - -open import group-theory.abelian-groups -open import group-theory.homomorphisms-abelian-groups -``` - -
- -## Idea - -The **precategory of abelian groups** consists of abelian groups and group -homomorphisms. - -## Definition - -### The large precategory of abelian groups - -```agda -Ab-Large-Precategory : Large-Precategory lsuc (_⊔_) -Large-Precategory.obj-Large-Precategory - Ab-Large-Precategory = - Ab -Large-Precategory.hom-set-Large-Precategory - Ab-Large-Precategory = - hom-set-Ab -Large-Precategory.comp-hom-Large-Precategory - Ab-Large-Precategory {X = A} {B} {C} = - comp-hom-Ab A B C -Large-Precategory.id-hom-Large-Precategory - Ab-Large-Precategory {X = A} = - id-hom-Ab A -Large-Precategory.associative-comp-hom-Large-Precategory - Ab-Large-Precategory {X = A} {B} {C} {D} = - associative-comp-hom-Ab A B C D -Large-Precategory.left-unit-law-comp-hom-Large-Precategory - Ab-Large-Precategory {X = A} {B} = - left-unit-law-comp-hom-Ab A B -Large-Precategory.right-unit-law-comp-hom-Large-Precategory - Ab-Large-Precategory {X = A} {B} = - right-unit-law-comp-hom-Ab A B -``` - -### The small categories of abelian groups - -```agda -Ab-Precategory : (l : Level) → Precategory (lsuc l) l -Ab-Precategory = precategory-Large-Precategory Ab-Large-Precategory -``` diff --git a/src/group-theory/substitution-functor-group-actions.lagda.md b/src/group-theory/substitution-functor-group-actions.lagda.md index 94ff4fc9dd..7b573d77db 100644 --- a/src/group-theory/substitution-functor-group-actions.lagda.md +++ b/src/group-theory/substitution-functor-group-actions.lagda.md @@ -15,6 +15,7 @@ open import foundation.dependent-pair-types open import foundation.equivalence-classes open import foundation.equivalence-relations open import foundation.existential-quantification +open import foundation.function-types open import foundation.identity-types open import foundation.propositional-truncations open import foundation.sets @@ -85,10 +86,9 @@ module _ preserves-comp-subst-Abstract-Group-Action X Y Z g f = refl subst-Abstract-Group-Action : - functor-Large-Precategory + functor-Large-Precategory id ( Abstract-Group-Action-Large-Precategory H) ( Abstract-Group-Action-Large-Precategory G) - ( λ l → l) obj-functor-Large-Precategory subst-Abstract-Group-Action = obj-subst-Abstract-Group-Action hom-functor-Large-Precategory subst-Abstract-Group-Action {X = X} {Y} = @@ -96,7 +96,8 @@ module _ preserves-comp-functor-Large-Precategory subst-Abstract-Group-Action {l1} {l2} {l3} {X} {Y} {Z} = preserves-comp-subst-Abstract-Group-Action X Y Z - preserves-id-functor-Large-Precategory subst-Abstract-Group-Action {l1} {X} = + preserves-id-functor-Large-Precategory + subst-Abstract-Group-Action {l1} {X} = preserves-id-subst-Abstract-Group-Action X ``` diff --git a/src/ring-theory/groups-of-units-rings.lagda.md b/src/ring-theory/groups-of-units-rings.lagda.md index 2c1bfce80b..80f85ac6eb 100644 --- a/src/ring-theory/groups-of-units-rings.lagda.md +++ b/src/ring-theory/groups-of-units-rings.lagda.md @@ -247,7 +247,10 @@ module _ ```agda group-of-units-ring-functor-Large-Precategory : - functor-Large-Precategory Ring-Large-Precategory Group-Large-Precategory id + functor-Large-Precategory + ( λ l → l) + ( Ring-Large-Precategory) + ( Group-Large-Precategory) obj-functor-Large-Precategory group-of-units-ring-functor-Large-Precategory = group-of-units-Ring diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md index 03be0502f7..0905d11402 100644 --- a/src/synthetic-homotopy-theory.lagda.md +++ b/src/synthetic-homotopy-theory.lagda.md @@ -53,10 +53,12 @@ open import synthetic-homotopy-theory.join-powers-of-types public open import synthetic-homotopy-theory.joins-of-types public open import synthetic-homotopy-theory.loop-spaces public open import synthetic-homotopy-theory.maps-of-prespectra public +open import synthetic-homotopy-theory.mere-spheres public open import synthetic-homotopy-theory.morphisms-descent-data-circle public open import synthetic-homotopy-theory.multiplication-circle public open import synthetic-homotopy-theory.plus-principle public open import synthetic-homotopy-theory.powers-of-loops public +open import synthetic-homotopy-theory.premanifolds public open import synthetic-homotopy-theory.prespectra public open import synthetic-homotopy-theory.pullback-property-pushouts public open import synthetic-homotopy-theory.pushouts public @@ -70,6 +72,7 @@ open import synthetic-homotopy-theory.suspension-prespectra public open import synthetic-homotopy-theory.suspension-structures public open import synthetic-homotopy-theory.suspensions-of-pointed-types public open import synthetic-homotopy-theory.suspensions-of-types public +open import synthetic-homotopy-theory.tangent-spheres public open import synthetic-homotopy-theory.triple-loop-spaces public open import synthetic-homotopy-theory.universal-cover-circle public open import synthetic-homotopy-theory.universal-property-circle public diff --git a/src/synthetic-homotopy-theory/mere-spheres.lagda.md b/src/synthetic-homotopy-theory/mere-spheres.lagda.md new file mode 100644 index 0000000000..70a895594b --- /dev/null +++ b/src/synthetic-homotopy-theory/mere-spheres.lagda.md @@ -0,0 +1,62 @@ +# Mere spheres + +```agda +module synthetic-homotopy-theory.mere-spheres where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.dependent-pair-types +open import foundation.mere-equivalences +open import foundation.propositions +open import foundation.universe-levels + +open import synthetic-homotopy-theory.spheres +``` + +
+ +## Idea + +A **mere `n`-sphere** is a type `X` that is +[merely equivalent](foundation.mere-equivalences.md) to the +[`n`-sphere](synthetic-homotopy-theory.spheres.md). + +## Definitions + +### The predicate of being a mere `n`-sphere + +```agda +module _ + {l : Level} (n : ℕ) (X : UU l) + where + + is-mere-sphere-Prop : Prop l + is-mere-sphere-Prop = mere-equiv-Prop (sphere n) X + + is-mere-sphere : UU l + is-mere-sphere = type-Prop is-mere-sphere-Prop + + is-prop-is-mere-sphere : is-prop is-mere-sphere + is-prop-is-mere-sphere = is-prop-type-Prop is-mere-sphere-Prop +``` + +### Mere spheres + +```agda +mere-sphere : (l : Level) (n : ℕ) → UU (lsuc l) +mere-sphere l n = Σ (UU l) (is-mere-sphere n) + +module _ + {l : Level} (n : ℕ) (X : mere-sphere l n) + where + + type-mere-sphere : UU l + type-mere-sphere = pr1 X + + mere-equiv-mere-sphere : mere-equiv (sphere n) type-mere-sphere + mere-equiv-mere-sphere = pr2 X +``` diff --git a/src/synthetic-homotopy-theory/premanifolds.lagda.md b/src/synthetic-homotopy-theory/premanifolds.lagda.md new file mode 100644 index 0000000000..99d31810ac --- /dev/null +++ b/src/synthetic-homotopy-theory/premanifolds.lagda.md @@ -0,0 +1,104 @@ +# Premanifolds + +```agda +module synthetic-homotopy-theory.premanifolds where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.commuting-squares-of-maps +open import foundation.dependent-pair-types +open import foundation.mere-equivalences +open import foundation.unit-type +open import foundation.universe-levels + +open import synthetic-homotopy-theory.cocones-under-spans +open import synthetic-homotopy-theory.mere-spheres +open import synthetic-homotopy-theory.pushouts +open import synthetic-homotopy-theory.spheres +open import synthetic-homotopy-theory.tangent-spheres +``` + +
+ +## Idea + +An **`n`-dimensional premanifold** is a type `M` such that every element `x : M` +comes equipped with a +[tangent `n`-sphere](synthetic-homotopy-theory.tangent-spheres.md). + +## Definitions + +### Premanifolds + +```agda +Premanifold : (l : Level) (n : ℕ) → UU (lsuc l) +Premanifold l n = Σ (UU l) (λ M → (x : M) → has-tangent-sphere n x) + +module _ + {l : Level} (n : ℕ) (M : Premanifold l n) + where + + type-Premanifold : UU l + type-Premanifold = pr1 M + + tangent-sphere-Premanifold : (x : type-Premanifold) → mere-sphere lzero n + tangent-sphere-Premanifold x = + tangent-sphere-has-tangent-sphere n (pr2 M x) + + type-tangent-sphere-Premanifold : (x : type-Premanifold) → UU lzero + type-tangent-sphere-Premanifold x = + type-tangent-sphere-has-tangent-sphere n (pr2 M x) + + mere-equiv-tangent-sphere-Premanifold : + (x : type-Premanifold) → + mere-equiv (sphere n) (type-tangent-sphere-Premanifold x) + mere-equiv-tangent-sphere-Premanifold x = + mere-equiv-tangent-sphere-has-tangent-sphere n (pr2 M x) + + complement-Premanifold : (x : type-Premanifold) → UU l + complement-Premanifold x = + complement-has-tangent-sphere n (pr2 M x) + + inclusion-tangent-sphere-Premanifold : + (x : type-Premanifold) → + type-tangent-sphere-Premanifold x → complement-Premanifold x + inclusion-tangent-sphere-Premanifold x = + inclusion-tangent-sphere-has-tangent-sphere n (pr2 M x) + + inclusion-complement-Premanifold : + (x : type-Premanifold) → complement-Premanifold x → type-Premanifold + inclusion-complement-Premanifold x = + inclusion-complement-has-tangent-sphere n (pr2 M x) + + coherence-square-Premanifold : + (x : type-Premanifold) → + coherence-square-maps + ( inclusion-tangent-sphere-Premanifold x) + ( terminal-map) + ( inclusion-complement-Premanifold x) + ( point x) + coherence-square-Premanifold x = + coherence-square-has-tangent-sphere n (pr2 M x) + + cocone-Premanifold : + (x : type-Premanifold) → + cocone + ( terminal-map) + ( inclusion-tangent-sphere-Premanifold x) + ( type-Premanifold) + cocone-Premanifold x = + cocone-has-tangent-sphere n (pr2 M x) + + is-pushout-Premanifold : + (x : type-Premanifold) → + is-pushout + ( terminal-map) + ( inclusion-tangent-sphere-Premanifold x) + ( cocone-Premanifold x) + is-pushout-Premanifold x = + is-pushout-has-tangent-sphere n (pr2 M x) +``` diff --git a/src/synthetic-homotopy-theory/tangent-spheres.lagda.md b/src/synthetic-homotopy-theory/tangent-spheres.lagda.md new file mode 100644 index 0000000000..94a327f9d6 --- /dev/null +++ b/src/synthetic-homotopy-theory/tangent-spheres.lagda.md @@ -0,0 +1,126 @@ +# Tangent spheres + +```agda +module synthetic-homotopy-theory.tangent-spheres where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.commuting-squares-of-maps +open import foundation.dependent-pair-types +open import foundation.mere-equivalences +open import foundation.unit-type +open import foundation.universe-levels + +open import synthetic-homotopy-theory.cocones-under-spans +open import synthetic-homotopy-theory.mere-spheres +open import synthetic-homotopy-theory.pushouts +open import synthetic-homotopy-theory.spheres +``` + +
+ +## Idea + +Consider a type `X` and a point `x : X`. We say that `x` **has a tangent +`n`-sphere** if we can construct the following data: + +- A [mere sphere](synthetic-homotopy-theory.mere-spheres.md) `T`, which we also + refer to as the **tangent sphere** of `x`. +- A type `C`, which we call the **complement** of `x`. +- A map `j : T → C` including the tangent sphere into the complement. +- A map `i : C → X` including the complement into the type `X`. +- A [homotopy](foundation-core.homotopies.md) witnessing that the square + ```text + j + T -----> C + | | + | | i + V V + 1 -----> X + x + ``` + [commutes](foundation.commuting-squares-of-maps.md), and is a + [pushout](synthetic-homotopy-theory.pushouts.md). + +In other words, a tangent `n`-sphere at a point `x` consistst of a mere sphere +and a complement such that the space `X` can be reconstructed by attaching the +point to the complement via the inclusion of the tangent sphere into the +complement. + +## Definitions + +### The predicate of having a tangent sphere + +```agda +module _ + {l : Level} (n : ℕ) {X : UU l} (x : X) + where + + has-tangent-sphere : UU (lsuc l) + has-tangent-sphere = + Σ ( mere-sphere lzero n) + ( λ T → + Σ ( UU l) + ( λ C → + Σ ( type-mere-sphere n T → C) + ( λ j → + Σ ( C → X) + ( λ i → + Σ ( coherence-square-maps j terminal-map i (point x)) + ( λ H → + is-pushout terminal-map j (point x , i , H)))))) + +module _ + {l : Level} (n : ℕ) {X : UU l} {x : X} (T : has-tangent-sphere n x) + where + + tangent-sphere-has-tangent-sphere : mere-sphere lzero n + tangent-sphere-has-tangent-sphere = pr1 T + + type-tangent-sphere-has-tangent-sphere : UU lzero + type-tangent-sphere-has-tangent-sphere = + type-mere-sphere n tangent-sphere-has-tangent-sphere + + mere-equiv-tangent-sphere-has-tangent-sphere : + mere-equiv (sphere n) type-tangent-sphere-has-tangent-sphere + mere-equiv-tangent-sphere-has-tangent-sphere = + mere-equiv-mere-sphere n tangent-sphere-has-tangent-sphere + + complement-has-tangent-sphere : UU l + complement-has-tangent-sphere = pr1 (pr2 T) + + inclusion-tangent-sphere-has-tangent-sphere : + type-tangent-sphere-has-tangent-sphere → complement-has-tangent-sphere + inclusion-tangent-sphere-has-tangent-sphere = pr1 (pr2 (pr2 T)) + + inclusion-complement-has-tangent-sphere : + complement-has-tangent-sphere → X + inclusion-complement-has-tangent-sphere = pr1 (pr2 (pr2 (pr2 T))) + + coherence-square-has-tangent-sphere : + coherence-square-maps + ( inclusion-tangent-sphere-has-tangent-sphere) + ( terminal-map) + ( inclusion-complement-has-tangent-sphere) + ( point x) + coherence-square-has-tangent-sphere = + pr1 (pr2 (pr2 (pr2 (pr2 T)))) + + cocone-has-tangent-sphere : + cocone terminal-map inclusion-tangent-sphere-has-tangent-sphere X + pr1 cocone-has-tangent-sphere = point x + pr1 (pr2 cocone-has-tangent-sphere) = inclusion-complement-has-tangent-sphere + pr2 (pr2 cocone-has-tangent-sphere) = coherence-square-has-tangent-sphere + + is-pushout-has-tangent-sphere : + is-pushout + ( terminal-map) + ( inclusion-tangent-sphere-has-tangent-sphere) + ( cocone-has-tangent-sphere) + is-pushout-has-tangent-sphere = + pr2 (pr2 (pr2 (pr2 (pr2 T)))) +``` diff --git a/tables/categories.md b/tables/categories.md index cf232bee88..67bddd649d 100644 --- a/tables/categories.md +++ b/tables/categories.md @@ -1,5 +1,6 @@ | Category | File | | ----------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | +| Abelian groups | [`group-theory.category-of-abelian-groups`](group-theory.category-of-abelian-groups.md) | | Commutative Rings | [`commutative-algebra.category-of-commutative-rings`](commutative-algebra.category-of-commutative-rings.md) | | Connected set bundles over 𝕊¹ | [`synthetic-homotopy-theory.category-of-connected-set-bundles-circle`](synthetic-homotopy-theory.category-of-connected-set-bundles-circle.md) | | Families of sets | [`foundation.category-of-families-of-sets`](foundation.category-of-families-of-sets.md) | diff --git a/tables/precategories.md b/tables/precategories.md index de35225da8..7d3f0c91f9 100644 --- a/tables/precategories.md +++ b/tables/precategories.md @@ -1,6 +1,6 @@ | Precategory | File | | ---------------------- | ------------------------------------------------------------------------------------------------------------------------- | -| Abelian groups | [`group-theory.precategory-of-abelian-groups`](group-theory.precategory-of-abelian-groups.md) | +| Abelian groups | [`group-theory.category-of-abelian-groups`](group-theory.category-of-abelian-groups.md) | | Commutative monoids | [`group-theory.precategory-of-commutative-monoids`](group-theory.precategory-of-commutative-monoids.md) | | Commutative rings | [`commutative-algebra.precategory-of-commutative-rings`](commutative-algebra.precategory-of-commutative-rings.md) | | Commutative semirings | [`commutative-algebra.precategory-of-commutative-semirings`](commutative-algebra.precategory-of-commutative-semirings.md) |