Documentation

Mathlib.Condensed.Basic

Condensed Objects #

This file defines the category of condensed objects in a category C, following the work of Clausen-Scholze and Barwick-Haine.

Implementation Details #

We use the coherent Grothendieck topology on CompHaus, and define condensed objects in C to be C-valued sheaves, with respect to this Grothendieck topology.

Note: Our definition more closely resembles "Pyknotic objects" in the sense of Barwick-Haine, as we do not impose cardinality bounds, and manage universes carefully instead.

References #

source
def Condensed (C : Type w) [CategoryTheory.Category.{v, w} C] :
Type (max (max (max (u + 1) w) u) v)

Condensed.{u} C is the category of condensed objects in a category C, which are defined as sheaves on CompHaus.{u} with respect to the coherent Grothendieck topology.

Equations
Instances For
    source
    instance instCategoryCondensed {C : Type w} [CategoryTheory.Category.{v, w} C] :
    CategoryTheory.Category.{max (u + 1) v, max (max (u + 1) w) v} (Condensed C)
    Equations
    • instCategoryCondensed = let_fun this := inferInstance; this
    source
    @[reducible, inline]
    abbrev CondensedSet :
    Type (u + 2)

    Condensed sets (types) with the appropriate universe levels, i.e. Type (u+1)-valued sheaves on CompHaus.{u}.

    Equations
    Instances For
      source
      @[simp]
      theorem Condensed.id_val {C : Type w} [CategoryTheory.Category.{v, w} C] (X : Condensed C) :
      (CategoryTheory.CategoryStruct.id X).val = CategoryTheory.CategoryStruct.id X.val
      source
      @[simp]
      theorem Condensed.comp_val {C : Type w} [CategoryTheory.Category.{v, w} C] {X : Condensed C} {Y : Condensed C} {Z : Condensed C} (f : X ⟶ Y) (g : Y ⟶ Z) :
      (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val
      source
      theorem Condensed.hom_ext {C : Type w} [CategoryTheory.Category.{v, w} C] {X : Condensed C} {Y : Condensed C} (f : X ⟶ Y) (g : X ⟶ Y) (h : ∀ (S : CompHausᵒᵖ), f.val.app S = g.val.app S) :
      f = g
      source
      @[simp]
      theorem CondensedSet.hom_naturality_apply {X : CondensedSet} {Y : CondensedSet} (f : X ⟶ Y) {S : CompHausᵒᵖ} {T : CompHausᵒᵖ} (g : S ⟶ T) (x : X.val.obj S) :
      f.val.app T (X.val.map g x) = Y.val.map g (f.val.app S x)