Module

exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk

8 declarations indexed from sourceView source ↗

Module documentation

exists comp eq of is Open Immersion of is Proper of is Discrete Valuation Ring stalk

Imports7

Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.ValuativeCriterion
Mathlib.AlgebraicGeometry.SpreadingOut
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Gluing
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.Tactic.Choose

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

abbrev

ηK

L46 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk.AlgebraicGeometry.ExtendDVR.ηK

Documentation

The morphism from the spectrum of the function field to the integral scheme.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ExtendDVR
open _root_.AlgebraicGeometry
variable {κ : Type u} [Field κ] {C : Scheme.{u}} [IsIntegral C] (c : C ⟶ Spec (CommRingCat.of κ))

Lean source · statement

abbrev ηK : Spec C.functionField ⟶ C

theorem

genericPoint_mem_of_isOpen

L48 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk.AlgebraicGeometry.ExtendDVR.genericPoint_mem_of_isOpen

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ExtendDVR
open _root_.AlgebraicGeometry
variable {κ : Type u} [Field κ] {C : Scheme.{u}} [IsIntegral C] (c : C ⟶ Spec (CommRingCat.of κ))
omit [IsIntegral C] in

Lean source · statement

theorem genericPoint_mem_of_isOpen [IrreducibleSpace C] {W : Set C} (hW : IsOpen W) (hne :
  W.Nonempty) :
    genericPoint C ∈ W

theorem

ηK_base

L53 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk.AlgebraicGeometry.ExtendDVR.ηK_base

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ExtendDVR
open _root_.AlgebraicGeometry
variable {κ : Type u} [Field κ] {C : Scheme.{u}} [IsIntegral C] (c : C ⟶ Spec (CommRingCat.of κ))

Lean source · statement

theorem ηK_base (z : Spec C.functionField) : (ηK (C := C)).base z = genericPoint C

theorem

isDominant_of_comp_eq_ηK

L60 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk.AlgebraicGeometry.ExtendDVR.isDominant_of_comp_eq_ηK

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ExtendDVR
open _root_.AlgebraicGeometry
variable {κ : Type u} [Field κ] {C : Scheme.{u}} [IsIntegral C] (c : C ⟶ Spec (CommRingCat.of κ))

Lean source · statement

theorem isDominant_of_comp_eq_ηK {V : Scheme.{u}} (j : V ⟶ C) [IsOpenImmersion j]
    (w : Spec C.functionField ⟶ V) (hw : w ≫ j = ηK) : IsDominant w

theorem

fst_comp_eq_snd_comp

L72 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk.AlgebraicGeometry.ExtendDVR.fst_comp_eq_snd_comp

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ExtendDVR
open _root_.AlgebraicGeometry
variable {κ : Type u} [Field κ] {C : Scheme.{u}} [IsIntegral C] (c : C ⟶ Spec (CommRingCat.of κ))

Lean source · statement

theorem fst_comp_eq_snd_comp {P : Scheme.{u}} (p : P ⟶ Spec (CommRingCat.of κ)) [IsSeparated p]
    {V₁ V₂ : Scheme.{u}} (j₁ : V₁ ⟶ C) (j₂ : V₂ ⟶ C) [IsOpenImmersion j₁] [IsOpenImmersion j₂]
    (g₁ : V₁ ⟶ P) (g₂ : V₂ ⟶ P) (hg₁ : g₁ ≫ p = j₁ ≫ c) (hg₂ : g₂ ≫ p = j₂ ≫ c)
    (w₁ : Spec C.functionField ⟶ V₁) (w₂ : Spec C.functionField ⟶ V₂)
    (hw₁ : w₁ ≫ j₁ = ηK) (hw₂ : w₂ ≫ j₂ = ηK) (hgw : w₁ ≫ g₁ = w₂ ≫ g₂) :
    pullback.fst j₁ j₂ ≫ g₁ = pullback.snd j₁ j₂ ≫ g₂

theorem

specMap_algebraMap_fromSpecStalk

L86 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk.AlgebraicGeometry.ExtendDVR.specMap_algebraMap_fromSpecStalk

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ExtendDVR
open _root_.AlgebraicGeometry
variable {κ : Type u} [Field κ] {C : Scheme.{u}} [IsIntegral C] (c : C ⟶ Spec (CommRingCat.of κ))

Lean source · statement

theorem specMap_algebraMap_fromSpecStalk (x : C) :
    Spec.map (CommRingCat.ofHom (algebraMap (C.presheaf.stalk x) C.functionField)) ≫
      C.fromSpecStalk x = ηK

theorem

exists_chart

L94 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk.AlgebraicGeometry.ExtendDVR.exists_chart

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ExtendDVR
open _root_.AlgebraicGeometry
variable {κ : Type u} [Field κ] {C : Scheme.{u}} [IsIntegral C] (c : C ⟶ Spec (CommRingCat.of κ))
variable {P : Scheme.{u}} (p : P ⟶ Spec (CommRingCat.of κ))

Lean source · statement

theorem exists_chart [IsProper p] (t : Spec C.functionField ⟶ P) (ht : t ≫ p = ηK ≫ c)
    (x : C) (hx : IsDiscreteValuationRing (C.presheaf.stalk x)) :
    ∃ (V : C.Opens) (_ : x ∈ V) (g : (V : Scheme.{u}) ⟶ P) (a : Spec C.functionField ⟶ (V :
      Scheme.{u})),
      g ≫ p = V.ι ≫ c ∧ a ≫ V.ι = ηK ∧ a ≫ g = t

theorem

exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk

L139 ↗

AlgebraicGeometry.exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits
universe u
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk in
open AlgebraicGeometry.ExtendDVR in

Lean source · statement

theorem exists_comp_eq_of_isOpenImmersion_of_isProper_of_isDiscreteValuationRing_stalk
    {κ : Type u} [Field κ] {C U P : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of κ)) [IsIntegral C]
    (u : U ⟶ C) [IsOpenImmersion u] [Nonempty U]
    (hreg : ∀ x : C, x ∉ Set.range u.base → IsDiscreteValuationRing (C.presheaf.stalk x))
    (p : P ⟶ Spec (CommRingCat.of κ)) [IsProper p]
    (f : U ⟶ P) (hf : f ≫ p = u ≫ c) :
    ∃ g : C ⟶ P, g ≫ p = c ∧ u ≫ g = f

Module documentation

exists comp eq of is Open Immersion of is Proper of is Discrete Valuation Ring stalk

Declarations