Module

Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain

5 declarations indexed from sourceView source ↗

Module documentation

Scheme Rational Map exists specializes ring Krull Dim le one of not mem domain

Imports4

Mathlib.AlgebraicGeometry.Birational.RationalMap
Mathlib.RingTheory.Ideal.Height
Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Nyll.AlgebraicCurves.Geometry.Schemes.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk

Imported by3

theorem

ringKrullDim_stalk_eq_height

L36 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain.FltWs29.C4.ringKrullDim_stalk_eq_height

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain
universe u
open CategoryTheory AlgebraicGeometry Topology
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Topology
namespace FltWs29
namespace C4

Lean source · statement

theorem ringKrullDim_stalk_eq_height {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) (a : U) :
    ringKrullDim (X.presheaf.stalk (a : X)) = (hU.primeIdealOf a).asIdeal.height

theorem

ringKrullDim_stalk_le_of_specializes

L42 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain.FltWs29.C4.ringKrullDim_stalk_le_of_specializes

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain
universe u
open CategoryTheory AlgebraicGeometry Topology
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Topology
namespace FltWs29
namespace C4

Lean source · statement

theorem ringKrullDim_stalk_le_of_specializes {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U)
    (a b : U) (h : (a : X) ⤳ (b : X)) :
    ringKrullDim (X.presheaf.stalk (a : X)) ≤ ringKrullDim (X.presheaf.stalk (b : X))

theorem

ringKrullDim_stalk_opens

L51 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain.FltWs29.C4.ringKrullDim_stalk_opens

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain
universe u
open CategoryTheory AlgebraicGeometry Topology
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Topology
namespace FltWs29
namespace C4

Lean source · statement

theorem ringKrullDim_stalk_opens {X : Scheme.{u}} (U : X.Opens) (y : U) :
    ringKrullDim ((U : Scheme.{u}).presheaf.stalk y) = ringKrullDim (X.presheaf.stalk (y : X))

theorem

main

L55 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain.FltWs29.C4.main

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain
universe u
open CategoryTheory AlgebraicGeometry Topology
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Topology
namespace FltWs29
namespace C4

Lean source · statement

theorem main
    {X Y : Scheme.{u}} [IsIntegral X] [IsLocallyNoetherian X]
    (hX : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x)) [IsAffine Y]
    (u : X ⤏ Y) (x : X) (hx : x ∉ u.domain) :
    ∃ z : X, z ∉ u.domain ∧ z ⤳ x ∧ ringKrullDim (X.presheaf.stalk z) ≤ 1

theorem

exists_specializes_ringKrullDim_le_one_of_not_mem_domain

L183 ↗

AlgebraicGeometry.Scheme.RationalMap.exists_specializes_ringKrullDim_le_one_of_not_mem_domain

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicGeometry.Scheme.RationalMap
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Topology
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open Scheme_RationalMap_exists_specializes_ringKrullDim_le_one_of_not_mem_domain in

Lean source · statement

theorem exists_specializes_ringKrullDim_le_one_of_not_mem_domain
    {X Y : Scheme.{u}} [IsIntegral X] [IsLocallyNoetherian X]
    (hX : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x)) [IsAffine Y]
    (u : X ⤏ Y) (x : X) (hx : x ∉ u.domain) :
    ∃ z : X, z ∉ u.domain ∧ z ⤳ x ∧ ringKrullDim (X.presheaf.stalk z) ≤ 1

Module documentation

Scheme Rational Map exists specializes ring Krull Dim le one of not mem domain

Declarations

ringKrullDim_stalk_eq_height

ringKrullDim_stalk_le_of_specializes

ringKrullDim_stalk_opens

main

exists_specializes_ringKrullDim_le_one_of_not_mem_domain