English
F preserves sheafification iff the adjunction data imply the isomorphism condition on sheaf compose after whiskering, equivalently for all P.
Русский
F сохраняет шарообразование эквивалентно условию изогломления композиции после whiskering во всём P.
LaTeX
$$$J.PreservesSheafification F \iff \forall P, IsIso (G_2.map (whiskerRight (adj_1.unit.app P) F))$$$
Lean4
theorem preservesSheafification_iff_of_adjunctions (adj₂ : G₂ ⊣ sheafToPresheaf J B) :
J.PreservesSheafification F ↔ ∀ (P : Cᵒᵖ ⥤ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F)) :=
by
simp only [← J.W_iff_isIso_map_of_adjunction adj₂]
constructor
· intro _ P
apply W_of_preservesSheafification
rw [J.W_iff_isIso_map_of_adjunction adj₁]
infer_instance
· intro h
constructor
intro P₁ P₂ f hf
rw [J.W_iff_isIso_map_of_adjunction adj₁] at hf
dsimp [MorphismProperty.inverseImage]
rw [← (W _).postcomp_iff _ _ (h P₂), ← whiskerRight_comp]
erw [adj₁.unit.naturality f]
dsimp only [Functor.comp_map]
rw [whiskerRight_comp, (W _).precomp_iff _ _ (h P₁)]
apply Localization.LeftBousfield.W_of_isIso
