mem_grothendieckTopology_iff — Mathlib

English

A restatement of the equality between jointlySurjectiveTopology and the Grothendieck version derived from jointlySurjectivePretopology.

Русский

Переформулировка равенства между jointlySurjectiveTopology и его версией в топологии Гротендик, полученной из jointlySurjectivePretopology.

LaTeX

$$$jointlySurjectiveTopology = jointlySurjectivePretopology.toGrothendieck$$$

Lean4

theorem mem_grothendieckTopology_iff {X : Scheme.{u}} {S : Sieve X} :
    S ∈ grothendieckTopology P X ↔ ∃ (𝒰 : Cover.{u} (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S :=
  by
  simp_rw [grothendieckTopology, Pretopology.mem_toGrothendieck]
  refine ⟨fun ⟨R, hR, hle⟩ ↦ ?_, fun ⟨𝒰, hle⟩ ↦ ⟨.ofArrows 𝒰.X 𝒰.f, 𝒰.mem_pretopology, hle⟩⟩
  rw [mem_pretopology_iff] at hR
  obtain ⟨𝒰, rfl⟩ := hR
  use 𝒰.ulift, le_trans (fun Y g ⟨i⟩ ↦ .mk _) hle

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