Precomposition of lifts of families of elements by maps
Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.
Created on 2024-01-27.
Last modified on 2024-04-25.
module orthogonal-factorization-systems.precomposition-lifts-families-of-elements where
Imports
open import foundation.action-on-identifications-dependent-functions open import foundation.commuting-squares-of-homotopies open import foundation.commuting-squares-of-maps open import foundation.commuting-triangles-of-maps open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.homotopy-induction open import foundation.identity-types open import foundation.precomposition-functions open import foundation.transport-along-identifications open import foundation.type-theoretic-principle-of-choice open import foundation.universe-levels open import foundation.whiskering-higher-homotopies-composition open import foundation.whiskering-homotopies-composition open import foundation.whiskering-identifications-concatenation open import orthogonal-factorization-systems.lifts-families-of-elements
Idea
Consider a type family B : A → 𝓤 and a map a : I → A. Then, given a map
f : J → I, we may pull back a
lift of a to
a lift of a ∘ f.
In other words, given a diagram
Σ (x : A) (B x)
|
| pr1
|
∨
J ------> I ------> A ,
f a
we get a map of lifts of families of elements
((i : I) → B (a i)) → ((j : J) → B (a (f j))) .
This map of lifts induces a map from lifted families of elements indexed by I
to lifted families of elements indexed by J.
Definitions
Precomposition of lifts of families of elements by functions
module _ {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A → UU l3) {J : UU l4} (f : J → I) where precomp-lift-family-of-elements : (a : I → A) → lift-family-of-elements B a → lift-family-of-elements B (a ∘ f) precomp-lift-family-of-elements a b i = b (f i)
Precomposition in lifted families of elements
module _ {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A → UU l3) {J : UU l4} (f : J → I) where precomp-lifted-family-of-elements : lifted-family-of-elements I B → lifted-family-of-elements J B precomp-lifted-family-of-elements = map-Σ ( lift-family-of-elements B) ( precomp f A) ( precomp-lift-family-of-elements B f)
Properties
Homotopies between maps induce commuting triangles of precompositions of lifts of families of elements
Consider two maps f, g : J → I and a homotopy H : f ~ g between them. The
precomposition functions they induce on lifts of families of elements have
different codomains, namely lift-family-of-elements B (a ∘ f) and
lift-family-of-elements B (a ∘ g), but they fit into a
commuting triangle with
transport in the type of lifts:
precomp-lift B f a
lift-family-of-elements B a ------------------> lift-family-of-elements B (a ∘ f)
\ /
\ /
\ /
precomp-lift B g a \ / tr (lift-family-of-elements B) (htpy-precomp H A a)
\ /
∨ ∨
lift-family-of-elements B (a ∘ g)
module _ {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A → UU l3) (a : I → A) {J : UU l4} {f : J → I} where statement-triangle-precomp-lift-family-of-elements-htpy : {g : J → I} (H : f ~ g) → UU (l1 ⊔ l3 ⊔ l4) statement-triangle-precomp-lift-family-of-elements-htpy {g} H = coherence-triangle-maps' ( precomp-lift-family-of-elements B g a) ( tr (lift-family-of-elements B) (htpy-precomp H A a)) ( precomp-lift-family-of-elements B f a) triangle-precomp-lift-family-of-elements-htpy-refl-htpy : statement-triangle-precomp-lift-family-of-elements-htpy refl-htpy triangle-precomp-lift-family-of-elements-htpy-refl-htpy b = tr-lift-family-of-elements-precomp B a refl-htpy (b ∘ f) abstract triangle-precomp-lift-family-of-elements-htpy : {g : J → I} (H : f ~ g) → statement-triangle-precomp-lift-family-of-elements-htpy H triangle-precomp-lift-family-of-elements-htpy = ind-htpy f ( λ g → statement-triangle-precomp-lift-family-of-elements-htpy) ( triangle-precomp-lift-family-of-elements-htpy-refl-htpy) compute-triangle-precomp-lift-family-of-elements-htpy : triangle-precomp-lift-family-of-elements-htpy refl-htpy ＝ triangle-precomp-lift-family-of-elements-htpy-refl-htpy compute-triangle-precomp-lift-family-of-elements-htpy = compute-ind-htpy f ( λ g → statement-triangle-precomp-lift-family-of-elements-htpy) ( triangle-precomp-lift-family-of-elements-htpy-refl-htpy)
triangle-precomp-lift-family-of-elements-htpy factors through transport along a homotopy in the famiy B ∘ a
Instead of defining the homotopy triangle-precomp-lift-family-of-elements-htpy
by homotopy induction, we could have defined it manually using the
characterization of transport in the type of lifts of a family of elements.
We show that these two definitions are homotopic.
module _ {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A → UU l3) (a : I → A) {J : UU l4} {f : J → I} where statement-coherence-triangle-precomp-lift-family-of-elements : {g : J → I} (H : f ~ g) → UU (l1 ⊔ l3 ⊔ l4) statement-coherence-triangle-precomp-lift-family-of-elements H = ( triangle-precomp-lift-family-of-elements-htpy B a H) ~ ( ( ( tr-lift-family-of-elements-precomp B a H) ·r ( precomp-lift-family-of-elements B f a)) ∙h ( λ b → eq-htpy (λ j → apd b (H j)))) coherence-triangle-precomp-lift-family-of-elements-refl-htpy : statement-coherence-triangle-precomp-lift-family-of-elements ( refl-htpy) coherence-triangle-precomp-lift-family-of-elements-refl-htpy b = ( htpy-eq (compute-triangle-precomp-lift-family-of-elements-htpy B a) b) ∙ ( inv right-unit) ∙ ( left-whisker-concat ( triangle-precomp-lift-family-of-elements-htpy-refl-htpy B a b) ( inv (eq-htpy-refl-htpy (b ∘ f)))) abstract coherence-triangle-precomp-lift-family-of-elements : {g : J → I} (H : f ~ g) → statement-coherence-triangle-precomp-lift-family-of-elements H coherence-triangle-precomp-lift-family-of-elements = ind-htpy f ( λ g → statement-coherence-triangle-precomp-lift-family-of-elements) ( coherence-triangle-precomp-lift-family-of-elements-refl-htpy) compute-coherence-triangle-precomp-lift-family-of-elements : coherence-triangle-precomp-lift-family-of-elements refl-htpy ＝ coherence-triangle-precomp-lift-family-of-elements-refl-htpy compute-coherence-triangle-precomp-lift-family-of-elements = compute-ind-htpy f ( λ g → statement-coherence-triangle-precomp-lift-family-of-elements) ( coherence-triangle-precomp-lift-family-of-elements-refl-htpy)
precomp-lifted-family-of-elements is homotopic to the precomposition map on functions up to equivalence
We have a commuting square like this:
precomp-lifted-family f
Σ (a : I → A) ((i : I) → B (a i)) ------------------------> Σ (a : J → A) ((j : J) → B (a j))
| |
| |
| map-inv-distributive-Π-Σ ⇗ map-inv-distributive-Π-Σ |
| |
∨ ∨
I → Σ A B ------------------------------------------------> J → Σ A B ,
- ∘ f
which shows that precomp-lifted-family-of-elements f is a good choice for a
precomposition map in the type of lifted families of elements, since it's
homotopic to the regular precomposition map up to equivalence.
module _ {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A → UU l3) {J : UU l4} (f : J → I) where coherence-square-precomp-map-inv-distributive-Π-Σ : coherence-square-maps ( precomp-lifted-family-of-elements B f) ( map-inv-distributive-Π-Σ) ( map-inv-distributive-Π-Σ) ( precomp f (Σ A B)) coherence-square-precomp-map-inv-distributive-Π-Σ = refl-htpy
Precomposition of lifted families of elements preserves homotopies
module _ {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A → UU l3) {J : UU l4} {f : J → I} where htpy-precomp-lifted-family-of-elements : {g : J → I} (H : f ~ g) → ( precomp-lifted-family-of-elements B f) ~ ( precomp-lifted-family-of-elements B g) htpy-precomp-lifted-family-of-elements H = htpy-map-Σ ( lift-family-of-elements B) ( htpy-precomp H A) ( precomp-lift-family-of-elements B f) ( λ a → triangle-precomp-lift-family-of-elements-htpy B a H) abstract compute-htpy-precomp-lifted-family-of-elements : htpy-precomp-lifted-family-of-elements refl-htpy ~ refl-htpy compute-htpy-precomp-lifted-family-of-elements = htpy-htpy-map-Σ-refl-htpy ( lift-family-of-elements B) ( compute-htpy-precomp-refl-htpy f A) ( λ a → ( htpy-eq ( compute-triangle-precomp-lift-family-of-elements-htpy B a)) ∙h ( λ b → htpy-eq (compute-tr-lift-family-of-elements-precomp B a) (b ∘ f)))
coherence-square-precomp-map-inv-distributive-Π-Σ commutes with induced homotopies between precompositions maps
Diagrammatically, we have two ways of composing homotopies to connect - ∘ f
and precomp-lifted-family-of-elements g. One factors through
precomp-lifted-family-of-elements f:
precomp-lifted-family g
-----------------------------------
/ \
/ ⇗ htpy-precomp-lifted-family H \
/ ∨
Σ (a : I → A) ((i : I) → B (a i)) ------------------------> Σ (a : J → A) ((j : J) → B (a j))
| precomp-lifted-family f |
| |
| ⇗ |
| map-inv-distributive-Π-Σ map-inv-distributive-Π-Σ |
∨ ∨
I → Σ A B ------------------------------------------------> J → Σ A B ,
- ∘ f
while the other factors through - ∘ g:
precomp-lifted-family g
Σ (a : I → A) ((i : I) → B (a i)) ------------------------> Σ (a : J → A) ((j : J) → B (a j))
| |
| |
| map-inv-distributive-Π-Σ ⇗ map-inv-distributive-Π-Σ |
| |
∨ - ∘ g ∨
I → Σ A B ------------------------------------------------> J → Σ A B .
\ >
\ ⇗ htpy-precomp H /
\ /
-------------------------------------
- ∘ f
We show that these homotopies are themselves homotopic, filling the cylinder.
module _ {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A → UU l3) {J : UU l4} {f : J → I} where statement-coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ : {g : J → I} (H : f ~ g) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) statement-coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ {g} H = coherence-square-homotopies ( htpy-precomp H (Σ A B) ·r map-inv-distributive-Π-Σ) ( coherence-square-precomp-map-inv-distributive-Π-Σ B f) ( coherence-square-precomp-map-inv-distributive-Π-Σ B g) ( ( map-inv-distributive-Π-Σ) ·l ( htpy-precomp-lifted-family-of-elements B H)) coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ-refl-htpy : statement-coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ ( refl-htpy) coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ-refl-htpy = ( left-whisker-comp² ( map-inv-distributive-Π-Σ) ( compute-htpy-precomp-lifted-family-of-elements B)) ∙h ( inv-htpy ( λ h → compute-htpy-precomp-refl-htpy f ( Σ A B) ( map-inv-distributive-Π-Σ h))) ∙h ( inv-htpy-right-unit-htpy) coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ : {g : J → I} (H : f ~ g) → statement-coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ ( H) coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ = ind-htpy f ( λ g → statement-coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ) ( coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ-refl-htpy)
Recent changes
- 2024-04-25. Fredrik Bakke. chore: Fix arrowheads in character diagrams (#1124).
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2024-01-27. Vojtěch Štěpančík. Refactor properties of lifts of families out of 26-descent (#988).