Theorems · Theorem · category theory

TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_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)
  (X_1 : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso F U).inv.app X_1).hom =
    CategoryTheory.CategoryStruct.id X_1.pt

Defined in

Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasProducts