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 σ)
Exernal links
- cd-structure at the Lab
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
- 2024-04-25. Fredrik Bakke. chore: Fix arrowheads in character diagrams (#1124).
- 2024-03-12. Fredrik Bakke. Bibliographies (#1058).
- 2024-01-28. Egbert Rijke. Span diagrams (#1007).
- 2023-11-30. Egbert Rijke. Initial definitions for the cd-excision project (#931).