ofArrows_mem_precoverage_iff — Mathlib

English

For any X, ι, and family f: ∀ i, X_i ⟶ S, the arrow family 𝒰.ofArrows ∼ is in precoverage P X iff every point of S is hit by some base of f i and P holds for each f i.

Русский

Для любого X и семейства ф, состоящего из стрелок f_i: X_i → S, семейство стрелок 𝒰.ofArrows принадлежит precoverage P X тогда и только тогда, когда каждый элемент S попадает под некоторым основанием f_i, и каждое f_i удовлетворяет P.

LaTeX

$$\\ofArrows_mem_precoverage_iff$$

Lean4

@[simp]
theorem ofArrows_mem_precoverage_iff {S : Scheme.{u}} {ι : Type*} {X : ι → Scheme.{u}} {f : ∀ i, X i ⟶ S} :
    .ofArrows X f ∈ precoverage P S ↔ (∀ x, ∃ i, x ∈ Set.range (f i).base) ∧ ∀ i, P (f i) :=
  by
  simp_rw [← Scheme.forget_map, ← Scheme.forget_obj, ← Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff]
  exact ⟨fun hmem ↦ ⟨hmem.1, fun i ↦ hmem.2 ⟨i⟩⟩, fun h ↦ ⟨h.1, fun {Y} g ⟨i⟩ ↦ h.2 i⟩⟩

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