Documentation

Mathlib.CategoryTheory.Sites.DenseSubsite

Dense subsites #

We define IsCoverDense functors into sites as functors such that there exists a covering sieve that factors through images of the functor for each object in D.

Main results #

References #

An auxiliary structure that witnesses the fact that f factors through an image object of G.

Instances For

    For a functor G : C ⥤ D, and an object U : D, Presieve.coverByImage G U is the presieve of U consisting of those arrows that factor through images of G.

    Equations
    Instances For

      For a functor G : C ⥤ D, and an object U : D, Sieve.coverByImage G U is the sieve of U consisting of those arrows that factor through images of G.

      Equations
      Instances For

        A functor G : (C, J) ⥤ (D, K) is cover dense if for each object in D, there exists a covering sieve in D that factors through images of G.

        This definition can be found in https://ncatlab.org/nlab/show/dense+sub-site Definition 2.2.

        Instances
          theorem CategoryTheory.Functor.IsCoverDense.ext {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} (G : CategoryTheory.Functor C D) [G.IsCoverDense K] (ℱ : CategoryTheory.SheafOfTypes K) (X : D) {s : .val.obj (Opposite.op X)} {t : .val.obj (Opposite.op X)} (h : ∀ ⦃Y : C⦄ (f : G.obj Y X), .val.map f.op s = .val.map f.op t) :
          s = t
          @[simp]
          theorem CategoryTheory.Functor.IsCoverDense.homOver_app {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : G.op.comp G.op.comp ℱ'.val) (X : A) (X : Cᵒᵖ) :
          ∀ (a : (CategoryTheory.coyoneda.obj (Opposite.op X✝)).obj ((G.op.comp ).obj X)), (CategoryTheory.Functor.IsCoverDense.homOver α X✝).app X a = CategoryTheory.CategoryStruct.comp a (α.app X)
          def CategoryTheory.Functor.IsCoverDense.homOver {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : G.op.comp G.op.comp ℱ'.val) (X : A) :
          G.op.comp (.comp (CategoryTheory.coyoneda.obj (Opposite.op X))) G.op.comp (CategoryTheory.sheafOver ℱ' X).val

          (Implementation). Given a hom between the pullbacks of two sheaves, we can whisker it with coyoneda to obtain a hom between the pullbacks of the sheaves of maps from X.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Functor.IsCoverDense.isoOver_hom_app {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (α : G.op.comp .val G.op.comp ℱ'.val) (X : A) (X : Cᵒᵖ) :
            ∀ (a : (CategoryTheory.coyoneda.obj (Opposite.op X✝)).obj ((G.op.comp .val).obj X)), (CategoryTheory.Functor.IsCoverDense.isoOver α X✝).hom.app X a = CategoryTheory.CategoryStruct.comp a (α.hom.app X)
            @[simp]
            theorem CategoryTheory.Functor.IsCoverDense.isoOver_inv_app {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (α : G.op.comp .val G.op.comp ℱ'.val) (X : A) (X : Cᵒᵖ) :
            ∀ (a : (CategoryTheory.coyoneda.obj (Opposite.op X✝)).obj ((G.op.comp ℱ'.val).obj X)), (CategoryTheory.Functor.IsCoverDense.isoOver α X✝).inv.app X a = CategoryTheory.CategoryStruct.comp a (α.inv.app X)

            (Implementation). Given an iso between the pullbacks of two sheaves, we can whisker it with coyoneda to obtain an iso between the pullbacks of the sheaves of maps from X.

            Equations
            Instances For
              theorem CategoryTheory.Functor.IsCoverDense.sheaf_eq_amalgamation {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_6, u_4} A] (ℱ : CategoryTheory.Sheaf K A) {X : A} {U : D} {T : CategoryTheory.Sieve U} (hT : T K U) (x : CategoryTheory.Presieve.FamilyOfElements (.val.comp (CategoryTheory.coyoneda.obj (Opposite.op X))) T.arrows) (hx : x.Compatible) (t : (.val.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).obj (Opposite.op U)) (h : x.IsAmalgamation t) :
              t = .amalgamate x hx
              theorem CategoryTheory.Functor.IsCoverDense.Types.naturality_apply {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : G.op.comp G.op.comp ℱ'.val) [G.IsLocallyFull K] {X : C} {Y : C} (i : G.obj X G.obj Y) (x : (G.op.comp ).obj (Opposite.op Y)) :
              ℱ'.val.map i.op (α.app (Opposite.op Y) x) = α.app (Opposite.op X) (.map i.op x)
              theorem CategoryTheory.Functor.IsCoverDense.Types.naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : G.op.comp G.op.comp ℱ'.val) [G.IsLocallyFull K] {X : C} {Y : C} (i : G.obj X G.obj Y) {Z : Type v} (h : ℱ'.val.obj (Opposite.op (G.obj X)) Z) :
              theorem CategoryTheory.Functor.IsCoverDense.Types.naturality {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : G.op.comp G.op.comp ℱ'.val) [G.IsLocallyFull K] {X : C} {Y : C} (i : G.obj X G.obj Y) :
              CategoryTheory.CategoryStruct.comp (α.app (Opposite.op Y)) (ℱ'.val.map i.op) = CategoryTheory.CategoryStruct.comp (.map i.op) (α.app (Opposite.op X))

              (Implementation). Given a section of on X, we can obtain a family of elements valued in ℱ' that is defined on a cover generated by the images of G.

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_def {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : G.op.comp G.op.comp ℱ'.val) {X : D} (x : .obj (Opposite.op X)) :
                CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x = fun (x_1 : D) (x_2 : x_1 X) (hf : CategoryTheory.Presieve.coverByImage G X x_2) => ℱ'.val.map (Nonempty.some hf).lift.op (α.app (Opposite.op (Nonempty.some hf).1) (.map (Nonempty.some hf).map.op x))
                @[simp]
                theorem CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_apply {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : G.op.comp G.op.comp ℱ'.val) [G.IsLocallyFull K] {X : D} (x : .obj (Opposite.op X)) {Y : C} (f : G.obj Y X) :

                (Implementation). The pushforwardFamily defined is compatible.

                noncomputable def CategoryTheory.Functor.IsCoverDense.Types.appHom {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : G.op.comp G.op.comp ℱ'.val) [G.IsCoverDense K] [G.IsLocallyFull K] (X : D) :
                .obj (Opposite.op X) ℱ'.val.obj (Opposite.op X)

                (Implementation). The morphism ℱ(X) ⟶ ℱ'(X) given by gluing the pushforwardFamily.

                Equations
                Instances For
                  @[simp]
                  theorem CategoryTheory.Functor.IsCoverDense.Types.appHom_restrict {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : G.op.comp G.op.comp ℱ'.val) [G.IsCoverDense K] [G.IsLocallyFull K] {X : D} {Y : C} (f : Opposite.op X Opposite.op (G.obj Y)) (x : .obj (Opposite.op X)) :
                  ℱ'.val.map f (CategoryTheory.Functor.IsCoverDense.Types.appHom α X x) = α.app (Opposite.op Y) (.map f x)
                  noncomputable def CategoryTheory.Functor.IsCoverDense.Types.appIso {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : G.op.comp .val G.op.comp ℱ'.val) (X : D) :
                  .val.obj (Opposite.op X) ℱ'.val.obj (Opposite.op X)

                  (Implementation). The maps given in appIso is inverse to each other and gives a ℱ(X) ≅ ℱ'(X).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    noncomputable def CategoryTheory.Functor.IsCoverDense.Types.presheafHom {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} [G.IsCoverDense K] [G.IsLocallyFull K] (α : G.op.comp G.op.comp ℱ'.val) :
                    ℱ'.val

                    Given a natural transformation G ⋙ ℱ ⟶ G ⋙ ℱ' between presheaves of types, where G is locally-full and cover-dense, and ℱ' is a sheaf, we may obtain a natural transformation between sheaves.

                    Equations
                    Instances For
                      noncomputable def CategoryTheory.Functor.IsCoverDense.Types.presheafIso {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : G.op.comp .val G.op.comp ℱ'.val) :
                      .val ℱ'.val

                      Given a natural isomorphism G ⋙ ℱ ≅ G ⋙ ℱ' between presheaves of types, where G is locally-full and cover-dense, and ℱ, ℱ' are sheaves, we may obtain a natural isomorphism between presheaves.

                      Equations
                      Instances For
                        noncomputable def CategoryTheory.Functor.IsCoverDense.Types.sheafIso {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : G.op.comp .val G.op.comp ℱ'.val) :
                        ℱ'

                        Given a natural isomorphism G ⋙ ℱ ≅ G ⋙ ℱ' between presheaves of types, where G is locally-full and cover-dense, and ℱ, ℱ' are sheaves, we may obtain a natural isomorphism between sheaves.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          noncomputable def CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : G.op.comp G.op.comp ℱ'.val) :
                          CategoryTheory.coyoneda.comp ((CategoryTheory.whiskeringLeft Dᵒᵖ A (Type u_7)).obj ) CategoryTheory.coyoneda.comp ((CategoryTheory.whiskeringLeft Dᵒᵖ A (Type u_7)).obj ℱ'.val)

                          (Implementation). The sheaf map given in types.sheaf_hom is natural in terms of X.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            noncomputable def CategoryTheory.Functor.IsCoverDense.sheafYonedaHom {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : G.op.comp G.op.comp ℱ'.val) :
                            .comp CategoryTheory.yoneda ℱ'.val.comp CategoryTheory.yoneda

                            (Implementation). sheafCoyonedaHom but the order of the arguments of the functor are swapped.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              noncomputable def CategoryTheory.Functor.IsCoverDense.sheafHom {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : G.op.comp G.op.comp ℱ'.val) :
                              ℱ'.val

                              Given a natural transformation G ⋙ ℱ ⟶ G ⋙ ℱ' between presheaves of arbitrary category, where G is locally-full and cover-dense, and ℱ' is a sheaf, we may obtain a natural transformation between presheaves.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem CategoryTheory.Functor.IsCoverDense.presheafIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (i : G.op.comp .val G.op.comp ℱ'.val) (X : Dᵒᵖ) :
                                noncomputable def CategoryTheory.Functor.IsCoverDense.presheafIso {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (i : G.op.comp .val G.op.comp ℱ'.val) :
                                .val ℱ'.val

                                Given a natural isomorphism G ⋙ ℱ ≅ G ⋙ ℱ' between presheaves of arbitrary category, where G is locally-full and cover-dense, and ℱ', ℱ are sheaves, we may obtain a natural isomorphism between presheaves.

                                Equations
                                Instances For
                                  noncomputable def CategoryTheory.Functor.IsCoverDense.sheafIso {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (i : G.op.comp .val G.op.comp ℱ'.val) :
                                  ℱ'

                                  Given a natural isomorphism G ⋙ ℱ ≅ G ⋙ ℱ' between presheaves of arbitrary category, where G is locally-full and cover-dense, and ℱ', ℱ are sheaves, we may obtain a natural isomorphism between presheaves.

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

                                    The constructed sheafHom α is equal to α when restricted onto C.

                                    If the pullback map is obtained via whiskering, then the result sheaf_hom (whisker_left G.op α) is equal to α.

                                    noncomputable def CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} :
                                    (G.op.comp G.op.comp ℱ'.val) ( ℱ'.val)

                                    A locally-full and cover-dense functor G induces an equivalence between morphisms into a sheaf and morphisms over the restrictions via G.

                                    Equations
                                    • CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom = { toFun := CategoryTheory.Functor.IsCoverDense.sheafHom, invFun := CategoryTheory.whiskerLeft G.op, left_inv := , right_inv := }
                                    Instances For

                                      Given a locally-full and cover-dense functor G and a natural transformation of sheaves α : ℱ ⟶ ℱ', if the pullback of α along G is iso, then α is also iso.

                                      A locally-fully-faithful and cover-dense functor preserves compatible families.

                                      instance CategoryTheory.Functor.IsCoverDense.full_sheafPushforwardContinuous {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_7, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {A : Type u_4} [CategoryTheory.Category.{u_5, u_4} A] (G : CategoryTheory.Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] [G.IsContinuous J K] :
                                      (G.sheafPushforwardContinuous A J K).Full
                                      Equations
                                      • =
                                      instance CategoryTheory.Functor.IsCoverDense.faithful_sheafPushforwardContinuous {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_7, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {A : Type u_4} [CategoryTheory.Category.{u_5, u_4} A] (G : CategoryTheory.Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] [G.IsContinuous J K] :
                                      (G.sheafPushforwardContinuous A J K).Faithful
                                      Equations
                                      • =

                                      If G : C ⥤ D is cover dense and full, then the map (P ⟶ Q) → (G.op ⋙ P ⟶ G.op ⋙ Q) is bijective when Q is a sheaf`.

                                      The functor G : C ⥤ D exhibits (C, J) as a dense subsite of (D, K) if G is cover-dense, locally fully-faithful, and S is a cover of C if and only if the image of S in D is a cover.

                                      Instances

                                        If G : C ⥤ D exhibits (C, J) as a dense subsite of (D, K), it induces an equivalence of category of sheaves valued in a category with suitable limits.

                                        Equations
                                        Instances For