NYLL
Module

CurveModel_ffEquiv_symm_germToFunctionField_mem_and_sub_algebraMap_appLE_mem_nonunits_pointEquivPlace.lean

Nyll.AlgebraicCurves.Models.CurveModel_ffEquiv_symm_germToFunctionField_mem_and_sub_algebraMap_appLE_mem_nonunits_pointEquivPlace
10 declarations indexed from sourceView source ↗

Module documentation

Curve Model ff Equiv symm germ To Function Field mem and sub algebra Map app LE mem

nonunits point Equiv Place

Imports1
Imported by2

Declarations

theorem

base_closedPoint_eq

L34 ↗
AlgebraicCurves.Models.Proofs.GermsAtPointPlace.P2mValueAtPoint.base_closedPoint_eq
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.GermsAtPointPlace
open CategoryTheory AlgebraicGeometry
universe u v
namespace P2mValueAtPoint
open AlgebraicCurve IsLocalRing
variable {K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
theorem base_closedPoint_eq (M : CurveModel K L)
    (z : {q : Spec (CommRingCat.of K) ⟶ M.C // q ≫ M.toBase = 𝟙 _}) :
    z.1.base (closedPoint K) = (pointEquivClosedPoint M.toBase z).1
def

theta

L43 ↗
AlgebraicCurves.Models.Proofs.GermsAtPointPlace.P2mValueAtPoint.theta
Documentation

Map the local ring at a point into the modelled function field using the inverse field equivalence.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.GermsAtPointPlace
open CategoryTheory AlgebraicGeometry
universe u v
namespace P2mValueAtPoint
open AlgebraicCurve IsLocalRing
variable {K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
def theta (M : CurveModel K L) (x : M.C) : M.C.presheaf.stalk x →+* L
theorem

theta_germ

L47 ↗
AlgebraicCurves.Models.Proofs.GermsAtPointPlace.P2mValueAtPoint.theta_germ
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.GermsAtPointPlace
open CategoryTheory AlgebraicGeometry
universe u v
namespace P2mValueAtPoint
open AlgebraicCurve IsLocalRing
variable {K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
omit [IsAlgClosed K] in
Lean source · statement
theorem theta_germ (M : CurveModel K L) (U : M.C.Opens) [Nonempty (Scheme.Opens.toScheme U)]
    (x : M.C) (hx : x ∈ U) (s : Γ(M.C, U)) :
    theta M x ((M.C.presheaf.germ U x hx).hom s) = M.ffEquiv.symm ((M.C.germToFunctionField U).hom
      s)
theorem

range_theta

L57 ↗
AlgebraicCurves.Models.Proofs.GermsAtPointPlace.P2mValueAtPoint.range_theta
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.GermsAtPointPlace
open CategoryTheory AlgebraicGeometry
universe u v
namespace P2mValueAtPoint
open AlgebraicCurve IsLocalRing
variable {K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
omit [IsAlgClosed K] in
Lean source · statement
theorem range_theta (M : CurveModel K L) (x : closedPoints M.C) :
    (theta M x.1).range = (M.placeOfPoint x).toValuationSubring.toSubring
theorem

theta_mem_nonunits

L61 ↗
AlgebraicCurves.Models.Proofs.GermsAtPointPlace.P2mValueAtPoint.theta_mem_nonunits
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.GermsAtPointPlace
open CategoryTheory AlgebraicGeometry
universe u v
namespace P2mValueAtPoint
open AlgebraicCurve IsLocalRing
variable {K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
omit [IsAlgClosed K] in
Lean source · statement
theorem theta_mem_nonunits (M : CurveModel K L) (x : closedPoints M.C)
    (g : M.C.presheaf.stalk x.1) (hg : ¬ IsUnit g) :
    theta M x.1 g ∈ (M.placeOfPoint x).toValuationSubring.nonunits
def

constSec

L83 ↗
AlgebraicCurves.Models.Proofs.GermsAtPointPlace.P2mValueAtPoint.constSec
Documentation

The section obtained by pulling back a base-field constant to the chosen open set.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.GermsAtPointPlace
open CategoryTheory AlgebraicGeometry
universe u v
namespace P2mValueAtPoint
open AlgebraicCurve IsLocalRing
variable {K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
def constSec (M : CurveModel K L) (c : K) (U : M.C.Opens) : Γ(M.C, U)
theorem

germToFunctionField_constSec

L86 ↗
AlgebraicCurves.Models.Proofs.GermsAtPointPlace.P2mValueAtPoint.germToFunctionField_constSec
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.GermsAtPointPlace
open CategoryTheory AlgebraicGeometry
universe u v
namespace P2mValueAtPoint
open AlgebraicCurve IsLocalRing
variable {K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
omit [IsAlgClosed K] in
Lean source · statement
theorem germToFunctionField_constSec (M : CurveModel K L) (c : K) (U : M.C.Opens)
    [Nonempty (Scheme.Opens.toScheme U)] :
    (M.C.germToFunctionField U).hom (constSec M c U) = M.ffEquiv (algebraMap K L c)
theorem

appLE_constSec

L106 ↗
AlgebraicCurves.Models.Proofs.GermsAtPointPlace.P2mValueAtPoint.appLE_constSec
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.GermsAtPointPlace
open CategoryTheory AlgebraicGeometry
universe u v
namespace P2mValueAtPoint
open AlgebraicCurve IsLocalRing
variable {K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
omit [IsAlgClosed K] in
Lean source · statement
theorem appLE_constSec (M : CurveModel K L) (c : K) (U : M.C.Opens)
    (z : {q : Spec (CommRingCat.of K) ⟶ M.C // q ≫ M.toBase = 𝟙 _}) (hz : ⊤ ≤ z.1 ⁻¹ᵁ U) :
    (z.1.appLE U ⊤ hz).hom (constSec M c U) = (Scheme.ΓSpecIso (CommRingCat.of K)).inv c
theorem

main

L123 ↗
AlgebraicCurves.Models.Proofs.GermsAtPointPlace.P2mValueAtPoint.main
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.GermsAtPointPlace
open CategoryTheory AlgebraicGeometry
universe u v
namespace P2mValueAtPoint
open AlgebraicCurve IsLocalRing
variable {K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
theorem main (M : CurveModel K L) (U : M.C.Opens) [Nonempty (Scheme.Opens.toScheme U)] (s : Γ(M.C,
  U))
    (z : {q : Spec (CommRingCat.of K) ⟶ M.C // q ≫ M.toBase = 𝟙 _}) (hz : ⊤ ≤ z.1 ⁻¹ᵁ U) :
    M.ffEquiv.symm ((M.C.germToFunctionField U).hom s) ∈ (M.pointEquivPlace z).toValuationSubring ∧
    M.ffEquiv.symm ((M.C.germToFunctionField U).hom s) -
        algebraMap K L ((Scheme.ΓSpecIso (CommRingCat.of K)).hom ((z.1.appLE U ⊤ hz).hom s)) ∈
      (M.pointEquivPlace z).toValuationSubring.nonunits
theorem

ffEquiv_symm_germToFunctionField_mem_and_sub_algebraMap_appLE_mem_nonunits_pointEquivPlace

L178 ↗
AlgebraicCurve.CurveModel.ffEquiv_symm_germToFunctionField_mem_and_sub_algebraMap_appLE_mem_nonunits_pointEquivPlace
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurve.CurveModel
open _root_.AlgebraicCurves.Models.Proofs.GermsAtPointPlace
open _root_.CategoryTheory _root_.AlgebraicGeometry
universe u v
open _root_.AlgebraicCurve in
Lean source · statement
theorem ffEquiv_symm_germToFunctionField_mem_and_sub_algebraMap_appLE_mem_nonunits_pointEquivPlace
    {K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
    (M : CurveModel K L) (U : M.C.Opens) [Nonempty (Scheme.Opens.toScheme U)] (s : Γ(M.C, U))
    (z : {q : Spec (CommRingCat.of K) ⟶ M.C // q ≫ M.toBase = 𝟙 _}) (hz : ⊤ ≤ z.1 ⁻¹ᵁ U) :
    M.ffEquiv.symm (M.C.germToFunctionField U s) ∈ (M.pointEquivPlace z).toValuationSubring ∧
    M.ffEquiv.symm (M.C.germToFunctionField U s) -
        algebraMap K L ((Scheme.ΓSpecIso (CommRingCat.of K)).hom (z.1.appLE U ⊤ hz s)) ∈
      (M.pointEquivPlace z).toValuationSubring.nonunits

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