Π Rᵢ-Points of Schemes

We show that the canonical map X(Π Rᵢ) ⟶ Π X(Rᵢ) (AlgebraicGeometry.pointsPi) is injective and surjective under various assumptions.

theorem AlgebraicGeometry.Ideal.span_eq_top_of_span_image_evalRingHom {ι : Type u_2} {R : ι → Type u_1} [(i : ι) → CommRing (R i)] (s : Set ((i : ι) → R i)) (hs : s.Finite) (hs' : ∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun (x : ι) => R x) i) '' s) = ⊤) : Ideal.span s = ⊤

theorem AlgebraicGeometry.eq_top_of_sigmaSpec_subset_of_isCompact {ι : Type u} (R : ι → CommRingCat) (U : (Spec ↧((i : ι) → ↑(R i))).Opens) (V : Set ↥(Spec ↧((i : ι) → ↑(R i)))) (hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V) (hV' : IsCompact V) (hVU : V ⊆ ↑U) : U = ⊤

theorem AlgebraicGeometry.eq_bot_of_comp_quotientMk_eq_sigmaSpec {ι : Type u} (R : ι → CommRingCat) (I : Ideal ((i : ι) → ↑(R i))) (f : (∐ fun (i : ι) => Spec (R i)) ⟶ Spec ↧(((i : ι) → ↑(R i)) ⧸ I)) (hf : CategoryTheory.CategoryStruct.comp f (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = sigmaSpec R) : I = ⊥

theorem AlgebraicGeometry.isIso_of_comp_eq_sigmaSpec {ι : Type u} (R : ι → CommRingCat) {V : Scheme} (f : (∐ fun (i : ι) => Spec (R i)) ⟶ V) (g : V ⟶ Spec ↧((i : ι) → ↑(R i))) [IsImmersion g] [CompactSpace ↥V] (hU' : CategoryTheory.CategoryStruct.comp f g = sigmaSpec R) : CategoryTheory.IsIso g

If V is a locally closed subscheme of Spec (Π Rᵢ) containing ∐ Spec Rᵢ, then V = Spec (Π Rᵢ).

noncomputable def AlgebraicGeometry.pointsPi {ι : Type u} (R : ι → CommRingCat) (X : Scheme) : (Spec ↧((i : ι) → ↑(R i)) ⟶ X) → (i : ι) → Spec (R i) ⟶ X

The canonical map X(Π Rᵢ) ⟶ Π X(Rᵢ). This is injective if X is quasi-separated, surjective if X is affine, or if X is compact and each Rᵢ is local.

Equations

• AlgebraicGeometry.pointsPi R X f i = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) => ↑(R x)) i))) f

theorem AlgebraicGeometry.pointsPi_injective {ι : Type u} (R : ι → CommRingCat) (X : Scheme) [QuasiSeparatedSpace ↥X] : Function.Injective (pointsPi R X)

theorem AlgebraicGeometry.pointsPi_surjective_of_isAffine {ι : Type u} (R : ι → CommRingCat) (X : Scheme) [IsAffine X] : Function.Surjective (pointsPi R X)

theorem AlgebraicGeometry.pointsPi_surjective {ι : Type u} (R : ι → CommRingCat) (X : Scheme) [CompactSpace ↥X] [∀ (i : ι), IsLocalRing ↑(R i)] : Function.Surjective (pointsPi R X)