Theorems · Definition · category theory

TopologicalSpace.Opens.sheafEquivOver

{X : Type u} →
  [inst : TopologicalSpace X] →
    (U : TopologicalSpace.Opens X) →
      {A : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
          CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A ≌
            CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A

Sheaves on the over category of U are equivalent to sheaves on U as a topological space.

Defined in

Mathlib.Topology.Sheaves.Over

Cited by

10 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCategoryTheory.Category