diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index 4e78e73234..fdcd9c6cd7 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -25,6 +25,7 @@ open import category-theory.category-of-functors public open import category-theory.category-of-functors-from-small-to-large-categories public open import category-theory.category-of-maps-categories public open import category-theory.category-of-maps-from-small-to-large-categories public +open import category-theory.category-of-simplicial-sets public open import category-theory.commuting-squares-of-morphisms-in-large-precategories public open import category-theory.commuting-squares-of-morphisms-in-precategories public open import category-theory.commuting-squares-of-morphisms-in-set-magmoids public diff --git a/src/category-theory/category-of-simplicial-sets.lagda.md b/src/category-theory/category-of-simplicial-sets.lagda.md new file mode 100644 index 0000000000..6797000786 --- /dev/null +++ b/src/category-theory/category-of-simplicial-sets.lagda.md @@ -0,0 +1,169 @@ +# The category of simplicial sets + +```agda +module category-theory.category-of-simplicial-sets where +``` + +
Imports + +```agda +open import category-theory.categories +open import category-theory.large-categories +open import category-theory.large-precategories +open import category-theory.precategories +open import category-theory.presheaf-categories +open import category-theory.simplex-category + +open import foundation.commuting-squares-of-maps +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.sets +open import foundation.strictly-involutive-identity-types +open import foundation.universe-levels +``` + +
+ +## Idea + +The {{#concept "large category of simplicial sets" Agda=sSet-Large-Category}} is +the [presheaf category](category-theory.presheaf-categories.md) on the +[simplex category](category-theory.simplex-category.md) + +```text + Δᵒᵖ → Set. +``` + +To this large category, there is an associated +[small category](category-theory.categories.md) of **small simplicial sets**, +taking values in small [sets](foundation-core.sets.md). + +## Definitions + +### The large category of simplicial sets + +```agda +sSet-Large-Precategory : + Large-Precategory lsuc (_⊔_) +sSet-Large-Precategory = + presheaf-large-precategory-Precategory simplex-Precategory + +is-large-category-sSet-Large-Category : + is-large-category-Large-Precategory sSet-Large-Precategory +is-large-category-sSet-Large-Category = + is-large-category-presheaf-large-category-Precategory simplex-Precategory + +sSet-Large-Category : + Large-Category lsuc (_⊔_) +sSet-Large-Category = + presheaf-large-category-Precategory simplex-Precategory + +sSet : (l : Level) → UU (lsuc l) +sSet = obj-Large-Category sSet-Large-Category + +module _ + {l1 : Level} (X : sSet l1) + where + + element-set-sSet : obj-simplex-Category → Set l1 + element-set-sSet = element-set-presheaf-Precategory simplex-Precategory X + + element-sSet : obj-simplex-Category → UU l1 + element-sSet X = type-Set (element-set-sSet X) + + action-sSet : + {X Y : obj-simplex-Category} → + hom-simplex-Category X Y → element-sSet Y → element-sSet X + action-sSet = action-presheaf-Precategory simplex-Precategory X + + preserves-id-action-sSet : + {X : obj-simplex-Category} → + action-sSet {X} {X} (id-hom-simplex-Category X) ~ id + preserves-id-action-sSet = + preserves-id-action-presheaf-Precategory simplex-Precategory X + + preserves-comp-action-sSet : + {X Y Z : obj-simplex-Category} + (g : hom-simplex-Category Y Z) (f : hom-simplex-Category X Y) → + action-sSet (comp-hom-simplex-Category g f) ~ + action-sSet f ∘ action-sSet g + preserves-comp-action-sSet = + preserves-comp-action-presheaf-Precategory simplex-Precategory X + +hom-set-sSet : {l1 l2 : Level} (X : sSet l1) (Y : sSet l2) → Set (l1 ⊔ l2) +hom-set-sSet = hom-set-Large-Category sSet-Large-Category + +hom-sSet : {l1 l2 : Level} (X : sSet l1) (Y : sSet l2) → UU (l1 ⊔ l2) +hom-sSet = hom-Large-Category sSet-Large-Category + +module _ + {l1 l2 : Level} (X : sSet l1) (Y : sSet l2) (h : hom-sSet X Y) + where + + map-hom-sSet : + (F : obj-simplex-Category) → element-sSet X F → element-sSet Y F + map-hom-sSet = map-hom-presheaf-Precategory simplex-Precategory X Y h + + naturality-hom-sSet : + {F E : obj-simplex-Category} (f : hom-simplex-Category F E) → + coherence-square-maps + ( action-sSet X f) + ( map-hom-sSet E) + ( map-hom-sSet F) + ( action-sSet Y f) + naturality-hom-sSet = + naturality-hom-presheaf-Precategory simplex-Precategory X Y h + +comp-hom-sSet : + {l1 l2 l3 : Level} (X : sSet l1) (Y : sSet l2) (Z : sSet l3) → + hom-sSet Y Z → hom-sSet X Y → hom-sSet X Z +comp-hom-sSet = comp-hom-presheaf-Precategory simplex-Precategory + +id-hom-sSet : {l1 : Level} (X : sSet l1) → hom-sSet X X +id-hom-sSet = id-hom-presheaf-Precategory simplex-Precategory + +associative-comp-hom-sSet : + {l1 l2 l3 l4 : Level} + (X : sSet l1) (Y : sSet l2) (Z : sSet l3) (W : sSet l4) + (h : hom-sSet Z W) (g : hom-sSet Y Z) (f : hom-sSet X Y) → + comp-hom-sSet X Y W (comp-hom-sSet Y Z W h g) f ＝ + comp-hom-sSet X Z W h (comp-hom-sSet X Y Z g f) +associative-comp-hom-sSet = + associative-comp-hom-presheaf-Precategory simplex-Precategory + +involutive-eq-associative-comp-hom-sSet : + {l1 l2 l3 l4 : Level} + (X : sSet l1) (Y : sSet l2) (Z : sSet l3) (W : sSet l4) + (h : hom-sSet Z W) (g : hom-sSet Y Z) (f : hom-sSet X Y) → + comp-hom-sSet X Y W (comp-hom-sSet Y Z W h g) f ＝ⁱ + comp-hom-sSet X Z W h (comp-hom-sSet X Y Z g f) +involutive-eq-associative-comp-hom-sSet = + involutive-eq-associative-comp-hom-presheaf-Precategory simplex-Precategory + +left-unit-law-comp-hom-sSet : + {l1 l2 : Level} (X : sSet l1) (Y : sSet l2) (f : hom-sSet X Y) → + comp-hom-sSet X Y Y (id-hom-sSet Y) f ＝ f +left-unit-law-comp-hom-sSet = + left-unit-law-comp-hom-presheaf-Precategory simplex-Precategory + +right-unit-law-comp-hom-sSet : + {l1 l2 : Level} (X : sSet l1) (Y : sSet l2) (f : hom-sSet X Y) → + comp-hom-sSet X X Y f (id-hom-sSet X) ＝ f +right-unit-law-comp-hom-sSet = + right-unit-law-comp-hom-presheaf-Precategory simplex-Precategory +``` + +### The category of small simplicial sets + +```agda +sSet-Precategory : (l : Level) → Precategory (lsuc l) l +sSet-Precategory = precategory-Large-Category sSet-Large-Category + +sSet-Category : (l : Level) → Category (lsuc l) l +sSet-Category = category-Large-Category sSet-Large-Category +``` + +## External links + +- [simplicial set](https://ncatlab.org/nlab/show/simplicial+set) on $n$Lab diff --git a/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md b/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md index d4e50dfdf4..bf33a03810 100644 --- a/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md +++ b/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md @@ -217,12 +217,15 @@ module _ ### Being unital is a property of composition operations on binary families of sets -**Proof:** Suppose `e e' : (x : A) → hom-set x x` are both right and left units -with regard to composition. It is enough to show that `e ＝ e'` since the right -and left unit laws are propositions (because all hom-types are sets). By -function extensionality, it is enough to show that `e x ＝ e' x` for all -`x : A`. But by the unit laws we have the following chain of equalities: -`e x ＝ (e' x) ∘ (e x) ＝ e' x.` +**Proof:** Suppose `e e' : (x : A) → hom x x` are both two-sided units with +respect to composition. It is enough to show that `e ＝ e'` since the right and +left unit laws are propositions by the set-condition on hom-types. By function +extensionality, it is enough to show that `e x ＝ e' x` for all `x : A`, and by +the unit laws we have: + +```text + e x ＝ (e' x) ∘ (e x) ＝ e' x. ∎ +``` ```agda module _ diff --git a/src/category-theory/set-magmoids.lagda.md b/src/category-theory/set-magmoids.lagda.md index 27ed64102e..c037ebaff6 100644 --- a/src/category-theory/set-magmoids.lagda.md +++ b/src/category-theory/set-magmoids.lagda.md @@ -22,18 +22,20 @@ open import foundation.universe-levels ## Idea -A **set-magmoid** is the [structure](foundation.structure.md) of a +A {{#concept "set-magmoid" Agda=Set-Magmoid}} is the +[structure](foundation.structure.md) of a [composition operation on a binary family of sets](category-theory.composition-operations-on-binary-families-of-sets.md), -and are in one sense the "oidification" of [magmas](structured-types.magmas.md) -in [sets](foundation-core.sets.md). We call elements of the indexing type -**objects**, and elements of the set-family **morphisms** or **homomorphisms**. +and are the _oidification_ of [magmas](structured-types.magmas.md) in +[sets](foundation-core.sets.md) in one sense of the term. We call elements of +the indexing type **objects**, and elements of the set-family **morphisms** or +**homomorphisms**. -These objects serve as our starting point in the study of the +Set-magmoids serve as our starting point in the study of the [structure](foundation.structure.md) of [categories](category-theory.categories.md). Indeed, categories form a [subtype](foundation-core.subtypes.md) of set-magmoids, although -structure-preserving maps of set-magmoids do not automatically preserve -identity-morphisms. +structure-preserving maps of set-magmoids do not automatically preserve identity +morphisms. Set-magmoids are commonly referred to as _magmoids_ in the literature, but we use the "set-" prefix to make clear its relation to magmas. Set-magmoids should @@ -152,12 +154,15 @@ module _ ### The predicate on set-magmoids of being unital **Proof:** To show that unitality is a proposition, suppose -`e e' : (x : A) → hom-set x x` are both right and left units with regard to -composition. It is enough to show that `e ＝ e'` since the right and left unit -laws are propositions (because all hom-types are sets). By function -extensionality, it is enough to show that `e x ＝ e' x` for all `x : A`. But by -the unit laws we have the following chain of equalities: -`e x ＝ (e' x) ∘ (e x) ＝ e' x.` +`e e' : (x : A) → hom x x` are both two-sided units with respect to composition. +It is enough to show that `e ＝ e'` since the right and left unit laws are +propositions by the set-condition on hom-types. By function extensionality, it +is enough to show that `e x ＝ e' x` for all `x : A`, and by the unit laws we +have: + +```text + e x ＝ (e' x) ∘ (e x) ＝ e' x. ∎ +``` ```agda module _ @@ -218,6 +223,8 @@ module _ ## See also +- [Magmas](structured-types.magmas.md) are types equipped with a binary + operation. - [Nonunital precategories](category-theory.nonunital-precategories.md) are associative set-magmoids. - [Precategories](category-theory.precategories.md) are associative and unital diff --git a/tables/categories.md b/tables/categories.md index 36d52caf02..54b3136228 100644 --- a/tables/categories.md +++ b/tables/categories.md @@ -1,13 +1,23 @@ -| 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) | -| Groups | [`group-theory.category-of-groups`](group-theory.category-of-groups.md) | -| `G`-sets | [`group-theory.category-of-group-actions`](group-theory.category-of-group-actions.md) | -| Metric spaces and isometries | [`metric-spaces.category-of-metric-spaces-and-isometries`](metric-spaces.category-of-metric-spaces-and-isometries.md) | -| Metric spaces and short functions | [`metric-spaces.category-of-metric-spaces-and-short-functions`](metric-spaces.category-of-metric-spaces-and-short-functions.md) | -| Rings | [`ring-theory.category-of-rings`](ring-theory.category-of-rings.md) | -| Semigroups | [`group-theory.category-of-semigroups`](group-theory.category-of-semigroups.md) | -| Sets | [`foundation.category-of-sets`](foundation.category-of-sets.md) | +| Category | File | +| --------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Abelian groups | [`group-theory.category-of-abelian-groups`](group-theory.category-of-abelian-groups.md) | +| Augmented simplex category | [`category-theory.augmented-simplex-category`](category-theory.augmented-simplex-category.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) | +| Copresheaves on a precategory | [`category-theory.copresheaf-categories`](category-theory.copresheaf-categories.md) | +| Cyclic rings | [`ring-theory.category-of-cyclic-rings`](ring-theory.category-of-cyclic-rings.md) | +| Functors between two categories | [`category-theory.category-of-functors`](category-theory.category-of-functors.md) [`category-theory.category-of-functors-from-small-to-large-categories`](category-theory.category-of-functors-from-small-to-large-categories.md) | +| Families of sets | [`foundation.category-of-families-of-sets`](foundation.category-of-families-of-sets.md) | +| Groups | [`group-theory.category-of-groups`](group-theory.category-of-groups.md) | +| `G`-sets | [`group-theory.category-of-group-actions`](group-theory.category-of-group-actions.md) | +| Maps between two categories | [`category-theory.category-of-maps-categories`](category-theory.category-of-maps-categories.md) [`category-theory.category-of-maps-from-small-to-large-categories`](category-theory.category-of-maps-from-small-to-large-categories.md) | +| Metric spaces and isometries | [`metric-spaces.category-of-metric-spaces-and-isometries`](metric-spaces.category-of-metric-spaces-and-isometries.md) | +| Metric spaces and short functions | [`metric-spaces.category-of-metric-spaces-and-short-functions`](metric-spaces.category-of-metric-spaces-and-short-functions.md) | +| Orbits of a group | [`group-theory.category-of-orbits-groups`](group-theory.category-of-orbits-groups.md) | +| Presheaves on a precategory | [`category-theory.presheaf-categories`](category-theory.presheaf-categories.md) | +| Representing arrow category | [`category-theory.representing-arrow-category`](category-theory.representing-arrow-category.md) | +| Rings | [`ring-theory.category-of-rings`](ring-theory.category-of-rings.md) | +| Semigroups | [`group-theory.category-of-semigroups`](group-theory.category-of-semigroups.md) | +| Sets | [`foundation.category-of-sets`](foundation.category-of-sets.md) | +| Simplex category | [`category-theory.simplex-category`](category-theory.simplex-category.md) | +| Simplicial sets | [`category-theory.category-of-simplicial-sets`](category-theory.category-of-simplicial-sets.md) | diff --git a/tables/precategories.md b/tables/precategories.md index 12c7fd2edf..b14b8f58e3 100644 --- a/tables/precategories.md +++ b/tables/precategories.md @@ -1,21 +1,17 @@ -| Precategory | File | -| --------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------- | -| 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) | -| Concrete groups | [`group-theory.precategory-of-concrete-groups`](group-theory.precategory-of-concrete-groups.md) | -| Decidable total orders | [`order-theory.precategory-of-decidable-total-orders`](order-theory.precategory-of-decidable-total-orders.md) | -| Finite species | [`species.precategory-of-finite-species`](species.precategory-of-finite-species.md) | -| `G`-sets | [`group-theory.precategory-of-group-actions`](group-theory.precategory-of-group-actions.md) | -| Groups | [`group-theory.precategory-of-groups`](group-theory.precategory-of-groups.md) | -| Metric spaces and functions | [`metric-spaces.precategory-of-metric-spaces-and-functions`](metric-spaces.precategory-of-metric-spaces-and-functions.md) | -| Metric spaces and isometries | [`metric-spaces.precategory-of-metric-spaces-and-isometries`](metric-spaces.precategory-of-metric-spaces-and-isometries.md) | -| Metric spaces and short functions | [`metric-spaces.precategory-of-metric-spaces-and-short-functions`](metric-spaces.precategory-of-metric-spaces-and-short-functions.md) | -| Monoids | [`group-theory.precategory-of-monoids`](group-theory.precategory-of-monoids.md) | -| Posets | [`order-theory.precategory-of-posets`](order-theory.precategory-of-posets.md) | -| Rings | [`ring-theory.precategory-of-rings`](ring-theory.precategory-of-rings.md) | -| Semigroups | [`group-theory.precategory-of-semigroups`](group-theory.precategory-of-semigroups.md) | -| Semirings | [`ring-theory.precategory-of-semirings`](ring-theory.precategory-of-semirings.md) | -| Sets | [`foundation.category-of-sets`](foundation.category-of-sets.md) | -| Total orders | [`order-theory.precategory-of-total-orders`](order-theory.precategory-of-total-orders.md) | +| Precategory | File | +| ----------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------- | +| Algebras of a monad on a precategory | [`category-theory.precategory-of-algebras-monads-on-precategories`](category-theory.precategory-of-algebras-monads-on-precategories.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) | +| Concrete groups | [`group-theory.precategory-of-concrete-groups`](group-theory.precategory-of-concrete-groups.md) | +| Decidable total orders | [`order-theory.precategory-of-decidable-total-orders`](order-theory.precategory-of-decidable-total-orders.md) | +| Finite posets | [`order-theory.precategory-of-finite-posets`](order-theory.precategory-of-finite-posets.md) | +| Finite species | [`species.precategory-of-finite-species`](species.precategory-of-finite-species.md) | +| Free algebras of a monad on a precategory | [`category-theory.precategory-of-free-algebras-monads-on-precategories`](category-theory.precategory-of-free-algebras-monads-on-precategories.md) | +| Monoids | [`group-theory.precategory-of-monoids`](group-theory.precategory-of-monoids.md) | +| Orbits of a monoid action | [`group-theory.precategory-of-orbits-monoid-actions`](group-theory.precategory-of-orbits-monoid-actions.md) | +| Posets | [`order-theory.precategory-of-posets`](order-theory.precategory-of-posets.md) | +| Semirings | [`ring-theory.precategory-of-semirings`](ring-theory.precategory-of-semirings.md) | +| Sets | [`foundation.category-of-sets`](foundation.category-of-sets.md) | +| Total orders | [`order-theory.precategory-of-total-orders`](order-theory.precategory-of-total-orders.md) |