mathlib3 documentation

category_theory.sites.pushforward

Pushforward of sheaves #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

category_theory.sites.pushforward: the induced functor Sheaf J A ⥤ Sheaf K A for a cover-preserving and compatible-preserving functor G : (C, J) ⥤ (D, K).

@[protected, instance]

noncomputable def category_theory.Sheaf_to_presheaf.creates_limits {C : Type v₁} [category_theory.small_category C] (A : Type u₁) [category_theory.category A] (J : category_theory.grothendieck_topology C) [category_theory.limits.has_limits A] :

category_theory.creates_limits (category_theory.Sheaf_to_presheaf J A)

Equations

category_theory.Sheaf_to_presheaf.creates_limits A J = category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits

@[protected, instance]

def category_theory.grothendieck_topology.cover.is_cofiltered {C : Type v₁} [category_theory.small_category C] (J : category_theory.grothendieck_topology C) {X : C} :

category_theory.is_cofiltered (J.cover X)

@[simp]

theorem category_theory.sites.pushforward_map_val_app {C : Type v₁} [category_theory.small_category C] {D : Type v₁} [category_theory.small_category D] (A : Type u₁) [category_theory.category A] (J : category_theory.grothendieck_topology C) (K : category_theory.grothendieck_topology D) [category_theory.concrete_category A] [category_theory.limits.preserves_limits (category_theory.forget A)] [category_theory.limits.has_colimits A] [category_theory.limits.has_limits A] [category_theory.limits.preserves_filtered_colimits (category_theory.forget A)] [category_theory.reflects_isomorphisms (category_theory.forget A)] (G : C ⥤ D) (_x _x_1 : category_theory.Sheaf J A) (f : _x ⟶ _x_1) (X : Dᵒᵖ) :

((category_theory.sites.pushforward A J K G).map f).val.app X = category_theory.limits.colim_map (K.diagram_nat_trans (K.plus_map ((category_theory.Lan G.op).map f.val)) (opposite.unop X))

noncomputable def category_theory.sites.pushforward {C : Type v₁} [category_theory.small_category C] {D : Type v₁} [category_theory.small_category D] (A : Type u₁) [category_theory.category A] (J : category_theory.grothendieck_topology C) (K : category_theory.grothendieck_topology D) [category_theory.concrete_category A] [category_theory.limits.preserves_limits (category_theory.forget A)] [category_theory.limits.has_colimits A] [category_theory.limits.has_limits A] [category_theory.limits.preserves_filtered_colimits (category_theory.forget A)] [category_theory.reflects_isomorphisms (category_theory.forget A)] (G : C ⥤ D) :

category_theory.Sheaf J A ⥤ category_theory.Sheaf K A

The pushforward functor Sheaf J A ⥤ Sheaf K A associated to a functor G : C ⥤ D in the same direction as G.

Equations

category_theory.sites.pushforward A J K G = category_theory.Sheaf_to_presheaf J A ⋙ category_theory.Lan G.op ⋙ category_theory.presheaf_to_Sheaf K A

Instances for category_theory.sites.pushforward

category_theory.sites.pushforward.limits.preserves_finite_limits

@[simp]

theorem category_theory.sites.pushforward_obj_val_obj {C : Type v₁} [category_theory.small_category C] {D : Type v₁} [category_theory.small_category D] (A : Type u₁) [category_theory.category A] (J : category_theory.grothendieck_topology C) (K : category_theory.grothendieck_topology D) [category_theory.concrete_category A] [category_theory.limits.preserves_limits (category_theory.forget A)] [category_theory.limits.has_colimits A] [category_theory.limits.has_limits A] [category_theory.limits.preserves_filtered_colimits (category_theory.forget A)] [category_theory.reflects_isomorphisms (category_theory.forget A)] (G : C ⥤ D) (X : category_theory.Sheaf J A) (X_1 : Dᵒᵖ) :

((category_theory.sites.pushforward A J K G).obj X).val.obj X_1 = category_theory.limits.colimit (K.diagram (K.plus_obj ((category_theory.Lan G.op).obj X.val)) (opposite.unop X_1))

@[simp]

theorem category_theory.sites.pushforward_obj_val_map {C : Type v₁} [category_theory.small_category C] {D : Type v₁} [category_theory.small_category D] (A : Type u₁) [category_theory.category A] (J : category_theory.grothendieck_topology C) (K : category_theory.grothendieck_topology D) [category_theory.concrete_category A] [category_theory.limits.preserves_limits (category_theory.forget A)] [category_theory.limits.has_colimits A] [category_theory.limits.has_limits A] [category_theory.limits.preserves_filtered_colimits (category_theory.forget A)] [category_theory.reflects_isomorphisms (category_theory.forget A)] (G : C ⥤ D) (X : category_theory.Sheaf J A) (X_1 Y : Dᵒᵖ) (f : X_1 ⟶ Y) :

((category_theory.sites.pushforward A J K G).obj X).val.map f = category_theory.limits.colim_map (K.diagram_pullback (K.plus_obj ((category_theory.Lan G.op).obj X.val)) f.unop) ≫ category_theory.limits.colimit.pre (K.diagram (K.plus_obj ((category_theory.Lan G.op).obj X.val)) (opposite.unop Y)) (K.pullback f.unop).op

@[protected, instance]

noncomputable def category_theory.sites.pushforward.limits.preserves_finite_limits {C : Type v₁} [category_theory.small_category C] {D : Type v₁} [category_theory.small_category D] (A : Type u₁) [category_theory.category A] (J : category_theory.grothendieck_topology C) (K : category_theory.grothendieck_topology D) [category_theory.concrete_category A] [category_theory.limits.preserves_limits (category_theory.forget A)] [category_theory.limits.has_colimits A] [category_theory.limits.has_limits A] [category_theory.limits.preserves_filtered_colimits (category_theory.forget A)] [category_theory.reflects_isomorphisms (category_theory.forget A)] (G : C ⥤ D) [category_theory.representably_flat G] :

category_theory.limits.preserves_finite_limits (category_theory.sites.pushforward A J K G)

Equations

category_theory.sites.pushforward.limits.preserves_finite_limits A J K G = category_theory.limits.comp_preserves_finite_limits (category_theory.Sheaf_to_presheaf J A) (category_theory.Lan G.op ⋙ category_theory.presheaf_to_Sheaf K A)

noncomputable def category_theory.sites.pullback_pushforward_adjunction {C : Type v₁} [category_theory.small_category C] {D : Type v₁} [category_theory.small_category D] (A : Type u₁) [category_theory.category A] (J : category_theory.grothendieck_topology C) (K : category_theory.grothendieck_topology D) [category_theory.concrete_category A] [category_theory.limits.preserves_limits (category_theory.forget A)] [category_theory.limits.has_colimits A] [category_theory.limits.has_limits A] [category_theory.limits.preserves_filtered_colimits (category_theory.forget A)] [category_theory.reflects_isomorphisms (category_theory.forget A)] {G : C ⥤ D} (hG₁ : category_theory.compatible_preserving K G) (hG₂ : category_theory.cover_preserving J K G) :

category_theory.sites.pushforward A J K G ⊣ category_theory.sites.pullback A hG₁ hG₂

The pushforward functor is left adjoint to the pullback functor.

Equations

category_theory.sites.pullback_pushforward_adjunction A J K hG₁ hG₂ = category_theory.adjunction.restrict_fully_faithful (category_theory.Sheaf_to_presheaf J A) (𝟭 (category_theory.Sheaf K A)) ((category_theory.Lan.adjunction A G.op).comp (category_theory.sheafification_adjunction K A)) (category_theory.nat_iso.of_components (λ (_x : category_theory.Sheaf J A), category_theory.iso.refl ((category_theory.Sheaf_to_presheaf J A ⋙ category_theory.Lan G.op ⋙ category_theory.presheaf_to_Sheaf K A).obj _x)) _) (category_theory.nat_iso.of_components (λ (_x : category_theory.Sheaf K A), category_theory.iso.refl ((𝟭 (category_theory.Sheaf K A) ⋙ category_theory.Sheaf_to_presheaf K A ⋙ (category_theory.whiskering_left Cᵒᵖ Dᵒᵖ A).obj G.op).obj _x)) _)