Documentation

Mathlib.Condensed.Explicit

The explicit sheaf condition for condensed sets #

We give the following three explicit descriptions of condensed objects:

The property EqualizerCondition is defined in Mathlib/CategoryTheory/Sites/RegularSheaves.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 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 condensed object associated to a finite-product-preserving presheaf on Stonean.

Equations
Instances For

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

    Equations
    Instances For

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

      Equations
      Instances For

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

        Equations
        Instances For

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

          Equations
          Instances For

            A condensed object satisfies the equalizer condition.

            A condensed object preserves finite products.

            Equations
            • X.instPreservesFiniteProductsOppositeCompHausVal = .some