Dense subsites #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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: IfG : C ⥤ (D, K)is full and cover-dense, then given any presheafℱand sheafℱ'onD, 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: IfG : C ⥤ (D, K)is full and cover-dense, then given any sheavesℱ, ℱ'onD, and a morphismα : ℱ ⟶ ℱ', thenαis an iso ifG ⋙ ℱ ⟶ G ⋙ ℱ'is iso.category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting: IfG : (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 #
- [Joh02]: Sketches of an Elephant, ℱ. T. Johnstone: C2.2.
- https://ncatlab.org/nlab/show/dense+sub-site
- https://ncatlab.org/nlab/show/comparison+lemma
@[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)
- obj : C
- lift : V ⟶ G.obj self.obj
- map : G.obj self.obj ⟶ U
- fac' : self.lift ≫ self.map = f . "obviously"
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) :
@[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') :
def
category_theory.presieve.cover_by_image
{C : Type u_1}
[category_theory.category C]
{D : Type u_3}
[category_theory.category D]
(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
- category_theory.presieve.cover_by_image G U = λ (Y : D) (f : Y ⟶ U), nonempty (category_theory.presieve.cover_by_image_structure G f)
def
category_theory.sieve.cover_by_image
{C : Type u_1}
[category_theory.category C]
{D : Type u_3}
[category_theory.category D]
(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}
[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
- is_cover : ∀ (U : D), category_theory.sieve.cover_by_image G U ∈ ⇑K U
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
theorem
category_theory.cover_dense.functor_pullback_pushforward_covering
{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}
[category_theory.full G]
(H : category_theory.cover_dense K G)
{X : C}
(T : ↥(⇑K (G.obj X))) :
@[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)) :
(category_theory.cover_dense.hom_over α X).app X_1 ᾰ = ᾰ ≫ α.app X_1
def
category_theory.cover_dense.hom_over
{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) :
G.op ⋙ ℱ ⋙ category_theory.coyoneda.obj (opposite.op X) ⟶ G.op ⋙ (category_theory.sheaf_over ℱ' X).val
(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}
[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) :
G.op ⋙ (category_theory.sheaf_over ℱ X).val ≅ G.op ⋙ (category_theory.sheaf_over ℱ' 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
@[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)) :
theorem
category_theory.cover_dense.sheaf_eq_amalgamation
{D : Type u_3}
[category_theory.category D]
{K : category_theory.grothendieck_topology D}
{A : Type u_7}
[category_theory.category A]
(ℱ : category_theory.Sheaf K A)
{X : A}
{U : D}
{T : category_theory.sieve U}
(hT : T ∈ ⇑K U)
(x : category_theory.presieve.family_of_elements (ℱ.val ⋙ category_theory.coyoneda.obj (opposite.op X)) ⇑T)
(hx : x.compatible)
(t : (ℱ.val ⋙ category_theory.coyoneda.obj (opposite.op X)).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}
[category_theory.category C]
{D : Type u_3}
[category_theory.category D]
{K : category_theory.grothendieck_topology D}
{G : C ⥤ D}
[category_theory.full 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
- category_theory.cover_dense.types.pushforward_family α x = λ (Y : D) (f : Y ⟶ X) (hf : category_theory.presieve.cover_by_image G X f), ℱ'.val.map (nonempty.some hf).lift.op (α.app (opposite.op (nonempty.some hf).obj) (ℱ.map (nonempty.some hf).map.op x))
theorem
category_theory.cover_dense.types.pushforward_family_compatible
{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}
(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}
[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) :
ℱ.obj (opposite.op X) ⟶ ℱ'.val.obj (opposite.op X)
(Implementation). The morphism ℱ(X) ⟶ ℱ'(X) given by gluing the pushforward_family.
Equations
- category_theory.cover_dense.types.app_hom H α X = λ (x : ℱ.obj (opposite.op X)), _.amalgamate (category_theory.cover_dense.types.pushforward_family α x) _
@[simp]
theorem
category_theory.cover_dense.types.pushforward_family_apply
{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}
[category_theory.full 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) :
category_theory.cover_dense.types.pushforward_family α x f _ = α.app (opposite.op Y) (ℱ.map f.op x)
@[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)) :
ℱ'.val.map f (category_theory.cover_dense.types.app_hom H α X x) = α.app (opposite.op Y) (ℱ.map f x)
@[simp]
theorem
category_theory.cover_dense.types.app_hom_valid_glue
{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)) :
category_theory.cover_dense.types.app_hom H α X ≫ ℱ'.val.map f = ℱ.map f ≫ α.app (opposite.op Y)
@[simp]
theorem
category_theory.cover_dense.types.app_iso_inv
{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]
{ℱ ℱ' : 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}
[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]
{ℱ ℱ' : 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}
[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]
{ℱ ℱ' : category_theory.SheafOfTypes K}
(i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val)
(X : D) :
ℱ.val.obj (opposite.op X) ≅ ℱ'.val.obj (opposite.op X)
(Implementation). The maps given in app_iso is inverse to each other and gives a ℱ(X) ≅ ℱ'(X).
Equations
- category_theory.cover_dense.types.app_iso H i X = {hom := category_theory.cover_dense.types.app_hom H i.hom X, inv := category_theory.cover_dense.types.app_hom H i.inv X, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.cover_dense.types.presheaf_hom_app
{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ᵒᵖ)
(ᾰ : ℱ.obj (opposite.op (opposite.unop X))) :
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) :
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
- category_theory.cover_dense.types.presheaf_hom H α = {app := λ (X : Dᵒᵖ), category_theory.cover_dense.types.app_hom H α (opposite.unop X), naturality' := _}
@[simp]
theorem
category_theory.cover_dense.types.presheaf_iso_inv_app
{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]
{ℱ ℱ' : 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}
[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]
{ℱ ℱ' : 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}
[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]
{ℱ ℱ' : 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 presheaves.
Equations
noncomputable
def
category_theory.cover_dense.types.sheaf_iso
{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]
{ℱ ℱ' : 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
- category_theory.cover_dense.types.sheaf_iso H i = {hom := {val := (category_theory.cover_dense.types.presheaf_iso H i).hom}, inv := {val := (category_theory.cover_dense.types.presheaf_iso H i).inv}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.cover_dense.types.sheaf_iso_inv_val
{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]
{ℱ ℱ' : 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}
[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]
{ℱ ℱ' : 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}
[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)
(X : Aᵒᵖ) :
noncomputable
def
category_theory.cover_dense.sheaf_coyoneda_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) :
category_theory.coyoneda ⋙ (category_theory.whiskering_left Dᵒᵖ A (Type u_8)).obj ℱ ⟶ category_theory.coyoneda ⋙ (category_theory.whiskering_left Dᵒᵖ A (Type u_8)).obj ℱ'.val
(Implementation). The sheaf map given in types.sheaf_hom is natural in terms of X.
Equations
- H.sheaf_coyoneda_hom α = {app := λ (X : Aᵒᵖ), category_theory.cover_dense.types.presheaf_hom H (category_theory.cover_dense.hom_over α (opposite.unop X)), naturality' := _}
noncomputable
def
category_theory.cover_dense.sheaf_yoneda_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) :
(Implementation). sheaf_coyoneda_hom but the order of the arguments of the functor are swapped.
Equations
- H.sheaf_yoneda_hom α = let α_1 : category_theory.coyoneda ⋙ (category_theory.whiskering_left Dᵒᵖ A (Type u_8)).obj ℱ ⟶ category_theory.coyoneda ⋙ (category_theory.whiskering_left Dᵒᵖ A (Type u_8)).obj ℱ'.val := H.sheaf_coyoneda_hom α in {app := λ (U : Dᵒᵖ), {app := λ (X : Aᵒᵖ), (α_1.app X).app U, naturality' := _}, naturality' := _}
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) :
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
- H.sheaf_hom α = let α' : ℱ ⋙ category_theory.yoneda ⟶ ℱ'.val ⋙ category_theory.yoneda := H.sheaf_yoneda_hom α in {app := λ (X : Dᵒᵖ), category_theory.yoneda.preimage (α'.app X), naturality' := _}
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) :
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
- H.presheaf_iso i = category_theory.as_iso (H.sheaf_hom i.hom)
@[simp]
theorem
category_theory.cover_dense.presheaf_iso_inv
{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) :
(H.presheaf_iso i).inv = category_theory.inv (H.sheaf_hom i.hom)
@[simp]
theorem
category_theory.cover_dense.presheaf_iso_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}
(H : category_theory.cover_dense K G)
[category_theory.full G]
{ℱ ℱ' : category_theory.Sheaf K A}
(i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val)
(X : Dᵒᵖ) :
(H.presheaf_iso i).hom.app X = category_theory.yoneda.preimage ((H.sheaf_yoneda_hom i.hom).app X)
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
- H.sheaf_iso i = {hom := {val := (H.presheaf_iso i).hom}, inv := {val := (H.presheaf_iso i).inv}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.cover_dense.sheaf_iso_inv_val
{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) :
@[simp]
theorem
category_theory.cover_dense.sheaf_iso_hom_val
{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) :
theorem
category_theory.cover_dense.sheaf_hom_restrict_eq
{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) :
category_theory.whisker_left G.op (H.sheaf_hom α) = α
The constructed sheaf_hom α is equal to α when restricted onto C.
theorem
category_theory.cover_dense.sheaf_hom_eq
{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}
(α : ℱ ⟶ ℱ'.val) :
H.sheaf_hom (category_theory.whisker_left G.op α) = α
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} :
A full and cover-dense functor G induces an equivalence between morphisms into a sheaf and
morphisms over the restrictions via G.
theorem
category_theory.cover_dense.iso_of_restrict_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 : category_theory.is_iso (category_theory.whisker_left G.op α.val)) :
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}
[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]
[category_theory.faithful 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}
[category_theory.category C]
{D : Type u_3}
[category_theory.category D]
(J : category_theory.grothendieck_topology C)
{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.faithful G]
(Hp : category_theory.cover_preserving J K G) :
Equations
- category_theory.cover_dense.sites.pullback.full J H Hp = {preimage := λ (ℱ ℱ' : category_theory.Sheaf K A) (α : (category_theory.sites.pullback A _ Hp).obj ℱ ⟶ (category_theory.sites.pullback A _ Hp).obj ℱ'), {val := H.sheaf_hom α.val}, witness' := _}
@[protected, instance]
def
category_theory.cover_dense.sites.pullback.faithful
{C : Type u_1}
[category_theory.category C]
{D : Type u_3}
[category_theory.category D]
(J : category_theory.grothendieck_topology C)
{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.faithful G]
(Hp : category_theory.cover_preserving J K G) :
@[simp]
theorem
category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting_functor
{C D : Type u}
[category_theory.category C]
[category_theory.category D]
{G : C ⥤ D}
[category_theory.full G]
[category_theory.faithful G]
{J : category_theory.grothendieck_topology C}
{K : category_theory.grothendieck_topology D}
{A : Type w}
[category_theory.category A]
[category_theory.limits.has_limits A]
(Hd : category_theory.cover_dense K G)
(Hp : category_theory.cover_preserving J K G)
(Hl : category_theory.cover_lifting J K G) :
@[simp]
theorem
category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting_inverse
{C D : Type u}
[category_theory.category C]
[category_theory.category D]
{G : C ⥤ D}
[category_theory.full G]
[category_theory.faithful G]
{J : category_theory.grothendieck_topology C}
{K : category_theory.grothendieck_topology D}
{A : Type w}
[category_theory.category A]
[category_theory.limits.has_limits A]
(Hd : category_theory.cover_dense K G)
(Hp : category_theory.cover_preserving J K G)
(Hl : category_theory.cover_lifting J K G) :
(Hd.Sheaf_equiv_of_cover_preserving_cover_lifting Hp Hl).inverse = category_theory.sites.pullback A _ Hp
noncomputable
def
category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting
{C D : Type u}
[category_theory.category C]
[category_theory.category D]
{G : C ⥤ D}
[category_theory.full G]
[category_theory.faithful G]
{J : category_theory.grothendieck_topology C}
{K : category_theory.grothendieck_topology D}
{A : Type w}
[category_theory.category A]
[category_theory.limits.has_limits A]
(Hd : category_theory.cover_dense K G)
(Hp : category_theory.cover_preserving J K G)
(Hl : category_theory.cover_lifting J K 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
- Hd.Sheaf_equiv_of_cover_preserving_cover_lifting Hp Hl = (let α : category_theory.sites.pullback A _ Hp ⊣ category_theory.sites.copullback A Hl := category_theory.sites.pullback_copullback_adjunction A Hp Hl _ in {functor := category_theory.sites.pullback A _ Hp, inverse := category_theory.sites.copullback A Hl, unit_iso := category_theory.as_iso α.unit _, counit_iso := category_theory.as_iso α.counit _, functor_unit_iso_comp' := _}).symm