eval_section_surjective_of_surjective

English

If F is Mittag-Leffler and all maps are surjective, then for any i the evaluation map s ↦ s.obj i on sections is surjective.

Русский

Если F удовлетворяет Mittag-Leffler и все отображения сюръективны, то для любого i отображение s ↦ s.obj i на секциях сюръективно.

LaTeX

$$$\text{If } FIsMittagLeffler \text{ then } (\lambda s: F.sections \to F.obj i)\text{ is surjective}.$$$

Lean4

theorem eval_section_surjective_of_surjective (i : J) : (fun s : F.sections => s.val i).Surjective := fun x =>
  by
  let s : Set (F.obj i) := { x }
  haveI := F.toPreimages_nonempty_of_surjective s Fsur (singleton_nonempty x)
  obtain ⟨sec, h⟩ := nonempty_sections_of_finite_cofiltered_system (F.toPreimages s)
  refine ⟨⟨fun j => (sec j).val, fun jk => by simpa [Subtype.ext_iff] using h jk⟩, ?_⟩
  · have := (sec i).prop
    simp only [mem_iInter, mem_preimage] at this
    have := this (𝟙 i)
    rwa [map_id_apply] at this

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