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 pullback C f : Y.Presheaf C ⥤ X.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 (Opposite.op U) = g.app (Opposite.op 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

          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]

                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
                    @[simp]
                    theorem TopCat.Presheaf.pushforward_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ C) :
                    ∀ {X_1 Y_1 : (TopologicalSpace.Opens Y)ᵒᵖ} (f_1 : X_1 Y_1), ((TopCat.Presheaf.pushforward C f).obj G).map f_1 = G.map ((TopologicalSpace.Opens.map f).map f_1.unop).op
                    @[simp]

                    push forward of a presheaf

                    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)ᵒᵖ} :

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

                      Equations
                      Instances For

                        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
                          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) :

                          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) :
                            @[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)ᵒᵖ) :
                            @[simp]
                            @[simp]
                            @[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

                            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} (α : (TopCat.Presheaf.pushforward C H.hom).obj 𝒢) :
                              (TopCat.Presheaf.pushforward C H.inv).obj 𝒢

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

                              Equations
                              Instances For
                                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₂ : (TopCat.Presheaf.pushforward C H₁.hom).obj 𝒢) :
                                (TopCat.Presheaf.pushforward C H₁.inv).obj 𝒢

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

                                Equations
                                Instances For

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

                                  Equations
                                  Instances For

                                    The pullback and pushforward along a continuous map are adjoint to each other.

                                    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
                                          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.pullback C f).obj ).obj (Opposite.op U) .obj (Opposite.op { 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