English
The limit of a cofiltered diagram of nonempty quasi-compact schemes with affine transition maps is nonempty.
Русский
Предельный объект кофильтрованной диаграммы из непустых квазикомпактных схем с аффинными переходами также непуст.
LaTeX
$$$Nonempty\ c.pt$ under assumptions: [IsCofilteredOrEmpty I], [∀ f, IsAffineHom (D.map f)], [∀ i, Nonempty (D.obj i)], [∀ i, CompactSpace (D.obj i)]$$
Lean4
/-- Suppose we have a cofiltered diagram of nonempty quasi-compact schemes,
whose transition maps are affine. Then the limit is also nonempty.
-/
@[stacks 01Z2]
theorem nonempty_of_isLimit [IsCofilteredOrEmpty I] [∀ {i j} (f : i ⟶ j), IsAffineHom (D.map f)]
[∀ i, Nonempty (D.obj i)] [∀ i, CompactSpace (D.obj i)] : Nonempty c.pt := by
classical
cases isEmpty_or_nonempty I
· have e := (isLimitEquivIsTerminalOfIsEmpty _ _ hc).uniqueUpToIso specULiftZIsTerminal
exact Nonempty.map e.inv.base inferInstance
· have i := Nonempty.some ‹Nonempty I›
have : IsCofiltered I := ⟨⟩
let 𝒰 := (D.obj i).affineCover.finiteSubcover
have (i' : _) : IsAffine (𝒰.X i') := inferInstanceAs (IsAffine (Spec _))
obtain ⟨j, H⟩ : ∃ j : 𝒰.I₀, ∀ {i'} (f : i' ⟶ i), Nonempty ((𝒰.pullback₁ (D.map f)).X j) :=
by
by_contra! H
choose i' f hf using H
let g (j) :=
IsCofiltered.infTo (insert i (Finset.univ.image i'))
(Finset.univ.image fun j : 𝒰.I₀ ↦ ⟨_, _, by simp, by simp, f j⟩) (X := j)
have (j : 𝒰.I₀) : IsEmpty ((𝒰.pullback₁ (D.map (g i (by simp)))).X j) :=
by
let F : (𝒰.pullback₁ (D.map (g i (by simp)))).X j ⟶ (𝒰.pullback₁ (D.map (f j))).X j :=
pullback.map _ _ _ _ (D.map (g _ (by simp))) (𝟙 _) (𝟙 _)
(by
rw [← D.map_comp, IsCofiltered.infTo_commutes]
· simp [g]
· simp
· exact Finset.mem_image_of_mem _ (Finset.mem_univ _))
(by simp)
exact Function.isEmpty F.base
obtain ⟨x, -⟩ := Cover.covers (𝒰.pullback₁ (D.map (g i (by simp)))) (Nonempty.some inferInstance)
exact (this _).elim x
let F := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget _
have (i' : _) : IsAffine (F.obj i') :=
have : IsAffineHom (pullback.snd (D.map i'.hom) (𝒰.f j)) := MorphismProperty.pullback_snd _ _ inferInstance
isAffine_of_isAffineHom (pullback.snd (D.map i'.hom) (𝒰.f j))
have (i' : _) : Nonempty (F.obj i') := H i'.hom
let e : F ⟶ (F ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := Functor.whiskerLeft F ΓSpec.adjunction.unit
have (i : _) : IsIso (e.app i) := IsAffine.affine
have : IsIso e := NatIso.isIso_of_isIso_app e
let c' : LimitCone F :=
⟨_,
(IsLimit.postcomposeInvEquiv (asIso e) _).symm
(isLimitOfPreserves Scheme.Spec (limit.isLimit (F ⋙ Scheme.Γ.rightOp)))⟩
have : Nonempty c'.1.pt :=
by
apply (config := { allowSynthFailures := true }) PrimeSpectrum.instNonemptyOfNontrivial
have (i' : _) : Nontrivial ((F ⋙ Scheme.Γ.rightOp).leftOp.obj i') :=
by
apply (config := { allowSynthFailures := true }) Scheme.component_nontrivial
simp
exact
CommRingCat.FilteredColimits.nontrivial (isColimitCoconeLeftOpOfCone _ (limit.isLimit (F ⋙ Scheme.Γ.rightOp)))
let α : F ⟶ Over.forget _ ⋙ D :=
Functor.whiskerRight (Functor.whiskerLeft (Over.post D) (Over.mapPullbackAdj (𝒰.f j)).counit) (Over.forget _)
exact
this.map
(((Functor.Initial.isLimitWhiskerEquiv (Over.forget i) c).symm hc).lift ((Cones.postcompose α).obj c'.1)).base
