Contractible maps
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-02-07.
Last modified on 2023-09-11.
module foundation-core.contractible-maps where
Imports
open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.universe-levels open import foundation-core.coherently-invertible-maps open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types
Idea
A map is often said to satisfy a property P
if each of its fibers satisfy
property P
. Thus, we define contractible maps to be maps of which each fiber
is contractible. In other words, contractible maps are maps f : A → B
such
that for each element b : B
there is a unique a : A
equipped with an
identification (f a) = b
, i.e., contractible maps are the type theoretic
bijections.
Definition
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where is-contr-map : (A → B) → UU (l1 ⊔ l2) is-contr-map f = (y : B) → is-contr (fiber f y)
Properties
Any contractible map is an equivalence
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where map-inv-is-contr-map : is-contr-map f → B → A map-inv-is-contr-map H y = pr1 (center (H y)) is-section-map-inv-is-contr-map : (H : is-contr-map f) → (f ∘ (map-inv-is-contr-map H)) ~ id is-section-map-inv-is-contr-map H y = pr2 (center (H y)) is-retraction-map-inv-is-contr-map : (H : is-contr-map f) → ((map-inv-is-contr-map H) ∘ f) ~ id is-retraction-map-inv-is-contr-map H x = ap ( pr1 {B = λ z → (f z) = (f x)}) ( ( inv ( contraction ( H (f x)) ( pair ( map-inv-is-contr-map H (f x)) ( is-section-map-inv-is-contr-map H (f x))))) ∙ ( contraction (H (f x)) (pair x refl))) abstract is-equiv-is-contr-map : is-contr-map f → is-equiv f is-equiv-is-contr-map H = is-equiv-is-invertible ( map-inv-is-contr-map H) ( is-section-map-inv-is-contr-map H) ( is-retraction-map-inv-is-contr-map H)
Any coherently invertible map is a contractible map
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where abstract center-fiber-is-coherently-invertible : is-coherently-invertible f → (y : B) → fiber f y pr1 (center-fiber-is-coherently-invertible H y) = map-inv-is-coherently-invertible H y pr2 (center-fiber-is-coherently-invertible H y) = is-retraction-is-coherently-invertible H y contraction-fiber-is-coherently-invertible : (H : is-coherently-invertible f) → (y : B) → (t : fiber f y) → (center-fiber-is-coherently-invertible H y) = t contraction-fiber-is-coherently-invertible H y (pair x refl) = eq-Eq-fiber f y ( is-section-is-coherently-invertible H x) ( ( right-unit) ∙ ( inv ( coh-is-coherently-invertible H x))) is-contr-map-is-coherently-invertible : is-coherently-invertible f → is-contr-map f pr1 (is-contr-map-is-coherently-invertible H y) = center-fiber-is-coherently-invertible H y pr2 (is-contr-map-is-coherently-invertible H y) = contraction-fiber-is-coherently-invertible H y
Any equivalence is a contractible map
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where abstract is-contr-map-is-equiv : is-equiv f → is-contr-map f is-contr-map-is-equiv = is-contr-map-is-coherently-invertible ∘ is-coherently-invertible-is-equiv
See also
- For the notion of biinvertible maps see
foundation.equivalences
. - For the notions of inverses and coherently invertible maps, also known as
half-adjoint equivalences, see
foundation.coherently-invertible-maps
. - For the notion of path-split maps see
foundation.path-split-maps
.
Recent changes
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-09-06. Egbert Rijke. Rename fib to fiber (#722).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).