Module

SmoothProperCurve_FiniteMapData_exists_isAffineOpen_le_preimage_of_finset.lean

Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_FiniteMapData_exists_isAffineOpen_le_preimage_of_finset

1 declaration indexed from sourceView source ↗

Module documentation

Affine neighbourhoods from finite-map data

Finite-map data on a smooth proper curve gives an affine open containing prescribed finitely many points over a fixed affine open of the base.

Imports5

Imported by3

theorem

exists_isAffineOpen_le_preimage_of_finset

L38 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.exists_isAffineOpen_le_preimage_of_finset

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_isAffineOpen_le_preimage_of_finset
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
with_weak_namespace _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData

Lean source · statement

theorem exists_isAffineOpen_le_preimage_of_finset
    {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : SmoothProperCurve.FiniteMapData c ε)
    (V : (Spec (CommRingCat.of R)).affineOpens) (F : Finset C)
    (hF : ∀ x ∈ F, c x ∈ (V : (Spec (CommRingCat.of R)).Opens)) :
    ∃ U : C.Opens, IsAffineOpen U ∧ U ≤ c ⁻¹ᵁ (V : (Spec (CommRingCat.of R)).Opens) ∧ ∀ x ∈ F, x
        ∈ U

Module documentation

Affine neighbourhoods from finite-map data

Declarations

exists_isAffineOpen_le_preimage_of_finset