Module

exists_isAffineOpen_forall_mem_of_isAffineHom_proj.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_isAffineOpen_forall_mem_of_isAffineHom_proj

2 declarations indexed from sourceView source ↗

Module documentation

Affine neighbourhoods of finitely many points over projective space

Finitely many points of a scheme affine over a projective spectrum lie in a common affine open, obtained from a homogeneous basic open of the projective spectrum.

Imports4

Mathlib.Util.WithWeakNamespace
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Mathlib.AlgebraicGeometry.Morphisms.Affine
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HomogeneousIdeal_exists_homogeneous_pos_mem_forall_notMem

Imported by3

theorem

exists_basicOpen_le_forall_mem_of_finset

L43 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_isAffineOpen_forall_mem_of_isAffineHom_proj.AlgebraicGeometry.Proj.exists_basicOpen_le_forall_mem_of_finset

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_isAffineOpen_forall_mem_of_isAffineHom_proj
universe u v
open CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section ProjOpen
variable {A σ : Type*} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜]
open scoped _root_.AlgebraicGeometry.Proj in

Lean source · statement

theorem Proj.exists_basicOpen_le_forall_mem_of_finset (U : (Proj 𝒜).Opens) (S : Finset (Proj 𝒜))
    (hS : ∀ x ∈ S, x ∈ U) :
    ∃ (n : ℕ) (f : A), 0 < n ∧ f ∈ 𝒜 n ∧ Proj.basicOpen 𝒜 f ≤ U ∧ ∀ x ∈ S, x ∈ Proj.basicOpen 𝒜
        f

theorem