This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
Extensions of maps
module orthogonal-factorization-systems.extensions-of-maps where
Imports
open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions open import foundation.contractible-maps open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.homotopy-induction open import foundation.identity-types open import foundation.monomorphisms open import foundation.postcomposition-functions open import foundation.precomposition-dependent-functions open import foundation.propositions open import foundation.sets open import foundation.structure-identity-principle open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.truncation-levels open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation-core.torsorial-type-families open import orthogonal-factorization-systems.local-types
Idea
An extension of a map f : (x : A) → P x along a map i : A → B is a map
g : (y : B) → Q y such that Q restricts along i to P and g restricts
along i to f.
A
| \
i f
| \
∨ ∨
B - g -> P
Definition
Extensions of dependent functions
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) where is-extension : {P : B → UU l3} → ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3) is-extension f g = f ~ (g ∘ i) extension-dependent-type : (P : B → UU l3) → ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3) extension-dependent-type P f = Σ ((y : B) → P y) (is-extension f) extension : {X : UU l3} → (A → X) → UU (l1 ⊔ l2 ⊔ l3) extension {X} = extension-dependent-type (λ _ → X) total-extension-dependent-type : (P : B → UU l3) → UU (l1 ⊔ l2 ⊔ l3) total-extension-dependent-type P = Σ ((x : A) → P (i x)) (extension-dependent-type P) total-extension : (X : UU l3) → UU (l1 ⊔ l2 ⊔ l3) total-extension X = total-extension-dependent-type (λ _ → X) module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {i : A → B} {P : B → UU l3} {f : (x : A) → P (i x)} where map-extension : extension-dependent-type i P f → (y : B) → P y map-extension = pr1 is-extension-map-extension : (E : extension-dependent-type i P f) → is-extension i f (map-extension E) is-extension-map-extension = pr2
Operations
Vertical composition of extensions of maps
A
| \
i f
| \
∨ ∨
B - g -> P
| ∧
j /
| h
∨ /
C
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4} {i : A → B} {j : B → C} {f : (x : A) → P (j (i x))} {g : (x : B) → P (j x)} {h : (x : C) → P x} where is-extension-comp-vertical : is-extension j g h → is-extension i f g → is-extension (j ∘ i) f h is-extension-comp-vertical H G x = G x ∙ H (i x)
Horizontal composition of extensions of maps
A
/ | \
f g h
/ | \
∨ ∨ ∨
B - i -> C - j -> P
Horizontal composition of extensions of dependent functions
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4} {f : A → B} {g : A → C} {h : (x : A) → P (g x)} {i : B → C} {j : (z : C) → P z} where is-extension-dependent-type-comp-horizontal : (I : is-extension f g i) → is-extension g h j → is-extension f (λ x → tr P (I x) (h x)) (j ∘ i) is-extension-dependent-type-comp-horizontal I J x = ap (tr P (I x)) (J x) ∙ apd j (I x)
Horizontal composition of extensions of ordinary maps
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {f : A → B} {g : A → C} {h : A → X} {i : B → C} {j : C → X} where is-extension-comp-horizontal : (I : is-extension f g i) → is-extension g h j → is-extension f h (j ∘ i) is-extension-comp-horizontal I J x = (J x) ∙ ap j (I x)
Left whiskering of extensions of maps
A
| \
i f
| \
∨ ∨
B - g -> C - h -> P
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4} {i : A → B} {f : A → C} {g : B → C} where is-extension-left-whisker : (h : (x : C) → P x) (F : is-extension i f g) → (is-extension i (λ x → tr P (F x) (h (f x))) (h ∘ g)) is-extension-left-whisker h F = apd h ∘ F
Right whiskering of extensions of maps
X - h -> A
| \
i f
| \
∨ ∨
B - g -> P
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {P : B → UU l3} {X : UU l4} {i : A → B} {f : (x : A) → P (i x)} {g : (y : B) → P y} where is-extension-right-whisker : (F : is-extension i f g) (h : X → A) → is-extension (i ∘ h) (f ∘ h) g is-extension-right-whisker F h = F ∘ h
Postcomposition of extensions
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} where postcomp-extension : (f : A → B) (i : A → X) (g : X → Y) → extension f i → extension f (g ∘ i) postcomp-extension f i g = map-Σ (is-extension f (g ∘ i)) (postcomp B g) (λ j H → g ·l H)
Properties
Characterizing identifications of extensions of maps
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) {P : B → UU l3} (f : (x : A) → P (i x)) where coherence-htpy-extension : (e e' : extension-dependent-type i P f) → map-extension e ~ map-extension e' → UU (l1 ⊔ l3) coherence-htpy-extension e e' K = (is-extension-map-extension e ∙h (K ·r i)) ~ is-extension-map-extension e' htpy-extension : (e e' : extension-dependent-type i P f) → UU (l1 ⊔ l2 ⊔ l3) htpy-extension e e' = Σ ( map-extension e ~ map-extension e') ( coherence-htpy-extension e e') refl-htpy-extension : (e : extension-dependent-type i P f) → htpy-extension e e pr1 (refl-htpy-extension e) = refl-htpy pr2 (refl-htpy-extension e) = right-unit-htpy htpy-eq-extension : (e e' : extension-dependent-type i P f) → e ＝ e' → htpy-extension e e' htpy-eq-extension e .e refl = refl-htpy-extension e is-torsorial-htpy-extension : (e : extension-dependent-type i P f) → is-torsorial (htpy-extension e) is-torsorial-htpy-extension e = is-torsorial-Eq-structure ( is-torsorial-htpy (map-extension e)) ( map-extension e , refl-htpy) ( is-torsorial-htpy (is-extension-map-extension e ∙h refl-htpy)) is-equiv-htpy-eq-extension : (e e' : extension-dependent-type i P f) → is-equiv (htpy-eq-extension e e') is-equiv-htpy-eq-extension e = fundamental-theorem-id ( is-torsorial-htpy-extension e) ( htpy-eq-extension e) extensionality-extension : (e e' : extension-dependent-type i P f) → (e ＝ e') ≃ (htpy-extension e e') pr1 (extensionality-extension e e') = htpy-eq-extension e e' pr2 (extensionality-extension e e') = is-equiv-htpy-eq-extension e e' eq-htpy-extension : (e e' : extension-dependent-type i P f) (H : map-extension e ~ map-extension e') → coherence-htpy-extension e e' H → e ＝ e' eq-htpy-extension e e' H K = map-inv-equiv (extensionality-extension e e') (H , K)
The total type of extensions is equivalent to (y : B) → P y
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) where inv-compute-total-extension-dependent-type : {P : B → UU l3} → total-extension-dependent-type i P ≃ ((y : B) → P y) inv-compute-total-extension-dependent-type = ( right-unit-law-Σ-is-contr (λ f → is-torsorial-htpy' (f ∘ i))) ∘e ( equiv-left-swap-Σ) compute-total-extension-dependent-type : {P : B → UU l3} → ((y : B) → P y) ≃ total-extension-dependent-type i P compute-total-extension-dependent-type = inv-equiv (inv-compute-total-extension-dependent-type) inv-compute-total-extension : {X : UU l3} → total-extension i X ≃ (B → X) inv-compute-total-extension = inv-compute-total-extension-dependent-type compute-total-extension : {X : UU l3} → (B → X) ≃ total-extension i X compute-total-extension = compute-total-extension-dependent-type
The truncation level of the type of extensions is bounded by the truncation level of the codomains
module _ {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (i : A → B) where is-trunc-is-extension-dependent-type : {P : B → UU l3} (f : (x : A) → P (i x)) → ((x : A) → is-trunc (succ-𝕋 k) (P (i x))) → (g : (x : B) → P x) → is-trunc k (is-extension i f g) is-trunc-is-extension-dependent-type f is-trunc-P g = is-trunc-Π k λ x → is-trunc-P x (f x) (g (i x)) is-trunc-extension-dependent-type : {P : B → UU l3} (f : (x : A) → P (i x)) → ((x : B) → is-trunc k (P x)) → is-trunc k (extension-dependent-type i P f) is-trunc-extension-dependent-type f is-trunc-P = is-trunc-Σ ( is-trunc-Π k is-trunc-P) ( is-trunc-is-extension-dependent-type f ( is-trunc-succ-is-trunc k ∘ (is-trunc-P ∘ i))) is-trunc-total-extension-dependent-type : {P : B → UU l3} → ((x : B) → is-trunc k (P x)) → is-trunc k (total-extension-dependent-type i P) is-trunc-total-extension-dependent-type {P} is-trunc-P = is-trunc-equiv' k ( (y : B) → P y) ( compute-total-extension-dependent-type i) ( is-trunc-Π k is-trunc-P) module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) where is-contr-is-extension : {P : B → UU l3} (f : (x : A) → P (i x)) → ((x : A) → is-prop (P (i x))) → (g : (x : B) → P x) → is-contr (is-extension i f g) is-contr-is-extension f is-prop-P g = is-contr-Π λ x → is-prop-P x (f x) (g (i x)) is-prop-is-extension : {P : B → UU l3} (f : (x : A) → P (i x)) → ((x : A) → is-set (P (i x))) → (g : (x : B) → P x) → is-prop (is-extension i f g) is-prop-is-extension f is-set-P g = is-prop-Π (λ x → is-set-P x (f x) (g (i x)))
Every map has a unique extension along i if and only if P is i-local
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (i : A → B) {l : Level} (P : B → UU l) where equiv-fiber'-precomp-extension-dependent-type : (f : (x : A) → P (i x)) → fiber' (precomp-Π i P) f ≃ extension-dependent-type i P f equiv-fiber'-precomp-extension-dependent-type f = equiv-tot (λ g → equiv-funext {f = f} {g ∘ i}) equiv-fiber-precomp-extension-dependent-type : (f : (x : A) → P (i x)) → fiber (precomp-Π i P) f ≃ extension-dependent-type i P f equiv-fiber-precomp-extension-dependent-type f = ( equiv-fiber'-precomp-extension-dependent-type f) ∘e ( equiv-fiber (precomp-Π i P) f) equiv-is-contr-extension-dependent-type-is-local-dependent-type : is-local-dependent-type i P ≃ ((f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f)) equiv-is-contr-extension-dependent-type-is-local-dependent-type = ( equiv-Π-equiv-family ( equiv-is-contr-equiv ∘ equiv-fiber-precomp-extension-dependent-type)) ∘e ( equiv-is-contr-map-is-equiv (precomp-Π i P)) is-contr-extension-dependent-type-is-local-dependent-type : is-local-dependent-type i P → (f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f) is-contr-extension-dependent-type-is-local-dependent-type = map-equiv equiv-is-contr-extension-dependent-type-is-local-dependent-type is-local-dependent-type-is-contr-extension-dependent-type : ((f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f)) → is-local-dependent-type i P is-local-dependent-type-is-contr-extension-dependent-type = map-inv-equiv equiv-is-contr-extension-dependent-type-is-local-dependent-type
Examples
Every map is an extension of itself along the identity
is-extension-self : {l1 l2 : Level} {A : UU l1} {P : A → UU l2} (f : (x : A) → P x) → is-extension id f f is-extension-self _ = refl-htpy
The identity is an extension of every map along themselves
is-extension-along-self : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-extension f f id is-extension-along-self _ = refl-htpy
Postcomposition of extensions by an embedding is an embedding
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} where is-emb-postcomp-extension : (f : A → B) (i : A → X) (g : X → Y) → is-emb g → is-emb (postcomp-extension f i g) is-emb-postcomp-extension f i g H = is-emb-map-Σ ( is-extension f (g ∘ i)) ( is-mono-is-emb g H B) ( λ j → is-emb-is-equiv ( is-equiv-map-Π-is-fiberwise-equiv ( λ x → H (i x) (j (f x)))))
See also
orthogonal-factorization-systems.lifts-of-mapsfor the dual notion.