Lifting structures on commuting squares of maps
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2024-02-06.
Last modified on 2024-03-20.
module orthogonal-factorization-systems.lifting-structures-on-squares where
Imports
open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-homotopies open import foundation.commuting-squares-of-maps open import foundation.commuting-tetrahedra-of-homotopies open import foundation.commuting-triangles-of-homotopies open import foundation.commuting-triangles-of-identifications open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.higher-homotopies-morphisms-arrows open import foundation.homotopies open import foundation.homotopies-morphisms-arrows open import foundation.homotopy-induction open import foundation.identity-types open import foundation.morphisms-arrows open import foundation.path-algebra open import foundation.structure-identity-principle open import foundation.torsorial-type-families open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation.whiskering-identifications-concatenation open import orthogonal-factorization-systems.extensions-of-maps open import orthogonal-factorization-systems.lifts-of-maps open import orthogonal-factorization-systems.pullback-hom
Idea
A lifting structure¶ of a commuting square
h
A ------> X
| |
f| |g
| |
∨ ∨
B ------> Y
i
consists of a
diagonal lift¶
j : B → X such that the complete diagram
h
A --------> X
| ∧ |
f | j / | g
| / |
∨ / ∨
B --------> Y
i
commutes. We refer to a square equipped with a lifting structure as a lifting square¶. Observe that there is a canonical map
pullback-hom f g : (B → X) → hom-arrow f g.
Therefore we see that a lifting square consists of a
morphism of arrows α : hom-arrow f g from
f to g, a map j : B → X, and a
homotopy of morphisms of arrows
pullback-hom f g j ~ α.
Terminology. In the literature, a lifting structure on a square is commonly
referred to as a solution to the lifting problem α.
Definitions
The predicate of being a diagonal lift of a square
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {X : UU l2} {B : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (α : hom-arrow f g) (j : B → X) where is-diagonal-lift-square : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) is-diagonal-lift-square = htpy-hom-arrow f g α (pullback-hom f g j) is-extension-is-diagonal-lift-square : is-diagonal-lift-square → is-extension f (map-domain-hom-arrow f g α) j is-extension-is-diagonal-lift-square = pr1 is-lift-is-diagonal-lift-square : is-diagonal-lift-square → is-lift g (map-codomain-hom-arrow f g α) j is-lift-is-diagonal-lift-square = pr1 ∘ pr2 coherence-is-diagonal-lift-square : (l : is-diagonal-lift-square) → coherence-square-homotopies ( is-lift-is-diagonal-lift-square l ·r f) ( coh-hom-arrow f g α) ( coh-pullback-hom f g j) ( g ·l is-extension-is-diagonal-lift-square l) coherence-is-diagonal-lift-square = pr2 ∘ pr2
Lifting structures on squares
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {X : UU l2} {B : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (α : hom-arrow f g) where lifting-structure-square : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) lifting-structure-square = Σ (B → X) (is-diagonal-lift-square f g α) diagonal-map-lifting-structure-square : lifting-structure-square → (B → X) diagonal-map-lifting-structure-square = pr1 is-lifting-diagonal-map-lifting-structure-square : (l : lifting-structure-square) → is-diagonal-lift-square f g α (diagonal-map-lifting-structure-square l) is-lifting-diagonal-map-lifting-structure-square = pr2 is-extension-diagonal-map-lifting-structure-square : (l : lifting-structure-square) → is-extension f ( map-domain-hom-arrow f g α) ( diagonal-map-lifting-structure-square l) is-extension-diagonal-map-lifting-structure-square = pr1 ∘ pr2 extension-lifting-structure-square : lifting-structure-square → extension f (map-domain-hom-arrow f g α) pr1 (extension-lifting-structure-square L) = diagonal-map-lifting-structure-square L pr2 (extension-lifting-structure-square L) = is-extension-diagonal-map-lifting-structure-square L is-lift-diagonal-map-lifting-structure-square : (l : lifting-structure-square) → is-lift g ( map-codomain-hom-arrow f g α) ( diagonal-map-lifting-structure-square l) is-lift-diagonal-map-lifting-structure-square = pr1 ∘ (pr2 ∘ pr2) lift-lifting-structure-square : lifting-structure-square → lift g (map-codomain-hom-arrow f g α) pr1 (lift-lifting-structure-square L) = diagonal-map-lifting-structure-square L pr2 (lift-lifting-structure-square L) = is-lift-diagonal-map-lifting-structure-square L coherence-lifting-structure-square : (l : lifting-structure-square) → coherence-square-homotopies ( is-lift-diagonal-map-lifting-structure-square l ·r f) ( coh-hom-arrow f g α) ( coh-pullback-hom f g (diagonal-map-lifting-structure-square l)) ( g ·l is-extension-diagonal-map-lifting-structure-square l) coherence-lifting-structure-square = pr2 ∘ (pr2 ∘ pr2)
Homotopies of lifting squares
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {X : UU l2} {B : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (α : hom-arrow f g) (k l : lifting-structure-square f g α) where coherence-htpy-lifting-structure-square : diagonal-map-lifting-structure-square f g α k ~ diagonal-map-lifting-structure-square f g α l → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) coherence-htpy-lifting-structure-square H = htpy-htpy-hom-arrow f g α ( pullback-hom f g (diagonal-map-lifting-structure-square f g α l)) ( concat-htpy-hom-arrow f g α ( pullback-hom f g (diagonal-map-lifting-structure-square f g α k)) ( pullback-hom f g (diagonal-map-lifting-structure-square f g α l)) ( is-lifting-diagonal-map-lifting-structure-square f g α k) ( htpy-hom-arrow-htpy f g H)) ( is-lifting-diagonal-map-lifting-structure-square f g α l) htpy-lifting-structure-square : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) htpy-lifting-structure-square = Σ ( diagonal-map-lifting-structure-square f g α k ~ diagonal-map-lifting-structure-square f g α l) ( coherence-htpy-lifting-structure-square) module _ (H : htpy-lifting-structure-square) where htpy-diagonal-map-htpy-lifting-structure-square : diagonal-map-lifting-structure-square f g α k ~ diagonal-map-lifting-structure-square f g α l htpy-diagonal-map-htpy-lifting-structure-square = pr1 H coh-htpy-lifting-structure-square : coherence-htpy-lifting-structure-square ( htpy-diagonal-map-htpy-lifting-structure-square) coh-htpy-lifting-structure-square = pr2 H
The reflexivity homotopy of a lifting square
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {X : UU l2} {B : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (α : hom-arrow f g) (k : lifting-structure-square f g α) where htpy-diagonal-map-refl-htpy-lifting-structure-square : diagonal-map-lifting-structure-square f g α k ~ diagonal-map-lifting-structure-square f g α k htpy-diagonal-map-refl-htpy-lifting-structure-square = refl-htpy coh-refl-htpy-lifting-structure-square : coherence-htpy-lifting-structure-square f g α k k ( htpy-diagonal-map-refl-htpy-lifting-structure-square) coh-refl-htpy-lifting-structure-square = right-unit-law-concat-htpy-hom-arrow f g α ( pullback-hom f g (diagonal-map-lifting-structure-square f g α k)) ( is-lifting-diagonal-map-lifting-structure-square f g α k) refl-htpy-lifting-structure-square : htpy-lifting-structure-square f g α k k pr1 refl-htpy-lifting-structure-square = htpy-diagonal-map-refl-htpy-lifting-structure-square pr2 refl-htpy-lifting-structure-square = coh-refl-htpy-lifting-structure-square
Trivial lifting squares
The diagram
A X
| ∧ |
f | j / |g
| / |
∨ / ∨
B Y
gives rise to a lifting square
j ∘ f
A -------> X
| ∧ |
f | j / | g
| / |
∨ / ∨
B -------> Y
g ∘ j
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {X : UU l2} {B : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) where is-diagonal-lift-square-pullback-hom : (j : B → X) → is-diagonal-lift-square f g (pullback-hom f g j) j is-diagonal-lift-square-pullback-hom j = refl-htpy-hom-arrow f g (pullback-hom f g j)
Properties
The types of lifting squares are equivalent to the fibers of the pullback-hom
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (h : hom-arrow f g) where inv-compute-fiber-pullback-hom : fiber (pullback-hom f g) h ≃ lifting-structure-square f g h inv-compute-fiber-pullback-hom = equiv-tot ( λ j → extensionality-hom-arrow f g _ _ ∘e equiv-inv (pullback-hom f g j) h) compute-fiber-pullback-hom : lifting-structure-square f g h ≃ fiber (pullback-hom f g) h compute-fiber-pullback-hom = inv-equiv inv-compute-fiber-pullback-hom
Characterization of identifications of lifting squares
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (α : hom-arrow f g) (l : lifting-structure-square f g α) where htpy-eq-lifting-structure-square : (k : lifting-structure-square f g α) → l ＝ k → htpy-lifting-structure-square f g α l k htpy-eq-lifting-structure-square .l refl = refl-htpy-lifting-structure-square f g α l is-torsorial-htpy-lifting-structure-square : is-torsorial (htpy-lifting-structure-square f g α l) is-torsorial-htpy-lifting-structure-square = is-torsorial-Eq-structure ( is-torsorial-htpy _) ( diagonal-map-lifting-structure-square f g α l , refl-htpy) ( is-torsorial-htpy-htpy-hom-arrow f g α ( pullback-hom f g (diagonal-map-lifting-structure-square f g α l)) ( _)) is-equiv-htpy-eq-lifting-structure-square : (k : lifting-structure-square f g α) → is-equiv (htpy-eq-lifting-structure-square k) is-equiv-htpy-eq-lifting-structure-square = fundamental-theorem-id ( is-torsorial-htpy-lifting-structure-square) ( htpy-eq-lifting-structure-square) extensionality-lifting-structure-square : (k : lifting-structure-square f g α) → (l ＝ k) ≃ htpy-lifting-structure-square f g α l k pr1 (extensionality-lifting-structure-square k) = htpy-eq-lifting-structure-square k pr2 (extensionality-lifting-structure-square k) = is-equiv-htpy-eq-lifting-structure-square k eq-htpy-lifting-structure-square : (k : lifting-structure-square f g α) → htpy-lifting-structure-square f g α l k → l ＝ k eq-htpy-lifting-structure-square k = map-inv-equiv (extensionality-lifting-structure-square k)
External links
- lift at Lab.
Recent changes
- 2024-03-20. Fredrik Bakke. chore: Janitorial work in foundation (#1086).
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).