mem_overGrothendieckTopology — Mathlib

English

Characterization of when a sieve lies in the over Grothendieck topology via covers by 𝒰.

Русский

Характеризация принадлежности сита к overGrothendieckTopology через покрытия 𝒰.

LaTeX

$$$R \\in S.overGrothendieckTopology P X \\leftrightarrow \\exists 𝒰, 𝒰.Over S, 𝒰.toPresieveOver \\le R.arrows$$$

Lean4

theorem mem_overGrothendieckTopology (X : Over S) (R : Sieve X) :
    R ∈ S.overGrothendieckTopology P X ↔
      ∃ (𝒰 : Cover.{u} (precoverage P) X.left) (_ : 𝒰.Over S), 𝒰.toPresieveOver ≤ R.arrows :=
  by
  rw [overGrothendieckTopology_eq_toGrothendieck_overPretopology]
  constructor
  · rintro ⟨T, ⟨𝒰, h, rfl⟩, hle⟩
    use 𝒰, h
  · rintro ⟨𝒰, h𝒰, hle⟩
    exact ⟨𝒰.toPresieveOver, ⟨𝒰, h𝒰, rfl⟩, hle⟩

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