Descent for surjective maps

Content created by Fredrik Bakke.

Created on 2026-02-02.
Last modified on 2026-02-02.

module foundation.descent-surjective-maps where

open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-fibers-of-maps
open import foundation.logical-equivalences
open import foundation.surjective-maps
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.pullbacks

Idea

The descent property^¶ of surjective maps asserts that in a commuting diagram of the form

        p         q
   A ----->> B ------> C
   | ⌟       |         |
  f|        g|         |h
   ∨         ∨         ∨
   X ----->> Y ------> Z,
        i         j

where the maps i and p are surjective and the left hand square is a pullback, then the right square is a pullback if and only if the outer rectangle is a pullback.

This descent property appears as Theorem 2.3 in [CR21].

Theorem

In the formalization we do not presuppose that p is surjective, as this follows by base change stability of surjections.

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
  where

  descent-is-surjective :
    (i : X → Y) (j : Y → Z) (h : C → Z)
    (c : cone j h B) (d : cone i (vertical-map-cone j h c) A) →
    is-surjective i →
    is-pullback i (vertical-map-cone j h c) d →
    is-pullback (j ∘ i) h (pasting-horizontal-cone i j h c d) →
    is-pullback j h c
  descent-is-surjective i j h c d
    is-surjective-i is-pb-d is-pb-rectangle =
    is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone j h c
      ( map-inv-is-equiv-precomp-Π-Prop-is-surjective
        ( is-surjective-i)
        ( λ y → is-equiv-Prop (map-fiber-vertical-map-cone j h c y))
        ( λ x →
          is-equiv-right-map-triangle
            ( map-fiber-vertical-map-cone (j ∘ i) h
              ( pasting-horizontal-cone i j h c d)
              ( x))
            ( map-fiber-vertical-map-cone j h c (i x))
            ( map-fiber-vertical-map-cone i (vertical-map-cone j h c) d x)
            ( preserves-pasting-horizontal-map-fiber-vertical-map-cone
                i j h c d x)
            ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
              ( j ∘ i)
              ( h)
              ( pasting-horizontal-cone i j h c d)
              ( is-pb-rectangle)
              ( x))
            ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback i
              ( vertical-map-cone j h c)
              ( d)
              ( is-pb-d)
              ( x))))

  descent-surjection :
    (i : X ↠ Y) (j : Y → Z) (h : C → Z)
    (c : cone j h B)
    (d : cone (map-surjection i) (vertical-map-cone j h c) A) →
    is-pullback (map-surjection i) (vertical-map-cone j h c) d →
    is-pullback
      ( j ∘ map-surjection i)
      ( h)
      ( pasting-horizontal-cone (map-surjection i) j h c d) →
    is-pullback j h c
  descent-surjection (i , I) j h c d =
    descent-is-surjective i j h c d I

  iff-descent-is-surjective :
    (i : X → Y) (j : Y → Z) (h : C → Z)
    (c : cone j h B) (d : cone i (vertical-map-cone j h c) A) →
    is-surjective i →
    is-pullback i (vertical-map-cone j h c) d →
    is-pullback (j ∘ i) h (pasting-horizontal-cone i j h c d) ↔
    is-pullback j h c
  iff-descent-is-surjective i j h c d is-surjective-i is-pb-d =
    ( descent-is-surjective i j h c d is-surjective-i is-pb-d ,
      ( λ C →
        is-pullback-rectangle-is-pullback-left-square i j h c d C is-pb-d))

  iff-descent-surjection :
    (i : X ↠ Y) (j : Y → Z) (h : C → Z)
    (c : cone j h B)
    (d : cone (map-surjection i) (vertical-map-cone j h c) A) →
    is-pullback (map-surjection i) (vertical-map-cone j h c) d →
    is-pullback
      ( j ∘ map-surjection i)
      ( h)
      ( pasting-horizontal-cone (map-surjection i) j h c d) ↔
    is-pullback j h c
  iff-descent-surjection (i , I) j h c d =
    iff-descent-is-surjective i j h c d I

References

[CR21]

Felix Cherubini and Egbert Rijke. Modal descent. Mathematical Structures in Computer Science, 31(4):363–391, 04 2021. arXiv:2003.09713, doi:10.1017/S0960129520000201.

Table of descent properties

Recent changes

• 2026-02-02. Fredrik Bakke. Descent for surjective maps (#1732).