Continuous functors between sites. #

We define the notion of continuous functor between sites: these are functors F such that the precomposition with F.op preserves sheaves of types (and actually sheaves in any category).

Main definitions #

Functor.IsContinuous: a functor between sites is continuous if the precomposition with this functor preserves sheaves with values in the category Type t for a certain auxiliary universe t.
Functor.sheafPushforwardContinuous: the induced functor Sheaf K A ⥤ Sheaf J A for a continuous functor G : (C, J) ⥤ (D, K). In case this is part of a morphism of sites, this would be understood as the pushforward functor even though it goes in the opposite direction as the functor G. (Here, the auxiliary universe t in the assumption that G is continuous is the one such that morphisms in the category A are in Type t.)
Functor.PreservesOneHypercovers: a type-class expressing that a functor preserves 1-hypercovers of a certain size

Main result #

Functor.isContinuous_of_preservesOneHypercovers: if the topology on C is generated by 1-hypercovers of size w and that F : C ⥤ D preserves 1-hypercovers of size w, then F is continuous (for any auxiliary universe parameter t). This is an instance for w = max u₁ v₁ when C : Type u₁ and [Category.{v₁} C]

References #

https://stacks.math.columbia.edu/tag/00WU

source

def CategoryTheory.PreOneHypercover.map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} (E : PreOneHypercover X) (F : Functor C D) :

PreOneHypercover (F.obj X)

The image of a 1-pre-hypercover by a functor.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.PreOneHypercover.map_p₁ {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} (E : PreOneHypercover X) (F : Functor C D) (x✝ x✝¹ : E.I₀) (j : E.I₁ x✝ x✝¹) :

(E.map F).p₁ j = F.map (E.p₁ j)

source

@[simp]

theorem CategoryTheory.PreOneHypercover.map_Y {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} (E : PreOneHypercover X) (F : Functor C D) (x✝ x✝¹ : E.I₀) (j : E.I₁ x✝ x✝¹) :

(E.map F).Y j = F.obj (E.Y j)

source

@[simp]

theorem CategoryTheory.PreOneHypercover.map_I₀ {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} (E : PreOneHypercover X) (F : Functor C D) :

(E.map F).I₀ = E.I₀

source

@[simp]

theorem CategoryTheory.PreOneHypercover.map_f {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} (E : PreOneHypercover X) (F : Functor C D) (i : E.I₀) :

(E.map F).f i = F.map (E.f i)

source

@[simp]

theorem CategoryTheory.PreOneHypercover.map_I₁ {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} (E : PreOneHypercover X) (F : Functor C D) (i₁ i₂ : E.I₀) :

(E.map F).I₁ i₁ i₂ = E.I₁ i₁ i₂

source

@[simp]

theorem CategoryTheory.PreOneHypercover.map_X {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} (E : PreOneHypercover X) (F : Functor C D) (i : E.I₀) :

(E.map F).X i = F.obj (E.X i)

source

@[simp]

theorem CategoryTheory.PreOneHypercover.map_p₂ {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} (E : PreOneHypercover X) (F : Functor C D) (x✝ x✝¹ : E.I₀) (j : E.I₁ x✝ x✝¹) :

(E.map F).p₂ j = F.map (E.p₂ j)

source

def CategoryTheory.PreOneHypercover.isLimitMapMultiforkEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} (E : PreOneHypercover X) (F : Functor C D) {A : Type u} [Category.{t, u} A] (P : Functor Dᵒᵖ A) :

Limits.IsLimit ((E.map F).multifork P) ≃ Limits.IsLimit (E.multifork (F.op.comp P))

If F : C ⥤ D, P : Dᵒᵖ ⥤ A and E is a 1-pre-hypercover of an object of X, then (E.map F).multifork P is a limit iff E.multifork (F.op ⋙ P) is a limit.

Equations

E.isLimitMapMultiforkEquiv F P = Equiv.refl (CategoryTheory.Limits.IsLimit ((E.map F).multifork P))

Instances For

source

class CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : GrothendieckTopology C} {X : C} (E : J.OneHypercover X) (F : Functor C D) (K : GrothendieckTopology D) :

Prop

A 1-hypercover in C is preserved by a functor F : C ⥤ D if the mapped 1-pre-hypercover in D is a 1-hypercover for the given topology on D.

mem₀ : (E.map F).sieve₀ ∈ K (F.obj X)
mem₁ (i₁ i₂ : E.I₀) ⦃W : D⦄ (p₁ : W ⟶ F.obj (E.X i₁)) (p₂ : W ⟶ F.obj (E.X i₂)) (w : CategoryStruct.comp p₁ (F.map (E.f i₁)) = CategoryStruct.comp p₂ (F.map (E.f i₂))) : (E.map F).sieve₁ p₁ p₂ ∈ K W

Instances

source

def CategoryTheory.GrothendieckTopology.OneHypercover.map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : GrothendieckTopology C} {X : C} (E : J.OneHypercover X) (F : Functor C D) (K : GrothendieckTopology D) [E.IsPreservedBy F K] :

K.OneHypercover (F.obj X)

Given a 1-hypercover E : J.OneHypercover X of an object of C, a functor F : C ⥤ D such that E.IsPreversedBy F K for a Grothendieck topology K on D, this is the image of E by F, as a 1-hypercover of F.obj X for K.

Equations