Module

OpenBoundary.lean

Nyll.AlgebraicCurves.Models.OpenBoundary

4 declarations indexed from sourceView source ↗

Module documentation

The actual finite boundary of an open subscheme of a proper curve

Imports3

Nyll.AlgebraicCurves.Models.Basic
Nyll.AlgebraicCurves.Models.Finite_compl_of_isOpen
Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Imported by3

def

openBoundaryPlaces

L27 ↗

AlgebraicCurve.CurveModel.openBoundaryPlaces

Documentation

The omitted places are exactly those whose actual closed points are outside the image of the given open immersion.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isProper CurveModel.isIntegral CurveModel.smooth
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]

Lean source · statement

def openBoundaryPlaces (M : CurveModel K F)
    {X : Scheme.{u}} (j : X ⟶ M.C) : Set (Place K F)

theorem

place_not_mem_openBoundaryPlaces

L32 ↗

AlgebraicCurve.CurveModel.place_not_mem_openBoundaryPlaces

Documentation

Interior points avoid the actual boundary set.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isProper CurveModel.isIntegral CurveModel.smooth
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]

Lean source · statement

theorem place_not_mem_openBoundaryPlaces
    (M : CurveModel K F) {X : Scheme.{u}} (j : X ⟶ M.C)
    (y : X) (x : closedPoints M.C) (hx : x.val = j y) :
    M.placeOfPoint x ∉ M.openBoundaryPlaces j

theorem

openBoundaryPlaces_finite

L41 ↗

AlgebraicCurve.CurveModel.openBoundaryPlaces_finite

Documentation

The geometric boundary is finite for a nonempty open curve.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isProper CurveModel.isIntegral CurveModel.smooth
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]

Lean source · statement

theorem openBoundaryPlaces_finite
    (M : CurveModel K F) {X : Scheme.{u}} [Nonempty X]
    (j : X ⟶ M.C) [IsOpenImmersion j] :
    (M.openBoundaryPlaces j).Finite

theorem

exists_closedPoint_of_not_mem_openBoundaryPlaces

L55 ↗

AlgebraicCurve.CurveModel.exists_closedPoint_of_not_mem_openBoundaryPlaces

Documentation

Every place outside the actual boundary is represented by a closed point of the actual open curve.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isProper CurveModel.isIntegral CurveModel.smooth
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]

Lean source · statement

theorem exists_closedPoint_of_not_mem_openBoundaryPlaces
    (M : CurveModel K F) {X : Scheme.{u}}
    (j : X ⟶ M.C) [IsOpenImmersion j]
    (v : Place K F) (hv : v ∉ M.openBoundaryPlaces j) :
    ∃ x : closedPoints X, j x.val = (M.placeEquiv.symm v).val

Module documentation

The actual finite boundary of an open subscheme of a proper curve

Declarations

openBoundaryPlaces

place_not_mem_openBoundaryPlaces

openBoundaryPlaces_finite

exists_closedPoint_of_not_mem_openBoundaryPlaces