Theorems · Definition · category theory

TopCat.toSheafCompHausLike

(P : TopCat → Prop) →
  TopCat →
    [inst : CompHausLike.HasExplicitFiniteCoproducts P] →
      [inst_1 : CompHausLike.HasExplicitPullbacks P] →
        (hs :
            ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
              CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
          have this := ⋯;
          CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))

The sheaf on CompHausLike P of continuous maps to a topological space.

Defined in

Mathlib.Condensed.TopComparison

Cited by

4 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompHausLike.HasExplicitFiniteCoproductsCompHausLike.HasExplicitPullbacks