Documentation

Mathlib.Condensed.Light.Explicit

The explicit sheaf condition for light condensed sets #

We give explicit description of light condensed sets:

The property EqualizerCondition is defined in Mathlib/CategoryTheory/Sites/RegularExtensive.lean and it says that for any effective epi X ⟶ B (in this case that is equivalent to being a continuous surjection), the presheaf F exhibits F(B) as the equalizer of the two maps F(X) ⇉ F(X ×_B X)

We also give variants for light condensed objects in concrete categories whose forgetful functor reflects finite limits (resp. products), where it is enough to check the sheaf condition after postcomposing with the forgetful functor.

The light condensed object associated to a presheaf on LightProfinite which preserves finite products and satisfies the equalizer condition.

Equations
Instances For

    The light condensed object associated to a presheaf on LightProfinite whose postcomposition with the forgetful functor preserves finite products and satisfies the equalizer condition.

    Equations
    Instances For

      A light condensed object satisfies the equalizer condition.

      A light condensed object preserves finite products.

      Equations
      • X.instPreservesFiniteProductsOppositeLightProfiniteVal = .some