Project: Sheaves and excision with respect to regular cd-structures

[EgbertRijke]

The cd-excision project

Project description

A complete cd-structure consists of a class of distinguished squares of maps, i.e., distinguished morphisms in the arrow category, that is stable under base change. A complete cd-structure is said to be regular if the following three conditions hold:

1. The codomain of any distinguished square is a mono.
2. Any distinguished square is cartesian
3. The diagonal of any distinguished square is distinguished.

A type F is said to be a sheaf with respect to a cd-structure if F is right orthogonal to inclusion-im (cogap d) for any distinguished square d.

A type F is said to satisfy excision with respect to a cd-structure if F is right orthogonal to cogap d for any distinguished square d.

Goal of the project: Show that F is a sheaf with respect to a regular cd-structure if and only if it satisfies excision.

Current participants: Reid Barton, Egbert Rijke, Fredrik Bakke.

Outline and tasks

Descent

• [ ] Show that in a commuting cube, if the two back faces are pullback and the bottom face is pushout, then the top face is pushout if and only if the two front faces are pullback
• [ ] Show that pushouts of monos are monos, and that the pushout square of a mono is a pullback square. This is a direct application of the above formulation of descent.

The closed modality

• [ ] Prepare the files about modalities for real-world applications
• [ ] Define lex modalities, and give characterizations of lex modalities from RSS and CR.
• [x] Define the closed modality
• [ ] Show that the closed modality is lex. This step is needed for Anel's proof of Wärn's first lemma.

The arrow category

• [x] Prepare the file pullback-squares for real-world applications, and possibly rename it to cartesian squares. Alternatively, introduce a file for cartesian morphisms of arrows.
• [x] Define cocartesian squares/cocartesian morphisms of arrows.
• [ ] Define base change of morphisms of arrows.
• [ ] Define cogap map of morphisms of arrows.
• [ ] Define the image inclusions of the cogap maps of morphisms of arrows.

Wärn's first lemma

• [ ] Prove Wärn's first lemma, which asserts that diagonals of cocartesian morphisms of arrows out of embeddings are again cocartesian. Anel gave a beautiful elementary proof, bypassing the zigzag argument.

       Δ i
    A -----> A x_X A
    |           |
  f |           | functoriality Δ g
    V         ⌜ V
    B -----> B x_Y B
       Δ j

Orthogonality

• [x] Basic properties of orthogonal maps
  • [x] Equivalences between pullback-hom condition, pullback condition, universal property, fiber condition
  • [x] Composition closure and cancellation properties of orthogonal maps
  • [x] Right orthogonal maps are closed under Π, left orthogonal maps under Σ
  • [x] Right orthogonality is preserved under base change
• [x] Define fiberwise orthogonal maps
• [ ] Basic properties of fiberwise orthogonal maps
  • [x] Equivalence between pullback condition and fiber condition
  • [x] The left class is closed under base change
  • [x] The left class is closed under composition and have the right cancellation property
  • [ ] The left class is closed under cobase change
  • [ ] The left class is closed under coproducts in the arrow category
  • [ ] The left class is closed under pushouts in the arrow category
  • [ ] The left class is closed under sequential colimits in the arrow category
  • [ ] The left class is closed under coequalizers in the arrow category
  • [ ] The left class is closed under transfinite composition
  • [ ] The left class satisfies descent: Given a jointly surjective family of maps $q_i : B_i \to B$, if each base change $q^*_if : A_i \to B_i$ is fiberwise orthogonal to $g$, then so is $f$.
  • [ ] The left class is closed under fiberwise join with any map.
  • [ ] The left class is closed under taking image inclusions.
  • [x] The right class has all the closure properties of right orthogonal maps.
• [ ] Derive properties of fiberwise f-local types (what is called fiberwise orthogonal in the notes)

Cd-structures

• [x] Define cd-structures as classes of morphisms in the arrow category
• [ ] Define complete cd-structures
• [ ] Define regular cd-structures
• [ ] Define for each cd-structure the class of cogap maps of distinguished squares
• [ ] Define for each cd-structure the class of image inclusions of cogap maps of distinguished squares
• [ ] Define sheaves with respect to complete cd-structures
• [ ] Define types satisfying excision with respect to complete cd-structures
• [ ] Show that for a regular cd-structure, a type is a sheaf if and only if it satisfies excision

Resources

• Reid's note

[fredrik-bakke]

I've already defined the closed modality. It's in orthogonal-factorization-systems.closed-modalities.

[fredrik-bakke]

• [X] Prepare the file pullback-squares for real-world applications, and possibly rename it tocartesian squares`. Alternatively, introduce a file for cartesian morphisms of arrows.

Cartesian morphisms of arrows were added in #979.

[fredrik-bakke]

This issue seems to be missing any mention of orthogonal maps or fiberwise orthogonal maps. Are they not needed?

[fredrik-bakke]

When you write

• [ ] Define base change of morphisms of arrows.

Are you looking for a file about the following construct?

base-change-arrow :
  {l1 l2 : Level} (l3 l4 : Level) {A : UU l1} {B : UU l2} → (A → B) →
  UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
base-change-arrow l3 l4 f =
  Σ (UU l3) (λ C → Σ (UU l4) (λ D → Σ (C → D) (λ g → cartesian-hom-arrow g f)))

Otherwise, just using cartesian morphisms of arrows seems to be working fine with me for now. Although I would probably say the same about cartesian morphisms of arrows vs. pullback cones if we didn't already have cartesian morphisms of arrows.

EDIT: Oh, wait, you want a base change of morphisms of arrows.