Cd-structures

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-30.
Last modified on 2024-04-25.

module orthogonal-factorization-systems.cd-structures where
Imports 
open import foundation.morphisms-arrows
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

Idea

A cd-structure on a category consists of a class 𝒟 of distinguished squares

        i
    A -----> X
    |        |
  f |        | g
    ∨        ∨
    B -----> Y.
        j

On this page we will consider internal cd-structures, i.e., cd-structure on types. In other words, a cd-structure is a family of subtypes

  (f : A → B) (g : X → Y) → hom-arrow f g → Prop,

where hom-arrow f g is the type of morphisms of arrows from f to g.

The terminology "cd-structure" originates from the idea that a Grothendieck topology is completely decomposable if it is generated by covering families that are given as pairs of maps with a common codomain that fit in a distinguished square.

Definitions

Cd-structures

module _
  (α : Level → Level → Level → Level → Level)
  where

  cd-structure : UUω
  cd-structure =
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} →
    (f : A → B) (g : X → Y) → subtype (α l1 l2 l3 l4) (hom-arrow f g)

  is-distinguished-square-cd-structure :
    (Σ : cd-structure) →
    {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 → UU (α l1 l2 l3 l4)
  is-distinguished-square-cd-structure Σ f g σ =
    type-Prop (Σ f g σ)

References

[Voe10]
Vladimir Voevodsky. Unstable motivic homotopy categories in Nisnevich and cdh-topologies. Journal of Pure and Applied Algebra, 214(8):1399–1406, 08 2010. URL: https://www.sciencedirect.com/science/article/pii/S0022404909002643, arXiv:0805.4576, doi:10.1016/j.jpaa.2009.11.005.

Recent changes