NYLL
Module

Scheme_Opens_isProper_toSpecPolynomial_of_maximal.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
11 declarations indexed from sourceView source ↗

Module documentation

Properness of a polynomial map from a maximal open

For an integral proper curve, the maximal open on which a function is regular maps properly to the polynomial spectrum. The valuative criterion extends points through stalks and compares their specializations.

Imports11
  • Mathlib.Algebra.Category.Ring.Basic
  • Mathlib.Algebra.Polynomial.Eval.Defs
  • Mathlib.AlgebraicGeometry.FunctionField
  • Mathlib.AlgebraicGeometry.Stalk
  • Mathlib.AlgebraicGeometry.Noetherian
  • Mathlib.AlgebraicGeometry.GammaSpecAdjunction
  • Mathlib.AlgebraicGeometry.OpenImmersion
  • Mathlib.AlgebraicGeometry.Morphisms.Proper
  • Mathlib.AlgebraicGeometry.ValuativeCriterion
  • Mathlib.RingTheory.Valuation.ValuationRing
  • Mathlib.Tactic.Ext
Imported by2

Declarations

abbrev

baseRingHom

L58 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal.AlgebraicGeometry.Scheme.Opens.baseRingHom
Documentation

The base field homomorphism into global sections on the open subscheme.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
abbrev Scheme.Opens.baseRingHom (U : C.Opens) : k →+* Γ((U : Scheme.{u}), ⊤)
abbrev

toSpecPolynomial

L63 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal.AlgebraicGeometry.Scheme.Opens.toSpecPolynomial
Documentation

The morphism to the affine line defined by a section on the open subscheme.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
abbrev Scheme.Opens.toSpecPolynomial (U : C.Opens) (s : Γ(C, U)) :
    (U : Scheme.{u}) ⟶ Spec (CommRingCat.of k[X])
theorem

toSpecPolynomial_comp_C

L69 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal.AlgebraicGeometry.Scheme.Opens.toSpecPolynomial_comp_C
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.toSpecPolynomial_comp_C (U : C.Opens) (s : Γ(C, U)) :
    Scheme.Opens.toSpecPolynomial c U s ≫ Spec.map (CommRingCat.ofHom (Polynomial.C : k →+* k[X])) =
      U.ι ≫ c
theorem

comp_appTop'

L98 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal.AlgebraicGeometry.Scheme.comp_appTop'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
section general
open IsLocalRing
open scoped _root_.AlgebraicGeometry.Scheme in
Lean source · statement
theorem Scheme.comp_appTop' {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g).appTop = g.appTop ≫ f.appTop
theorem

stalkClosedPointTo_germ_top

L102 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal.AlgebraicGeometry.Scheme.stalkClosedPointTo_germ_top
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
section general
open IsLocalRing
open scoped _root_.AlgebraicGeometry.Scheme in
Lean source · statement
theorem Scheme.stalkClosedPointTo_germ_top {Y : Scheme.{u}} {R : CommRingCat.{u}} [IsLocalRing R]
    (f : Spec R ⟶ Y) (t : Γ(Y, ⊤)) :
    (Scheme.stalkClosedPointTo f).hom (Y.presheaf.germ ⊤ (f.base (closedPoint R)) trivial t) =
      (Scheme.ΓSpecIso R).hom (f.appTop t)
theorem

ι_app_self_apply

L123 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal.AlgebraicGeometry.Scheme.Opens.ι_app_self_apply
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
section general
open IsLocalRing
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.ι_app_self_apply {X : Scheme.{u}} (U : X.Opens) (s : Γ(X, U)) :
    U.ι.app U s = (U : Scheme.{u}).presheaf.map (eqToHom U.ι_preimage_self).op (U.topIso.inv s)
theorem

toSpecPolynomial_appTop_X

L133 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal.AlgebraicGeometry.Scheme.Opens.toSpecPolynomial_appTop_X
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.toSpecPolynomial_appTop_X (U : C.Opens) (s : Γ(C, U)) :
    (Scheme.Opens.toSpecPolynomial c U s).appTop
      ((Scheme.ΓSpecIso (CommRingCat.of k[X])).inv X) = U.topIso.inv s
theorem

ΓSpecIso_appTop_topIso_inv_eq

L146 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal.AlgebraicGeometry.Scheme.Opens.ΓSpecIso_appTop_topIso_inv_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.ΓSpecIso_appTop_topIso_inv_eq (U : C.Opens) (s : Γ(C, U))
    {R K : Type u} [CommRing R] [Field K] [Algebra R K]
    {i₁ : Spec (.of K) ⟶ (U : Scheme.{u})} {i₂ : Spec (.of R) ⟶ Spec (.of k[X])}
    (w : i₁ ≫ Scheme.Opens.toSpecPolynomial c U s =
      Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂) :
    (Scheme.ΓSpecIso (.of K)).hom (i₁.appTop (U.topIso.inv s)) =
      algebraMap R K ((Scheme.ΓSpecIso (.of R)).hom
        (i₂.appTop ((Scheme.ΓSpecIso (CommRingCat.of k[X])).inv X)))
theorem

valuativeCriterion_existence_toSpecPolynomial

L167 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal.AlgebraicGeometry.Scheme.Opens.valuativeCriterion_existence_toSpecPolynomial
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
open IsLocalRing in
Lean source · statement
theorem Scheme.Opens.valuativeCriterion_existence_toSpecPolynomial
    [IsIntegral C] [IsProper c] (hval : ∀ x : C, ValuationRing (C.presheaf.stalk x))
    (U : C.Opens) [Nonempty U] (s : Γ(C, U))
    (hU : ∀ x : C, C.germToFunctionField U s ∈
      (algebraMap (C.presheaf.stalk x) C.functionField).range → x ∈ U) :
    ValuativeCriterion.Existence (Scheme.Opens.toSpecPolynomial c U s)
theorem

isProper_toSpecPolynomial_of_maximal'

L275 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal.AlgebraicGeometry.Scheme.Opens.isProper_toSpecPolynomial_of_maximal'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.isProper_toSpecPolynomial_of_maximal'
    [IsIntegral C] [IsProper c] (hval : ∀ x : C, ValuationRing (C.presheaf.stalk x))
    (U : C.Opens) [Nonempty U] (s : Γ(C, U))
    (hU : ∀ x : C, C.germToFunctionField U s ∈
      (algebraMap (C.presheaf.stalk x) C.functionField).range → x ∈ U) :
    IsProper (Scheme.Opens.toSpecPolynomial c U s)
theorem

isProper_toSpecPolynomial_of_maximal

L304 ↗
AlgebraicGeometry.Scheme.Opens.isProper_toSpecPolynomial_of_maximal
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_isProper_toSpecPolynomial_of_maximal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Opens.isProper_toSpecPolynomial_of_maximal
    {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
    [IsIntegral C] [IsProper c] (hval : ∀ x : C, ValuationRing (C.presheaf.stalk x))
    (U : C.Opens) [Nonempty U] (s : Γ(C, U))
    (hU : ∀ x : C, C.germToFunctionField U s ∈
      (algebraMap (C.presheaf.stalk x) C.functionField).range → x ∈ U) :
    IsProper ((U : Scheme.{u}).toSpecΓ ≫ Spec.map (CommRingCat.ofHom
      (Polynomial.eval₂RingHom ((U.ι ≫ c).appTop.hom.comp (Scheme.ΓSpecIso (CommRingCat.of
          k)).inv.hom)
        (U.topIso.inv s))))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.