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

E.map F K = { toPreOneHypercover := E.map F, mem₀ := ⋯, mem₁ := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.map_toPreOneHypercover {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] :

(E.map F K).toPreOneHypercover = E.map F

source

instance CategoryTheory.GrothendieckTopology.OneHypercover.instIsPreservedById {C : Type u₁} [Category.{v₁, u₁} C] {J : GrothendieckTopology C} {X : C} (E : J.OneHypercover X) :

E.IsPreservedBy (Functor.id C) J

source

@[reducible, inline]

abbrev CategoryTheory.Functor.PreservesOneHypercovers {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) :

Prop

The condition that a functor F : C ⥤ D sends 1-hypercovers for J : GrothendieckTopology C to 1-hypercovers for K : GrothendieckTopology D.

Equations

F.PreservesOneHypercovers J K = ∀ {X : C} (E : J.OneHypercover X), E.IsPreservedBy F K

Instances For

source

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

Prop

A functor F is continuous if the precomposition with F.op sends sheaves of Type t to sheaves.

op_comp_isSheaf_of_types (G : Sheaf K (Type t)) : Presieve.IsSheaf J (F.op.comp G.val)

Instances

source

theorem CategoryTheory.Functor.op_comp_isSheaf_of_types {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] (G : Sheaf K (Type t)) :

Presieve.IsSheaf J (F.op.comp G.val)

source

theorem CategoryTheory.Functor.op_comp_isSheaf {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {A : Type u} [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] (G : Sheaf K A) :

Presheaf.IsSheaf J (F.op.comp G.val)

source

theorem CategoryTheory.Functor.isContinuous_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F₁.IsContinuous J K] :

F₂.IsContinuous J K

source

instance CategoryTheory.Functor.isContinuous_id {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) :

(Functor.id C).IsContinuous J J

source

theorem CategoryTheory.Functor.isContinuous_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F₁ : Functor C D) (F₂ : Functor D E) (J : GrothendieckTopology C) (K : GrothendieckTopology D) (L : GrothendieckTopology E) [F₁.IsContinuous J K] [F₂.IsContinuous K L] :

(F₁.comp F₂).IsContinuous J L

source

theorem CategoryTheory.Functor.isContinuous_comp' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F₁ : Functor C D} {F₂ : Functor D E} {F₁₂ : Functor C E} (e : F₁.comp F₂ ≅ F₁₂) (J : GrothendieckTopology C) (K : GrothendieckTopology D) (L : GrothendieckTopology E) [F₁.IsContinuous J K] [F₂.IsContinuous K L] :

F₁₂.IsContinuous J L

source

instance CategoryTheory.Functor.instIsContinuousCompId {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] :

(F.comp (Functor.id D)).IsContinuous J K

source

instance CategoryTheory.Functor.instIsContinuousCompId_1 {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] :

((Functor.id C).comp F).IsContinuous J K

source

theorem CategoryTheory.Functor.op_comp_isSheaf_of_preservesOneHypercovers {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {A : Type u} [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.PreservesOneHypercovers J K] [J.IsGeneratedByOneHypercovers] (P : Functor Dᵒᵖ A) (hP : Presheaf.IsSheaf K P) :

Presheaf.IsSheaf J (F.op.comp P)

source

theorem CategoryTheory.Functor.isContinuous_of_preservesOneHypercovers {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.PreservesOneHypercovers J K] [J.IsGeneratedByOneHypercovers] :

F.IsContinuous J K

source

instance CategoryTheory.Functor.instIsContinuousOfPreservesOneHypercovers {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.PreservesOneHypercovers J K] :

F.IsContinuous J K

source

def CategoryTheory.Functor.sheafPushforwardContinuous {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] :

Functor (Sheaf K A) (Sheaf J A)

The induced functor Sheaf K A ⥤ Sheaf J A given by F.op ⋙ _ if F is a continuous functor.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuous_obj_val_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] (ℱ : Sheaf K A) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) :

((F.sheafPushforwardContinuous A J K).obj ℱ).val.map f = ℱ.val.map (F.map f.unop).op

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuous_obj_val_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] (ℱ : Sheaf K A) (X : Cᵒᵖ) :

((F.sheafPushforwardContinuous A J K).obj ℱ).val.obj X = ℱ.val.obj (Opposite.op (F.obj (Opposite.unop X)))

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuous_map_val_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] {X✝ Y✝ : Sheaf K A} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) :

((F.sheafPushforwardContinuous A J K).map f).val.app X = f.val.app (Opposite.op (F.obj (Opposite.unop X)))

source

def CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] :

(F.sheafPushforwardContinuous A J K).comp (sheafToPresheaf J A) ≅ (sheafToPresheaf K A).comp ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op)

The functor F.sheafPushforwardContinuous A J K : Sheaf K A ⥤ Sheaf J A is induced by the precomposition with F.op.

Equations

F.sheafPushforwardContinuousCompSheafToPresheafIso A J K = CategoryTheory.Iso.refl ((F.sheafPushforwardContinuous A J K).comp (CategoryTheory.sheafToPresheaf J A))

Instances For

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] (X : Sheaf K A) (X✝ : Cᵒᵖ) :

((F.sheafPushforwardContinuousCompSheafToPresheafIso A J K).hom.app X).app X✝ = CategoryStruct.id (X.val.obj (Opposite.op (F.obj (Opposite.unop X✝))))

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] (X : Sheaf K A) (X✝ : Cᵒᵖ) :

((F.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app X).app X✝ = CategoryStruct.id (X.val.obj (Opposite.op (F.obj (Opposite.unop X✝))))

source

def CategoryTheory.Functor.sheafPushforwardContinuousId {C : Type u₁} [Category.{v₁, u₁} C] (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) :

(Functor.id C).sheafPushforwardContinuous A J J ≅ Functor.id (Sheaf J A)

The functor sheafPushforwardContinuous corresponding to the identity functor identifies to the identity functor.

Equations

CategoryTheory.Functor.sheafPushforwardContinuousId A J = CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).sheafPushforwardContinuous A J J)

Instances For

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousId_inv_app_val_app {C : Type u₁} [Category.{v₁, u₁} C] (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (X : Sheaf J A) (X✝ : Cᵒᵖ) :

((sheafPushforwardContinuousId A J).inv.app X).val.app X✝ = CategoryStruct.id (X.val.obj X✝)

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousId_hom_app_val_app {C : Type u₁} [Category.{v₁, u₁} C] (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (X : Sheaf J A) (X✝ : Cᵒᵖ) :

((sheafPushforwardContinuousId A J).hom.app X).val.app X✝ = CategoryStruct.id (X.val.obj X✝)

source

def CategoryTheory.Functor.sheafPushforwardContinuousComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (L : GrothendieckTopology E) [F.IsContinuous J K] [G.IsContinuous K L] :

(G.sheafPushforwardContinuous A K L).comp (F.sheafPushforwardContinuous A J K) ≅ (F.comp G).sheafPushforwardContinuous A J L

The composition of two pushforward functors on sheaves identifies to the pushforward for the composition of the two functors.

Equations

F.sheafPushforwardContinuousComp G A J K L = CategoryTheory.Iso.refl ((G.sheafPushforwardContinuous A K L).comp (F.sheafPushforwardContinuous A J K))

Instances For

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousComp_hom_app_val_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (L : GrothendieckTopology E) [F.IsContinuous J K] [G.IsContinuous K L] (X : Sheaf L A) (X✝ : Cᵒᵖ) :

((F.sheafPushforwardContinuousComp G A J K L).hom.app X).val.app X✝ = CategoryStruct.id (X.val.obj (Opposite.op (G.obj (F.obj (Opposite.unop X✝)))))

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousComp_inv_app_val_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (L : GrothendieckTopology E) [F.IsContinuous J K] [G.IsContinuous K L] (X : Sheaf L A) (X✝ : Cᵒᵖ) :

((F.sheafPushforwardContinuousComp G A J K L).inv.app X).val.app X✝ = CategoryStruct.id (X.val.obj (Opposite.op (G.obj (F.obj (Opposite.unop X✝)))))

source

def CategoryTheory.Functor.sheafPushforwardContinuousNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F F' : Functor C D} (τ : F ⟶ F') (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] [F'.IsContinuous J K] :

F'.sheafPushforwardContinuous A J K ⟶ F.sheafPushforwardContinuous A J K

The action of a natural transformation on pushforward functors of sheaves.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousNatTrans_app_val {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F F' : Functor C D} (τ : F ⟶ F') (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] [F'.IsContinuous J K] (M : Sheaf K A) :

((sheafPushforwardContinuousNatTrans τ A J K).app M).val = whiskerRight (NatTrans.op τ) M.val

source

def CategoryTheory.Functor.sheafPushforwardContinuousIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F F' : Functor C D} (e : F ≅ F') (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] [F'.IsContinuous J K] :

F.sheafPushforwardContinuous A J K ≅ F'.sheafPushforwardContinuous A J K

The action of a natural isomorphism on pushforward functors of sheaves.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F F' : Functor C D} (e : F ≅ F') (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] [F'.IsContinuous J K] :

(sheafPushforwardContinuousIso e A J K).hom = sheafPushforwardContinuousNatTrans e.inv A J K

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F F' : Functor C D} (e : F ≅ F') (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.IsContinuous J K] [F'.IsContinuous J K] :

(sheafPushforwardContinuousIso e A J K).inv = sheafPushforwardContinuousNatTrans e.hom A J K

source

def CategoryTheory.Functor.sheafPushforwardContinuousId' {C : Type u₁} [Category.{v₁, u₁} C] {F'' : Functor C C} (eF'' : F'' ≅ Functor.id C) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) [F''.IsContinuous J J] :

F''.sheafPushforwardContinuous A J J ≅ Functor.id (Sheaf J A)

If a continuous functor between sites is isomorphic to the identity functor, then the corresponding pushforward functor on sheaves identifies to the identity functor.

Equations

CategoryTheory.Functor.sheafPushforwardContinuousId' eF'' A J = CategoryTheory.Functor.sheafPushforwardContinuousIso eF'' A J J ≪≫ CategoryTheory.Functor.sheafPushforwardContinuousId A J

Instances For

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousId'_hom_app_val_app {C : Type u₁} [Category.{v₁, u₁} C] {F'' : Functor C C} (eF'' : F'' ≅ Functor.id C) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) [F''.IsContinuous J J] (X : Sheaf J A) (X✝ : Cᵒᵖ) :

((sheafPushforwardContinuousId' eF'' A J).hom.app X).val.app X✝ = X.val.map (eF''.inv.app (Opposite.unop X✝)).op

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousId'_inv_app_val_app {C : Type u₁} [Category.{v₁, u₁} C] {F'' : Functor C C} (eF'' : F'' ≅ Functor.id C) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) [F''.IsContinuous J J] (X : Sheaf J A) (X✝ : Cᵒᵖ) :

((sheafPushforwardContinuousId' eF'' A J).inv.app X).val.app X✝ = X.val.map (eF''.hom.app (Opposite.unop X✝)).op

source

def CategoryTheory.Functor.sheafPushforwardContinuousComp' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C D} {G : Functor D E} {FG : Functor C E} (eFG : F.comp G ≅ FG) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (L : GrothendieckTopology E) [F.IsContinuous J K] [G.IsContinuous K L] [FG.IsContinuous J L] :

(G.sheafPushforwardContinuous A K L).comp (F.sheafPushforwardContinuous A J K) ≅ FG.sheafPushforwardContinuous A J L

When we have an isomorphism F ⋙ G ≅ FG between continuous functors between sites, the composition of the pushforward functors for G and F identifies to the pushforward functor for FG.

Equations

CategoryTheory.Functor.sheafPushforwardContinuousComp' eFG A J K L = F.sheafPushforwardContinuousComp G A J K L ≪≫ CategoryTheory.Functor.sheafPushforwardContinuousIso eFG A J L

Instances For

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousComp'_inv_app_val_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C D} {G : Functor D E} {FG : Functor C E} (eFG : F.comp G ≅ FG) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (L : GrothendieckTopology E) [F.IsContinuous J K] [G.IsContinuous K L] [FG.IsContinuous J L] (X : Sheaf L A) (X✝ : Cᵒᵖ) :

((sheafPushforwardContinuousComp' eFG A J K L).inv.app X).val.app X✝ = X.val.map (eFG.hom.app (Opposite.unop X✝)).op

source

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardContinuousComp'_hom_app_val_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C D} {G : Functor D E} {FG : Functor C E} (eFG : F.comp G ≅ FG) (A : Type u) [Category.{t, u} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (L : GrothendieckTopology E) [F.IsContinuous J K] [G.IsContinuous K L] [FG.IsContinuous J L] (X : Sheaf L A) (X✝ : Cᵒᵖ) :

((sheafPushforwardContinuousComp' eFG A J K L).hom.app X).val.app X✝ = X.val.map (eFG.inv.app (Opposite.unop X✝)).op

Documentation

Mathlib.CategoryTheory.Sites.Continuous

Continuous functors between sites. #

Main definitions #

Main result #

References #