mem_grothendieckTopology_iff_sectionsOfPresieve

English

A sieve S on U lies in the Grothendieck topology iff the span of its sections equals the top submodule

Русский

Сито S на U принадлежит Grothendieck topology тогда и только тогда, когда порождающее множество секций имеет полноту

LaTeX

$$$S \in grothendieckTopology X U \iff \mathrm{span}(\text{sectionsOfPresieve } S.1) = \top$$$

Lean4

theorem mem_grothendieckTopology_iff_sectionsOfPresieve {U : X.AffineZariskiSite} {S : Sieve U} :
    S ∈ grothendieckTopology X U ↔ Ideal.span (sectionsOfPresieve S.1) = ⊤ := by
  rw [← generate_presieveOfSections_mem_grothendieckTopology, presieveOfSections_sectionsOfPresieve,
    Sieve.generate_sieve]

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