stalkPushforward_iso_of_isInducing

English

Same principle as above, asserting isomorphism of stalk pushforward under inducing maps.

Русский

То же самое для индуктивных отображений, изоморфизм стэла pushforward.

LaTeX

$$IsIso (F.stalkPushforward _ f x) under IsInducing f.$$

Lean4

theorem stalkPushforward_iso_of_isInducing {f : X ⟶ Y} (hf : IsInducing f) (F : X.Presheaf C) (x : X) :
    IsIso (F.stalkPushforward _ f x) :=
  by
  haveI := Functor.initial_of_adjunction (hf.adjunctionNhds x)
  convert (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).isIso_hom
  refine stalk_hom_ext _ fun U hU ↦ (stalkPushforward_germ _ f F _ x hU).trans ?_
  symm
  exact colimit.ι_pre ((OpenNhds.inclusion x).op ⋙ F) (OpenNhds.map f x).op _

Похожие утверждения