The universal property of sequential limits
Content created by Fredrik Bakke, Egbert Rijke and Vojtěch Štěpančík.
Created on 2023-10-16.
Last modified on 2024-01-14.
module foundation.universal-property-sequential-limits where
Imports
open import foundation.action-on-identifications-functions open import foundation.cones-over-inverse-sequential-diagrams open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.inverse-sequential-diagrams open import foundation.postcomposition-functions open import foundation.subtype-identity-principle open import foundation.universe-levels open import foundation-core.contractible-maps 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 open import foundation-core.identity-types open import foundation-core.propositions
Idea
Given an inverse sequential diagram of types
fₙ f₁ f₀
⋯ ---> Aₙ₊₁ ---> Aₙ ---> ⋯ ---> A₂ ---> A₁ ---> A₀
the sequential limit limₙ Aₙ is a universal type completing the diagram
fₙ f₁ f₀
limₙ Aₙ ---> ⋯ ---> Aₙ₊₁ ---> Aₙ ---> ⋯ ---> A₂ ---> A₁ ---> A₀.
The universal property of the sequential limit states that limₙ Aₙ is the
terminal such type, by which we mean that given any
cone over A with
domain X, there is a unique map
g : X → limₙ Aₙ exhibiting that cone as a composite of g with the cone of
limₙ Aₙ over A.
Definition
The universal property of sequential limits
module _ {l1 l2 : Level} (A : inverse-sequential-diagram l1) {X : UU l2} (c : cone-inverse-sequential-diagram A X) where universal-property-sequential-limit : UUω universal-property-sequential-limit = {l : Level} (Y : UU l) → is-equiv (cone-map-inverse-sequential-diagram A {Y = Y} c) module _ {l1 l2 l3 : Level} (A : inverse-sequential-diagram l1) {X : UU l2} (c : cone-inverse-sequential-diagram A X) where map-universal-property-sequential-limit : universal-property-sequential-limit A c → {Y : UU l3} (c' : cone-inverse-sequential-diagram A Y) → Y → X map-universal-property-sequential-limit up-c {Y} c' = map-inv-is-equiv (up-c Y) c' compute-map-universal-property-sequential-limit : (up-c : universal-property-sequential-limit A c) → {Y : UU l3} (c' : cone-inverse-sequential-diagram A Y) → cone-map-inverse-sequential-diagram A c ( map-universal-property-sequential-limit up-c c') ＝ c' compute-map-universal-property-sequential-limit up-c {Y} c' = is-section-map-inv-is-equiv (up-c Y) c'
Properties
3-for-2 property of sequential limits
module _ {l1 l2 l3 : Level} {A : inverse-sequential-diagram l1} {X : UU l2} {Y : UU l3} (c : cone-inverse-sequential-diagram A X) (c' : cone-inverse-sequential-diagram A Y) (h : Y → X) (KLM : htpy-cone-inverse-sequential-diagram A ( cone-map-inverse-sequential-diagram A c h) c') where inv-triangle-cone-cone-inverse-sequential-diagram : {l6 : Level} (D : UU l6) → cone-map-inverse-sequential-diagram A c ∘ postcomp D h ~ cone-map-inverse-sequential-diagram A c' inv-triangle-cone-cone-inverse-sequential-diagram D k = ap ( λ t → cone-map-inverse-sequential-diagram A t k) ( eq-htpy-cone-inverse-sequential-diagram A ( cone-map-inverse-sequential-diagram A c h) c' KLM) triangle-cone-cone-inverse-sequential-diagram : {l6 : Level} (D : UU l6) → cone-map-inverse-sequential-diagram A c' ~ cone-map-inverse-sequential-diagram A c ∘ postcomp D h triangle-cone-cone-inverse-sequential-diagram D k = inv (inv-triangle-cone-cone-inverse-sequential-diagram D k) abstract is-equiv-universal-property-sequential-limit-universal-property-sequential-limit : universal-property-sequential-limit A c → universal-property-sequential-limit A c' → is-equiv h is-equiv-universal-property-sequential-limit-universal-property-sequential-limit up up' = is-equiv-is-equiv-postcomp h ( λ D → is-equiv-top-map-triangle ( cone-map-inverse-sequential-diagram A c') ( cone-map-inverse-sequential-diagram A c) ( postcomp D h) ( triangle-cone-cone-inverse-sequential-diagram D) ( up D) ( up' D)) abstract universal-property-sequential-limit-universal-property-sequential-limit-is-equiv : is-equiv h → universal-property-sequential-limit A c → universal-property-sequential-limit A c' universal-property-sequential-limit-universal-property-sequential-limit-is-equiv is-equiv-h up D = is-equiv-left-map-triangle ( cone-map-inverse-sequential-diagram A c') ( cone-map-inverse-sequential-diagram A c) ( postcomp D h) ( triangle-cone-cone-inverse-sequential-diagram D) ( is-equiv-postcomp-is-equiv h is-equiv-h D) ( up D) abstract universal-property-sequential-limit-is-equiv-universal-property-sequential-limit : universal-property-sequential-limit A c' → is-equiv h → universal-property-sequential-limit A c universal-property-sequential-limit-is-equiv-universal-property-sequential-limit up' is-equiv-h D = is-equiv-right-map-triangle ( cone-map-inverse-sequential-diagram A c') ( cone-map-inverse-sequential-diagram A c) ( postcomp D h) ( triangle-cone-cone-inverse-sequential-diagram D) ( up' D) ( is-equiv-postcomp-is-equiv h is-equiv-h D)
Uniqueness of maps obtained via the universal property of sequential limits
module _ {l1 l2 : Level} (A : inverse-sequential-diagram l1) {X : UU l2} (c : cone-inverse-sequential-diagram A X) where abstract uniqueness-universal-property-sequential-limit : universal-property-sequential-limit A c → {l3 : Level} (Y : UU l3) (c' : cone-inverse-sequential-diagram A Y) → is-contr ( Σ ( Y → X) ( λ h → htpy-cone-inverse-sequential-diagram A ( cone-map-inverse-sequential-diagram A c h) (c'))) uniqueness-universal-property-sequential-limit up Y c' = is-contr-equiv' ( Σ (Y → X) (λ h → cone-map-inverse-sequential-diagram A c h ＝ c')) ( equiv-tot ( λ h → extensionality-cone-inverse-sequential-diagram A ( cone-map-inverse-sequential-diagram A c h) ( c'))) ( is-contr-map-is-equiv (up Y) c')
The homotopy of cones obtained from the universal property of sequential limits
module _ {l1 l2 : Level} (A : inverse-sequential-diagram l1) {X : UU l2} where htpy-cone-map-universal-property-sequential-limit : (c : cone-inverse-sequential-diagram A X) (up : universal-property-sequential-limit A c) → {l3 : Level} {Y : UU l3} (c' : cone-inverse-sequential-diagram A Y) → htpy-cone-inverse-sequential-diagram A ( cone-map-inverse-sequential-diagram A c ( map-universal-property-sequential-limit A c up c')) ( c') htpy-cone-map-universal-property-sequential-limit c up c' = htpy-eq-cone-inverse-sequential-diagram A ( cone-map-inverse-sequential-diagram A c ( map-universal-property-sequential-limit A c up c')) ( c') ( compute-map-universal-property-sequential-limit A c up c')
Unique uniqueness of sequential limits
module _ {l1 l2 l3 : Level} (A : inverse-sequential-diagram l1) {X : UU l2} {Y : UU l3} where abstract uniquely-unique-sequential-limit : ( c' : cone-inverse-sequential-diagram A Y) ( c : cone-inverse-sequential-diagram A X) → ( up-c' : universal-property-sequential-limit A c') → ( up-c : universal-property-sequential-limit A c) → is-contr ( Σ (Y ≃ X) ( λ e → htpy-cone-inverse-sequential-diagram A ( cone-map-inverse-sequential-diagram A c (map-equiv e)) c')) uniquely-unique-sequential-limit c' c up-c' up-c = is-torsorial-Eq-subtype ( uniqueness-universal-property-sequential-limit A c up-c Y c') ( is-property-is-equiv) ( map-universal-property-sequential-limit A c up-c c') ( htpy-cone-map-universal-property-sequential-limit A c up-c c') ( is-equiv-universal-property-sequential-limit-universal-property-sequential-limit ( c) ( c') ( map-universal-property-sequential-limit A c up-c c') ( htpy-cone-map-universal-property-sequential-limit A c up-c c') ( up-c) ( up-c'))
Table of files about sequential limits
The following table lists files that are about sequential limits as a general concept.
| Concept | File |
|---|---|
| Inverse sequential diagrams of types | foundation.inverse-sequential-diagrams |
| Dependent inverse sequential diagrams of types | foundation.dependent-inverse-sequential-diagrams |
| Composite maps in inverse sequential diagrams | foundation.composite-maps-in-inverse-sequential-diagrams |
| Morphisms of inverse sequential diagrams | foundation.morphisms-inverse-sequential-diagrams |
| Equivalences of inverse sequential diagrams | foundation.equivalences-inverse-sequential-diagrams |
| Cones over inverse sequential diagrams | foundation.cones-over-inverse-sequential-diagrams |
| The universal property of sequential limits | foundation.universal-property-sequential-limits |
| Sequential limits | foundation.sequential-limits |
| Functoriality of sequential limits | foundation.functoriality-sequential-limits |
| Transfinite cocomposition of maps | foundation.transfinite-cocomposition-of-maps |
See also
- For sequential colimits, see
synthetic-homotopy-theory.universal-property-sequential-colimits
Recent changes
- 2024-01-14. Fredrik Bakke. Exponentiating retracts of maps (#989).
- 2024-01-11. Fredrik Bakke. Rename "towers" to "inverse sequential diagrams" (#990).
- 2023-12-10. Fredrik Bakke. Refactor universal properties for various limits (#963).
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-11-09. Egbert Rijke and Fredrik Bakke. Refactoring of retractions, sections, and equivalences, and adding the 6-for-2 property of equivalences (#903).