Theorems · Theorem · category theory

TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  {c c' : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)} (f : c ⟶ c'),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).map f).hom = f.hom

Defined in

Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasProducts