mathlibdocumentation

category_theory.sites.compatible_sheafification

In this file, we prove that sheafification is compatible with functors which preserve the correct limits and colimits.

noncomputable def category_theory.grothendieck_topology.sheafify_comp_iso {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) :
J.sheafify P F J.sheafify (P F)

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F.

Use the lemmas whisker_right_to_sheafify_sheafify_comp_iso_hom, to_sheafify_comp_sheafify_comp_iso_inv and sheafify_comp_iso_inv_eq_sheafify_lift to reduce the components of this isomorphisms to a state that can be handled using the universal property of sheafification.

Equations
noncomputable def category_theory.grothendieck_topology.sheafification_whisker_left_iso {C : Type u} {D : Type w₁} {E : Type w₂} [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] (P : Cᵒᵖ D) [Π (F : D E) (X : C), ] [Π (F : D E) (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] :
.obj (J.sheafify P) .obj P

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F, functorially in F.

Equations
@[simp]
theorem category_theory.grothendieck_topology.sheafification_whisker_left_iso_hom_app {C : Type u} {D : Type w₁} {E : Type w₂} [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] (P : Cᵒᵖ D) (F : D E) [Π (F : D E) (X : C), ] [Π (F : D E) (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] :
= P).hom
@[simp]
theorem category_theory.grothendieck_topology.sheafification_whisker_left_iso_inv_app {C : Type u} {D : Type w₁} {E : Type w₂} [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] (P : Cᵒᵖ D) (F : D E) [Π (F : D E) (X : C), ] [Π (F : D E) (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] :
= P).inv
noncomputable def category_theory.grothendieck_topology.sheafification_whisker_right_iso {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] :
F F

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F, functorially in P.

Equations
@[simp]
theorem category_theory.grothendieck_topology.sheafification_whisker_right_iso_hom_app {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) :
= P).hom
@[simp]
theorem category_theory.grothendieck_topology.sheafification_whisker_right_iso_inv_app {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) :
= P).inv
@[simp]
theorem category_theory.grothendieck_topology.whisker_right_to_sheafify_sheafify_comp_iso_hom_assoc {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) {X' : Cᵒᵖ E} (f' : J.sheafify (P F) X') :
P).hom f' = J.to_sheafify (P F) f'
@[simp]
theorem category_theory.grothendieck_topology.whisker_right_to_sheafify_sheafify_comp_iso_hom {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) :
P).hom = J.to_sheafify (P F)
@[simp]
theorem category_theory.grothendieck_topology.to_sheafify_comp_sheafify_comp_iso_inv_assoc {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) {X' : Cᵒᵖ E} (f' : J.sheafify P F X') :
J.to_sheafify (P F) P).inv f' = f'
@[simp]
theorem category_theory.grothendieck_topology.to_sheafify_comp_sheafify_comp_iso_inv {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) :
J.to_sheafify (P F) P).inv =
@[simp]
theorem category_theory.grothendieck_topology.sheafify_comp_iso_inv_eq_sheafify_lift {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) [Π (X : C), ]  :
P).inv = _