sigmaDesc_of_union_range_eq_univ — Mathlib

English

Let {Y_i → X} be a family of morphisms indexed by i, and suppose the union of their base ranges covers X. Then the canonical morphism from the coproduct of all Y_i to X is surjective.

Русский

Пусть имеется семейство морфизмов {Y_i → X} с индексами i, чьё покрытие образов на базисах открывает X. Тогда каноническое морфизм от копроизодукта всех Y_i к X сюръективен.

LaTeX

$$$\mathrm{Surjective}(\mathrm{Limits.Sigma.desc}\ f)$$$

Lean4

theorem sigmaDesc_of_union_range_eq_univ {X : Scheme.{u}} {ι : Type v} [Small.{u} ι] {Y : ι → Scheme.{u}}
    {f : ∀ i, Y i ⟶ X} (H : ⋃ i, Set.range (f i).base = Set.univ) : Surjective (Limits.Sigma.desc f) :=
  by
  refine ⟨fun x ↦ ?_⟩
  simp_rw [Set.eq_univ_iff_forall, Set.mem_iUnion] at H
  obtain ⟨i, x, rfl⟩ := H x
  use (Limits.Sigma.ι (fun i ↦ Y i) i).base x
  rw [← Scheme.comp_base_apply, Limits.Sigma.ι_desc]

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