Cartesian morphisms of arrows
Content created by Fredrik Bakke and Egbert Rijke.
Created on 2024-01-25.
Last modified on 2024-08-18.
module foundation.cartesian-morphisms-arrows where
Imports
open import foundation.action-on-identifications-functions open import foundation.commuting-triangles-of-maps open import foundation.commuting-triangles-of-morphisms-arrows open import foundation.cones-over-cospan-diagrams open import foundation.coproducts-pullbacks open import foundation.dependent-pair-types open import foundation.dependent-products-pullbacks open import foundation.dependent-sums-pullbacks open import foundation.diagonal-maps-cartesian-products-of-types open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.function-types open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-coproduct-types open import foundation.functoriality-dependent-pair-types open import foundation.functoriality-fibers-of-maps open import foundation.homotopies-morphisms-arrows open import foundation.identity-types open import foundation.morphisms-arrows open import foundation.postcomposition-functions open import foundation.postcomposition-pullbacks open import foundation.products-pullbacks open import foundation.pullbacks open import foundation.standard-pullbacks open import foundation.unit-type open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation-core.commuting-squares-of-maps open import foundation-core.homotopies open import foundation-core.propositions open import foundation-core.universal-property-pullbacks
Idea
A morphism of arrows h : f → g is said to be
cartesian¶
if the commuting square
i
A -----> X
| |
f | h | g
∨ ∨
B -----> Y
j
is a pullback square. In this instance, we also say
that f is a base change¶ of g.
Definitions
The predicate of being a cartesian morphism of arrows
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 is-cartesian-hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) is-cartesian-hom-arrow = is-pullback (map-codomain-hom-arrow f g h) g (cone-hom-arrow f g h) is-prop-is-cartesian-hom-arrow : is-prop is-cartesian-hom-arrow is-prop-is-cartesian-hom-arrow = is-prop-is-pullback (map-codomain-hom-arrow f g h) g (cone-hom-arrow f g h) is-cartesian-hom-arrow-Prop : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4) pr1 is-cartesian-hom-arrow-Prop = is-cartesian-hom-arrow pr2 is-cartesian-hom-arrow-Prop = is-prop-is-cartesian-hom-arrow
The type of cartesian morphisms of arrows
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 cartesian-hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) cartesian-hom-arrow = Σ (hom-arrow f g) (is-cartesian-hom-arrow f g) 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 : cartesian-hom-arrow f g) where hom-arrow-cartesian-hom-arrow : hom-arrow f g hom-arrow-cartesian-hom-arrow = pr1 h is-cartesian-cartesian-hom-arrow : is-cartesian-hom-arrow f g hom-arrow-cartesian-hom-arrow is-cartesian-cartesian-hom-arrow = pr2 h map-domain-cartesian-hom-arrow : A → X map-domain-cartesian-hom-arrow = map-domain-hom-arrow f g hom-arrow-cartesian-hom-arrow map-codomain-cartesian-hom-arrow : B → Y map-codomain-cartesian-hom-arrow = map-codomain-hom-arrow f g hom-arrow-cartesian-hom-arrow coh-cartesian-hom-arrow : coherence-square-maps ( map-domain-cartesian-hom-arrow) ( f) ( g) ( map-codomain-cartesian-hom-arrow) coh-cartesian-hom-arrow = coh-hom-arrow f g hom-arrow-cartesian-hom-arrow cone-cartesian-hom-arrow : cone map-codomain-cartesian-hom-arrow g A cone-cartesian-hom-arrow = cone-hom-arrow f g hom-arrow-cartesian-hom-arrow universal-property-cartesian-hom-arrow : universal-property-pullback ( map-codomain-cartesian-hom-arrow) ( g) ( cone-cartesian-hom-arrow) universal-property-cartesian-hom-arrow = universal-property-pullback-is-pullback ( map-codomain-cartesian-hom-arrow) ( g) ( cone-cartesian-hom-arrow) ( is-cartesian-cartesian-hom-arrow)
Properties
Cartesian morphisms of arrows arising from standard pullbacks
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) where standard-pullback-cartesian-hom-arrow : cartesian-hom-arrow vertical-map-standard-pullback g standard-pullback-cartesian-hom-arrow = ( hom-arrow-cone f g (cone-standard-pullback f g) , is-equiv-id)
Cartesian morphisms of arrows arising from fibers
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (y : B) where fiber-cartesian-hom-arrow : cartesian-hom-arrow (terminal-map (fiber f y)) f pr1 fiber-cartesian-hom-arrow = hom-arrow-cone (point y) f (swap-cone f (point y) (cone-fiber f y)) pr2 fiber-cartesian-hom-arrow = is-pullback-swap-cone f (point y) ( cone-fiber f y) ( is-pullback-cone-fiber f y)
The induced family of equivalences of fibers of cartesian morphisms of arrows
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 : cartesian-hom-arrow f g) where equiv-fibers-cartesian-hom-arrow : (b : B) → fiber f b ≃ fiber g (map-codomain-cartesian-hom-arrow f g h b) equiv-fibers-cartesian-hom-arrow b = ( map-fiber-vertical-map-cone ( map-codomain-cartesian-hom-arrow f g h) ( g) ( cone-cartesian-hom-arrow f g h) ( b)) , ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback ( map-codomain-cartesian-hom-arrow f g h) ( g) ( cone-cartesian-hom-arrow f g h) ( is-cartesian-cartesian-hom-arrow f g h) ( b))
Transposing cartesian morphisms of arrows
The transposition¶ of a cartesian morphism of arrows
i
A -----> X
| ⌟ |
f | | g
∨ ∨
B -----> Y
j
is the cartesian morphism of arrows
f
A -----> B
| ⌟ |
i | | j
∨ ∨
X -----> Y.
g
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (α : cartesian-hom-arrow f g) where is-cartesian-transpose-cartesian-hom-arrow : is-cartesian-hom-arrow ( map-domain-cartesian-hom-arrow f g α) ( map-codomain-cartesian-hom-arrow f g α) ( transpose-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α)) is-cartesian-transpose-cartesian-hom-arrow = is-pullback-swap-cone ( map-codomain-cartesian-hom-arrow f g α) ( g) ( cone-cartesian-hom-arrow f g α) ( is-cartesian-cartesian-hom-arrow f g α) transpose-cartesian-hom-arrow : cartesian-hom-arrow ( map-domain-cartesian-hom-arrow f g α) ( map-codomain-cartesian-hom-arrow f g α) transpose-cartesian-hom-arrow = ( transpose-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α) , is-cartesian-transpose-cartesian-hom-arrow)
If the target of a cartesian morphism is an equivalence then so is the source
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (α : cartesian-hom-arrow f g) where is-equiv-source-is-equiv-target-cartesian-hom-arrow : is-equiv g → is-equiv f is-equiv-source-is-equiv-target-cartesian-hom-arrow G = is-equiv-vertical-map-is-pullback ( map-codomain-cartesian-hom-arrow f g α) ( g) ( cone-cartesian-hom-arrow f g α) ( G) ( is-cartesian-cartesian-hom-arrow f g α)
If the target and source of a morphism of arrows are equivalences then the morphism is cartesian
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) where is-cartesian-hom-arrow-is-equiv-source-is-equiv-target : is-equiv g → is-equiv f → is-cartesian-hom-arrow f g α is-cartesian-hom-arrow-is-equiv-source-is-equiv-target = is-pullback-is-equiv-vertical-maps ( map-codomain-hom-arrow f g α) ( g) ( cone-hom-arrow f g α)
Cartesian morphisms of arrows are preserved under homotopies of arrows
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} where abstract is-cartesian-hom-arrow-htpy : {f f' : A → B} (F' : f' ~ f) {g g' : X → Y} (G : g ~ g') (α : hom-arrow f g) → is-cartesian-hom-arrow f g α → is-cartesian-hom-arrow f' g' (hom-arrow-htpy F' G α) is-cartesian-hom-arrow-htpy {f} F' {g} G α = is-pullback-htpy ( refl-htpy) ( inv-htpy G) ( cone-hom-arrow f g α) ( ( F') , ( refl-htpy) , ( ( assoc-htpy ( map-codomain-hom-arrow f g α ·l F' ∙h coh-hom-arrow f g α) ( G ·r map-domain-hom-arrow f g α) ( inv-htpy (G ·r map-domain-hom-arrow f g α))) ∙h ( ap-concat-htpy ( map-codomain-hom-arrow f g α ·l F' ∙h coh-hom-arrow f g α) ( right-inv-htpy G ·r map-domain-hom-arrow f g α)) ∙h ( right-unit-htpy) ∙h ( ap-concat-htpy' (coh-hom-arrow f g α) inv-htpy-right-unit-htpy))) cartesian-hom-arrow-htpy : {f f' : A → B} (F' : f' ~ f) {g g' : X → Y} (G : g ~ g') → cartesian-hom-arrow f g → cartesian-hom-arrow f' g' cartesian-hom-arrow-htpy F' G (α , H) = ( hom-arrow-htpy F' G α , is-cartesian-hom-arrow-htpy F' G α H)
Cartesian morphisms of arrows are preserved under homotopies of morphisms of arrows
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 abstract is-cartesian-htpy-hom-arrow : (α β : hom-arrow f g) (H : htpy-hom-arrow f g β α) → is-cartesian-hom-arrow f g α → is-cartesian-hom-arrow f g β is-cartesian-htpy-hom-arrow α β H = is-pullback-htpy ( htpy-codomain-htpy-hom-arrow f g β α H) ( refl-htpy) ( cone-hom-arrow f g α) ( htpy-parallell-cone-htpy-hom-arrow f g β α H)
The identity cartesian morphism of arrows
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where is-cartesian-id-hom-arrow : is-cartesian-hom-arrow f f id-hom-arrow is-cartesian-id-hom-arrow = is-pullback-is-equiv-horizontal-maps id f ( f , id , refl-htpy) ( is-equiv-id) ( is-equiv-id) id-cartesian-hom-arrow : cartesian-hom-arrow f f id-cartesian-hom-arrow = (id-hom-arrow , is-cartesian-id-hom-arrow)
Composition of cartesian morphisms of arrows
module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6} (f : A → B) (g : X → Y) (h : U → V) (b : hom-arrow g h) (a : hom-arrow f g) where is-cartesian-comp-hom-arrow : is-cartesian-hom-arrow g h b → is-cartesian-hom-arrow f g a → is-cartesian-hom-arrow f h (comp-hom-arrow f g h b a) is-cartesian-comp-hom-arrow = is-pullback-rectangle-is-pullback-left-square ( map-codomain-hom-arrow f g a) ( map-codomain-hom-arrow g h b) ( h) ( cone-hom-arrow g h b) ( cone-hom-arrow f g a) module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6} (f : A → B) (g : X → Y) (h : U → V) (b : cartesian-hom-arrow g h) (a : cartesian-hom-arrow f g) where comp-cartesian-hom-arrow : cartesian-hom-arrow f h comp-cartesian-hom-arrow = ( ( comp-hom-arrow f g h ( hom-arrow-cartesian-hom-arrow g h b) ( hom-arrow-cartesian-hom-arrow f g a)) , ( is-cartesian-comp-hom-arrow f g h ( hom-arrow-cartesian-hom-arrow g h b) ( hom-arrow-cartesian-hom-arrow f g a) ( is-cartesian-cartesian-hom-arrow g h b) ( is-cartesian-cartesian-hom-arrow f g a)))
Left cancellation of cartesian morphisms of arrows
module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6} (f : A → B) (g : X → Y) (h : U → V) (b : hom-arrow g h) (a : hom-arrow f g) where is-cartesian-hom-arrow-right-factor : is-cartesian-hom-arrow g h b → is-cartesian-hom-arrow f h (comp-hom-arrow f g h b a) → is-cartesian-hom-arrow f g a is-cartesian-hom-arrow-right-factor = is-pullback-left-square-is-pullback-rectangle ( map-codomain-hom-arrow f g a) ( map-codomain-hom-arrow g h b) ( h) ( cone-hom-arrow g h b) ( cone-hom-arrow f g a)
The left morphism in a commuting triangle of morphisms of arrows is cartesian if the other two are
module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6} (f : A → B) (g : X → Y) (h : U → V) (left : hom-arrow f h) (right : hom-arrow g h) (top : hom-arrow f g) (H : coherence-triangle-hom-arrow f g h left right top) where abstract is-cartesian-left-hom-arrow-triangle : is-cartesian-hom-arrow g h right → is-cartesian-hom-arrow f g top → is-cartesian-hom-arrow f h left is-cartesian-left-hom-arrow-triangle R T = is-cartesian-htpy-hom-arrow f h ( comp-hom-arrow f g h right top) ( left) ( H) ( is-cartesian-comp-hom-arrow f g h right top R T) module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6} (f : A → B) (g : X → Y) (h : U → V) (top : cartesian-hom-arrow f g) (left : hom-arrow f h) (right : cartesian-hom-arrow g h) (H : coherence-triangle-hom-arrow f g h ( left) ( hom-arrow-cartesian-hom-arrow g h right) ( hom-arrow-cartesian-hom-arrow f g top)) where abstract is-cartesian-left-cartesian-hom-arrow-triangle : is-cartesian-hom-arrow f h left is-cartesian-left-cartesian-hom-arrow-triangle = is-cartesian-left-hom-arrow-triangle f g h ( left) ( hom-arrow-cartesian-hom-arrow g h right) ( hom-arrow-cartesian-hom-arrow f g top) ( H) ( is-cartesian-cartesian-hom-arrow g h right) ( is-cartesian-cartesian-hom-arrow f g top)
The top morphism in a commuting triangle of morphisms of arrows is cartesian if the other two are
module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6} (f : A → B) (g : X → Y) (h : U → V) (left : hom-arrow f h) (right : hom-arrow g h) (top : hom-arrow f g) where abstract is-cartesian-top-hom-arrow-triangle' : (H : coherence-triangle-hom-arrow' f g h left right top) → is-cartesian-hom-arrow g h right → is-cartesian-hom-arrow f h left → is-cartesian-hom-arrow f g top is-cartesian-top-hom-arrow-triangle' H R L = is-cartesian-hom-arrow-right-factor f g h right top R ( is-cartesian-htpy-hom-arrow f h ( left) ( comp-hom-arrow f g h right top) ( H) ( L)) abstract is-cartesian-top-hom-arrow-triangle : (H : coherence-triangle-hom-arrow f g h left right top) → is-cartesian-hom-arrow g h right → is-cartesian-hom-arrow f h left → is-cartesian-hom-arrow f g top is-cartesian-top-hom-arrow-triangle H = is-cartesian-top-hom-arrow-triangle' ( inv-htpy-hom-arrow f h left (comp-hom-arrow f g h right top) H) module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6} (f : A → B) (g : X → Y) (h : U → V) (top : hom-arrow f g) (left : cartesian-hom-arrow f h) (right : cartesian-hom-arrow g h) where abstract is-cartesian-top-cartesian-hom-arrow-triangle' : (H : coherence-triangle-hom-arrow' f g h ( hom-arrow-cartesian-hom-arrow f h left) ( hom-arrow-cartesian-hom-arrow g h right) ( top)) → is-cartesian-hom-arrow f g top is-cartesian-top-cartesian-hom-arrow-triangle' H = is-cartesian-top-hom-arrow-triangle' f g h ( hom-arrow-cartesian-hom-arrow f h left) ( hom-arrow-cartesian-hom-arrow g h right) ( top) ( H) ( is-cartesian-cartesian-hom-arrow g h right) ( is-cartesian-cartesian-hom-arrow f h left) abstract is-cartesian-top-cartesian-hom-arrow-triangle : (H : coherence-triangle-hom-arrow f g h ( hom-arrow-cartesian-hom-arrow f h left) ( hom-arrow-cartesian-hom-arrow g h right) ( top)) → is-cartesian-hom-arrow f g top is-cartesian-top-cartesian-hom-arrow-triangle H = is-cartesian-top-hom-arrow-triangle f g h ( hom-arrow-cartesian-hom-arrow f h left) ( hom-arrow-cartesian-hom-arrow g h right) ( top) ( H) ( is-cartesian-cartesian-hom-arrow g h right) ( is-cartesian-cartesian-hom-arrow f h left)
Dependent products of cartesian morphisms of arrows
Given a family of cartesian morphisms of arrows αᵢ : fᵢ → gᵢ, then there is a
cartesian morphism of arrows map-Π f → map-Π g.
module _ {l1 l2 l3 l4 l5 : Level} {I : UU l5} {A : I → UU l1} {B : I → UU l2} {X : I → UU l3} {Y : I → UU l4} (f : (i : I) → A i → B i) (g : (i : I) → X i → Y i) (α : (i : I) → cartesian-hom-arrow (f i) (g i)) where hom-arrow-Π-cartesian-hom-arrow : hom-arrow (map-Π f) (map-Π g) hom-arrow-Π-cartesian-hom-arrow = Π-hom-arrow f g (λ i → hom-arrow-cartesian-hom-arrow (f i) (g i) (α i)) is-cartesian-Π-cartesian-hom-arrow : is-cartesian-hom-arrow (map-Π f) (map-Π g) hom-arrow-Π-cartesian-hom-arrow is-cartesian-Π-cartesian-hom-arrow = is-pullback-Π ( λ i → map-codomain-cartesian-hom-arrow (f i) (g i) (α i)) ( g) ( λ i → cone-cartesian-hom-arrow (f i) (g i) (α i)) ( λ i → is-cartesian-cartesian-hom-arrow (f i) (g i) (α i)) Π-cartesian-hom-arrow : cartesian-hom-arrow (map-Π f) (map-Π g) pr1 Π-cartesian-hom-arrow = hom-arrow-Π-cartesian-hom-arrow pr2 Π-cartesian-hom-arrow = is-cartesian-Π-cartesian-hom-arrow
Dependent sums of cartesian morphisms of arrows
Given a family of cartesian morphisms of arrows αᵢ : fᵢ → gᵢ, then there is a
cartesian morphism of arrows tot f → tot g.
module _ {l1 l2 l3 l4 l5 : Level} {I : UU l5} {A : I → UU l1} {B : I → UU l2} {X : I → UU l3} {Y : I → UU l4} (f : (i : I) → A i → B i) (g : (i : I) → X i → Y i) (α : (i : I) → cartesian-hom-arrow (f i) (g i)) where hom-arrow-tot-cartesian-hom-arrow : hom-arrow (tot f) (tot g) hom-arrow-tot-cartesian-hom-arrow = tot-hom-arrow f g (λ i → hom-arrow-cartesian-hom-arrow (f i) (g i) (α i)) is-cartesian-tot-cartesian-hom-arrow : is-cartesian-hom-arrow (tot f) (tot g) hom-arrow-tot-cartesian-hom-arrow is-cartesian-tot-cartesian-hom-arrow = is-pullback-tot-is-pullback-family-id-cone ( λ i → map-codomain-cartesian-hom-arrow (f i) (g i) (α i)) ( g) ( λ i → cone-cartesian-hom-arrow (f i) (g i) (α i)) ( λ i → is-cartesian-cartesian-hom-arrow (f i) (g i) (α i)) tot-cartesian-hom-arrow : cartesian-hom-arrow (tot f) (tot g) pr1 tot-cartesian-hom-arrow = hom-arrow-tot-cartesian-hom-arrow pr2 tot-cartesian-hom-arrow = is-cartesian-tot-cartesian-hom-arrow
Cartesian morphisms of arrows are preserved under products
module _ {l1 l2 l3 l4 l5 l6 l7 l8 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {C : UU l5} {D : UU l6} {Z : UU l7} {W : UU l8} (f : A → B) (g : X → Y) (h : C → D) (i : Z → W) (α : cartesian-hom-arrow f g) (β : cartesian-hom-arrow h i) where is-cartesian-product-cartesian-hom-arrow : is-cartesian-hom-arrow ( map-product f h) ( map-product g i) ( product-hom-arrow f g h i ( hom-arrow-cartesian-hom-arrow f g α) ( hom-arrow-cartesian-hom-arrow h i β)) is-cartesian-product-cartesian-hom-arrow = is-pullback-product-is-pullback ( map-codomain-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α)) ( g) ( map-codomain-hom-arrow h i (hom-arrow-cartesian-hom-arrow h i β)) ( i) ( cone-cartesian-hom-arrow f g α) ( cone-cartesian-hom-arrow h i β) ( is-cartesian-cartesian-hom-arrow f g α) ( is-cartesian-cartesian-hom-arrow h i β) product-cartesian-hom-arrow : cartesian-hom-arrow (map-product f h) (map-product g i) product-cartesian-hom-arrow = ( ( product-hom-arrow f g h i ( hom-arrow-cartesian-hom-arrow f g α) ( hom-arrow-cartesian-hom-arrow h i β)) , ( is-cartesian-product-cartesian-hom-arrow))
Cartesian morphisms of arrows are preserved under coproducts
module _ {l1 l2 l3 l4 l5 l6 l7 l8 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {C : UU l5} {D : UU l6} {Z : UU l7} {W : UU l8} (f : A → B) (g : X → Y) (h : C → D) (i : Z → W) (α : cartesian-hom-arrow f g) (β : cartesian-hom-arrow h i) where is-cartesian-coproduct-cartesian-hom-arrow : is-cartesian-hom-arrow ( map-coproduct f h) ( map-coproduct g i) ( coproduct-hom-arrow f g h i ( hom-arrow-cartesian-hom-arrow f g α) ( hom-arrow-cartesian-hom-arrow h i β)) is-cartesian-coproduct-cartesian-hom-arrow = is-pullback-coproduct-is-pullback ( map-codomain-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α)) ( g) ( map-codomain-hom-arrow h i (hom-arrow-cartesian-hom-arrow h i β)) ( i) ( cone-cartesian-hom-arrow f g α) ( cone-cartesian-hom-arrow h i β) ( is-cartesian-cartesian-hom-arrow f g α) ( is-cartesian-cartesian-hom-arrow h i β) coproduct-cartesian-hom-arrow : cartesian-hom-arrow (map-coproduct f h) (map-coproduct g i) coproduct-cartesian-hom-arrow = ( ( coproduct-hom-arrow f g h i ( hom-arrow-cartesian-hom-arrow f g α) ( hom-arrow-cartesian-hom-arrow h i β)) , ( is-cartesian-coproduct-cartesian-hom-arrow))
Cartesian morphisms of arrows are preserved under exponentiation
module _ {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (α : cartesian-hom-arrow f g) (S : UU l5) where hom-arrow-postcomp-cartesian-hom-arrow : hom-arrow (postcomp S f) (postcomp S g) hom-arrow-postcomp-cartesian-hom-arrow = postcomp-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α) S is-cartesian-postcomp-cartesian-hom-arrow : is-cartesian-hom-arrow ( postcomp S f) ( postcomp S g) ( hom-arrow-postcomp-cartesian-hom-arrow) is-cartesian-postcomp-cartesian-hom-arrow = is-pullback-postcomp-is-pullback ( map-codomain-cartesian-hom-arrow f g α) ( g) ( cone-cartesian-hom-arrow f g α) ( is-cartesian-cartesian-hom-arrow f g α) ( S) postcomp-cartesian-hom-arrow : cartesian-hom-arrow (postcomp S f) (postcomp S g) pr1 postcomp-cartesian-hom-arrow = hom-arrow-postcomp-cartesian-hom-arrow pr2 postcomp-cartesian-hom-arrow = is-cartesian-postcomp-cartesian-hom-arrow
A folding operation on cartesian morphisms of arrows
A morphism of arrows
i
A ------> X
| |
f | | g
∨ ∨
B ------> Y
j
is cartesian if and only if either of the folded morphisms
(f , i) (f , i)
A ------> B × X A ------> B × X
| | | |
g ∘ i | | j × g j ∘ f | | j × g
∨ ∨ ∨ ∨
Y ------> Y × Y Y ------> Y × Y
Δ Δ
is.
It remains to formalize the right-hand version.
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) where transpose-fold-hom-arrow : hom-arrow ( λ x → (f x , map-domain-hom-arrow f g α x)) ( diagonal-product Y) transpose-fold-hom-arrow = hom-arrow-cone ( map-product (map-codomain-hom-arrow f g α) g) ( diagonal-product Y) ( fold-cone (map-codomain-hom-arrow f g α) g (cone-hom-arrow f g α)) fold-hom-arrow : hom-arrow ( g ∘ map-domain-hom-arrow f g α) ( map-product (map-codomain-hom-arrow f g α) g) fold-hom-arrow = transpose-hom-arrow ( λ a → f a , map-domain-hom-arrow f g α a) ( diagonal-product Y) ( transpose-fold-hom-arrow) is-cartesian-transpose-fold-hom-arrow : is-cartesian-hom-arrow f g α → is-cartesian-hom-arrow ( λ x → (f x , map-domain-hom-arrow f g α x)) ( diagonal-product Y) ( transpose-fold-hom-arrow) is-cartesian-transpose-fold-hom-arrow = is-pullback-fold-cone-is-pullback ( map-codomain-hom-arrow f g α) ( g) ( cone-hom-arrow f g α) is-cartesian-is-cartesian-transpose-fold-hom-arrow : is-cartesian-hom-arrow ( λ x → (f x , map-domain-hom-arrow f g α x)) ( diagonal-product Y) ( transpose-fold-hom-arrow) → is-cartesian-hom-arrow f g α is-cartesian-is-cartesian-transpose-fold-hom-arrow = is-pullback-is-pullback-fold-cone ( map-codomain-hom-arrow f g α) ( g) ( cone-hom-arrow f g α) is-cartesian-fold-hom-arrow : is-cartesian-hom-arrow f g α → is-cartesian-hom-arrow ( g ∘ map-domain-hom-arrow f g α) ( map-product (map-codomain-hom-arrow f g α) g) ( fold-hom-arrow) is-cartesian-fold-hom-arrow H = is-cartesian-transpose-cartesian-hom-arrow ( λ x → (f x , map-domain-hom-arrow f g α x)) ( diagonal-product Y) ( transpose-fold-hom-arrow , is-cartesian-transpose-fold-hom-arrow H) module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (α : cartesian-hom-arrow f g) where transpose-fold-cartesian-hom-arrow : cartesian-hom-arrow ( λ x → (f x , map-domain-cartesian-hom-arrow f g α x)) ( diagonal-product Y) pr1 transpose-fold-cartesian-hom-arrow = transpose-fold-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α) pr2 transpose-fold-cartesian-hom-arrow = is-cartesian-transpose-fold-hom-arrow f g ( hom-arrow-cartesian-hom-arrow f g α) ( is-cartesian-cartesian-hom-arrow f g α) fold-cartesian-hom-arrow : cartesian-hom-arrow ( g ∘ map-domain-cartesian-hom-arrow f g α) ( map-product (map-codomain-cartesian-hom-arrow f g α) g) pr1 fold-cartesian-hom-arrow = fold-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α) pr2 fold-cartesian-hom-arrow = is-cartesian-fold-hom-arrow f g ( hom-arrow-cartesian-hom-arrow f g α) ( is-cartesian-cartesian-hom-arrow f g α)
Lifting cartesian morphisms along lifts of the codomain
Suppose given a cospan diagram of arrows
A ------> C <------ B
| | ⌞ |
f | α h β | g
∨ ∨ ∨
A' -----> C' <----- B'
where β is cartesian. Moreover, suppose we have a map i : A' → B' from the
codomain of the source of α to the codomain of the source of β such that the
triangle
i
A' ---> B'
\ /
\ /
∨ ∨
C'
commutes. Then there is a unique morphism of arrows γ : f → g with a homotopy
β ~ α ∘ γ extending the triangle, and this morphism is cartesian if and only
if α is.
Proof. The unique existence of γ and the homotopy follows from the
pullback property of β. The rest is a reiteration of the 3-for-2 property of
cartesian morphisms.
We begin by constructing the commuting triangle of morphisms of arrows:
module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {A' : UU l2} {B : UU l3} {B' : UU l4} {C : UU l5} {C' : UU l6} (f : A → A') (g : B → B') (h : C → C') (β : cartesian-hom-arrow g h) (α : hom-arrow f h) (i : A' → B') (H : coherence-triangle-maps' ( map-codomain-hom-arrow f h α) ( map-codomain-cartesian-hom-arrow g h β) ( i)) where cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow : cone (map-codomain-cartesian-hom-arrow g h β) h A cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow = ( i ∘ f , map-domain-hom-arrow f h α , H ·r f ∙h coh-hom-arrow f h α) map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow : A → B map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow = gap-is-pullback ( map-codomain-cartesian-hom-arrow g h β) ( h) ( cone-cartesian-hom-arrow g h β) ( is-cartesian-cartesian-hom-arrow g h β) ( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow) hom-arrow-lift-map-codomain-cartesian-hom-arrow : hom-arrow f g pr1 hom-arrow-lift-map-codomain-cartesian-hom-arrow = map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow pr1 (pr2 hom-arrow-lift-map-codomain-cartesian-hom-arrow) = i pr2 (pr2 hom-arrow-lift-map-codomain-cartesian-hom-arrow) = inv-htpy ( htpy-vertical-map-gap-is-pullback ( map-codomain-cartesian-hom-arrow g h β) ( h) ( cone-cartesian-hom-arrow g h β) ( is-cartesian-cartesian-hom-arrow g h β) ( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow)) abstract inv-coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow : coherence-triangle-hom-arrow' f g h ( α) ( hom-arrow-cartesian-hom-arrow g h β) ( hom-arrow-lift-map-codomain-cartesian-hom-arrow) inv-coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow = ( htpy-horizontal-map-gap-is-pullback ( map-codomain-cartesian-hom-arrow g h β) ( h) ( cone-cartesian-hom-arrow g h β) ( is-cartesian-cartesian-hom-arrow g h β) ( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow)) , ( H) , ( ( ap-concat-htpy' ( ( h) ·l ( htpy-horizontal-map-gap-is-pullback ( map-codomain-cartesian-hom-arrow g h β) ( h) ( cone-cartesian-hom-arrow g h β) ( pr2 β) ( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow))) ( ap-concat-htpy' ( coh-cartesian-hom-arrow g h β ·r map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow) ( left-whisker-inv-htpy ( map-codomain-cartesian-hom-arrow g h β) ( htpy-vertical-map-gap-is-pullback ( map-codomain-cartesian-hom-arrow g h β) ( h) ( cone-cartesian-hom-arrow g h β) ( pr2 β) ( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow))))) ∙h ( assoc-htpy ( inv-htpy ( ( map-codomain-cartesian-hom-arrow g h β) ·l ( htpy-vertical-map-gap-is-pullback ( map-codomain-cartesian-hom-arrow g h β) ( h) ( cone-cartesian-hom-arrow g h β) ( pr2 β) ( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow)))) ( coh-cartesian-hom-arrow g h β ·r map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow) ( ( h) ·l ( htpy-horizontal-map-gap-is-pullback ( map-codomain-cartesian-hom-arrow g h β) ( h) ( cone-cartesian-hom-arrow g h β) ( pr2 β) ( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow)))) ∙h ( inv-htpy-left-transpose-htpy-concat ( ( map-codomain-cartesian-hom-arrow g h β) ·l ( htpy-vertical-map-gap-is-pullback ( map-codomain-cartesian-hom-arrow g h β) ( h) ( cone-cartesian-hom-arrow g h β) ( pr2 β) ( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow))) ( H ·r f ∙h coh-hom-arrow f h α) ( ( coh-cartesian-hom-arrow g h β ·r map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow) ∙h ( h) ·l ( htpy-horizontal-map-gap-is-pullback ( map-codomain-cartesian-hom-arrow g h β) ( h) ( cone-cartesian-hom-arrow g h β) ( is-cartesian-cartesian-hom-arrow g h β) ( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow))) ( inv-htpy ( coh-htpy-cone-gap-is-pullback ( map-codomain-cartesian-hom-arrow g h β) ( h) ( cone-cartesian-hom-arrow g h β) ( is-cartesian-cartesian-hom-arrow g h β) ( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow))))) coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow : coherence-triangle-hom-arrow f g h ( α) ( hom-arrow-cartesian-hom-arrow g h β) ( hom-arrow-lift-map-codomain-cartesian-hom-arrow) coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow = inv-htpy-hom-arrow f h ( comp-hom-arrow f g h ( hom-arrow-cartesian-hom-arrow g h β) ( hom-arrow-lift-map-codomain-cartesian-hom-arrow)) ( α) ( inv-coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow)
Now, if α was cartesian to begin with, the lift is also.
module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {A' : UU l2} {B : UU l3} {B' : UU l4} {C : UU l5} {C' : UU l6} (f : A → A') (g : B → B') (h : C → C') (β : cartesian-hom-arrow g h) (α : cartesian-hom-arrow f h) (i : A' → B') (H : coherence-triangle-maps' ( map-codomain-cartesian-hom-arrow f h α) ( map-codomain-cartesian-hom-arrow g h β) ( i)) where abstract is-cartesian-cartesian-hom-arrow-lift-map-codomain-cartesian-hom-arrow : is-cartesian-hom-arrow f g ( hom-arrow-lift-map-codomain-cartesian-hom-arrow f g h ( β) ( hom-arrow-cartesian-hom-arrow f h α) ( i) ( H)) is-cartesian-cartesian-hom-arrow-lift-map-codomain-cartesian-hom-arrow = is-cartesian-top-cartesian-hom-arrow-triangle' f g h ( hom-arrow-lift-map-codomain-cartesian-hom-arrow ( f) g h β (hom-arrow-cartesian-hom-arrow f h α) i H) ( α) ( β) ( inv-coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow ( f) g h β (hom-arrow-cartesian-hom-arrow f h α) i H) cartesian-hom-arrow-lift-map-codomain-cartesian-hom-arrow : cartesian-hom-arrow f g cartesian-hom-arrow-lift-map-codomain-cartesian-hom-arrow = ( hom-arrow-lift-map-codomain-cartesian-hom-arrow ( f) g h β (hom-arrow-cartesian-hom-arrow f h α) i H) , ( is-cartesian-cartesian-hom-arrow-lift-map-codomain-cartesian-hom-arrow)
See also
- Cocartesian morphisms of arrows for the dual.
- Diagonals of morphisms of arrows is another operation that preserves cartesianness.
Recent changes
- 2024-08-18. Fredrik Bakke. Maps in subuniverses (#1163).
- 2024-08-17. Fredrik Bakke. Horizontal fiber condition for pullbacks (#1142).
- 2024-04-25. Fredrik Bakke. chore: Fix arrowheads in character diagrams (#1124).
- 2024-04-11. Fredrik Bakke. Refactor diagonals (#1096).
- 2024-03-22. Fredrik Bakke. Additions to cartesian morphisms (#1087).