Theorems · Theorem · category theory

TopCat.Sheaf.interUnionPullbackConeLift_right

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Sheaf C X)
  (U V : TopologicalSpace.Opens ↑X)
  (s :
    CategoryTheory.Limits.PullbackCone (F.obj.map (CategoryTheory.homOfLE ⋯).op)
      (F.obj.map (CategoryTheory.homOfLE ⋯).op)),
  CategoryTheory.CategoryStruct.comp (F.interUnionPullbackConeLift U V s) (F.obj.map (CategoryTheory.homOfLE ⋯).op) =
    s.snd

Defined in

Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category