category_theory.sites.left_exact

@[simp]

theorem category_theory.grothendieck_topology.cone_comp_evaluation_of_cone_comp_diagram_functor_comp_evaluation_π_app {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] {X : C} {K : Type (max v u)} [category_theory.small_category K] {F : K ⥤ Cᵒᵖ ⥤ D} {W : J.cover X} (i : W.arrow) (E : category_theory.limits.cone (F ⋙ J.diagram_functor D X ⋙ (category_theory.evaluation (J.cover X)ᵒᵖ D).obj (opposite.op W))) (k : K) :

(category_theory.grothendieck_topology.cone_comp_evaluation_of_cone_comp_diagram_functor_comp_evaluation i E).π.app k = E.π.app k ≫ category_theory.limits.multiequalizer.ι (W.index (F.obj k)) i

source

@[simp]

theorem category_theory.grothendieck_topology.cone_comp_evaluation_of_cone_comp_diagram_functor_comp_evaluation_X {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] {X : C} {K : Type (max v u)} [category_theory.small_category K] {F : K ⥤ Cᵒᵖ ⥤ D} {W : J.cover X} (i : W.arrow) (E : category_theory.limits.cone (F ⋙ J.diagram_functor D X ⋙ (category_theory.evaluation (J.cover X)ᵒᵖ D).obj (opposite.op W))) :

(category_theory.grothendieck_topology.cone_comp_evaluation_of_cone_comp_diagram_functor_comp_evaluation i E).X = E.X

source

noncomputable def category_theory.grothendieck_topology.cone_comp_evaluation_of_cone_comp_diagram_functor_comp_evaluation {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] {X : C} {K : Type (max v u)} [category_theory.small_category K] {F : K ⥤ Cᵒᵖ ⥤ D} {W : J.cover X} (i : W.arrow) (E : category_theory.limits.cone (F ⋙ J.diagram_functor D X ⋙ (category_theory.evaluation (J.cover X)ᵒᵖ D).obj (opposite.op W))) :

category_theory.limits.cone (F ⋙ (category_theory.evaluation Cᵒᵖ D).obj (opposite.op i.Y))

An auxiliary definition to be used in the proof of the fact that J.diagram_functor D X preserves limits.

Equations

category_theory.grothendieck_topology.cone_comp_evaluation_of_cone_comp_diagram_functor_comp_evaluation i E = {X := E.X, π := {app := λ (k : K), E.π.app k ≫ category_theory.limits.multiequalizer.ι (W.index (F.obj k)) i, naturality' := _}}

source

@[reducible]

noncomputable def category_theory.grothendieck_topology.lift_to_diagram_limit_obj {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] {X : C} {K : Type (max v u)} [category_theory.small_category K] [category_theory.limits.has_limits_of_shape K D] {W : (J.cover X)ᵒᵖ} (F : K ⥤ Cᵒᵖ ⥤ D) (E : category_theory.limits.cone (F ⋙ J.diagram_functor D X ⋙ (category_theory.evaluation (J.cover X)ᵒᵖ D).obj W)) :

E.X ⟶ (J.diagram (category_theory.limits.limit F) X).obj W

An auxiliary definition to be used in the proof of the fact that J.diagram_functor D X preserves limits.

source

@[protected, instance]

noncomputable def category_theory.grothendieck_topology.diagram_functor.category_theory.limits.preserves_limit {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (X : C) (K : Type (max v u)) [category_theory.small_category K] [category_theory.limits.has_limits_of_shape K D] (F : K ⥤ Cᵒᵖ ⥤ D) :

category_theory.limits.preserves_limit F (J.diagram_functor D X)

Equations

source

@[protected, instance]

noncomputable def category_theory.grothendieck_topology.diagram_functor.category_theory.limits.preserves_limits_of_shape {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (X : C) (K : Type (max v u)) [category_theory.small_category K] [category_theory.limits.has_limits_of_shape K D] :

category_theory.limits.preserves_limits_of_shape K (J.diagram_functor D X)

Equations

category_theory.grothendieck_topology.diagram_functor.category_theory.limits.preserves_limits_of_shape X K = {preserves_limit := λ {K_1 : K ⥤ Cᵒᵖ ⥤ D}, category_theory.grothendieck_topology.diagram_functor.category_theory.limits.preserves_limit X K K_1}

source

@[protected, instance]

noncomputable def category_theory.grothendieck_topology.diagram_functor.category_theory.limits.preserves_limits {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (X : C) [category_theory.limits.has_limits D] :

category_theory.limits.preserves_limits (J.diagram_functor D X)

Equations

category_theory.grothendieck_topology.diagram_functor.category_theory.limits.preserves_limits X = {preserves_limits_of_shape := λ {J_1 : Type (max v u)} [_inst_4_1 : category_theory.category J_1], category_theory.grothendieck_topology.diagram_functor.category_theory.limits.preserves_limits_of_shape X J_1}

source

noncomputable def category_theory.grothendieck_topology.lift_to_plus_obj_limit_obj {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.concrete_category D] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)] {K : Type (max v u)} [category_theory.small_category K] [category_theory.fin_category K] [category_theory.limits.has_limits_of_shape K D] [category_theory.limits.preserves_limits_of_shape K (category_theory.forget D)] [category_theory.limits.reflects_limits_of_shape K (category_theory.forget D)] (F : K ⥤ Cᵒᵖ ⥤ D) (X : C) (S : category_theory.limits.cone (F ⋙ J.plus_functor D ⋙ (category_theory.evaluation Cᵒᵖ D).obj (opposite.op X))) :

S.X ⟶ (J.plus_obj (category_theory.limits.limit F)).obj (opposite.op X)

An auxiliary definition to be used in the proof that J.plus_functor D commutes with finite limits.

Equations

category_theory.grothendieck_topology.lift_to_plus_obj_limit_obj F X S = let e : category_theory.limits.colimit (category_theory.limits.limit (F ⋙ J.diagram_functor D X)) ≅ category_theory.limits.limit (category_theory.limits.colimit (F ⋙ J.diagram_functor D X).flip) := category_theory.limits.colimit_limit_iso (F ⋙ J.diagram_functor D X), t : J.diagram (category_theory.limits.limit F) X ≅ category_theory.limits.limit (F ⋙ J.diagram_functor D X) := (category_theory.limits.is_limit_of_preserves (J.diagram_functor D X) (category_theory.limits.limit.is_limit F)).cone_point_unique_up_to_iso (category_theory.limits.limit.is_limit (F ⋙ J.diagram_functor D X)), p : (J.plus_obj (category_theory.limits.limit F)).obj (opposite.op X) ≅ category_theory.limits.colimit (category_theory.limits.limit (F ⋙ J.diagram_functor D X)) := category_theory.limits.has_colimit.iso_of_nat_iso t, s : category_theory.limits.colimit (F ⋙ J.diagram_functor D X).flip ≅ F ⋙ J.plus_functor D ⋙ (category_theory.evaluation Cᵒᵖ D).obj (opposite.op X) := category_theory.nat_iso.of_components (λ (k : K), category_theory.limits.colimit_obj_iso_colimit_comp_evaluation (F ⋙ J.diagram_functor D X).flip k) _ in category_theory.limits.limit.lift (F ⋙ J.plus_functor D ⋙ (category_theory.evaluation Cᵒᵖ D).obj (opposite.op X)) S ≫ (category_theory.limits.has_limit.iso_of_nat_iso s.symm).hom ≫ e.inv ≫ p.inv

source

theorem category_theory.grothendieck_topology.lift_to_plus_obj_limit_obj_fac {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.concrete_category D] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)] {K : Type (max v u)} [category_theory.small_category K] [category_theory.fin_category K] [category_theory.limits.has_limits_of_shape K D] [category_theory.limits.preserves_limits_of_shape K (category_theory.forget D)] [category_theory.limits.reflects_limits_of_shape K (category_theory.forget D)] (F : K ⥤ Cᵒᵖ ⥤ D) (X : C) (S : category_theory.limits.cone (F ⋙ J.plus_functor D ⋙ (category_theory.evaluation Cᵒᵖ D).obj (opposite.op X))) (k : K) :

category_theory.grothendieck_topology.lift_to_plus_obj_limit_obj F X S ≫ (J.plus_map (category_theory.limits.limit.π F k)).app (opposite.op X) = S.π.app k

source

@[protected, instance]

noncomputable def category_theory.grothendieck_topology.plus_functor.category_theory.limits.preserves_limits_of_shape {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.concrete_category D] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)] (K : Type (max v u)) [category_theory.small_category K] [category_theory.fin_category K] [category_theory.limits.has_limits_of_shape K D] [category_theory.limits.preserves_limits_of_shape K (category_theory.forget D)] [category_theory.limits.reflects_limits_of_shape K (category_theory.forget D)] :

category_theory.limits.preserves_limits_of_shape K (J.plus_functor D)

Equations

category_theory.grothendieck_topology.plus_functor.category_theory.limits.preserves_limits_of_shape K = {preserves_limit := id (λ (F : K ⥤ Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit_of_evaluation (J.plus_functor D) F (λ (X : Cᵒᵖ), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) {lift := λ (S : category_theory.limits.cone (F ⋙ J.plus_functor D ⋙ (category_theory.evaluation Cᵒᵖ D).obj X)), category_theory.grothendieck_topology.lift_to_plus_obj_limit_obj F (opposite.unop X) S, fac' := _, uniq' := _}))}

source

@[protected, instance]

noncomputable def category_theory.grothendieck_topology.plus_functor.category_theory.limits.preserves_finite_limits {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.concrete_category D] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)] [category_theory.limits.has_finite_limits D] [category_theory.limits.preserves_finite_limits (category_theory.forget D)] [category_theory.reflects_isomorphisms (category_theory.forget D)] :

category_theory.limits.preserves_finite_limits (J.plus_functor D)

Equations

category_theory.grothendieck_topology.plus_functor.category_theory.limits.preserves_finite_limits = category_theory.limits.preserves_finite_limits_of_preserves_finite_limits_of_size (J.plus_functor D) (λ (K : Type (max v u)) (𝒥 : category_theory.small_category K) (hJ : category_theory.fin_category K), category_theory.grothendieck_topology.plus_functor.category_theory.limits.preserves_limits_of_shape K)

source

@[protected, instance]

noncomputable def category_theory.grothendieck_topology.sheafification.category_theory.limits.preserves_limits_of_shape {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.concrete_category D] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)] (K : Type (max v u)) [category_theory.small_category K] [category_theory.fin_category K] [category_theory.limits.has_limits_of_shape K D] [category_theory.limits.preserves_limits_of_shape K (category_theory.forget D)] [category_theory.limits.reflects_limits_of_shape K (category_theory.forget D)] :

category_theory.limits.preserves_limits_of_shape K (J.sheafification D)

Equations

category_theory.grothendieck_topology.sheafification.category_theory.limits.preserves_limits_of_shape K = category_theory.limits.comp_preserves_limits_of_shape (J.plus_functor D) (J.plus_functor D)

source

@[protected, instance]

noncomputable def category_theory.grothendieck_topology.sheafification.category_theory.limits.preserves_finite_limits {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.concrete_category D] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)] [category_theory.limits.has_finite_limits D] [category_theory.limits.preserves_finite_limits (category_theory.forget D)] [category_theory.reflects_isomorphisms (category_theory.forget D)] :

category_theory.limits.preserves_finite_limits (J.sheafification D)

Equations

category_theory.grothendieck_topology.sheafification.category_theory.limits.preserves_finite_limits = category_theory.limits.comp_preserves_finite_limits (J.plus_functor D) (J.plus_functor D)

source

@[protected, instance]

noncomputable def category_theory.presheaf_to_Sheaf.limits.preserves_limits_of_shape {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.concrete_category D] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)] [category_theory.limits.preserves_limits (category_theory.forget D)] [category_theory.reflects_isomorphisms (category_theory.forget D)] (K : Type (max v u)) [category_theory.small_category K] [category_theory.fin_category K] [category_theory.limits.has_limits_of_shape K D] :

category_theory.limits.preserves_limits_of_shape K (category_theory.presheaf_to_Sheaf J D)

Equations

category_theory.presheaf_to_Sheaf.limits.preserves_limits_of_shape K = {preserves_limit := id (λ (F : K ⥤ Cᵒᵖ ⥤ D), {preserves := λ (S : category_theory.limits.cone F) (hS : category_theory.limits.is_limit S), category_theory.limits.is_limit_of_reflects (category_theory.Sheaf_to_presheaf J D) (category_theory.limits.is_limit_of_preserves (J.sheafification D) hS)})}

source

@[protected, instance]

noncomputable def category_theory.presheaf_to_Sheaf.limits.preserves_finite_limits {C : Type (max v u)} [category_theory.category C] {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.concrete_category D] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)] [category_theory.limits.preserves_limits (category_theory.forget D)] [category_theory.reflects_isomorphisms (category_theory.forget D)] [category_theory.limits.has_finite_limits D] :

category_theory.limits.preserves_finite_limits (category_theory.presheaf_to_Sheaf J D)

Equations

category_theory.presheaf_to_Sheaf.limits.preserves_finite_limits = category_theory.limits.preserves_finite_limits_of_preserves_finite_limits_of_size (category_theory.presheaf_to_Sheaf J D) (λ (J_1 : Type (max v u)) (𝒥 : category_theory.small_category J_1) (hJ : category_theory.fin_category J_1), category_theory.presheaf_to_Sheaf.limits.preserves_limits_of_shape J_1)

mathlib3 documentation

Left exactness of sheafification #