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

• [Joh02]: 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 C] {D : Type u_2} [Category D] (G : Functor C D) {V U : D} (f : Quiver.Hom 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 : Quiver.Hom V (G.obj self.obj)
• map : Quiver.Hom (G.obj self.obj) U
• fac : Eq (CategoryStruct.comp self.lift self.map) f

theorem CategoryTheory.Presieve.CoverByImageStructure.fac_assoc {C : Type u_1} [Category C] {D : Type u_2} [Category D] {G : Functor C D} {V U : D} {f : Quiver.Hom V U} (self : CoverByImageStructure G f) {Z : D} (h : Quiver.Hom U Z) : Eq (CategoryStruct.comp self.lift (CategoryStruct.comp self.map h)) (CategoryStruct.comp f h)

def CategoryTheory.Presieve.coverByImage {C : Type u_1} [Category C] {D : Type u_2} [Category 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.

Equations

• Eq (CategoryTheory.Presieve.coverByImage G U f) (Nonempty (CategoryTheory.Presieve.CoverByImageStructure G f))

def CategoryTheory.Sieve.coverByImage {C : Type u_1} [Category C] {D : Type u_2} [Category 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.

Equations

• Eq (CategoryTheory.Sieve.coverByImage G U) { arrows := CategoryTheory.Presieve.coverByImage G U, downward_closed := ⋯ }

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

structure CategoryTheory.Functor.IsCoverDense {C : Type u_1} [Category C] {D : Type u_2} [Category 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) : Membership.mem (DFunLike.coe K U) (Sieve.coverByImage G U)

theorem CategoryTheory.Functor.is_cover_of_isCoverDense {C : Type u_1} [Category C] {D : Type u_2} [Category D] (G : Functor C D) (K : GrothendieckTopology D) [G.IsCoverDense K] (U : D) : Membership.mem (DFunLike.coe K U) (Sieve.coverByImage G U)

theorem CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_mem {C : Type u_1} [Category C] {D : Type u_2} [Category D] (G : Functor C D) (K : GrothendieckTopology D) (h : ∀ (B : D), Exists fun (X : C) => Exists fun (f : Quiver.Hom (G.obj X) B) => Membership.mem (DFunLike.coe K B) (Sieve.generate (Presieve.singleton f))) : G.IsCoverDense K

theorem CategoryTheory.Functor.IsCoverDense.ext {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} (G : Functor C D) [G.IsCoverDense K] (ℱ : Sheaf K (Type u_7)) (X : D) {s t : ℱ.val.obj { unop := X }} (h : ∀ ⦃Y : C⦄ (f : Quiver.Hom (G.obj Y) X), Eq (ℱ.val.map f.op s) (ℱ.val.map f.op t)) : Eq s t

theorem CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {X : C} (T : (DFunLike.coe K (G.obj X)).Elem) : Membership.mem (DFunLike.coe K (G.obj X)) (Sieve.functorPushforward G (Sieve.functorPullback G T.val))

def CategoryTheory.Functor.IsCoverDense.homOver {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] {G : Functor C D} {ℱ : Functor (Opposite D) A} {ℱ' : Sheaf K A} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) (X : A) : Quiver.Hom (G.op.comp (ℱ.comp (coyoneda.obj { unop := 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.

Equations

• Eq (CategoryTheory.Functor.IsCoverDense.homOver α X) (CategoryTheory.whiskerRight α (CategoryTheory.coyoneda.obj { unop := X }))

theorem CategoryTheory.Functor.IsCoverDense.homOver_app {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] {G : Functor C D} {ℱ : Functor (Opposite D) A} {ℱ' : Sheaf K A} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) (X : A) (X✝ : Opposite C) (a✝ : (coyoneda.obj { unop := X }).obj ((G.op.comp ℱ).obj X✝)) : Eq ((homOver α X).app X✝ a✝) (CategoryStruct.comp a✝ (α.app X✝))

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

Equations

• Eq (CategoryTheory.Functor.IsCoverDense.isoOver α X) (CategoryTheory.isoWhiskerRight α (CategoryTheory.coyoneda.obj { unop := X }))

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

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

theorem CategoryTheory.Functor.IsCoverDense.sheaf_eq_amalgamation {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] (ℱ : Sheaf K A) {X : A} {U : D} {T : Sieve U} (hT : Membership.mem (DFunLike.coe K U) T) (x : Presieve.FamilyOfElements (ℱ.val.comp (coyoneda.obj { unop := X })) T.arrows) (hx : x.Compatible) (t : (ℱ.val.comp (coyoneda.obj { unop := X })).obj { unop := U }) (h : x.IsAmalgamation t) : Eq t (⋯.amalgamate x hx)

theorem CategoryTheory.Functor.IsCoverDense.Types.naturality_apply {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor (Opposite D) (Type v)} {ℱ' : Sheaf K (Type v)} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) [G.IsLocallyFull K] {X Y : C} (i : Quiver.Hom (G.obj X) (G.obj Y)) (x : (G.op.comp ℱ).obj { unop := Y }) : Eq (ℱ'.val.map i.op (α.app { unop := Y } x)) (α.app { unop := X } (ℱ.map i.op x))

theorem CategoryTheory.Functor.IsCoverDense.Types.naturality {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor (Opposite D) (Type v)} {ℱ' : Sheaf K (Type v)} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) [G.IsLocallyFull K] {X Y : C} (i : Quiver.Hom (G.obj X) (G.obj Y)) : Eq (CategoryStruct.comp (α.app { unop := Y }) (ℱ'.val.map i.op)) (CategoryStruct.comp (ℱ.map i.op) (α.app { unop := X }))

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

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor (Opposite D) (Type v)} {ℱ' : Sheaf K (Type v)} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) {X : D} (x : ℱ.obj { unop := 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.

Equations

• Eq (CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x x✝ hf) (ℱ'.val.map (Nonempty.some hf).lift.op (α.app { unop := (Nonempty.some hf).1 } (ℱ.map (Nonempty.some hf).map.op x)))

theorem CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_def {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor (Opposite D) (Type v)} {ℱ' : Sheaf K (Type v)} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) {X : D} (x : ℱ.obj { unop := X }) : Eq (pushforwardFamily α x) fun (x_1 : D) (x_2 : Quiver.Hom x_1 X) (hf : Presieve.coverByImage G X x_2) => ℱ'.val.map (Nonempty.some hf).lift.op (α.app { unop := (Nonempty.some hf).1 } (ℱ.map (Nonempty.some hf).map.op x))

theorem CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_apply {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor (Opposite D) (Type v)} {ℱ' : Sheaf K (Type v)} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) [G.IsLocallyFull K] {X : D} (x : ℱ.obj { unop := X }) {Y : C} (f : Quiver.Hom (G.obj Y) X) : Eq (pushforwardFamily α x f ⋯) (α.app { unop := Y } (ℱ.map f.op x))

theorem CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor (Opposite D) (Type v)} {ℱ' : Sheaf K (Type v)} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) [G.IsCoverDense K] [G.IsLocallyFull K] {X : D} (x : ℱ.obj { unop := X }) : (pushforwardFamily α x).Compatible

(Implementation). The pushforwardFamily defined is compatible.

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.appHom {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor (Opposite D) (Type v)} {ℱ' : Sheaf K (Type v)} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) [G.IsCoverDense K] [G.IsLocallyFull K] (X : D) : Quiver.Hom (ℱ.obj { unop := X }) (ℱ'.val.obj { unop := X })

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

Equations

• Eq (CategoryTheory.Functor.IsCoverDense.Types.appHom α X x) (⋯.amalgamate (CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x) ⋯)

theorem CategoryTheory.Functor.IsCoverDense.Types.appHom_restrict {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor (Opposite D) (Type v)} {ℱ' : Sheaf K (Type v)} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) [G.IsCoverDense K] [G.IsLocallyFull K] {X : D} {Y : C} (f : Quiver.Hom { unop := X } { unop := G.obj Y }) (x : ℱ.obj { unop := X }) : Eq (ℱ'.val.map f (appHom α X x)) (α.app { unop := Y } (ℱ.map f x))

theorem CategoryTheory.Functor.IsCoverDense.Types.appHom_valid_glue {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor (Opposite D) (Type v)} {ℱ' : Sheaf K (Type v)} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) [G.IsCoverDense K] [G.IsLocallyFull K] {X : D} {Y : C} (f : Quiver.Hom { unop := X } { unop := G.obj Y }) : Eq (CategoryStruct.comp (appHom α X) (ℱ'.val.map f)) (CategoryStruct.comp (ℱ.map f) (α.app { unop := Y }))

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.appIso {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : Iso (G.op.comp ℱ.val) (G.op.comp ℱ'.val)) (X : D) : Iso (ℱ.val.obj { unop := X }) (ℱ'.val.obj { unop := 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.

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

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

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.presheafHom {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor (Opposite D) (Type v)} {ℱ' : Sheaf K (Type v)} [G.IsCoverDense K] [G.IsLocallyFull K] (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) : Quiver.Hom ℱ ℱ'.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

• Eq (CategoryTheory.Functor.IsCoverDense.Types.presheafHom α) { app := fun (X : Opposite D) => CategoryTheory.Functor.IsCoverDense.Types.appHom α (Opposite.unop X), naturality := ⋯ }

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

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

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

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

theorem CategoryTheory.Functor.IsCoverDense.Types.presheafIso_inv_app {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : Iso (G.op.comp ℱ.val) (G.op.comp ℱ'.val)) (X : Opposite D) (a✝ : ℱ'.val.obj X) : Eq ((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 C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : Iso (G.op.comp ℱ.val) (G.op.comp ℱ'.val)) : Iso ℱ ℱ'

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.

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

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

noncomputable def CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor (Opposite D) A} {ℱ' : Sheaf K A} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) : Quiver.Hom (coyoneda.comp ((whiskeringLeft (Opposite D) A (Type u_7)).obj ℱ)) (coyoneda.comp ((whiskeringLeft (Opposite 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.

theorem CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom_app {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor (Opposite D) A} {ℱ' : Sheaf K A} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) (X : Opposite A) : Eq ((sheafCoyonedaHom α).app X) (Types.presheafHom (homOver α (Opposite.unop X)))

noncomputable def CategoryTheory.Functor.IsCoverDense.sheafYonedaHom {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor (Opposite D) A} {ℱ' : Sheaf K A} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) : Quiver.Hom (ℱ.comp yoneda) (ℱ'.val.comp 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.

noncomputable def CategoryTheory.Functor.IsCoverDense.sheafHom {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor (Opposite D) A} {ℱ' : Sheaf K A} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) : Quiver.Hom ℱ ℱ'.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.

noncomputable def CategoryTheory.Functor.IsCoverDense.presheafIso {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (i : Iso (G.op.comp ℱ.val) (G.op.comp ℱ'.val)) : Iso ℱ.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

• Eq (CategoryTheory.Functor.IsCoverDense.presheafIso i) (CategoryTheory.asIso (CategoryTheory.Functor.IsCoverDense.sheafHom i.hom))

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

theorem CategoryTheory.Functor.IsCoverDense.presheafIso_hom_app {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (i : Iso (G.op.comp ℱ.val) (G.op.comp ℱ'.val)) (X : Opposite D) : Eq ((presheafIso i).hom.app X) (yoneda.preimage ((sheafYonedaHom i.hom).app X))

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

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.

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

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

theorem CategoryTheory.Functor.IsCoverDense.sheafHom_restrict_eq {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor (Opposite D) A} {ℱ' : Sheaf K A} (α : Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) : Eq (whiskerLeft G.op (sheafHom α)) α

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

theorem CategoryTheory.Functor.IsCoverDense.sheafHom_eq {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] (G : Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor (Opposite D) A} {ℱ' : Sheaf K A} (α : Quiver.Hom ℱ ℱ'.val) : Eq (sheafHom (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.Functor.IsCoverDense.restrictHomEquivHom {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor (Opposite D) A} {ℱ' : Sheaf K A} : Equiv (Quiver.Hom (G.op.comp ℱ) (G.op.comp ℱ'.val)) (Quiver.Hom ℱ ℱ'.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

• Eq CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom { toFun := CategoryTheory.Functor.IsCoverDense.sheafHom, invFun := CategoryTheory.whiskerLeft G.op, left_inv := ⋯, right_inv := ⋯ }

theorem CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso {C : Type u_1} [Category C] {D : Type u_2} [Category D] {K : GrothendieckTopology D} {A : Type u_4} [Category A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (α : Quiver.Hom ℱ ℱ') (i : IsIso (whiskerLeft G.op α.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 C] {D : Type u_2} [Category 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 C] {D : Type u_2} [Category 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

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

theorem CategoryTheory.Functor.IsCoverDense.faithful_sheafPushforwardContinuous {C : Type u_1} [Category C] {D : Type u_2} [Category D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type u_4} [Category 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 C] {D : Type u_2} [Category D] (K : GrothendieckTopology D) (G : Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] {A : Type u_4} [Category A] (P Q : Functor (Opposite D) A) (hQ : Presheaf.IsSheaf K Q) : Function.Bijective ((whiskeringLeft (Opposite C) (Opposite 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`.

structure CategoryTheory.Functor.IsDenseSubsite {C : Type u_1} [Category C] {D : Type u_2} [Category 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} : Iff (Membership.mem (DFunLike.coe K (G.obj X)) (Sieve.functorPushforward G S)) (Membership.mem (DFunLike.coe J X) S)

theorem CategoryTheory.Functor.functorPushforward_mem_iff {C : Type u_1} [Category C] {D : Type u_2} [Category D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) {X : C} {S : Sieve X} [IsDenseSubsite J K G] : Iff (Membership.mem (DFunLike.coe K (G.obj X)) (Sieve.functorPushforward G S)) (Membership.mem (DFunLike.coe J X) S)

theorem CategoryTheory.Functor.IsDenseSubsite.isCoverDense {C : Type u_1} [Category C] {D : Type u_2} [Category 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 C] {D : Type u_2} [Category 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 C] {D : Type u_2} [Category 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 C] {D : Type u_2} [Category D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [IsDenseSubsite J K G] : CoverPreserving J K G

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

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

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

theorem CategoryTheory.Functor.IsDenseSubsite.faithful_sheafPushforwardContinuous {C : Type u_1} [Category C] {D : Type u_2} [Category D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type u_4} [Category 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 C] {D : Type u_2} [Category D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [IsDenseSubsite J K G] {U V : C} (f : Quiver.Hom (G.obj U) (G.obj V)) : Membership.mem (DFunLike.coe J U) (G.imageSieve f)

theorem CategoryTheory.Functor.IsDenseSubsite.equalizer_mem {C : Type u_1} [Category C] {D : Type u_2} [Category D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) [IsDenseSubsite J K G] {U V : C} (f₁ f₂ : Quiver.Hom U V) (e : Eq (G.map f₁) (G.map f₂)) : Membership.mem (DFunLike.coe J U) (Sieve.equalizer f₁ f₂)