instSurjectiveDescI₀SchemeF — Mathlib

English

For any prezero hypercover 𝒰 of X, the sigma-desc map from the indexed family 𝒰.f i to X is surjective.

Русский

Для любого преднулевого гиперпокрытия 𝒰 схемы X сопоставление sigma-desc от семейства 𝒰.f i к X сюръективно.

LaTeX

$$$\mathrm{Surjective}(\mathrm{Limits.Sigma.desc}\ \text{fun } i \mapsto 𝒰.f_i)$$$

Lean4

instance {X : Scheme.{u}} {P : MorphismProperty Scheme.{u}} (𝒰 : X.Cover (Scheme.precoverage P)) :
    Surjective (Limits.Sigma.desc fun i ↦ 𝒰.f i) :=
  Surjective.sigmaDesc_of_union_range_eq_univ 𝒰.iUnion_range

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