instIsCoverDense — Mathlib

English

The isSheaf property for a presheaf in the coherent topology is equivalent to the equalizer condition.

Русский

Свойство равномерности (sheaf) для префункторa в когерентной топологии эквивалентно условию равнозначителя.

LaTeX

$$equalizerCondition_iff_isSheaf F$$

Lean4

instance : F.IsCoverDense (coherentTopology _) :=
  by
  refine F.isCoverDense_of_generate_singleton_functor_π_mem _ fun B ↦ ⟨_, F.effectiveEpiOver B, ?_⟩
  apply Coverage.Saturate.of
  refine ⟨Unit, inferInstance, fun _ => F.effectiveEpiOverObj B, fun _ => F.effectiveEpiOver B, ?_, ?_⟩
  · funext;
    ext -- Do we want `Presieve.ext`?

    refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩
    rintro ⟨⟩
    simp
  · rw [← effectiveEpi_iff_effectiveEpiFamily]
    infer_instance

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