The pullback-hom
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2023-02-18.
Last modified on 2023-09-12.
module orthogonal-factorization-systems.pullback-hom where
Imports
open import foundation.action-on-identifications-functions open import foundation.cones-over-cospans open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.fibered-maps open import foundation.fibers-of-maps open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.morphisms-cospans open import foundation.pullbacks open import foundation.type-arithmetic-dependent-pair-types open import foundation.universal-property-pullbacks open import foundation.universe-levels open import foundation.whiskering-homotopies open import orthogonal-factorization-systems.lifting-squares
Idea
Given a pair of maps f : A → B
and g : X → Y
, there is a
commuting square
- ∘ f
B → X ----> A → X
| |
g ∘ - | | g ∘ -
V V
B → Y ----> A → Y.
- ∘ f
The pullback-hom of f
and g
, f ⋔ g
, is the comparison map from B → X
to the pullback of the
cospan:
∙ ------> A → X
| ⌟ |
| | g ∘ -
V V
B → Y ----> A → Y.
- ∘ f
This pullback type can be understood as the type of
fibered maps from f
to g
, i.e.
commuting squares where the
vertical maps are f
and g
.
Definitions
The codomain of the pullback-hom
type-canonical-pullback-hom : {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) type-canonical-pullback-hom {A = A} {Y = Y} f g = canonical-pullback (precomp f Y) (postcomp A g)
The canonical pullback-hom type is equivalent to the type of fibered maps
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) where equiv-fibered-map-type-canonical-pullback-hom : type-canonical-pullback-hom f g ≃ fibered-map f g equiv-fibered-map-type-canonical-pullback-hom = equiv-tot (λ _ → equiv-tot (λ _ → equiv-funext)) equiv-type-canonical-pullback-hom-fibered-map : fibered-map f g ≃ type-canonical-pullback-hom f g equiv-type-canonical-pullback-hom-fibered-map = inv-equiv equiv-fibered-map-type-canonical-pullback-hom map-fibered-map-type-canonical-pullback-hom : type-canonical-pullback-hom f g → fibered-map f g map-fibered-map-type-canonical-pullback-hom = map-equiv equiv-fibered-map-type-canonical-pullback-hom map-type-canonical-pullback-hom-fibered-map : fibered-map f g → type-canonical-pullback-hom f g map-type-canonical-pullback-hom-fibered-map = map-equiv equiv-type-canonical-pullback-hom-fibered-map
Below are basic definitions related to the pullback property of the type of fibered maps.
cone-canonical-pullback-hom : cone (precomp f Y) (postcomp A g) (type-canonical-pullback-hom f g) cone-canonical-pullback-hom = cone-canonical-pullback (precomp f Y) (postcomp A g) cone-pullback-hom : cone (precomp f Y) (postcomp A g) (fibered-map f g) cone-pullback-hom = cone-map ( precomp f Y) ( postcomp A g) ( cone-canonical-pullback (precomp f Y) (postcomp A g)) ( map-type-canonical-pullback-hom-fibered-map) gap-canonical-pullback-hom : {l : Level} {C : UU l} → cone (precomp f Y) (postcomp A g) C → C → type-canonical-pullback-hom f g gap-canonical-pullback-hom = gap (precomp f Y) (postcomp A g) gap-pullback-hom : {l : Level} {C : UU l} → cone (precomp f Y) (postcomp A g) C → C → fibered-map f g gap-pullback-hom c x = map-fibered-map-type-canonical-pullback-hom (gap-canonical-pullback-hom c x) is-pullback-fibered-map : is-pullback (precomp f Y) (postcomp A g) (cone-pullback-hom) is-pullback-fibered-map = is-equiv-map-equiv equiv-type-canonical-pullback-hom-fibered-map universal-property-pullback-fibered-map : {l : Level} → universal-property-pullback l ( precomp f Y) (postcomp A g) (cone-pullback-hom) universal-property-pullback-fibered-map = universal-property-pullback-is-pullback ( precomp f Y) ( postcomp A g) ( cone-pullback-hom) ( is-pullback-fibered-map)
The pullback-hom map
The pullback-hom f ⋔ g
is the map (B → X) → fibered-map f g
, that takes a
diagonal map j
from the codomain of f
to the domain of g
to the fibered
map (g ∘ j , j ∘ f , refl-htpy)
.
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) where pullback-hom : (B → X) → fibered-map f g pullback-hom = gap-pullback-hom f g (postcomp B g , precomp f X , refl-htpy) infix 30 _⋔_ _⋔_ = pullback-hom
The symbol ⋔
is the pitchfork (agda-input:
\pitchfork
).
Properties
Functoriality 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) {l1' l2' l3' l4' : Level} {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} {Y' : UU l4'} (f' : A' → B') (g' : X' → Y') where map-pullback-hom : hom-cospan ( precomp f' Y') ( postcomp A' g') ( precomp f Y) ( postcomp A g) → fibered-map f' g' → fibered-map f g map-pullback-hom = map-is-pullback ( precomp f Y) ( postcomp A g) ( precomp f' Y') ( postcomp A' g') ( cone-pullback-hom f g) ( cone-pullback-hom f' g') ( is-pullback-fibered-map f g) ( is-pullback-fibered-map f' g')
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 : fibered-map f g) where inv-compute-fiber-pullback-hom : (fiber (pullback-hom f g) h) ≃ (lifting-square-fibered-map f g h) inv-compute-fiber-pullback-hom = equiv-tot ( λ j → ( equiv-Σ _ ( equiv-inv-htpy (j ∘ f) (map-total-fibered-map f g h)) ( λ E → equiv-Σ _ ( equiv-inv-htpy (g ∘ j) (map-base-fibered-map f g h)) ( λ L → ( equiv-concat-htpy' ( inv-htpy L ·r f) ( λ x → ap ( is-map-over-map-total-fibered-map f g h x ∙_) ( inv-htpy-left-whisk-inv-htpy g E x))) ∘e ( ( equiv-right-transpose-htpy-concat ( inv-htpy (L ·r f)) ( g ·l E) ( is-map-over-map-total-fibered-map f g h)) ∘e ( equiv-left-transpose-htpy-concat' ( g ·l E) ( L ·r f) ( is-map-over-map-total-fibered-map f g h)))))) ∘e ( ( equiv-left-swap-Σ) ∘e ( extensionality-fibered-map f g (pullback-hom f g j) h))) compute-fiber-pullback-hom : (lifting-square-fibered-map f g h) ≃ (fiber (pullback-hom f g) h) compute-fiber-pullback-hom = inv-equiv inv-compute-fiber-pullback-hom
Recent changes
- 2023-09-12. Egbert Rijke. Factoring out whiskering (#756).
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-06-29. Fredrik Bakke. Fix hyperlinks (#677).
- 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).