English
The hom app value of pushforward-continuous sheafification compatibility equals a lifted sheaf value.
Русский
Значение отображения типа hom для совместимости pushforward-continuous sheafification равно указанию подъема.
LaTeX
$$$\\bigl((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F\\bigr).val = \\dots$$$
Lean4
theorem toSheafify_pullbackSheafificationCompatibility (F : Dᵒᵖ ⥤ A) :
toSheafify J (G.op ⋙ F) ≫ ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
whiskerLeft _ (toSheafify K _) :=
by
let adj₁ := G.op.ranAdjunction A
let adj₂ := sheafificationAdjunction J A
let adj₃ := sheafificationAdjunction K A
let adj₄ := G.sheafAdjunctionCocontinuous A J K
change
adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
(sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F) =
((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F)
apply (adj₁.homEquiv _ _).injective
have eq := (adj₁.comp adj₂).unit_leftAdjointUniq_hom_app (adj₃.comp adj₄) F
rw [Adjunction.comp_unit_app, Adjunction.comp_unit_app, comp_map, Category.assoc] at eq
rw [adj₁.homEquiv_unit, Functor.map_comp, eq]
apply (adj₁.homEquiv _ _).symm.injective
simp only [Adjunction.homEquiv_counit, map_comp, Category.assoc, Adjunction.homEquiv_unit, Adjunction.unit_naturality]
congr 3
exact G.sheafAdjunctionCocontinuous_unit_app_val A J K ((presheafToSheaf K A).obj F)
