Mere path-cosplit maps
Content created by Fredrik Bakke.
Created on 2024-06-05.
Last modified on 2024-06-05.
module foundation.mere-path-cosplit-maps where
Imports
open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.inhabited-types open import foundation.iterated-dependent-product-types open import foundation.logical-equivalences open import foundation.propositional-truncations open import foundation.truncated-maps open import foundation.truncation-levels open import foundation.universe-levels open import foundation-core.contractible-maps open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.propositions open import foundation-core.retractions open import foundation-core.truncated-types
Idea
In Homotopy Type Theory, there are multiple nonequivalent ways to state that a
map is "injective" that are more or less informed by the homotopy structures of
its domain and codomain. A
mere path-cosplit map¶
is one such notion, lying somewhere between
embeddings and
injective maps. In fact, given an integer
k ≥ -2
, if we understand k
-injective map to mean the k+2
-dimensional
action on identifications
has a converse map, then we have proper inclusions
k-injective maps ⊃ k-path-cosplit maps ⊃ k-truncated maps.
While k
-truncatedness answers the question:
At which dimension is the action on higher identifications of a function always an equivalence?
Mere k
-path-cosplitting instead answers the question:
At which dimension is the action merely a retract?
Thus a merely -2
-path-cosplit map is a map that merely is a retract. A
merely k+1
-path-cosplit map is a map whose
action on identifications
is merely k
-path-cosplit.
We show that mere k
-path-cosplittness coincides with k
-truncatedness when
the codomain is k
-truncated, but more generally mere k
-path-cosplitting may
only induce mere retracts on higher homotopy groups.
Definitions
is-mere-path-cosplit : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) is-mere-path-cosplit neg-two-𝕋 f = is-inhabited (retraction f) is-mere-path-cosplit (succ-𝕋 k) {A} f = (x y : A) → is-mere-path-cosplit k (ap f {x} {y})
Properties
Being merely path-cosplit is a property
is-prop-is-mere-path-cosplit : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) → is-prop (is-mere-path-cosplit k f) is-prop-is-mere-path-cosplit neg-two-𝕋 f = is-property-is-inhabited (retraction f) is-prop-is-mere-path-cosplit (succ-𝕋 k) f = is-prop-Π (λ x → is-prop-Π λ y → is-prop-is-mere-path-cosplit k (ap f)) is-mere-path-cosplit-Prop : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} → (A → B) → Prop (l1 ⊔ l2) is-mere-path-cosplit-Prop k f = (is-mere-path-cosplit k f , is-prop-is-mere-path-cosplit k f)
If a map is k
-truncated then it is merely k
-path-cosplit
is-mere-path-cosplit-is-trunc : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {f : A → B} → is-trunc-map k f → is-mere-path-cosplit k f is-mere-path-cosplit-is-trunc neg-two-𝕋 is-trunc-f = unit-trunc-Prop (retraction-is-contr-map is-trunc-f) is-mere-path-cosplit-is-trunc (succ-𝕋 k) {f = f} is-trunc-f x y = is-mere-path-cosplit-is-trunc k ( is-trunc-map-ap-is-trunc-map k f is-trunc-f x y)
If a map is k
-path-cosplit then it is merely k+1
-path-cosplit
is-mere-path-cosplit-succ-is-mere-path-cosplit : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {f : A → B} → is-mere-path-cosplit k f → is-mere-path-cosplit (succ-𝕋 k) f is-mere-path-cosplit-succ-is-mere-path-cosplit neg-two-𝕋 {f = f} is-cosplit-f x y = rec-trunc-Prop ( is-mere-path-cosplit-Prop neg-two-𝕋 (ap f)) ( λ r → unit-trunc-Prop (retraction-ap f r)) ( is-cosplit-f) is-mere-path-cosplit-succ-is-mere-path-cosplit (succ-𝕋 k) is-cosplit-f x y = is-mere-path-cosplit-succ-is-mere-path-cosplit k (is-cosplit-f x y)
If a type maps into a k
-truncted type via a merely k
-path-cosplit map then it is k
-truncated
is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {f : A → B} → is-trunc k B → is-mere-path-cosplit k f → is-trunc k A is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain neg-two-𝕋 {A} {B} {f} is-trunc-B = rec-trunc-Prop ( is-trunc-Prop neg-two-𝕋 A) ( λ r → is-trunc-retract-of (f , r) is-trunc-B) is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain (succ-𝕋 k) {A} {B} {f} is-trunc-B is-cosplit-f x y = is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain k ( is-trunc-B (f x) (f y)) ( is-cosplit-f x y)
This result generalizes the following statements:
-
A type that injects into a set is a set.
-
A type that embeds into a
k+1
-truncated type isk+1
-truncated. -
A type that maps into a
k
-truncated type via ak
-truncated map isk
-truncated.
If the codomain of a mere k
-path-cosplit map is k
-truncated then the map is k
-truncated
is-trunc-map-is-mere-path-cosplit-is-trunc-codomain : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {f : A → B} → is-trunc k B → is-mere-path-cosplit k f → is-trunc-map k f is-trunc-map-is-mere-path-cosplit-is-trunc-codomain k is-trunc-B is-cosplit-f = is-trunc-map-is-trunc-domain-codomain k ( is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain k ( is-trunc-B) ( is-cosplit-f)) ( is-trunc-B)
See also
Recent changes
- 2024-06-05. Fredrik Bakke. Path-cosplit maps (#1153).