isCoverDense_of_generate_singleton_functor_π_mem

English

If a functor is cover-dense in K, then the generated sieve at any X is in K X.

Русский

Если функтор является cover-dense по отношению к K, то порожденная в X несетается в K X.

LaTeX

$$$G.IsCoverDense K \\Rightarrow \\; \\text{coverByImage } G X \\in K X$$$

Lean4

theorem isCoverDense_of_generate_singleton_functor_π_mem (G : C ⥤ D) (K : GrothendieckTopology D)
    (h : ∀ B, ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ K B) : G.IsCoverDense K where
  is_cover
    B := by
    obtain ⟨X, f, h⟩ := h B
    refine K.superset_covering ?_ h
    intro Y f ⟨Z, g, _, h, w⟩
    cases h
    exact ⟨⟨_, g, _, w⟩⟩

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