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.
• CategoryTheory.Functor.IsDenseSubsite.sheafEquiv: the equivalence of categories Sheaf J A ≌ Sheaf K A when (C, J) is a dense subsite of (D, K) and the pushforward functor Sheaf K A ⥤ Sheaf J A is an equivalence, which we show in two situations:
  • the sites are small and A has suitable limits (see the file Mathlib/CategoryTheory/Sites/DenseSubsite/SheafEquiv.lean).
  • the category A has limits of size w and G is 1-hypercover cover dense relatively to the universe w (see the file Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean).

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

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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.

Equations

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

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

Equations

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

theorem CategoryTheory.Presieve.in_coverByImage {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} (G : Functor C D) [G.IsCoverDense K] (ℱ : Sheaf K (Type u_5)) (X : D) {s t : ℱ.obj.obj (Opposite.op X)} (h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.obj.map f.op s = ℱ.obj.map f.op t) : s = t

theorem CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) (X : A) : G.op.comp (ℱ.comp (coyoneda.obj (Opposite.op X))) ⟶ G.op.comp (sheafOver ℱ' X).obj

(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

• CategoryTheory.Functor.IsCoverDense.homOver α X = CategoryTheory.Functor.whiskerRight α (CategoryTheory.coyoneda.obj (Opposite.op X))

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.homOver_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) (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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} {ℱ ℱ' : Sheaf K A} (α : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : A) : G.op.comp (sheafOver ℱ X).obj ≅ G.op.comp (sheafOver ℱ' X).obj

(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

• CategoryTheory.Functor.IsCoverDense.isoOver α X = CategoryTheory.Functor.isoWhiskerRight α (CategoryTheory.coyoneda.obj (Opposite.op X))

@[simp]

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

@[simp]

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

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

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

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) {X : D} (x : ℱ.obj (Opposite.op X)) : Presieve.FamilyOfElements ℱ'.obj (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

• CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x x✝ hf = ℱ'.obj.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_def {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) {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) => ℱ'.obj.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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) [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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) [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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} {ℱ : Functor Dᵒᵖ (Type v)} {ℱ' : Sheaf K (Type v)} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) [G.IsCoverDense K] [G.IsLocallyFull K] (X : D) : ℱ.obj (Opposite.op X) ⟶ ℱ'.obj.obj (Opposite.op X)

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

Equations

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

@[simp]

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

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

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.Types.appIso_inv {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : D) (a✝ : ℱ'.obj.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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : D) (a✝ : ℱ.obj.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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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 ℱ'.obj) : ℱ ⟶ ℱ'.obj

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

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

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.Types.presheafHom_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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 ℱ'.obj) (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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) : ℱ.obj ≅ ℱ'.obj

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

• CategoryTheory.Functor.IsCoverDense.Types.presheafIso i = CategoryTheory.NatIso.ofComponents (fun (X : Dᵒᵖ) => CategoryTheory.Functor.IsCoverDense.Types.appIso i (Opposite.unop X)) ⋯

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Functor.IsCoverDense.Types.sheafIso {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) : ℱ ≅ ℱ'

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

• CategoryTheory.Functor.IsCoverDense.Types.sheafIso i = (CategoryTheory.fullyFaithfulSheafToPresheaf K (Type ?u.108)).preimageIso (CategoryTheory.Functor.IsCoverDense.Types.presheafIso i)

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, 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 ℱ'.obj) : coyoneda.comp ((whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ) ⟶ coyoneda.comp ((whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ'.obj)

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

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, 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 ℱ'.obj) (X : Aᵒᵖ) : (sheafCoyonedaHom α).app X = Types.presheafHom (homOver α (Opposite.unop X))

noncomputable def CategoryTheory.Functor.IsCoverDense.sheafYonedaHom {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, 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 ℱ'.obj) : ℱ.comp yoneda ⟶ ℱ'.obj.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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, 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 ℱ'.obj) : ℱ ⟶ ℱ'.obj

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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) : ℱ.obj ≅ ℱ'.obj

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.presheafIso_hom_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) : ℱ ≅ ℱ'

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

• CategoryTheory.Functor.IsCoverDense.sheafIso i = (CategoryTheory.fullyFaithfulSheafToPresheaf K A).preimageIso (CategoryTheory.Functor.IsCoverDense.presheafIso i)

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.sheafIso_inv_hom {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) : (sheafIso i).inv.hom = CategoryTheory.inv (sheafHom i.hom)

@[simp]

theorem CategoryTheory.Functor.IsCoverDense.sheafIso_hom_hom {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) : (sheafIso i).hom.hom = (presheafIso i).hom

theorem CategoryTheory.Functor.IsCoverDense.sheafHom_restrict_eq {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, 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 ℱ'.obj) : 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] (G : Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} (α : ℱ ⟶ ℱ'.obj) : 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, 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 ℱ'.obj) ≃ (ℱ ⟶ ℱ'.obj)

A locally-full and cover-dense functor G induces an equivalence between morphisms into a sheaf and morphisms over the restrictions via G.

Equations

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

theorem CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} (f : ℱ ⟶ ℱ'.obj) {𝒢' : Sheaf K A} (g : ℱ' ⟶ 𝒢') : restrictHomEquivHom.symm (CategoryStruct.comp f g.hom) = CategoryStruct.comp (restrictHomEquivHom.symm f) (G.op.whiskerLeft g.hom)

theorem CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm_assoc {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} (f : ℱ ⟶ ℱ'.obj) {𝒢' : Sheaf K A} (g : ℱ' ⟶ 𝒢') {Z : Functor Cᵒᵖ A} (h : G.op.comp 𝒢'.obj ⟶ Z) : CategoryStruct.comp (restrictHomEquivHom.symm (CategoryStruct.comp f g.hom)) h = CategoryStruct.comp (restrictHomEquivHom.symm f) (CategoryStruct.comp (G.op.whiskerLeft g.hom) h)

theorem CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} (f : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) {𝒢' : Sheaf K A} (g : ℱ' ⟶ 𝒢') : restrictHomEquivHom (CategoryStruct.comp f (G.op.whiskerLeft g.hom)) = CategoryStruct.comp (restrictHomEquivHom f) g.hom

theorem CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_assoc {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} (f : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) {𝒢' : Sheaf K A} (g : ℱ' ⟶ 𝒢') {Z : Functor Dᵒᵖ A} (h : 𝒢'.obj ⟶ Z) : CategoryStruct.comp (restrictHomEquivHom (CategoryStruct.comp f (G.op.whiskerLeft g.hom))) h = CategoryStruct.comp (restrictHomEquivHom f) (CategoryStruct.comp g.hom h)

theorem CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_symm {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} {𝒢 : Functor Dᵒᵖ A} (f : 𝒢 ⟶ ℱ) (g : ℱ ⟶ ℱ'.obj) : restrictHomEquivHom.symm (CategoryStruct.comp f g) = CategoryStruct.comp (G.op.whiskerLeft f) (restrictHomEquivHom.symm g)

theorem CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_symm_assoc {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} {𝒢 : Functor Dᵒᵖ A} (f : 𝒢 ⟶ ℱ) (g : ℱ ⟶ ℱ'.obj) {Z : Functor Cᵒᵖ A} (h : G.op.comp ℱ'.obj ⟶ Z) : CategoryStruct.comp (restrictHomEquivHom.symm (CategoryStruct.comp f g)) h = CategoryStruct.comp (G.op.whiskerLeft f) (CategoryStruct.comp (restrictHomEquivHom.symm g) h)

theorem CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} {𝒢 : Functor Dᵒᵖ A} (f : 𝒢 ⟶ ℱ) (g : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) : restrictHomEquivHom (CategoryStruct.comp (G.op.whiskerLeft f) g) = CategoryStruct.comp f (restrictHomEquivHom g)

theorem CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_assoc {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ : Functor Dᵒᵖ A} {ℱ' : Sheaf K A} {𝒢 : Functor Dᵒᵖ A} (f : 𝒢 ⟶ ℱ) (g : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) {Z : Functor Dᵒᵖ A} (h : ℱ'.obj ⟶ Z) : CategoryStruct.comp (restrictHomEquivHom (CategoryStruct.comp (G.op.whiskerLeft f) g)) h = CategoryStruct.comp f (CategoryStruct.comp (restrictHomEquivHom g) h)

theorem CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {K : GrothendieckTopology D} {A : Type u_4} [Category.{v_4, u_4} A] {G : Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : Sheaf K A} (α : ℱ ⟶ ℱ') (i : IsIso (G.op.whiskerLeft α.hom)) : 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type u_4} [Category.{v_4, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type u_4} [Category.{v_4, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (K : GrothendieckTopology D) (G : Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] {A : Type u_4} [Category.{v_4, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] : (G.sheafPushforwardContinuous A J K).Full

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

theorem CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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

theorem CategoryTheory.Functor.IsDenseSubsite.map_eq_of_eq {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {J : GrothendieckTopology C} (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] (F : Sheaf J A) {X Y : C} (f₁ f₂ : X ⟶ Y) (h : G.map f₁ = G.map f₂) : F.obj.map f₁.op = F.obj.map f₂.op

noncomputable def CategoryTheory.Functor.IsDenseSubsite.mapPreimage {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {J : GrothendieckTopology C} (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] (F : Sheaf J A) {X Y : C} (f : G.obj X ⟶ G.obj Y) : F.obj.obj (Opposite.op Y) ⟶ F.obj.obj (Opposite.op X)

If G : C ⥤ D is a dense subsite and F a sheaf on C, this is the morphism F.val.obj (op Y) ⟶ F.val.obj (op X) induced by a morphism G.obj X ⟶ G.obj Y in the category D.

Equations

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

theorem CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_fac {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {J : GrothendieckTopology C} (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] (F : Sheaf J A) {X Y Z : C} (f : G.obj X ⟶ G.obj Y) (p : Z ⟶ X) (g : Z ⟶ Y) (fac : CategoryStruct.comp (G.map p) f = G.map g) : CategoryStruct.comp (mapPreimage K G F f) (F.obj.map p.op) = F.obj.map g.op

theorem CategoryTheory.Functor.IsDenseSubsite.mapPreimage_of_eq {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {J : GrothendieckTopology C} (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] (F : Sheaf J A) {X Y : C} (f : G.obj X ⟶ G.obj Y) (g : X ⟶ Y) (h : G.map g = f) : mapPreimage K G F f = F.obj.map g.op

@[simp]

theorem CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {J : GrothendieckTopology C} (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] (F : Sheaf J A) {X Y : C} (f : X ⟶ Y) : mapPreimage K G F (G.map f) = F.obj.map f.op

@[simp]

theorem CategoryTheory.Functor.IsDenseSubsite.mapPreimage_id {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {J : GrothendieckTopology C} (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] (F : Sheaf J A) (X : C) : mapPreimage K G F (CategoryStruct.id (G.obj X)) = CategoryStruct.id (F.obj.obj (Opposite.op X))

theorem CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {J : GrothendieckTopology C} (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] (F : Sheaf J A) {X Y Z : C} (f : G.obj X ⟶ G.obj Y) (g : G.obj Y ⟶ G.obj Z) : mapPreimage K G F (CategoryStruct.comp f g) = CategoryStruct.comp (mapPreimage K G F g) (mapPreimage K G F f)

theorem CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_assoc {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {J : GrothendieckTopology C} (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] (F : Sheaf J A) {X Y Z : C} (f : G.obj X ⟶ G.obj Y) (g : G.obj Y ⟶ G.obj Z) {Z✝ : A} (h : F.obj.obj (Opposite.op X) ⟶ Z✝) : CategoryStruct.comp (mapPreimage K G F (CategoryStruct.comp f g)) h = CategoryStruct.comp (mapPreimage K G F g) (CategoryStruct.comp (mapPreimage K G F f) h)

theorem CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {J : GrothendieckTopology C} (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] (F : Sheaf J A) {X Y Z : C} (f : G.obj X ⟶ G.obj Y) (g : Z ⟶ X) : CategoryStruct.comp (mapPreimage K G F f) (F.obj.map g.op) = mapPreimage K G F (CategoryStruct.comp (G.map g) f)

theorem CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map_assoc {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {J : GrothendieckTopology C} (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] (F : Sheaf J A) {X Y Z : C} (f : G.obj X ⟶ G.obj Y) (g : Z ⟶ X) {Z✝ : A} (h : F.obj.obj (Opposite.op Z) ⟶ Z✝) : CategoryStruct.comp (mapPreimage K G F f) (CategoryStruct.comp (F.obj.map g.op) h) = CategoryStruct.comp (mapPreimage K G F (CategoryStruct.comp (G.map g) f)) h

noncomputable def CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) (A : Type u_4) [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [HasWeakSheafify J A] [(G.sheafPushforwardContinuous A J K).IsEquivalence] : Functor (Functor Dᵒᵖ A) (Sheaf K A)

Assuming that (C, J) is a dense subsite of (D, K) (via a functor G : C ⥤ D) and sheafPushforwardContinuous G A J₀ J is an equivalence of categories this is a sheafification functor (Dᵒᵖ ⥤ A) ⥤ Sheaf K A when HasWeakSheafify J A holds.

Equations

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

noncomputable def CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalenceCompIso {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) (A : Type u_4) [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [HasWeakSheafify J A] [(G.sheafPushforwardContinuous A J K).IsEquivalence] : (sheafifyOfIsEquivalence J K G A).comp (G.sheafPushforwardContinuous A J K) ≅ ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp (presheafToSheaf J A)

Assuming that (C, J) is a dense subsite of (D, K) (via a functor G : C ⥤ D) and sheafPushforwardContinuous G A J₀ J is an equivalence of categories, this is the isomorphism between sheafifyOfIsEquivalence J K G A ⋙ G.sheafPushforwardContinuous A J K and the functor which sends a presheaf to the sheafification of its precomposition by G.op.

Equations

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

noncomputable def CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [HasWeakSheafify J A] {P : Functor Dᵒᵖ A} {Q : Sheaf K A} : ((sheafifyOfIsEquivalence J K G A).obj P ⟶ Q) ≃ (P ⟶ Q.obj)

Auxiliary definition for sheafifyAdjunctionOfIsEquivalence.

Equations

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

theorem CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [HasWeakSheafify J A] {P₁ P₂ : Functor Dᵒᵖ A} (f : P₁ ⟶ P₂) {Q : Sheaf K A} (g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q) : (sheafifyHomEquivOfIsEquivalence J K G) (CategoryStruct.comp ((sheafifyOfIsEquivalence J K G A).map f) g) = CategoryStruct.comp f ((sheafifyHomEquivOfIsEquivalence J K G) g)

theorem CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left_assoc {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [HasWeakSheafify J A] {P₁ P₂ : Functor Dᵒᵖ A} (f : P₁ ⟶ P₂) {Q : Sheaf K A} (g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q) {Z : Functor Dᵒᵖ A} (h : Q.obj ⟶ Z) : CategoryStruct.comp ((sheafifyHomEquivOfIsEquivalence J K G) (CategoryStruct.comp ((sheafifyOfIsEquivalence J K G A).map f) g)) h = CategoryStruct.comp f (CategoryStruct.comp ((sheafifyHomEquivOfIsEquivalence J K G) g) h)

theorem CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [HasWeakSheafify J A] {P : Functor Dᵒᵖ A} {Q₁ Q₂ : Sheaf K A} (f : (sheafifyOfIsEquivalence J K G A).obj P ⟶ Q₁) (g : Q₁ ⟶ Q₂) : (sheafifyHomEquivOfIsEquivalence J K G) (CategoryStruct.comp f g) = CategoryStruct.comp ((sheafifyHomEquivOfIsEquivalence J K G) f) g.hom

theorem CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right_assoc {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [HasWeakSheafify J A] {P : Functor Dᵒᵖ A} {Q₁ Q₂ : Sheaf K A} (f : (sheafifyOfIsEquivalence J K G A).obj P ⟶ Q₁) (g : Q₁ ⟶ Q₂) {Z : Functor Dᵒᵖ A} (h : Q₂.obj ⟶ Z) : CategoryStruct.comp ((sheafifyHomEquivOfIsEquivalence J K G) (CategoryStruct.comp f g)) h = CategoryStruct.comp ((sheafifyHomEquivOfIsEquivalence J K G) f) (CategoryStruct.comp g.hom h)

noncomputable def CategoryTheory.Functor.IsDenseSubsite.sheafifyAdjunctionOfIsEquivalence {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) (A : Type u_4) [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [HasWeakSheafify J A] : sheafifyOfIsEquivalence J K G A ⊣ sheafToPresheaf K A

Assuming that (C, J) is a dense subsite of (D, K) (via a functor G : C ⥤ D) and sheafPushforwardContinuous G A J K is an equivalence of categories, and that HasWeakSheafify J A holds, then this adjunction shows the existence of a left adjoint to sheafToPresheaf K A.

Equations

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

theorem CategoryTheory.Functor.IsDenseSubsite.hasWeakSheafify_of_isEquivalence {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) (A : Type u_4) [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [HasWeakSheafify J A] : HasWeakSheafify K A

theorem CategoryTheory.Functor.IsDenseSubsite.hasSheafify_of_isEquivalence {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) {A : Type u_4} [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [HasSheafify J A] [Limits.HasFiniteLimits A] : HasSheafify K A

noncomputable def CategoryTheory.Functor.IsDenseSubsite.sheafEquiv {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) (A : Type u_4) [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] : Sheaf J A ≌ Sheaf K A

If G : C ⥤ D exhibits (C, J) as a dense subsite of (D, K), and the pushforward functor Sheaf K A ⥤ Sheaf J A is an equivalence, then this is the equivalence Sheaf K A ≌ Sheaf J A.

Equations

• CategoryTheory.Functor.IsDenseSubsite.sheafEquiv J K G A = (G.sheafPushforwardContinuous A J K).asEquivalence.symm

@[simp]

theorem CategoryTheory.Functor.IsDenseSubsite.sheafEquiv_inverse {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) (A : Type u_4) [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] : (sheafEquiv J K G A).inverse = G.sheafPushforwardContinuous A J K

noncomputable def CategoryTheory.Functor.IsDenseSubsite.sheafEquivSheafificationCompatibility {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) (A : Type u_4) [Category.{v_4, u_4} A] [IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [HasWeakSheafify J A] [HasWeakSheafify K A] : ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp (presheafToSheaf J A) ≅ (presheafToSheaf K A).comp (sheafEquiv J K G A).inverse

The natural isomorphism exhibiting the compatibility of IsDenseSubsite.sheafEquiv with sheafification.

Equations

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