le_finestTopology — Mathlib

English

If each P ∈ Ps is a J-sheaf, then J is contained in the finest topology making all Ps sheaves.

Русский

Если каждый P ∈ Ps является J-шейфом, то J содержится в наилучшей топологии, делающей все Ps шейфами.

LaTeX

$$$\\forall P\\in Ps:\\; P\\text{ is a } J\\text{-sheaf} \\Rightarrow J \\le \\mathrm{finestTopology}(Ps)$$$

Lean4

/-- Check that if each `P ∈ Ps` is a sheaf for `J`, then `J` is a subtopology of `finestTopology Ps`.
-/
theorem le_finestTopology (Ps : Set (Cᵒᵖ ⥤ Type v)) (J : GrothendieckTopology C) (hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P) :
    J ≤ finestTopology Ps := by
  rintro X S hS _ ⟨⟨_, _, ⟨P, hP, rfl⟩, rfl⟩, rfl⟩
  intro Y f
  exact hJ P hP (S.pullback f) (J.pullback_stable f hS)

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