mathlib documentation

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 #

References #

@[nolint]
structure category_theory.presieve.cover_by_image_structure {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] (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} [category_theory.category C] {D : Type u_3} [category_theory.category D] {G : C D} {V U : D} {f : V U} (self : category_theory.presieve.cover_by_image_structure G f) :
self.lift self.map = f
@[simp]
theorem category_theory.presieve.cover_by_image_structure.fac_assoc {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {G : C D} {V U : D} {f : V U} (self : category_theory.presieve.cover_by_image_structure G f) {X' : D} (f' : U X') :
self.lift self.map f' = f f'

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

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} [category_theory.category C] {D : Type u_3} [category_theory.category D] (G : C D) {X : D} {Y : C} (f : G.obj Y X) :
structure category_theory.cover_dense {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] (K : category_theory.grothendieck_topology D) (G : C D) :
Prop

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} [category_theory.category C] {D : Type u_3} [category_theory.category D] {K : category_theory.grothendieck_topology D} {G : C D} (H : category_theory.cover_dense K G) (ℱ : category_theory.SheafOfTypes K) (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
@[simp]
theorem category_theory.cover_dense.hom_over_app {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {K : category_theory.grothendieck_topology D} {A : Type u_7} [category_theory.category A] {G : C D} {ℱ : Dᵒᵖ A} {ℱ' : category_theory.Sheaf K A} (α : G.op G.op ℱ'.val) (X : A) (X_1 : Cᵒᵖ) (ᾰ : (category_theory.coyoneda.obj (opposite.op X)).obj ((G.op ℱ).obj X_1)) :

(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

(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} [category_theory.category C] {D : Type u_3} [category_theory.category D] {K : category_theory.grothendieck_topology D} {A : Type u_7} [category_theory.category A] {G : C D} {ℱ ℱ' : category_theory.Sheaf K A} (α : G.op ℱ.val G.op ℱ'.val) (X : A) (X_1 : Cᵒᵖ) (ᾰ : (category_theory.coyoneda.obj (opposite.op X)).obj ((G.op ℱ.val).obj X_1)) :
@[simp]
theorem category_theory.cover_dense.iso_over_inv_app {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {K : category_theory.grothendieck_topology D} {A : Type u_7} [category_theory.category A] {G : C D} {ℱ ℱ' : category_theory.Sheaf K A} (α : G.op ℱ.val G.op ℱ'.val) (X : A) (X_1 : Cᵒᵖ) (ᾰ : (category_theory.coyoneda.obj (opposite.op X)).obj ((G.op ℱ'.val).obj X_1)) :
@[simp, nolint]

(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

(Implementation). The pushforward_family defined is compatible.

noncomputable def category_theory.cover_dense.types.app_hom {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {K : category_theory.grothendieck_topology D} {G : C D} (H : category_theory.cover_dense K G) [category_theory.full 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]
@[simp]
theorem category_theory.cover_dense.types.app_hom_restrict {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {K : category_theory.grothendieck_topology D} {G : C D} (H : category_theory.cover_dense K G) [category_theory.full G] {ℱ : Dᵒᵖ Type v} {ℱ' : category_theory.SheafOfTypes K} (α : G.op G.op ℱ'.val) {X : D} {Y : C} (f : opposite.op X opposite.op (G.obj Y)) (x : ℱ.obj (opposite.op X)) :

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

Equations
noncomputable def category_theory.cover_dense.types.presheaf_hom {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {K : category_theory.grothendieck_topology D} {G : C D} (H : category_theory.cover_dense K G) [category_theory.full 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

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

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

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

Equations

(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} [category_theory.category C] {D : Type u_3} [category_theory.category D] {K : category_theory.grothendieck_topology D} {A : Type u_7} [category_theory.category A] {G : C D} (H : category_theory.cover_dense K G) [category_theory.full G] {ℱ : Dᵒᵖ A} {ℱ' : category_theory.Sheaf K 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} [category_theory.category C] {D : Type u_3} [category_theory.category D] {K : category_theory.grothendieck_topology D} {A : Type u_7} [category_theory.category A] {G : C D} (H : category_theory.cover_dense K G) [category_theory.full G] {ℱ ℱ' : category_theory.Sheaf K 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
noncomputable def category_theory.cover_dense.sheaf_iso {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {K : category_theory.grothendieck_topology D} {A : Type u_7} [category_theory.category A] {G : C D} (H : category_theory.cover_dense K G) [category_theory.full G] {ℱ ℱ' : category_theory.Sheaf K 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

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

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

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

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.

A fully faithful cover-dense functor preserves compatible families.