Light condensed objects

This file defines the category of light condensed objects in a category C, following the work of Clausen-Scholze (see https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO).

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

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

@[implicit_reducible]

instance instCategoryLightCondensed {C : Type w} [CategoryTheory.Category.{v, w} C] : CategoryTheory.Category.{max (u + 1) v, max (max (u + 1) w) v} (LightCondensed C)

@[reducible, inline]

abbrev LightCondSet : Type (u + 1)

Light condensed sets. Because LightProfinite is an essentially small category, we don't need the same universe bump as in CondensedSet.

@[simp]

theorem LightCondensed.id_hom {C : Type w} [CategoryTheory.Category.{v, w} C] (X : LightCondensed C) : (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.obj

@[simp]

theorem LightCondensed.comp_hom {C : Type w} [CategoryTheory.Category.{v, w} C] {X Y Z : LightCondensed C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

@[deprecated LightCondensed.id_hom (since := "2026-03-05")]

theorem LightCondensed.id_val {C : Type w} [CategoryTheory.Category.{v, w} C] (X : LightCondensed C) : (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.obj

Alias of LightCondensed.id_hom.

@[deprecated LightCondensed.comp_hom (since := "2026-03-05")]

theorem LightCondensed.comp_val {C : Type w} [CategoryTheory.Category.{v, w} C] {X Y Z : LightCondensed C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

Alias of LightCondensed.comp_hom.

theorem LightCondensed.hom_ext {C : Type w} [CategoryTheory.Category.{v, w} C] {X Y : LightCondensed C} (f g : X ⟶ Y) (h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S) : f = g

theorem LightCondensed.hom_ext_iff {C : Type w} [CategoryTheory.Category.{v, w} C] {X Y : LightCondensed C} {f g : X ⟶ Y} : f = g ↔ ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S

@[simp]

theorem LightCondSet.hom_naturality_apply {X Y : LightCondSet} (f : X ⟶ Y) {S T : LightProfiniteᵒᵖ} (g : S ⟶ T) (x : X.obj.obj S) : f.hom.app T (X.obj.map g x) = Y.obj.map g (f.hom.app S x)