English
If X is a compact space and each R_i is a local ring, then pointsPi is surjective.
Русский
Если X компактна, и R_i — локальные кольца, то pointsPi сюръективен.
LaTeX
$$Surjectivity of pointsPi when [CompactSpace X] and ∀ i, IsLocalRing (R i).$$
Lean4
theorem pointsPi_surjective [CompactSpace X] [∀ i, IsLocalRing (R i)] : Function.Surjective (pointsPi R X) :=
by
intro f
let 𝒰 : X.OpenCover := X.affineCover.finiteSubcover
have (i : _) : ∃ j, Set.range (f i).base ⊆ (𝒰.f j).opensRange :=
by
refine ⟨𝒰.idx ((f i).base (IsLocalRing.closedPoint (R i))), ?_⟩
rintro _ ⟨x, rfl⟩
exact ((IsLocalRing.specializes_closedPoint x).map (f i).base.hom.2).mem_open (𝒰.f _).opensRange.2 (𝒰.covers _)
choose j hj using this
have (j₀ : _) :=
pointsPi_surjective_of_isAffine (ι := { i // j i = j₀ }) (R ·) (𝒰.X j₀)
(fun i ↦ IsOpenImmersion.lift (𝒰.f j₀) (f i.1) (by rcases i with ⟨i, rfl⟩; exact hj i))
choose g hg using this
simp_rw [funext_iff, pointsPi] at hg
let R' (j₀) := CommRingCat.of (Π i : { i // j i = j₀ }, R i)
let e : (Π i, R i) ≃+* Π j₀, R' j₀ :=
{ toFun f _ i := f i
invFun f i := f _ ⟨i, rfl⟩
right_inv _ := funext₂ fun j₀ i ↦ by rcases i with ⟨i, rfl⟩; rfl
map_mul' _ _ := rfl
map_add' _ _ := rfl }
refine ⟨Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀, ?_⟩
ext i : 1
have :
(Pi.evalRingHom (R ·) i).comp e.symm.toRingHom = (Pi.evalRingHom _ ⟨i, rfl⟩).comp (Pi.evalRingHom (R' ·) (j i)) :=
rfl
rw [pointsPi, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, this, CommRingCat.ofHom_comp, Spec.map_comp_assoc, ←
ι_sigmaSpec R', Category.assoc, IsIso.hom_inv_id_assoc, Sigma.ι_desc, ← Category.assoc, hg,
IsOpenImmersion.lift_fac]
