Theorems · Definition · category theory

TopCat.Presheaf.restrictOpen

{X : TopCat} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {FC : C → C → Type u_1} →
        {CC : C → Type u_2} →
          [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory C FC] →
              {F : TopCat.Presheaf C X} →
                {V : TopologicalSpace.Opens ↑X} →
                  CategoryTheory.ToType (F.obj (Opposite.op V)) →
                    (U : TopologicalSpace.Opens ↑X) →
                      autoParam (U ≤ V) TopCat.Presheaf.restrictOpen._auto_1 →
                        CategoryTheory.ToType (F.obj (Opposite.op U))

The restriction of a section along an inclusion of open sets. For x : F.obj (op V), we provide the notation x |_ U, where the proof U ≤ V is inferred by the tactic Top.presheaf.restrict_tac'

Defined in

Mathlib.Topology.Sheaves.Presheaf

Cited by

25 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategory