# mathlibdocumentation

category_theory.sites.dense_subsite

# Dense subsites #

We define cover_dense 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 #

• category_theory.cover_dense.presheaf_hom: 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 ℱ ⟶ ℱ'.
• category_theory.cover_dense.sheaf_iso: If ℱ above is a sheaf and α is an iso, then the result is also an iso.
• category_theory.cover_dense.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.
• category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting: 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 #

@[nolint]
structure category_theory.presieve.cover_by_image_structure {C : Type u_1} {D : Type u_3} (G : C D) {V U : D} (f : V U) :
Type (max u_1 u_4)

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

Instances for category_theory.presieve.cover_by_image_structure
• category_theory.presieve.cover_by_image_structure.has_sizeof_inst
@[simp]
theorem category_theory.presieve.cover_by_image_structure.fac {C : Type u_1} {D : Type u_3} {G : C D} {V U : D} {f : V U}  :
self.lift self.map = f
@[simp]
theorem category_theory.presieve.cover_by_image_structure.fac_assoc {C : Type u_1} {D : Type u_3} {G : C D} {V U : D} {f : V U} {X' : D} (f' : U X') :
self.lift self.map f' = f f'
def category_theory.presieve.cover_by_image {C : Type u_1} {D : Type u_3} (G : C D) (U : D) :

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

Equations
• = λ (Y : D) (f : Y U),
def category_theory.sieve.cover_by_image {C : Type u_1} {D : Type u_3} (G : C D) (U : D) :

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

Equations
theorem category_theory.presieve.in_cover_by_image {C : Type u_1} {D : Type u_3} (G : C D) {X : D} {Y : C} (f : G.obj Y X) :
structure category_theory.cover_dense {C : Type u_1} {D : Type u_3} (G : C D) :
Prop
• is_cover : ∀ (U : D),

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

theorem category_theory.cover_dense.ext {C : Type u_1} {D : Type u_3} {G : C D} (H : G) (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 category_theory.cover_dense.functor_pullback_pushforward_covering {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {X : C} (T : (K (G.obj X))) :
@[simp]
theorem category_theory.cover_dense.hom_over_app {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} {ℱ : Dᵒᵖ A} {ℱ' : A} (α : G.op G.op ℱ'.val) (X : A) (X_1 : Cᵒᵖ) (ᾰ : ((G.op ℱ).obj X_1)) :
X_1 = α.app X_1
def category_theory.cover_dense.hom_over {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} {ℱ : Dᵒᵖ A} {ℱ' : A} (α : G.op G.op ℱ'.val) (X : A) :

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

Equations
def category_theory.cover_dense.iso_over {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} {ℱ ℱ' : A} (α : G.op ℱ.val G.op ℱ'.val) (X : A) :

(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
@[simp]
theorem category_theory.cover_dense.iso_over_hom_app {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} {ℱ ℱ' : A} (α : G.op ℱ.val G.op ℱ'.val) (X : A) (X_1 : Cᵒᵖ) (ᾰ : ((G.op ℱ.val).obj X_1)) :
X_1 = α.hom.app X_1
@[simp]
theorem category_theory.cover_dense.iso_over_inv_app {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} {ℱ ℱ' : A} (α : G.op ℱ.val G.op ℱ'.val) (X : A) (X_1 : Cᵒᵖ) (ᾰ : ((G.op ℱ'.val).obj X_1)) :
X_1 = α.inv.app X_1
theorem category_theory.cover_dense.sheaf_eq_amalgamation {D : Type u_3} {A : Type u_7} (ℱ : A) {X : A} {U : D} {T : category_theory.sieve U} (hT : T K U) (hx : x.compatible) (t : .obj (opposite.op U)) (h : x.is_amalgamation t) :
t = _.amalgamate x hx
@[simp, nolint]
noncomputable def category_theory.cover_dense.types.pushforward_family {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ : Dᵒᵖ Type v} {ℱ' : category_theory.SheafOfTypes K} (α : G.op G.op ℱ'.val) {X : D} (x : ℱ.obj (opposite.op X)) :

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

Equations
theorem category_theory.cover_dense.types.pushforward_family_compatible {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ : Dᵒᵖ Type v} {ℱ' : category_theory.SheafOfTypes K} (α : G.op G.op ℱ'.val) {X : D} (x : ℱ.obj (opposite.op X)) :

(Implementation). The pushforward_family defined is compatible.

noncomputable def category_theory.cover_dense.types.app_hom {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ : Dᵒᵖ Type v} {ℱ' : category_theory.SheafOfTypes K} (α : G.op G.op ℱ'.val) (X : D) :

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

Equations
@[simp]
theorem category_theory.cover_dense.types.pushforward_family_apply {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ : Dᵒᵖ Type v} {ℱ' : category_theory.SheafOfTypes K} (α : G.op G.op ℱ'.val) {X : D} (x : ℱ.obj (opposite.op X)) {Y : C} (f : G.obj Y X) :
= α.app (opposite.op Y) (ℱ.map f.op x)
@[simp]
theorem category_theory.cover_dense.types.app_hom_restrict {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ : Dᵒᵖ Type v} {ℱ' : category_theory.SheafOfTypes K} (α : G.op G.op ℱ'.val) {X : D} {Y : C} (f : opposite.op (G.obj Y)) (x : ℱ.obj (opposite.op X)) :
ℱ'.val.map f = α.app (opposite.op Y) (ℱ.map f x)
@[simp]
theorem category_theory.cover_dense.types.app_hom_valid_glue {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ : Dᵒᵖ Type v} {ℱ' : category_theory.SheafOfTypes K} (α : G.op G.op ℱ'.val) {X : D} {Y : C} (f : opposite.op (G.obj Y)) :
ℱ'.val.map f = ℱ.map f α.app (opposite.op Y)
@[simp]
theorem category_theory.cover_dense.types.app_iso_inv {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ ℱ' : category_theory.SheafOfTypes K} (i : G.op ℱ.val G.op ℱ'.val) (X : D) (ᾰ : ℱ'.val.obj (opposite.op X)) :
@[simp]
theorem category_theory.cover_dense.types.app_iso_hom {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ ℱ' : category_theory.SheafOfTypes K} (i : G.op ℱ.val G.op ℱ'.val) (X : D) (ᾰ : ℱ.val.obj (opposite.op X)) :
noncomputable def category_theory.cover_dense.types.app_iso {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ ℱ' : category_theory.SheafOfTypes K} (i : G.op ℱ.val G.op ℱ'.val) (X : D) :

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

Equations
@[simp]
theorem category_theory.cover_dense.types.presheaf_hom_app {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ : Dᵒᵖ Type v} {ℱ' : category_theory.SheafOfTypes K} (α : G.op G.op ℱ'.val) (X : Dᵒᵖ) (ᾰ : ℱ.obj (opposite.op (opposite.unop X))) :
noncomputable def category_theory.cover_dense.types.presheaf_hom {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ : Dᵒᵖ Type v} {ℱ' : category_theory.SheafOfTypes K} (α : G.op G.op ℱ'.val) :
ℱ'.val

Given an 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.

Equations
@[simp]
theorem category_theory.cover_dense.types.presheaf_iso_inv_app {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ ℱ' : category_theory.SheafOfTypes K} (i : G.op ℱ.val G.op ℱ'.val) (X : Dᵒᵖ) (ᾰ : ℱ'.val.obj X) :
@[simp]
theorem category_theory.cover_dense.types.presheaf_iso_hom_app {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ ℱ' : category_theory.SheafOfTypes K} (i : G.op ℱ.val G.op ℱ'.val) (X : Dᵒᵖ) (ᾰ : ℱ.val.obj X) :
noncomputable def category_theory.cover_dense.types.presheaf_iso {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ ℱ' : category_theory.SheafOfTypes K} (i : G.op ℱ.val G.op ℱ'.val) :
ℱ.val ℱ'.val

Given an 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.

Equations
noncomputable def category_theory.cover_dense.types.sheaf_iso {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ ℱ' : category_theory.SheafOfTypes K} (i : G.op ℱ.val G.op ℱ'.val) :
ℱ'

Given an 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.

Equations
@[simp]
theorem category_theory.cover_dense.types.sheaf_iso_inv_val {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ ℱ' : category_theory.SheafOfTypes K} (i : G.op ℱ.val G.op ℱ'.val) :
@[simp]
theorem category_theory.cover_dense.types.sheaf_iso_hom_val {C : Type u_1} {D : Type u_3} {G : C D} (H : G) {ℱ ℱ' : category_theory.SheafOfTypes K} (i : G.op ℱ.val G.op ℱ'.val) :
@[simp]
theorem category_theory.cover_dense.sheaf_coyoneda_hom_app {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ : Dᵒᵖ A} {ℱ' : A} (α : G.op G.op ℱ'.val) (X : Aᵒᵖ) :
noncomputable def category_theory.cover_dense.sheaf_coyoneda_hom {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ : Dᵒᵖ A} {ℱ' : A} (α : G.op G.op ℱ'.val) :

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

Equations
noncomputable def category_theory.cover_dense.sheaf_yoneda_hom {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ : Dᵒᵖ A} {ℱ' : A} (α : G.op G.op ℱ'.val) :

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

Equations
noncomputable def category_theory.cover_dense.sheaf_hom {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ : Dᵒᵖ A} {ℱ' : A} (α : G.op G.op ℱ'.val) :
ℱ'.val

Given an 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.

Equations
noncomputable def category_theory.cover_dense.presheaf_iso {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ ℱ' : A} (i : G.op ℱ.val G.op ℱ'.val) :
ℱ.val ℱ'.val

Given an 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.

Equations
@[simp]
theorem category_theory.cover_dense.presheaf_iso_inv {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ ℱ' : A} (i : G.op ℱ.val G.op ℱ'.val) :
@[simp]
theorem category_theory.cover_dense.presheaf_iso_hom_app {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ ℱ' : A} (i : G.op ℱ.val G.op ℱ'.val) (X : Dᵒᵖ) :
noncomputable def category_theory.cover_dense.sheaf_iso {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ ℱ' : A} (i : G.op ℱ.val G.op ℱ'.val) :
ℱ'

Given an 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.

Equations
@[simp]
theorem category_theory.cover_dense.sheaf_iso_inv_val {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ ℱ' : A} (i : G.op ℱ.val G.op ℱ'.val) :
@[simp]
theorem category_theory.cover_dense.sheaf_iso_hom_val {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ ℱ' : A} (i : G.op ℱ.val G.op ℱ'.val) :
theorem category_theory.cover_dense.sheaf_hom_restrict_eq {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ : Dᵒᵖ A} {ℱ' : A} (α : G.op G.op ℱ'.val) :
= α

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

theorem category_theory.cover_dense.sheaf_hom_eq {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ : Dᵒᵖ A} {ℱ' : A} (α : ℱ ℱ'.val) :
= α

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

noncomputable def category_theory.cover_dense.restrict_hom_equiv_hom {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ : Dᵒᵖ A} {ℱ' : A} :
(G.op 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.

Equations
theorem category_theory.cover_dense.iso_of_restrict_iso {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) {ℱ ℱ' : A} (α : ℱ ℱ')  :

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 category_theory.cover_dense.compatible_preserving {C : Type u_1} {D : Type u_3} {G : C D} (H : G)  :

A fully faithful cover-dense functor preserves compatible families.

@[protected, instance]
noncomputable def category_theory.cover_dense.sites.pullback.full {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) (Hp : G) :
Equations
@[protected, instance]
def category_theory.cover_dense.sites.pullback.faithful {C : Type u_1} {D : Type u_3} {A : Type u_7} {G : C D} (H : G) (Hp : G) :
@[simp]
theorem category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting_functor {C D : Type u} {G : C D} {A : Type w} (Hd : G) (Hp : G) (Hl : G) :
@[simp]
theorem category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting_inverse {C D : Type u} {G : C D} {A : Type w} (Hd : G) (Hp : G) (Hl : G) :
noncomputable def category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting {C D : Type u} {G : C D} {A : Type w} (Hd : G) (Hp : G) (Hl : G) :

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.

Equations
• = (let α : := in .symm