Module

Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk

6 declarations indexed from sourceView source ↗

Module documentation

Scheme Partial Map mem domain to Rational Map of valuation Ring stalk

Imports2

Mathlib.AlgebraicGeometry.Birational.RationalMap
Mathlib.AlgebraicGeometry.ValuativeCriterion

Imported by3

theorem

fromSpecStalkOfMem_eq_of_specializes

L35 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk.ValuativePartialMap.fromSpecStalkOfMem_eq_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_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ValuativePartialMap
variable {X Y S : Scheme.{u}}

Lean source · statement

theorem fromSpecStalkOfMem_eq_of_specializes (U : X.Opens) {ξ x : X} (h : ξ ⤳ x)
    (hx : x ∈ U) (hξ : ξ ∈ U) :
    U.fromSpecStalkOfMem ξ hξ =
      Spec.map (X.presheaf.stalkSpecializes h) ≫ U.fromSpecStalkOfMem x hx

theorem

partialMap_fromSpecStalkOfMem_eq_of_specializes

L42 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk.ValuativePartialMap.partialMap_fromSpecStalkOfMem_eq_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_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ValuativePartialMap
variable {X Y S : Scheme.{u}}

Lean source · statement

theorem partialMap_fromSpecStalkOfMem_eq_of_specializes (f : X.PartialMap Y) {ξ x : X}
    (h : ξ ⤳ x) (hx : x ∈ f.domain) (hξ : ξ ∈ f.domain) :
    f.fromSpecStalkOfMem hξ =
      Spec.map (X.presheaf.stalkSpecializes h) ≫ f.fromSpecStalkOfMem hx

theorem

partialMap_fromFunctionField_eq_of_mem

L50 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk.ValuativePartialMap.partialMap_fromFunctionField_eq_of_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ValuativePartialMap
variable {X Y S : Scheme.{u}}

Lean source · statement

theorem partialMap_fromFunctionField_eq_of_mem [IrreducibleSpace X] (f : X.PartialMap Y)
    {x : X} (hx : x ∈ f.domain) :
    f.fromFunctionField =
      Spec.map (X.presheaf.stalkSpecializes (genericPoint_specializes x)) ≫
        f.fromSpecStalkOfMem hx

theorem

ofHom_algebraMap_stalk_functionField

L58 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk.ValuativePartialMap.ofHom_algebraMap_stalk_functionField

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ValuativePartialMap
variable {X Y S : Scheme.{u}}

Lean source · statement

theorem ofHom_algebraMap_stalk_functionField [IrreducibleSpace X] (x : X) :
    CommRingCat.ofHom (algebraMap (X.presheaf.stalk x) X.functionField) =
      X.presheaf.stalkSpecializes ((genericPoint_spec X).specializes trivial)

theorem

existence_of_universallyClosed

L64 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk.ValuativePartialMap.existence_of_universallyClosed

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace ValuativePartialMap
variable {X Y S : Scheme.{u}}

Lean source · statement

theorem existence_of_universallyClosed (f : Y ⟶ S) [hf : UniversallyClosed f] :
    ValuativeCriterion.Existence f

theorem

mem_domain_toRationalMap_of_valuationRing_stalk

L73 ↗

AlgebraicGeometry.Scheme.PartialMap.mem_domain_toRationalMap_of_valuationRing_stalk

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_PartialMap_mem_domain_toRationalMap_of_valuationRing_stalk
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
open ValuativePartialMap in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.PartialMap.mem_domain_toRationalMap_of_valuationRing_stalk
  {X Y S : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S) [IsIntegral X]
    [LocallyOfFiniteType sY] (hY : ValuativeCriterion.Existence sY) (f : X.PartialMap Y)
    (hf : f.hom ≫ sY = f.domain.ι ≫ sX) (x : X) (hx : ValuationRing (X.presheaf.stalk x)) :
    x ∈ f.toRationalMap.domain

Module documentation

Scheme Partial Map mem domain to Rational Map of valuation Ring stalk

Declarations

fromSpecStalkOfMem_eq_of_specializes

partialMap_fromSpecStalkOfMem_eq_of_specializes

partialMap_fromFunctionField_eq_of_mem

ofHom_algebraMap_stalk_functionField

existence_of_universallyClosed

mem_domain_toRationalMap_of_valuationRing_stalk