Documentation

Mathlib.Topology.Sheaves.Presheaf

Presheaves on a topological space #

We define TopCat.Presheaf C X simply as (TopologicalSpace.Opens X)ᵒᵖ ⥤ C, and inherit the category structure with natural transformations as morphisms.

We define

We also define the functors pushforward and pullback between the categories X.Presheaf C and Y.Presheaf C, and provide their adjunction at TopCat.Presheaf.pushforwardPullbackAdjunction.

The category of C-valued presheaves on a (bundled) topological space X.

Equations
Instances For
    theorem TopCat.Presheaf.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {P : TopCat.Presheaf C X} {Q : TopCat.Presheaf C X} {f : P Q} {g : P Q} (w : ∀ (U : TopologicalSpace.Opens X), f.app { unop := U } = g.app { unop := U }) :
    f = g

    attribute sheaf_restrict to mark lemmas related to restricting sheaves

    Equations
    Instances For

      restrict_tac solves relations among subsets (copied from aesop cat)

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        restrict_tac? passes along Try this from aesop

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def TopCat.Presheaf.restrict {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] {F : TopCat.Presheaf C X} {V : TopologicalSpace.Opens X} (x : (CategoryTheory.forget C).obj (F.obj { unop := V })) {U : TopologicalSpace.Opens X} (h : U V) :
          (CategoryTheory.forget C).obj (F.obj { unop := U })

          The restriction of a section along an inclusion of open sets. For x : F.obj (op V), we provide the notation x |_ₕ i (h stands for hom) for i : U ⟶ V, and the notation x |_ₗ U ⟪i⟫ (l stands for le) for i : U ≤ V.

          Equations
          Instances For

            restriction of a section along an inclusion

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              restriction of a section along a subset relation

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[reducible, inline]
                abbrev TopCat.Presheaf.restrictOpen {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] {F : TopCat.Presheaf C X} {V : TopologicalSpace.Opens X} (x : (CategoryTheory.forget C).obj (F.obj { unop := V })) (U : TopologicalSpace.Opens X) (e : autoParam (U V) _auto✝) :
                (CategoryTheory.forget C).obj (F.obj { unop := 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'

                Equations
                Instances For

                  restriction of a section to open subset

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem TopCat.Presheaf.map_restrict {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] {F : TopCat.Presheaf C X} {G : TopCat.Presheaf C X} (e : F G) {U : TopologicalSpace.Opens X} {V : TopologicalSpace.Opens X} (h : U V) (x : (CategoryTheory.forget C).obj (F.obj { unop := V })) :
                    (e.app { unop := U }) (TopCat.Presheaf.restrictOpen x U h) = TopCat.Presheaf.restrictOpen ((e.app { unop := V }) x) U h

                    Pushforward a presheaf on X along a continuous map f : X ⟶ Y, obtaining a presheaf on Y.

                    Equations
                    Instances For

                      push forward of a presheaf

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem TopCat.Presheaf.pushforwardObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens Y)ᵒᵖ) :
                        (f _* ).obj U = .obj ((TopologicalSpace.Opens.map f).op.obj U)
                        @[simp]
                        theorem TopCat.Presheaf.pushforwardObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : TopCat.Presheaf C X) {U : (TopologicalSpace.Opens Y)ᵒᵖ} {V : (TopologicalSpace.Opens Y)ᵒᵖ} (i : U V) :
                        (f _* ).map i = .map ((TopologicalSpace.Opens.map f).op.map i)
                        def TopCat.Presheaf.pushforwardEq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X Y} {g : X Y} (h : f = g) (ℱ : TopCat.Presheaf C X) :
                        f _* g _*

                        An equality of continuous maps induces a natural isomorphism between the pushforwards of a presheaf along those maps.

                        Equations
                        Instances For
                          theorem TopCat.Presheaf.pushforward_eq' {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X Y} {g : X Y} (h : f = g) (ℱ : TopCat.Presheaf C X) :
                          f _* = g _*
                          @[simp]
                          theorem TopCat.Presheaf.pushforwardEq_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X Y} {g : X Y} (h : f = g) (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens Y)ᵒᵖ) :
                          (TopCat.Presheaf.pushforwardEq h ).hom.app U = .map (id (CategoryTheory.eqToHom ).op)
                          theorem TopCat.Presheaf.pushforward_eq'_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X Y} {g : X Y} (h : f = g) (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens Y)ᵒᵖ) :
                          @[simp]
                          theorem TopCat.Presheaf.pushforwardEq_rfl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : TopCat.Presheaf C X) (U : TopologicalSpace.Opens Y) :
                          (TopCat.Presheaf.pushforwardEq ).hom.app { unop := U } = CategoryTheory.CategoryStruct.id ((f _* ).obj { unop := U })
                          theorem TopCat.Presheaf.pushforwardEq_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X Y} {g : X Y} (h₁ : f = g) (h₂ : f = g) (ℱ : TopCat.Presheaf C X) :

                          The natural isomorphism between the pushforward of a presheaf along the identity continuous map and the original presheaf.

                          Equations
                          Instances For
                            @[simp]
                            theorem TopCat.Presheaf.Pushforward.id_hom_app' {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (U : Set X) (p : IsOpen U) :
                            (TopCat.Presheaf.Pushforward.id ).hom.app { unop := { carrier := U, is_open' := p } } = .map (CategoryTheory.CategoryStruct.id { unop := { carrier := U, is_open' := p } })
                            @[simp]
                            theorem TopCat.Presheaf.Pushforward.id_inv_app' {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (U : Set X) (p : IsOpen U) :
                            (TopCat.Presheaf.Pushforward.id ).inv.app { unop := { carrier := U, is_open' := p } } = .map (CategoryTheory.CategoryStruct.id { unop := { carrier := U, is_open' := p } })

                            The natural isomorphism between the pushforward of a presheaf along the composition of two continuous maps and the corresponding pushforward of a pushforward.

                            Equations
                            Instances For
                              @[simp]
                              @[simp]
                              theorem TopCat.Presheaf.pushforwardMap_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C X} (α : 𝒢) (U : (TopologicalSpace.Opens Y)ᵒᵖ) :
                              def TopCat.Presheaf.pushforwardMap {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C X} (α : 𝒢) :
                              f _* f _* 𝒢

                              A morphism of presheaves gives rise to a morphisms of the pushforwards of those presheaves.

                              Equations
                              Instances For

                                Pullback a presheaf on Y along a continuous map f : X ⟶ Y, obtaining a presheaf on X.

                                This is defined in terms of left Kan extensions, which is just a fancy way of saying "take the colimits over the open sets whose preimage contains U".

                                Equations
                                Instances For

                                  Pulling back along continuous maps is functorial.

                                  Equations
                                  Instances For
                                    def TopCat.Presheaf.pullbackObjObjOfImageOpen {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X Y) (ℱ : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens X) (H : IsOpen (f '' U)) :
                                    (TopCat.Presheaf.pullbackObj f ).obj { unop := U } .obj { unop := { carrier := f '' U, is_open' := H } }

                                    If f '' U is open, then f⁻¹ℱ U ≅ ℱ (f '' U).

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      The pullback along the identity is isomorphic to the original presheaf.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        The pushforward functor.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem TopCat.Presheaf.pushforward_map_app' (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C X} (α : 𝒢) {U : (TopologicalSpace.Opens Y)ᵒᵖ} :
                                          ((TopCat.Presheaf.pushforward C f).map α).app U = α.app { unop := (TopologicalSpace.Opens.map f).obj U.unop }
                                          @[simp]
                                          theorem TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝¹ Y) (X : CategoryTheory.Functor (TopologicalSpace.Opens X✝¹)ᵒᵖ C) (X : (TopologicalSpace.Opens X✝¹)ᵒᵖ) :
                                          ((TopCat.Presheaf.presheafEquivOfIso C H).unitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.comp (X✝.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unit.app X)) (CategoryTheory.CategoryStruct.comp (X✝.map ((TopologicalSpace.Opens.map H.hom).map ((TopologicalSpace.Opens.mapMapIso H).symm.op.counitInv.app { unop := (TopologicalSpace.Opens.map H.inv).obj X.unop }).unop).op) (X✝.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unitInv.app { unop := (TopologicalSpace.Opens.map H.hom).obj ((TopologicalSpace.Opens.map H.inv).obj X.unop) })))
                                          @[simp]
                                          theorem TopCat.Presheaf.presheafEquivOfIso_inverse_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X Y) :
                                          ∀ {X_1 Y_1 : CategoryTheory.Functor (TopologicalSpace.Opens Y)ᵒᵖ C} (α : X_1 Y_1) (X_2 : (TopologicalSpace.Opens X)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.map α).app X_2 = α.app { unop := (TopologicalSpace.Opens.map H.inv).obj X_2.unop }
                                          @[simp]
                                          theorem TopCat.Presheaf.presheafEquivOfIso_functor_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X Y) :
                                          ∀ {X_1 Y_1 : CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ C} (α : X_1 Y_1) (X_2 : (TopologicalSpace.Opens Y)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).functor.map α).app X_2 = α.app { unop := (TopologicalSpace.Opens.map H.hom).obj X_2.unop }
                                          @[simp]
                                          theorem TopCat.Presheaf.presheafEquivOfIso_functor_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ C) :
                                          ∀ {X_1 Y_1 : (TopologicalSpace.Opens Y)ᵒᵖ} (f : X_1 Y_1), ((TopCat.Presheaf.presheafEquivOfIso C H).functor.obj G).map f = G.map ((TopologicalSpace.Opens.map H.hom).map f.unop).op
                                          @[simp]
                                          theorem TopCat.Presheaf.presheafEquivOfIso_inverse_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens Y)ᵒᵖ C) :
                                          ∀ {X_1 Y_1 : (TopologicalSpace.Opens X)ᵒᵖ} (f : X_1 Y_1), ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.obj G).map f = G.map ((TopologicalSpace.Opens.map H.inv).map f.unop).op
                                          @[simp]
                                          theorem TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝¹ Y) (X : CategoryTheory.Functor (TopologicalSpace.Opens X✝¹)ᵒᵖ C) (X : (TopologicalSpace.Opens X✝¹)ᵒᵖ) :
                                          ((TopCat.Presheaf.presheafEquivOfIso C H).unitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.comp (X✝.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unit.app { unop := (TopologicalSpace.Opens.map H.hom).obj ((TopologicalSpace.Opens.map H.inv).obj X.unop) })) (CategoryTheory.CategoryStruct.comp (X✝.map ((TopologicalSpace.Opens.map H.hom).map ((TopologicalSpace.Opens.mapMapIso H).symm.op.counit.app { unop := (TopologicalSpace.Opens.map H.inv).obj X.unop }).unop).op) (X✝.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unitInv.app X)))

                                          A homeomorphism of spaces gives an equivalence of categories of presheaves.

                                          Equations
                                          Instances For
                                            def TopCat.Presheaf.toPushforwardOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C Y} (α : H.hom _* 𝒢) :
                                            H.inv _* 𝒢

                                            If H : X ≅ Y is a homeomorphism, then given an H _* ℱ ⟶ 𝒢, we may obtain an ℱ ⟶ H ⁻¹ _* 𝒢.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem TopCat.Presheaf.toPushforwardOfIso_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H₁ : X Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C Y} (H₂ : H₁.hom _* 𝒢) (U : (TopologicalSpace.Opens X)ᵒᵖ) :
                                              (TopCat.Presheaf.toPushforwardOfIso H₁ H₂).app U = CategoryTheory.CategoryStruct.comp (.map (CategoryTheory.eqToHom )) (H₂.app { unop := (TopologicalSpace.Opens.map H₁.inv).obj U.unop })
                                              def TopCat.Presheaf.pushforwardToOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H₁ : X Y) {ℱ : TopCat.Presheaf C Y} {𝒢 : TopCat.Presheaf C X} (H₂ : H₁.hom _* 𝒢) :
                                              H₁.inv _* 𝒢

                                              If H : X ≅ Y is a homeomorphism, then given an H _* ℱ ⟶ 𝒢, we may obtain an ℱ ⟶ H ⁻¹ _* 𝒢.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem TopCat.Presheaf.pushforwardToOfIso_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H₁ : X Y) {ℱ : TopCat.Presheaf C Y} {𝒢 : TopCat.Presheaf C X} (H₂ : H₁.hom _* 𝒢) (U : (TopologicalSpace.Opens X)ᵒᵖ) :
                                                (TopCat.Presheaf.pushforwardToOfIso H₁ H₂).app U = CategoryTheory.CategoryStruct.comp (H₂.app { unop := (TopologicalSpace.Opens.map H₁.inv).obj U.unop }) (𝒢.map (CategoryTheory.eqToHom ))

                                                Pullback a presheaf on Y along a continuous map f : X ⟶ Y, obtaining a presheaf on X.

                                                Equations
                                                Instances For

                                                  Pulling back along a homeomorphism is the same as pushing forward along its inverse.

                                                  Equations
                                                  Instances For

                                                    Pulling back along the inverse of a homeomorphism is the same as pushing forward along it.

                                                    Equations
                                                    Instances For