Theorems · Theorem · category theory
TopCat.toSheafCompHausLike_obj_obj
∀ (P : TopCat → Prop) (X : 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))
(X_1 : (CompHausLike P)ᵒᵖ),
(TopCat.toSheafCompHausLike P X hs).obj.obj X_1 = C(↑((CompHausLike.compHausLikeToTop P).obj (Opposite.unop X_1)), ↑X)- Defined in
- Mathlib.Condensed.TopComparison
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CategoryTheory.Functorstatement · cited by 16,252
- Oppositestatement and proof · cited by 8,081
- CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
- TopCat.carrierstatement · cited by 3,184
- ContinuousMapstatement · cited by 2,491
- Opposite.unopstatement · cited by 2,231
- TopCatstatement and proof · cited by 1,889
- CategoryTheory.ObjectProperty.FullSubcategory.objstatement and proof · cited by 1,316
- CategoryTheory.Presheaf.IsSheafstatement · cited by 991
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.