isContinuous_of_preservesOneHypercovers

English

If F preserves one hypercovers and J is generated by one hypercover, then F is continuous with respect to J and K.

Русский

Если F сохраняет одно гиперпокрытие и J порождается одним гиперпокрытием, то F непрерывен по J и K.

LaTeX

$$$[PreservesOneHypercovers\\ F\\ J\\ K]\\ [GrothendieckTopology.IsGeneratedByOneHypercovers\\ J] \\Rightarrow IsContinuous\\ F\\ J\\ K$$

Lean4

theorem isContinuous_of_preservesOneHypercovers [PreservesOneHypercovers.{w} F J K]
    [GrothendieckTopology.IsGeneratedByOneHypercovers.{w} J] : IsContinuous.{t} F J K where
  op_comp_isSheaf_of_types := by
    rintro ⟨P, hP⟩
    rw [← isSheaf_iff_isSheaf_of_type]
    exact F.op_comp_isSheaf_of_preservesOneHypercovers J K P hP

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