Dense subsites

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

We will primarily consider cover-dense functors that are also full, since this notion is in general not well-behaved otherwise. Note that https://ncatlab.org/nlab/show/dense+sub-site indeed has a weaker notion of cover-dense that loosens this requirement, but it would not have all the properties we would need, and some sheafification would be needed for here and there.

Main results

• CategoryTheory.CoverDense.Types.presheafHom: If G : C ⥤ (D, K) is full and cover-dense, then given any presheaf ℱ and sheaf ℱ' on D, and a morphism α : G ⋙ ℱ ⟶ G ⋙ ℱ', we may glue them together to obtain a morphism of presheaves ℱ ⟶ ℱ'.
• CategoryTheory.CoverDense.sheafIso: If ℱ above is a sheaf and α is an iso, then the result is also an iso.
• CategoryTheory.CoverDense.iso_of_restrict_iso: If G : C ⥤ (D, K) is full and cover-dense, then given any sheaves ℱ, ℱ' on D, and a morphism α : ℱ ⟶ ℱ', then α is an iso if G ⋙ ℱ ⟶ G ⋙ ℱ' is iso.
• CategoryTheory.CoverDense.sheafEquivOfCoverPreservingCoverLifting: If G : (C, J) ⥤ (D, K) is fully-faithful, cover-lifting, cover-preserving, and cover-dense, then it will induce an equivalence of categories of sheaves valued in a complete category.

References

• [Elephant]: Sketches of an Elephant, ℱ. T. Johnstone: C2.2.
• https://ncatlab.org/nlab/show/dense+sub-site
• https://ncatlab.org/nlab/show/comparison+lemma

structure CategoryTheory.Presieve.CoverByImageStructure {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (G : CategoryTheory.Functor C D) {V : D} {U : D} (f : V ⟶ U) : Type (max u_1 u_5)

• obj : C
• lift : V ⟶ G.obj s.obj
• map : G.obj s.obj ⟶ U
• fac : CategoryTheory.CategoryStruct.comp s.lift s.map = f

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

@[simp]

theorem CategoryTheory.Presieve.CoverByImageStructure.fac_assoc {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] {G : CategoryTheory.Functor C D} {V : D} {U : D} {f : V ⟶ U} (self : CategoryTheory.Presieve.CoverByImageStructure G f) {Z : D} (h : U ⟶ Z) : CategoryTheory.CategoryStruct.comp self.lift (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp f h

def CategoryTheory.Presieve.coverByImage {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (G : CategoryTheory.Functor C D) (U : D) : CategoryTheory.Presieve U

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.

def CategoryTheory.Sieve.coverByImage {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (G : CategoryTheory.Functor C D) (U : D) : CategoryTheory.Sieve U

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.

theorem CategoryTheory.Presieve.in_coverByImage {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (G : CategoryTheory.Functor C D) {X : D} {Y : C} (f : G.obj Y ⟶ X) : CategoryTheory.Presieve.coverByImage G X f

structure CategoryTheory.CoverDense {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) : Prop

• is_cover : ∀ (U : D), CategoryTheory.Sieve.coverByImage G U ∈ CategoryTheory.GrothendieckTopology.sieves K U

A functor G : (C, J) ⥤ (D, K) is called CoverDense 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.

theorem CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) (ℱ : 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), Dᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type u_7) CategoryTheory.CategoryStruct.toQuiver ℱ.val.toPrefunctor (Opposite.op X) (Opposite.op (G.obj Y)) f.op s = Dᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type u_7) CategoryTheory.CategoryStruct.toQuiver ℱ.val.toPrefunctor (Opposite.op X) (Opposite.op (G.obj Y)) f.op t) : s = t

theorem CategoryTheory.CoverDense.functorPullback_pushforward_covering {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.Full G] (H : CategoryTheory.CoverDense K G) {X : C} (T : ↑(CategoryTheory.GrothendieckTopology.sieves K (G.obj X))) : CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPullback G ↑T) ∈ CategoryTheory.GrothendieckTopology.sieves K (G.obj X)

@[simp]

theorem CategoryTheory.CoverDense.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} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) (X : A) (X : Cᵒᵖ) : ∀ (a : (CategoryTheory.coyoneda.obj (Opposite.op X)).obj ((CategoryTheory.Functor.comp G.op ℱ).obj X)), Cᵒᵖ.app CategoryTheory.Category.opposite (Type u_7) CategoryTheory.types (CategoryTheory.Functor.comp G.op (CategoryTheory.Functor.comp ℱ (CategoryTheory.coyoneda.obj (Opposite.op X)))) (CategoryTheory.Functor.comp G.op (CategoryTheory.sheafOver ℱ' X).val) (CategoryTheory.CoverDense.homOver α X) X a = CategoryTheory.CategoryStruct.comp a (α.app X)

def CategoryTheory.CoverDense.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} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) (X : A) : CategoryTheory.Functor.comp G.op (CategoryTheory.Functor.comp ℱ (CategoryTheory.coyoneda.obj (Opposite.op X))) ⟶ CategoryTheory.Functor.comp G.op (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.

@[simp]

theorem CategoryTheory.CoverDense.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} (α : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) (X : A) (X : Cᵒᵖ) : ∀ (a : (CategoryTheory.coyoneda.obj (Opposite.op X)).obj ((CategoryTheory.Functor.comp G.op ℱ'.val).obj X)), Cᵒᵖ.app CategoryTheory.Category.opposite (Type u_7) CategoryTheory.types (((CategoryTheory.whiskeringRight Cᵒᵖ A (Type u_7)).obj (CategoryTheory.coyoneda.obj (Opposite.op X))).obj (CategoryTheory.Functor.comp G.op ℱ'.val)) (((CategoryTheory.whiskeringRight Cᵒᵖ A (Type u_7)).obj (CategoryTheory.coyoneda.obj (Opposite.op X))).obj (CategoryTheory.Functor.comp G.op ℱ.val)) (CategoryTheory.CoverDense.isoOver α X).inv X a = CategoryTheory.CategoryStruct.comp a (α.inv.app X)

@[simp]

theorem CategoryTheory.CoverDense.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} (α : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) (X : A) (X : Cᵒᵖ) : ∀ (a : (CategoryTheory.coyoneda.obj (Opposite.op X)).obj ((CategoryTheory.Functor.comp G.op ℱ.val).obj X)), Cᵒᵖ.app CategoryTheory.Category.opposite (Type u_7) CategoryTheory.types (((CategoryTheory.whiskeringRight Cᵒᵖ A (Type u_7)).obj (CategoryTheory.coyoneda.obj (Opposite.op X))).obj (CategoryTheory.Functor.comp G.op ℱ.val)) (((CategoryTheory.whiskeringRight Cᵒᵖ A (Type u_7)).obj (CategoryTheory.coyoneda.obj (Opposite.op X))).obj (CategoryTheory.Functor.comp G.op ℱ'.val)) (CategoryTheory.CoverDense.isoOver α X).hom X a = CategoryTheory.CategoryStruct.comp a (α.hom.app X)

def CategoryTheory.CoverDense.isoOver {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} (α : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) (X : A) : CategoryTheory.Functor.comp G.op (CategoryTheory.sheafOver ℱ X).val ≅ CategoryTheory.Functor.comp G.op (CategoryTheory.sheafOver ℱ' X).val

(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.

theorem CategoryTheory.CoverDense.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 ∈ CategoryTheory.GrothendieckTopology.sieves K U) (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ℱ.val (CategoryTheory.coyoneda.obj (Opposite.op X))) T.arrows) (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) (t : (CategoryTheory.Functor.comp ℱ.val (CategoryTheory.coyoneda.obj (Opposite.op X))).obj (Opposite.op U)) (h : CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation x t) : t = CategoryTheory.Presieve.IsSheafFor.amalgamate (_ : CategoryTheory.Presieve.IsSheafFor (CategoryTheory.Functor.comp ℱ.val (CategoryTheory.coyoneda.obj (Opposite.op X))) T.arrows) x hx

noncomputable def CategoryTheory.CoverDense.Types.pushforwardFamily {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} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) {X : D} (x : ℱ.obj (Opposite.op X)) : CategoryTheory.Presieve.FamilyOfElements ℱ'.val (CategoryTheory.Presieve.coverByImage G 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.

@[simp]

theorem CategoryTheory.CoverDense.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} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) {X : D} (x : ℱ.obj (Opposite.op X)) : CategoryTheory.CoverDense.Types.pushforwardFamily α x = fun x x_1 hf => Dᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver ℱ'.val.toPrefunctor (G.op.obj (Opposite.op (Nonempty.some hf).1)) (Opposite.op x) (Nonempty.some hf).lift.op (Cᵒᵖ.app CategoryTheory.Category.opposite (Type v) CategoryTheory.types (CategoryTheory.Functor.comp G.op ℱ) (CategoryTheory.Functor.comp G.op ℱ'.val) α (Opposite.op (Nonempty.some hf).1) (Dᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver ℱ.toPrefunctor (Opposite.op X) (G.op.obj (Opposite.op (Nonempty.some hf).1)) (Nonempty.some hf).map.op x))

theorem CategoryTheory.CoverDense.Types.pushforwardFamily_compatible {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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) {X : D} (x : ℱ.obj (Opposite.op X)) : CategoryTheory.Presieve.FamilyOfElements.Compatible (CategoryTheory.CoverDense.Types.pushforwardFamily α x)

(Implementation). The pushforwardFamily defined is compatible.

noncomputable def CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) (X : D) : ℱ.obj (Opposite.op X) ⟶ ℱ'.val.obj (Opposite.op X)

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

@[simp]

theorem CategoryTheory.CoverDense.Types.pushforwardFamily_apply {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.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) {X : D} (x : ℱ.obj (Opposite.op X)) {Y : C} (f : G.obj Y ⟶ X) : CategoryTheory.CoverDense.Types.pushforwardFamily α x f (_ : CategoryTheory.Presieve.coverByImage G X f) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type v) CategoryTheory.types (CategoryTheory.Functor.comp G.op ℱ) (CategoryTheory.Functor.comp G.op ℱ'.val) α (Opposite.op Y) (Dᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver ℱ.toPrefunctor (Opposite.op X) (Opposite.op (G.obj Y)) f.op x)

@[simp]

theorem CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) {X : D} {Y : C} (f : Opposite.op X ⟶ Opposite.op (G.obj Y)) (x : ℱ.obj (Opposite.op X)) : Dᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver ℱ'.val.toPrefunctor (Opposite.op X) (Opposite.op (G.obj Y)) f (CategoryTheory.CoverDense.Types.appHom H α X x) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type v) CategoryTheory.types (CategoryTheory.Functor.comp G.op ℱ) (CategoryTheory.Functor.comp G.op ℱ'.val) α (Opposite.op Y) (Dᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver ℱ.toPrefunctor (Opposite.op X) (Opposite.op (G.obj Y)) f x)

@[simp]

theorem CategoryTheory.CoverDense.Types.appHom_valid_glue {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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) {X : D} {Y : C} (f : Opposite.op X ⟶ Opposite.op (G.obj Y)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CoverDense.Types.appHom H α X) (ℱ'.val.map f) = CategoryTheory.CategoryStruct.comp (ℱ.map f) (α.app (Opposite.op Y))

@[simp]

theorem CategoryTheory.CoverDense.Types.appIso_inv {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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) (X : D) : ∀ (a : ℱ'.val.obj (Opposite.op X)), Type v.inv CategoryTheory.types (ℱ.val.obj (Opposite.op X)) (ℱ'.val.obj (Opposite.op X)) (CategoryTheory.CoverDense.Types.appIso H i X) a = CategoryTheory.CoverDense.Types.appHom H i.inv X a

@[simp]

theorem CategoryTheory.CoverDense.Types.appIso_hom {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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) (X : D) : ∀ (a : ℱ.val.obj (Opposite.op X)), Type v.hom CategoryTheory.types (ℱ.val.obj (Opposite.op X)) (ℱ'.val.obj (Opposite.op X)) (CategoryTheory.CoverDense.Types.appIso H i X) a = CategoryTheory.CoverDense.Types.appHom H i.hom X a

noncomputable def CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.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).

@[simp]

theorem CategoryTheory.CoverDense.Types.presheafHom_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} {G : CategoryTheory.Functor C D} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) (X : Dᵒᵖ) : ∀ (a : ℱ.obj (Opposite.op X.unop)), Dᵒᵖ.app CategoryTheory.Category.opposite (Type v) CategoryTheory.types ℱ ℱ'.val (CategoryTheory.CoverDense.Types.presheafHom H α) X a = CategoryTheory.CoverDense.Types.appHom H α X.unop a

noncomputable def CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) : ℱ ⟶ ℱ'.val

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

@[simp]

theorem CategoryTheory.CoverDense.Types.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} {G : CategoryTheory.Functor C D} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) (X : Dᵒᵖ) : ∀ (a : ℱ.val.obj X), Dᵒᵖ.app CategoryTheory.Category.opposite (Type v) CategoryTheory.types ℱ.val ℱ'.val (CategoryTheory.CoverDense.Types.presheafIso H i).hom X a = CategoryTheory.CoverDense.Types.appHom H i.hom X.unop a

@[simp]

theorem CategoryTheory.CoverDense.Types.presheafIso_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} {G : CategoryTheory.Functor C D} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) (X : Dᵒᵖ) : ∀ (a : ℱ'.val.obj X), Dᵒᵖ.app CategoryTheory.Category.opposite (Type v) CategoryTheory.types ℱ'.val ℱ.val (CategoryTheory.CoverDense.Types.presheafIso H i).inv X a = CategoryTheory.CoverDense.Types.appHom H i.inv X.unop a

noncomputable def CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) : ℱ.val ≅ ℱ'.val

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

@[simp]

theorem CategoryTheory.CoverDense.Types.sheafIso_inv_val {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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) : (CategoryTheory.CoverDense.Types.sheafIso H i).inv.val = (CategoryTheory.CoverDense.Types.presheafIso H i).inv

@[simp]

theorem CategoryTheory.CoverDense.Types.sheafIso_hom_val {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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) : (CategoryTheory.CoverDense.Types.sheafIso H i).hom.val = (CategoryTheory.CoverDense.Types.presheafIso H i).hom

noncomputable def CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.SheafOfTypes K} {ℱ' : CategoryTheory.SheafOfTypes K} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) : ℱ ≅ ℱ'

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

@[simp]

theorem CategoryTheory.CoverDense.sheafCoyonedaHom_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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) (X : Aᵒᵖ) : (CategoryTheory.CoverDense.sheafCoyonedaHom H α).app X = CategoryTheory.CoverDense.Types.presheafHom H (CategoryTheory.CoverDense.homOver α X.unop)

noncomputable def CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) : CategoryTheory.Functor.comp CategoryTheory.coyoneda ((CategoryTheory.whiskeringLeft Dᵒᵖ A (Type u_7)).obj ℱ) ⟶ CategoryTheory.Functor.comp CategoryTheory.coyoneda ((CategoryTheory.whiskeringLeft Dᵒᵖ A (Type u_7)).obj ℱ'.val)

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

noncomputable def CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) : CategoryTheory.Functor.comp ℱ CategoryTheory.yoneda ⟶ CategoryTheory.Functor.comp ℱ'.val CategoryTheory.yoneda

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

noncomputable def CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) : ℱ ⟶ ℱ'.val

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

@[simp]

theorem CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) (X : Dᵒᵖ) : (CategoryTheory.CoverDense.presheafIso H i).hom.app X = CategoryTheory.yoneda.preimage ((CategoryTheory.CoverDense.sheafYonedaHom H i.hom).app X)

@[simp]

theorem CategoryTheory.CoverDense.presheafIso_inv {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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) : (CategoryTheory.CoverDense.presheafIso H i).inv = CategoryTheory.inv (CategoryTheory.CoverDense.sheafHom H i.hom)

noncomputable def CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) : ℱ.val ≅ ℱ'.val

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

@[simp]

theorem CategoryTheory.CoverDense.sheafIso_hom_val {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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) : (CategoryTheory.CoverDense.sheafIso H i).hom.val = (CategoryTheory.CoverDense.presheafIso H i).hom

@[simp]

theorem CategoryTheory.CoverDense.sheafIso_inv_val {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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) : (CategoryTheory.CoverDense.sheafIso H i).inv.val = (CategoryTheory.CoverDense.presheafIso H i).inv

noncomputable def CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (i : CategoryTheory.Functor.comp G.op ℱ.val ≅ CategoryTheory.Functor.comp G.op ℱ'.val) : ℱ ≅ ℱ'

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

theorem CategoryTheory.CoverDense.sheafHom_restrict_eq {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_7, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_5, u_4} A] {G : CategoryTheory.Functor C D} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) : CategoryTheory.whiskerLeft G.op (CategoryTheory.CoverDense.sheafHom H α) = α

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

theorem CategoryTheory.CoverDense.sheafHom_eq {C : Type u_1} [CategoryTheory.Category.{u_7, 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_5, u_4} A] {G : CategoryTheory.Functor C D} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : ℱ ⟶ ℱ'.val) : CategoryTheory.CoverDense.sheafHom H (CategoryTheory.whiskerLeft G.op α) = α

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

noncomputable def CategoryTheory.CoverDense.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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} : (CategoryTheory.Functor.comp G.op ℱ ⟶ CategoryTheory.Functor.comp G.op ℱ'.val) ≃ (ℱ ⟶ ℱ'.val)

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

theorem CategoryTheory.CoverDense.iso_of_restrict_iso {C : Type u_1} [CategoryTheory.Category.{u_7, u_1} C] {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] {G : CategoryTheory.Functor C D} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] {ℱ : CategoryTheory.Sheaf K A} {ℱ' : CategoryTheory.Sheaf K A} (α : ℱ ⟶ ℱ') (i : CategoryTheory.IsIso (CategoryTheory.whiskerLeft G.op α.val)) : CategoryTheory.IsIso α

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

theorem CategoryTheory.CoverDense.compatiblePreserving {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} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] [CategoryTheory.Faithful G] : CategoryTheory.CompatiblePreserving K G

A fully faithful cover-dense functor preserves compatible families.

noncomputable instance CategoryTheory.CoverDense.Sites.Pullback.full {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] (J : CategoryTheory.GrothendieckTopology C) {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] [CategoryTheory.Faithful G] (Hp : CategoryTheory.CoverPreserving J K G) : CategoryTheory.Full (CategoryTheory.Sites.pullback A (_ : CategoryTheory.CompatiblePreserving K G) Hp)

instance CategoryTheory.CoverDense.Sites.Pullback.faithful {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] (J : CategoryTheory.GrothendieckTopology C) {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {G : CategoryTheory.Functor C D} (H : CategoryTheory.CoverDense K G) [CategoryTheory.Full G] [CategoryTheory.Faithful G] (Hp : CategoryTheory.CoverPreserving J K G) : CategoryTheory.Faithful (CategoryTheory.Sites.pullback A (_ : CategoryTheory.CompatiblePreserving K G) Hp)

@[simp]

theorem CategoryTheory.CoverDense.sheafEquivOfCoverPreservingCoverLifting_inverse {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} [CategoryTheory.Full G] [CategoryTheory.Faithful G] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (Hd : CategoryTheory.CoverDense K G) (Hp : CategoryTheory.CoverPreserving J K G) (Hl : CategoryTheory.CoverLifting J K G) : (CategoryTheory.CoverDense.sheafEquivOfCoverPreservingCoverLifting Hd Hp Hl).inverse = CategoryTheory.Sites.pullback A (_ : CategoryTheory.CompatiblePreserving K G) Hp

@[simp]

theorem CategoryTheory.CoverDense.sheafEquivOfCoverPreservingCoverLifting_functor {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} [CategoryTheory.Full G] [CategoryTheory.Faithful G] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (Hd : CategoryTheory.CoverDense K G) (Hp : CategoryTheory.CoverPreserving J K G) (Hl : CategoryTheory.CoverLifting J K G) : (CategoryTheory.CoverDense.sheafEquivOfCoverPreservingCoverLifting Hd Hp Hl).functor = CategoryTheory.Sites.copullback A Hl

noncomputable def CategoryTheory.CoverDense.sheafEquivOfCoverPreservingCoverLifting {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} [CategoryTheory.Full G] [CategoryTheory.Faithful G] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (Hd : CategoryTheory.CoverDense K G) (Hp : CategoryTheory.CoverPreserving J K G) (Hl : CategoryTheory.CoverLifting J K G) : CategoryTheory.Sheaf J A ≌ CategoryTheory.Sheaf K A

Given a functor between small sites that is cover-dense, cover-preserving, and cover-lifting, it induces an equivalence of category of sheaves valued in a complete category.

@[inline, reducible]

noncomputable abbrev CategoryTheory.CoverDense.sheafEquivOfCoverPreservingCoverLiftingSheafificationCompatibility {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} [CategoryTheory.Full G] [CategoryTheory.Faithful G] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (Hd : CategoryTheory.CoverDense K G) (Hp : CategoryTheory.CoverPreserving J K G) (Hl : CategoryTheory.CoverLifting J K G) [CategoryTheory.ConcreteCategory A] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget A)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget A)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ A] [(X : D) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover K X)ᵒᵖ (CategoryTheory.forget A)] [∀ (X : D), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover K X)ᵒᵖ A] : CategoryTheory.Functor.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op) (CategoryTheory.presheafToSheaf J A) ≅ CategoryTheory.Functor.comp (CategoryTheory.presheafToSheaf K A) (CategoryTheory.CoverDense.sheafEquivOfCoverPreservingCoverLifting Hd Hp Hl).inverse

The natural isomorphism exhibiting the compatibility of sheafEquivOfCoverPreservingCoverLifting with sheafification.