mem_smallGrothendieckTopology — Mathlib

English

Characterization of small Grothendieck topology membership on a fiber over S.

Русский

Характеризация принадлежности к малой топологии Гротендего над основанием S.

LaTeX

$$$R \\in S.smallGrothendieckTopology P X \\iff \\exists 𝒰, 𝒰.Over S, 𝒰.toPresieveOverProp \\le R.arrows$$$

Lean4

theorem mem_smallGrothendieckTopology [P.HasOfPostcompProperty P] (X : P.Over ⊤ S) (R : Sieve X) :
    R ∈ S.smallGrothendieckTopology P X ↔
      ∃ (𝒰 : Cover.{u} (precoverage P) X.left) (_ : 𝒰.Over S) (h : ∀ j, P (𝒰.X j ↘ S)),
        𝒰.toPresieveOverProp h ≤ R.arrows :=
  by
  rw [smallGrothendieckTopology_eq_toGrothendieck_smallPretopology]
  constructor
  · rintro ⟨T, ⟨𝒰, h, p, rfl⟩, hle⟩
    use 𝒰, h, p
  · rintro ⟨𝒰, h𝒰, p, hle⟩
    exact ⟨𝒰.toPresieveOverProp p, ⟨𝒰, h𝒰, p, rfl⟩, hle⟩

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