exists_mem_of_isClosed_of_nonempty

English

Given a cofiltered diagram of schemes with compatible nonempty closed qc sets Z_i, there exists a point s in the limit such that its projections lie in Z_i for all i.

Русский

Пусть имеется кофильтрована диаграмма схем вместе с совместимыми непустыми замкнутыми компактными множествами Z_i; тогда существует точка s в пределе, для которой проекции лежат в Z_i.

LaTeX

$$$\exists s\in c.pt, \forall i, (c.π.app i).base\,s \in Z_i$$$

Lean4

/-- Suppose we have a cofiltered diagram of schemes whose transition maps are affine. The limit of
a family of compatible nonempty quasicompact closed sets in the diagram is also nonempty.
-/
theorem exists_mem_of_isClosed_of_nonempty [IsCofilteredOrEmpty I] [∀ {i j} (f : i ⟶ j), IsAffineHom (D.map f)]
    (Z : ∀ (i : I), Set (D.obj i)) (hZc : ∀ (i : I), IsClosed (Z i)) (hZne : ∀ i, (Z i).Nonempty)
    (hZcpt : ∀ i, IsCompact (Z i)) (hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (D.map f).base (Z i) (Z i')) :
    ∃ (s : c.pt), ∀ i, (c.π.app i).base s ∈ Z i :=
  by
  let D' : I ⥤ Scheme :=
    { obj i := (vanishingIdeal ⟨Z i, hZc i⟩).subscheme
      map {X Y}
        f :=
        subschemeMap _ _ (D.map f)
          (by
            rw [map_vanishingIdeal, ← le_support_iff_le_vanishingIdeal]
            simpa [(hZc _).closure_subset_iff] using (hmapsTo f).subset_preimage)
      map_id _ := by simp [← cancel_mono (subschemeι _)]
      map_comp _ _ := by simp [← cancel_mono (subschemeι _)] }
  let ι : D' ⟶ D := { app i := subschemeι _, naturality _ _ _ := by simp [D'] }
  haveI {i j} (f : i ⟶ j) : IsAffineHom (D'.map f) :=
    by
    suffices IsAffineHom (D'.map f ≫ ι.app j) from .of_comp _ (ι.app j)
    simp only [subschemeMap_subschemeι, D', ι]
    infer_instance
  haveI _ (i) : Nonempty (D'.obj i) := Set.nonempty_coe_sort.mpr (hZne i)
  haveI _ (i) : CompactSpace (D'.obj i) := isCompact_iff_compactSpace.mp (hZcpt i)
  let c' : Cone D' :=
    { pt := (⨆ i, (vanishingIdeal ⟨Z i, hZc i⟩).comap (c.π.app i)).subscheme
      π :=
        { app i := subschemeMap _ _ (c.π.app i) (by simp [le_map_iff_comap_le, le_iSup_of_le i])
          naturality {i j} f := by simp [D', ← cancel_mono (subschemeι _)] } }
  let hc' : IsLimit c' :=
    { lift
        s :=
        IsClosedImmersion.lift (subschemeι _) (hc.lift ((Cones.postcompose ι).obj s))
          (by
            suffices ∀ i, vanishingIdeal ⟨Z i, hZc i⟩ ≤ (s.π.app i ≫ ι.app i).ker by
              simpa [← le_map_iff_comap_le, ← Scheme.Hom.ker_comp]
            refine fun i ↦ .trans ?_ (Scheme.Hom.le_ker_comp _ _)
            simp [ι])
      fac s i := by simp [← cancel_mono (subschemeι _), c', ι]
      uniq s m
        hm := by
        rw [← cancel_mono (subschemeι _)]
        refine hc.hom_ext fun i ↦ ?_
        simp [ι, c', ← hm] }
  have : Nonempty (⨆ i, (vanishingIdeal ⟨Z i, hZc i⟩).comap (c.π.app i)).support := Scheme.nonempty_of_isLimit D' c' hc'
  simpa using this

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