mem_grothendieckTopology — Mathlib

English

A sieve S on U belongs to the Grothendieck topology if and only if for every point x in the underlying open, there exists an object V and a morphism f: V→U with S.arrows f and x lying in V's open.

Русский

Сито S на U принадлежит топологии Гротендика тогда и только тогда, когда для каждой точки x в соответствующем открытом множестве существует объект V и морфизм f: V→U such that S содержит стрелы f и x ∈ V.

LaTeX

$$$S\\in grothendieckTopology\ \ X\\ U\\iff \\forall x\\in U^{toOpens},\\ \\exists V\\ ,\\ f:V\\to U,\\ S.arrows f \\land x\\in V^{toOpens}$$$

Lean4

theorem mem_grothendieckTopology {U : X.AffineZariskiSite} {S : Sieve U} :
    S ∈ grothendieckTopology X U ↔ ∀ x ∈ U.toOpens, ∃ (V : _) (f : V ⟶ U), S.arrows f ∧ x ∈ V.toOpens :=
  by
  apply forall₂_congr fun x hxU ↦ ⟨?_, ?_⟩
  · rintro ⟨V, f, ⟨W, g, h, hg, rfl⟩, hxV⟩
    exact ⟨W, g, hg, h.le hxV⟩
  · rintro ⟨W, g, hg, hxW⟩
    exact ⟨W.toOpens, homOfLE (toOpens_mono g.le), ⟨W, g, 𝟙 _, hg, rfl⟩, hxW⟩

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