instIsConstantObjSheafSheafCompose

English

IsConstant is preserved by the equivalence between dense-subsite-induced sheaves and the original topology: the inverse image of F is constant iff F is constant.

Русский

Константность сохраняется через эквивалентность между категориями касательных плотной подполоски: обратное изображение F константно тогда и только тогда, когда F константно.

LaTeX

$$$((\text{sheafEquiv } G J K D).inverse.obj F).IsConstant(J) \iff IsConstant(K,F)$$$

Lean4

instance [h : F.IsConstant J] : ((sheafCompose J U).obj F).IsConstant J :=
  by
  obtain ⟨Y, ⟨i⟩⟩ := h
  exact
    ⟨U.obj Y,
      ⟨(fullyFaithfulSheafToPresheaf _ _).preimageIso
          (((sheafifyComposeIso J U ((const Cᵒᵖ).obj Y)).symm ≪≫
                (presheafToSheaf J B ⋙ sheafToPresheaf J B).mapIso (constComp Cᵒᵖ Y U)).symm ≪≫
            (sheafToPresheaf _ _).mapIso ((sheafCompose J U).mapIso i))⟩⟩

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