mem_iff_exists_zeroHypercover — Mathlib

English

A presieve R on X belongs to the precoverage J X if and only if there exists a ZeroHypercover 𝒰 over X such that R is obtained from 𝒰 by taking arrows to X.

Русский

Пресив X принадлежит предпокрытию J X тогда и только тогда, когда существует нулевой гиперохват 𝒰 над X, такой что R получается из 𝒰 через стрелки в X.

LaTeX

$$$R \\in J(X) \\iff \\exists 𝒰:\\ ZeroHypercover^{max(u,v)} J X,\\; R = Presieve.ofArrows 𝒰.X 𝒰.f$$$

Lean4

theorem mem_iff_exists_zeroHypercover {X : C} {R : Presieve X} :
    R ∈ J X ↔ ∃ (𝒰 : ZeroHypercover.{max u v} J X), R = Presieve.ofArrows 𝒰.X 𝒰.f :=
  by
  refine ⟨fun hR ↦ ?_, fun ⟨𝒰, hR⟩ ↦ hR ▸ 𝒰.mem₀⟩
  obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows
  use ⟨⟨ι, Y, f⟩, hR⟩

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