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

• CategoryTheory.Functor.IsCoverDense.Types.presheafHom: If G : C ⥤ (D, K) is locally-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.Functor.IsCoverDense.sheafIso: If ℱ above is a sheaf and α is an iso, then the result is also an iso.
• CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso: If G : C ⥤ (D, K) is locally-full and cover-dense, then given any sheaves ℱ, ℱ' on D, and a morphism α : ℱ ⟶ ℱ', then α is an iso if G ⋙ ℱ ⟶ G ⋙ ℱ' is iso.
• CategoryTheory.Functor.IsDenseSubsite: 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 iff the image of S in D is a cover.

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} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] (G : Functor C D) {V U : D} (f : V ⟶ U) : Type (max u_1 u_5)

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

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

@[simp]

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

def CategoryTheory.Presieve.coverByImage {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] (G : Functor C D) (U : D) : 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} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] (G : Functor C D) (U : D) : 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} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] (G : Functor C D) {X : D} {Y : C} (f : G.obj Y ⟶ X) : coverByImage G X f

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

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.

• is_cover (U : D) : Sieve.coverByImage G U ∈ K U

theorem CategoryTheory.Functor.is_cover_of_isCoverDense {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] (G : Functor C D) (K : GrothendieckTopology D) [G.IsCoverDense K] (U : D) : Sieve.coverByImage G U ∈ K U

theorem CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_mem {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] (G : Functor C D) (K : GrothendieckTopology D) (h : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ K B) : G.IsCoverDense K

theorem CategoryTheory.Functor.IsCoverDense.ext {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} (G : Functor C D) [G.IsCoverDense K] (ℱ : Sheaf K (Type u_7)) (X : D) {s 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

theorem CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {X : C} (T : ↑(K (G.obj X))) : Sieve.functorPushforward G (Sieve.functorPullback G ↑T) ∈ K (G.obj X)

def CategoryTheory.Functor.IsCoverDense.homOver {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) (X : A) : G.op.comp (ℱ.comp (coyoneda.obj (Opposite.op X))) ⟶ G.op.comp (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.Functor.IsCoverDense.homOver_app {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) (X : A) (X✝ : Cᵒᵖ) (a✝ : (coyoneda.obj (Opposite.op X)).obj ((G.op.comp ℱ).obj X✝)) : (homOver α X).app X✝ a✝ = CategoryStruct.comp a✝ (α.app X✝)

def CategoryTheory.Functor.IsCoverDense.isoOver {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} {ℱ ℱ' : Sheaf K A} (α : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val) (X : A) : G.op.comp (sheafOver ℱ X).val ≅ G.op.comp (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.

@[simp]

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

@[simp]

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

theorem CategoryTheory.Functor.IsCoverDense.sheaf_eq_amalgamation {D : Type u_2} [Category.{u_5, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_6, u_4} A] (ℱ : Sheaf K A) {X : A} {U : D} {T : Sieve U} (hT : T ∈ K U) (x : Presieve.FamilyOfElements (ℱ.val.comp (coyoneda.obj (Opposite.op X))) T.arrows) (hx : x.Compatible) (t : (ℱ.val.comp (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} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) [G.IsLocallyFull K] {X 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 {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) [G.IsLocallyFull K] {X Y : C} (i : G.obj X ⟶ G.obj Y) : CategoryStruct.comp (α.app (Opposite.op Y)) (ℱ'.val.map i.op) = CategoryStruct.comp (ℱ.map i.op) (α.app (Opposite.op X))

theorem CategoryTheory.Functor.IsCoverDense.Types.naturality_assoc {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) [G.IsLocallyFull K] {X Y : C} (i : G.obj X ⟶ G.obj Y) {Z : Type v} (h : ℱ'.val.obj (Opposite.op (G.obj X)) ⟶ Z) : CategoryStruct.comp (α.app (Opposite.op Y)) (CategoryStruct.comp (ℱ'.val.map i.op) h) = CategoryStruct.comp (ℱ.map i.op) (CategoryStruct.comp (α.app (Opposite.op X)) h)

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) {X : D} (x : ℱ.obj (Opposite.op X)) : Presieve.FamilyOfElements ℱ'.val (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.Functor.IsCoverDense.Types.pushforwardFamily_def {C : Type u_1} [Category.{u_6, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) {X : D} (x : ℱ.obj (Opposite.op X)) : pushforwardFamily α x = fun (x_1 : D) (x_2 : x_1 ⟶ X) (hf : 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} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) [G.IsLocallyFull K] {X : D} (x : ℱ.obj (Opposite.op X)) {Y : C} (f : G.obj Y ⟶ X) : pushforwardFamily α x f ⋯ = α.app (Opposite.op Y) (ℱ.map f.op x)

theorem CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible {C : Type u_1} [Category.{u_6, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) [G.IsCoverDense K] [G.IsLocallyFull K] {X : D} (x : ℱ.obj (Opposite.op X)) : (pushforwardFamily α x).Compatible

(Implementation). The pushforwardFamily defined is compatible.

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.appHom {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : 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.

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.Types.appHom_restrict {C : Type u_1} [Category.{u_6, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : 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 (appHom α X x) = α.app (Opposite.op Y) (ℱ.map f x)

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.Types.appHom_valid_glue {C : Type u_1} [Category.{u_6, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : 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)) : CategoryStruct.comp (appHom α X) (ℱ'.val.map f) = CategoryStruct.comp (ℱ.map f) (α.app (Opposite.op Y))

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.appIso {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (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).

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.Types.appIso_inv {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val) (X : D) (a✝ : ℱ'.val.obj (Opposite.op X)) : (appIso i X).inv a✝ = appHom i.inv X a✝

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.Types.appIso_hom {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val) (X : D) (a✝ : ℱ.val.obj (Opposite.op X)) : (appIso i X).hom a✝ = appHom i.hom X a✝

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.presheafHom {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} [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.

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.Types.presheafHom_app {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} [G.IsCoverDense K] [G.IsLocallyFull K] (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) (X : Dᵒᵖ) (a✝ : ℱ.obj (Opposite.op (Opposite.unop X))) : (presheafHom α).app X a✝ = appHom α (Opposite.unop X) a✝

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.presheafIso {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (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.

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.Types.presheafIso_hom_app {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val) (X : Dᵒᵖ) (a✝ : ℱ.val.obj X) : (presheafIso i).hom.app X a✝ = appHom i.hom (Opposite.unop X) a✝

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.Types.presheafIso_inv_app {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val) (X : Dᵒᵖ) (a✝ : ℱ'.val.obj X) : (presheafIso i).inv.app X a✝ = appHom i.inv (Opposite.unop X) a✝

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.sheafIso {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (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.

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.Types.sheafIso_inv_val {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val) : (sheafIso i).inv.val = (presheafIso i).inv

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.Types.sheafIso_hom_val {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val) : (sheafIso i).hom.val = (presheafIso i).hom

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

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

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom_app {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) (X : Aᵒᵖ) : (sheafCoyonedaHom α).app X = Types.presheafHom (homOver α (Opposite.unop X))

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

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

noncomputable def CategoryTheory.Functor.IsCoverDense.sheafHom {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : 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.

noncomputable def CategoryTheory.Functor.IsCoverDense.presheafIso {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : 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.

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.presheafIso_inv {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val) : (presheafIso i).inv = CategoryTheory.inv (sheafHom i.hom)

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.presheafIso_hom_app {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val) (X : Dᵒᵖ) : (presheafIso i).hom.app X = yoneda.preimage ((sheafYonedaHom i.hom).app X)

noncomputable def CategoryTheory.Functor.IsCoverDense.sheafIso {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : 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.

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.sheafIso_inv_val {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val) : (sheafIso i).inv.val = (presheafIso i).inv

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.sheafIso_hom_val {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val) : (sheafIso i).hom.val = (presheafIso i).hom

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

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

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

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} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_7, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : 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.

theorem CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso {C : Type u_1} [Category.{u_7, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{u_6, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (α : ℱ ⟶ ℱ') (i : IsIso (G.op.whiskerLeft α.val)) : IsIso α

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.

theorem CategoryTheory.Functor.IsCoverDense.compatiblePreserving {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (K : GrothendieckTopology D) (G : Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K] : CompatiblePreserving K G

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

theorem CategoryTheory.Functor.IsCoverDense.isContinuous {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K] (Hp : CoverPreserving J K G) : G.IsContinuous J K

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

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

theorem CategoryTheory.Functor.whiskerLeft_obj_map_bijective_of_isCoverDense {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (K : GrothendieckTopology D) (G : Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] {A : Type u_4} [Category.{u_7, u_4} A] (P Q : Functor Dᵒᵖ A) (hQ : Presheaf.IsSheaf K Q) : Function.Bijective ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map

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

class CategoryTheory.Functor.IsDenseSubsite {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) : Prop

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.

• isCoverDense' : G.IsCoverDense K
• isLocallyFull' : G.IsLocallyFull K
• isLocallyFaithful' : G.IsLocallyFaithful K
• functorPushforward_mem_iff {X : C} {S : Sieve X} : Sieve.functorPushforward G S ∈ K (G.obj X) ↔ S ∈ J X

theorem CategoryTheory.Functor.functorPushforward_mem_iff {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) {X : C} {S : Sieve X} [IsDenseSubsite J K G] : Sieve.functorPushforward G S ∈ K (G.obj X) ↔ S ∈ J X

theorem CategoryTheory.Functor.IsDenseSubsite.isCoverDense {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [IsDenseSubsite J K G] : G.IsCoverDense K

theorem CategoryTheory.Functor.IsDenseSubsite.isLocallyFull {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [IsDenseSubsite J K G] : G.IsLocallyFull K

theorem CategoryTheory.Functor.IsDenseSubsite.isLocallyFaithful {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [IsDenseSubsite J K G] : G.IsLocallyFaithful K

theorem CategoryTheory.Functor.IsDenseSubsite.coverPreserving {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [IsDenseSubsite J K G] : CoverPreserving J K G

@[instance 900]

instance CategoryTheory.Functor.IsDenseSubsite.instIsContinuous {C : Type u_1} [Category.{u_6, u_1} C] {D : Type u_2} [Category.{u_7, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [IsDenseSubsite J K G] : G.IsContinuous J K

@[instance 900]

instance CategoryTheory.Functor.IsDenseSubsite.instIsCocontinuous {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [IsDenseSubsite J K G] : G.IsCocontinuous J K

instance CategoryTheory.Functor.IsDenseSubsite.full_sheafPushforwardContinuous {C : Type u_1} [Category.{u_7, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type u_4} [Category.{u_5, u_4} A] (G : Functor C D) [IsDenseSubsite J K G] : (G.sheafPushforwardContinuous A J K).Full

instance CategoryTheory.Functor.IsDenseSubsite.faithful_sheafPushforwardContinuous {C : Type u_1} [Category.{u_7, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type u_4} [Category.{u_5, u_4} A] (G : Functor C D) [IsDenseSubsite J K G] : (G.sheafPushforwardContinuous A J K).Faithful

theorem CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem {C : Type u_1} [Category.{u_6, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [IsDenseSubsite J K G] {U V : C} (f : G.obj U ⟶ G.obj V) : G.imageSieve f ∈ J U

theorem CategoryTheory.Functor.IsDenseSubsite.equalizer_mem {C : Type u_1} [Category.{u_5, u_1} C] {D : Type u_2} [Category.{u_6, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [IsDenseSubsite J K G] {U V : C} (f₁ f₂ : U ⟶ V) (e : G.map f₁ = G.map f₂) : Sieve.equalizer f₁ f₂ ∈ J U