NYLL
Module

Construction.lean

Nyll.AlgebraicCurves.Models.Construction
196 declarations indexed from sourceView source ↗

Module documentation

Construction

Imports12
Imported by9

Declarations

abbrev

specPoint

L45 ↗
AlgebraicCurve.CurveModel.specPoint
Documentation

The point of an affine scheme viewed through its underlying prime spectrum. This reducible bridge keeps type-sensitive stalk expressions stable across mathlib API changes.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
Lean source · statement
abbrev specPoint {R : Type u} [CommRing R]
    (p : Spec (CommRingCat.of R)) : PrimeSpectrum R
abbrev

schemePoint

L48 ↗
AlgebraicCurve.CurveModel.schemePoint
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
Lean source · statement
abbrev schemePoint {R : Type u} [CommRing R]
    (p : PrimeSpectrum R) : Spec (CommRingCat.of R)
abbrev

topPoint

L51 ↗
AlgebraicCurve.CurveModel.topPoint
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
Lean source · statement
abbrev topPoint {R : Type u} [CommRing R]
    (p : PrimeSpectrum R) : (PrimeSpectrum.Top R)
theorem

singleton_subset_pair

L56 ↗
AlgebraicCurve.CurveModel.singleton_subset_pair
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
theorem singleton_subset_pair : ({t} : Set L) ⊆ {t, t⁻¹}
theorem

singleton_inv_subset_pair

L59 ↗
AlgebraicCurve.CurveModel.singleton_inv_subset_pair
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
theorem singleton_inv_subset_pair : ({t⁻¹} : Set L) ⊆ {t, t⁻¹}
abbrev

incl₀

L63 ↗
AlgebraicCurve.CurveModel.incl₀
Documentation

The inclusion from the finite chart ring to the overlap ring.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
abbrev incl₀ : chartRing K ({t} : Set L) →ₐ[K] chartRing K ({t, t⁻¹} : Set L)
abbrev

inclInf

L67 ↗
AlgebraicCurve.CurveModel.inclInf
Documentation

The inclusion from the infinite chart ring to the overlap ring.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
abbrev inclInf : chartRing K ({t⁻¹} : Set L) →ₐ[K] chartRing K ({t, t⁻¹} : Set L)
def

tChart

L71 ↗
AlgebraicCurve.CurveModel.tChart
Documentation

The coordinate as an element of the finite chart ring.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
def tChart : chartRing K ({t} : Set L)
def

tInvChart

L74 ↗
AlgebraicCurve.CurveModel.tInvChart
Documentation

The inverse coordinate as an element of the infinite chart ring.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
def tInvChart : chartRing K ({t⁻¹} : Set L)
theorem

coe_tChart

L77 ↗
AlgebraicCurve.CurveModel.coe_tChart
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
theorem coe_tChart : (tChart K t : L) = t
theorem

coe_tInvChart

L79 ↗
AlgebraicCurve.CurveModel.coe_tInvChart
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
theorem coe_tInvChart : (tInvChart K t : L) = t⁻¹
theorem

isUnit_incl₀_tChart

L81 ↗
AlgebraicCurve.CurveModel.isUnit_incl₀_tChart
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
theorem isUnit_incl₀_tChart (ht : t ≠ 0) : IsUnit (incl₀ K t (tChart K t))
theorem

isUnit_inclInf_tInvChart

L86 ↗
AlgebraicCurve.CurveModel.isUnit_inclInf_tInvChart
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
theorem isUnit_inclInf_tInvChart (ht : t ≠ 0) : IsUnit (inclInf K t (tInvChart K t))
theorem

isLocalization_away_incl₀

L91 ↗
AlgebraicCurve.CurveModel.isLocalization_away_incl₀
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · full declaration
theorem isLocalization_away_incl₀ (ht : t ≠ 0) :
    letI := (incl₀ K t).toRingHom.toAlgebra
    IsLocalization.Away (tChart K t) (chartRing K ({t, t⁻¹} : Set L)) := by
  let := (incl₀ K t).toRingHom.toAlgebra
  refine (isLocalization_iff _ _).mpr ⟨?_, ?_, ?_⟩
  · rintro ⟨_, n, rfl⟩
    rw [RingHom.algebraMap_toAlgebra, map_pow]
    exact (isUnit_incl₀_tChart K t ht).pow n
  · intro z
    have hz : (z : L) ∈ chartRing K (insert t⁻¹ ({t} : Set L)) := by
      rw [show insert t⁻¹ ({t} : Set L) = {t, t⁻¹} from Set.pair_comm _ _]
      exact z.2
    obtain ⟨n, hn⟩ := exists_pow_mul_mem_chartRing (K := K) (Set.mem_singleton t) ht hz
    refine ⟨(⟨t ^ n * z, hn⟩, ⟨tChart K t ^ n, n, rfl⟩), Subtype.ext ?_⟩
    simp only [RingHom.algebraMap_toAlgebra, map_pow, Subalgebra.coe_mul, Subalgebra.coe_pow,
      AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, coe_chartIncl, coe_tChart]
    exact mul_comm _ _
  · intro x y h
    refine ⟨1, ?_⟩
    rw [RingHom.algebraMap_toAlgebra] at h
    rw [chartIncl_injective K _ h]
theorem

isLocalization_away_inclInf

L113 ↗
AlgebraicCurve.CurveModel.isLocalization_away_inclInf
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · full declaration
theorem isLocalization_away_inclInf (ht : t ≠ 0) :
    letI := (inclInf K t).toRingHom.toAlgebra
    IsLocalization.Away (tInvChart K t) (chartRing K ({t, t⁻¹} : Set L)) := by
  let := (inclInf K t).toRingHom.toAlgebra
  refine (isLocalization_iff _ _).mpr ⟨?_, ?_, ?_⟩
  · rintro ⟨_, n, rfl⟩
    rw [RingHom.algebraMap_toAlgebra, map_pow]
    exact (isUnit_inclInf_tInvChart K t ht).pow n
  · intro z
    have hz : (z : L) ∈ chartRing K (insert t⁻¹⁻¹ ({t⁻¹} : Set L)) := by
      rw [inv_inv]
      exact z.2
    obtain ⟨n, hn⟩ := exists_pow_mul_mem_chartRing (K := K) (Set.mem_singleton t⁻¹)
      (inv_ne_zero ht) hz
    refine ⟨(⟨t⁻¹ ^ n * z, hn⟩, ⟨tInvChart K t ^ n, n, rfl⟩), Subtype.ext ?_⟩
    simp only [RingHom.algebraMap_toAlgebra, map_pow, Subalgebra.coe_mul, Subalgebra.coe_pow,
      AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, coe_chartIncl, coe_tInvChart]
    exact mul_comm _ _
  · intro x y h
    refine ⟨1, ?_⟩
    rw [RingHom.algebraMap_toAlgebra] at h
    rw [chartIncl_injective K _ h]
abbrev

X₀

L137 ↗
AlgebraicCurve.CurveModel.X₀
Documentation

The affine scheme of the finite chart ring.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
abbrev X₀ : Scheme.{u}
abbrev

XInf

L140 ↗
AlgebraicCurve.CurveModel.XInf
Documentation

The affine scheme of the infinite chart ring.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
abbrev XInf : Scheme.{u}
abbrev

XOverlap

L143 ↗
AlgebraicCurve.CurveModel.XOverlap
Documentation

The affine scheme of the overlap ring.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
abbrev XOverlap : Scheme.{u}
abbrev

f₀

L146 ↗
AlgebraicCurve.CurveModel.f₀
Documentation

The overlap morphism to the finite chart.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
abbrev f₀ : XOverlap K t ⟶ X₀ K t
abbrev

fInf

L149 ↗
AlgebraicCurve.CurveModel.fInf
Documentation

The overlap morphism to the infinite chart.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
Lean source · statement
abbrev fInf : XOverlap K t ⟶ XInf K t
instance

isOpenImmersion_f₀

L153 ↗
AlgebraicCurve.CurveModel.isOpenImmersion_f₀
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
variable [Fact (t ≠ 0)]
Lean source · statement
instance isOpenImmersion_f₀ : IsOpenImmersion (f₀ K t)
instance

isOpenImmersion_fInf

L158 ↗
AlgebraicCurve.CurveModel.isOpenImmersion_fInf
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Charts
variable [Fact (t ≠ 0)]
Lean source · statement
instance isOpenImmersion_fInf : IsOpenImmersion (fInf K t)
def

glued

L170 ↗
AlgebraicCurve.CurveModel.glued
Documentation

The scheme obtained by gluing the finite and infinite charts.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
def glued : Scheme.{u}
def

ι₀

L173 ↗
AlgebraicCurve.CurveModel.ι₀
Documentation

The canonical finite-chart morphism into the glued scheme.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
def ι₀ : X₀ K t ⟶ glued K t
def

ιInf

L176 ↗
AlgebraicCurve.CurveModel.ιInf
Documentation

The canonical infinite-chart morphism into the glued scheme.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
def ιInf : XInf K t ⟶ glued K t
theorem

glue_condition

L178 ↗
AlgebraicCurve.CurveModel.glue_condition
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
theorem glue_condition : f₀ K t ≫ ι₀ K t = fInf K t ≫ ιInf K t
instance

isOpenImmersion_ι₀

L180 ↗
AlgebraicCurve.CurveModel.isOpenImmersion_ι₀
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
instance isOpenImmersion_ι₀ : IsOpenImmersion (ι₀ K t)
instance

isOpenImmersion_ιInf

L183 ↗
AlgebraicCurve.CurveModel.isOpenImmersion_ιInf
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
instance isOpenImmersion_ιInf : IsOpenImmersion (ιInf K t)
theorem

f₀_toBase_eq_fInf_toBase

L187 ↗
AlgebraicCurve.CurveModel.f₀_toBase_eq_fInf_toBase
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
omit [Fact (t ≠ 0)] in
Lean source · statement
theorem f₀_toBase_eq_fInf_toBase :
    f₀ K t ≫ Spec.map (CommRingCat.ofHom (algebraMap K (chartRing K ({t} : Set L)))) =
      fInf K t ≫ Spec.map (CommRingCat.ofHom (algebraMap K (chartRing K ({t⁻¹} : Set L))))
def

gluedToBase

L196 ↗
AlgebraicCurve.CurveModel.gluedToBase
Documentation

The structure morphism obtained by gluing the chart structure morphisms.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
def gluedToBase : glued K t ⟶ Spec (CommRingCat.of K)
theorem

ι₀_gluedToBase

L201 ↗
AlgebraicCurve.CurveModel.ι₀_gluedToBase
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
theorem ι₀_gluedToBase : ι₀ K t ≫ gluedToBase K t =
    Spec.map (CommRingCat.ofHom (algebraMap K (chartRing K ({t} : Set L))))
theorem

ιInf_gluedToBase

L205 ↗
AlgebraicCurve.CurveModel.ιInf_gluedToBase
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
theorem ιInf_gluedToBase : ιInf K t ≫ gluedToBase K t =
    Spec.map (CommRingCat.ofHom (algebraMap K (chartRing K ({t⁻¹} : Set L))))
theorem

smoothOfRelativeDimension_one_gluedToBase_of_charts

L209 ↗
AlgebraicCurve.CurveModel.smoothOfRelativeDimension_one_gluedToBase_of_charts
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
theorem smoothOfRelativeDimension_one_gluedToBase_of_charts
    (h₀ : SmoothOfRelativeDimension 1
      (Spec.map (CommRingCat.ofHom (algebraMap K (chartRing K ({t} : Set L))))))
    (hInf : SmoothOfRelativeDimension 1
      (Spec.map (CommRingCat.ofHom (algebraMap K (chartRing K ({t⁻¹} : Set L)))))) :
    SmoothOfRelativeDimension 1 (gluedToBase K t)
theorem

mem_range_ι₀_or_mem_range_ιInf

L238 ↗
AlgebraicCurve.CurveModel.mem_range_ι₀_or_mem_range_ιInf
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
theorem mem_range_ι₀_or_mem_range_ιInf (x : glued K t) :
    x ∈ Set.range (ι₀ K t).base ∨ x ∈ Set.range (ιInf K t).base
theorem

range_ιInf_inter_range_ι₀_nonempty

L252 ↗
AlgebraicCurve.CurveModel.range_ιInf_inter_range_ι₀_nonempty
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Glue
variable [Fact (t ≠ 0)]
Lean source · statement
theorem range_ιInf_inter_range_ι₀_nonempty :
    (Set.range (ιInf K t).base ∩ Set.range (ι₀ K t).base).Nonempty
instance

isIntegral_glued

L266 ↗
AlgebraicCurve.CurveModel.isIntegral_glued
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
instance isIntegral_glued : IsIntegral (glued K t)
theorem

smoothOfRelativeDimension_one_gluedToBase

L294 ↗
AlgebraicCurve.CurveModel.smoothOfRelativeDimension_one_gluedToBase
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem smoothOfRelativeDimension_one_gluedToBase (ht : Transcendental K t) :
    SmoothOfRelativeDimension 1 (gluedToBase K t)
instance

isFractionRing_overlap

L300 ↗
AlgebraicCurve.CurveModel.isFractionRing_overlap
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
instance isFractionRing_overlap : IsFractionRing (chartRing K ({t, t⁻¹} : Set L)) L
instance

algebra_overlap_functionField

L306 ↗
AlgebraicCurve.CurveModel.algebra_overlap_functionField
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
instance algebra_overlap_functionField :
    Algebra (chartRing K ({t, t⁻¹} : Set L)) (XOverlap K t).functionField
instance

isFractionRing_overlap_functionField

L311 ↗
AlgebraicCurve.CurveModel.isFractionRing_overlap_functionField
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
instance isFractionRing_overlap_functionField :
    IsFractionRing (chartRing K ({t, t⁻¹} : Set L)) (XOverlap K t).functionField
def

overlapFunctionFieldAlgEquiv

L316 ↗
AlgebraicCurve.CurveModel.overlapFunctionFieldAlgEquiv
Documentation

The fraction field identification for the overlap chart.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
def overlapFunctionFieldAlgEquiv :
    L ≃ₐ[chartRing K ({t, t⁻¹} : Set L)] (XOverlap K t).functionField
def

ιU

L321 ↗
AlgebraicCurve.CurveModel.ιU
Documentation

The overlap chart morphism into the glued scheme.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
def ιU : XOverlap K t ⟶ glued K t
theorem

ιU_eq

L324 ↗
AlgebraicCurve.CurveModel.ιU_eq
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem ιU_eq : ιU K t = f₀ K t ≫ ι₀ K t
theorem

ιU_eq'

L327 ↗
AlgebraicCurve.CurveModel.ιU_eq'
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem ιU_eq' : ιU K t = fInf K t ≫ ιInf K t
instance

isOpenImmersion_ιU

L329 ↗
AlgebraicCurve.CurveModel.isOpenImmersion_ιU
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
instance isOpenImmersion_ιU : IsOpenImmersion (ιU K t)
theorem

ιU_gluedToBase

L333 ↗
AlgebraicCurve.CurveModel.ιU_gluedToBase
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem ιU_gluedToBase : ιU K t ≫ gluedToBase K t =
    Spec.map (CommRingCat.ofHom (algebraMap K (chartRing K ({t, t⁻¹} : Set L))))
theorem

ιU_genericPoint

L342 ↗
AlgebraicCurve.CurveModel.ιU_genericPoint
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem ιU_genericPoint :
    (ιU K t).base (genericPoint (XOverlap K t)) = genericPoint (glued K t)
def

gluedFunctionFieldIsoOverlap

L347 ↗
AlgebraicCurve.CurveModel.gluedFunctionFieldIsoOverlap
Documentation

The stalk isomorphism identifying the glued and overlap function fields.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
def gluedFunctionFieldIsoOverlap :
    (glued K t).functionField ≅ (XOverlap K t).functionField
def

gluedFunctionFieldEquiv

L353 ↗
AlgebraicCurve.CurveModel.gluedFunctionFieldEquiv
Documentation

The identification of the given field with the glued scheme function field.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
def gluedFunctionFieldEquiv : L ≃+* (glued K t).functionField
theorem

gluedFunctionFieldIsoOverlap_baseToFunctionField

L358 ↗
AlgebraicCurve.CurveModel.gluedFunctionFieldIsoOverlap_baseToFunctionField
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem gluedFunctionFieldIsoOverlap_baseToFunctionField (a : K) :
    (gluedFunctionFieldIsoOverlap K t).hom (baseToFunctionField (gluedToBase K t) a) =
      algebraMap (chartRing K ({t, t⁻¹} : Set L)) (XOverlap K t).functionField
        (algebraMap K (chartRing K ({t, t⁻¹} : Set L)) a)
theorem

gluedFunctionFieldEquiv_algebraMap

L388 ↗
AlgebraicCurve.CurveModel.gluedFunctionFieldEquiv_algebraMap
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Qualities
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [CharZero K] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem gluedFunctionFieldEquiv_algebraMap (a : K) :
    gluedFunctionFieldEquiv K t (algebraMap K L a) =
      baseToFunctionField (gluedToBase K t) a
instance

isIntegral_adjoin_chartRing

L400 ↗
AlgebraicCurve.CurveModel.isIntegral_adjoin_chartRing
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
Lean source · statement
instance isIntegral_adjoin_chartRing (S : Set L) :
    Algebra.IsIntegral (Algebra.adjoin K S) (chartRing K S)
theorem

not_isField_chartRing

L404 ↗
AlgebraicCurve.CurveModel.not_isField_chartRing
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
Lean source · statement
theorem not_isField_chartRing (ht : Transcendental K t) :
    ¬ IsField (chartRing K ({t} : Set L))
theorem

isMaximal_iff_ne_bot

L413 ↗
AlgebraicCurve.CurveModel.isMaximal_iff_ne_bot
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
Lean source · statement
theorem isMaximal_iff_ne_bot (ht : Transcendental K t) [FiniteDimensional K⟮t⟯ L] [CharZero K]
    (𝔭 : Ideal (chartRing K ({t} : Set L))) [𝔭.IsPrime] : 𝔭.IsMaximal ↔ 𝔭 ≠ ⊥
instance

locallyOfFiniteType_gluedToBase

L422 ↗
AlgebraicCurve.CurveModel.locallyOfFiniteType_gluedToBase
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section FiniteType
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
instance locallyOfFiniteType_gluedToBase : LocallyOfFiniteType (gluedToBase K t)
instance

jacobsonSpace_glued

L447 ↗
AlgebraicCurve.CurveModel.jacobsonSpace_glued
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section FiniteType
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
instance jacobsonSpace_glued : JacobsonSpace (glued K t)
theorem

ι₀_mem_closedPoints_iff

L450 ↗
AlgebraicCurve.CurveModel.ι₀_mem_closedPoints_iff
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section FiniteType
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem ι₀_mem_closedPoints_iff (x : X₀ K t) :
    (ι₀ K t).base x ∈ closedPoints (glued K t) ↔ x ∈ closedPoints (X₀ K t)
theorem

ιInf_mem_closedPoints_iff

L454 ↗
AlgebraicCurve.CurveModel.ιInf_mem_closedPoints_iff
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section FiniteType
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem ιInf_mem_closedPoints_iff (x : XInf K t) :
    (ιInf K t).base x ∈ closedPoints (glued K t) ↔ x ∈ closedPoints (XInf K t)
theorem

ι₀_eq_ιInf_iff

L464 ↗
AlgebraicCurve.CurveModel.ι₀_eq_ιInf_iff
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Overlap
variable [Fact (t ≠ 0)]
Lean source · statement
theorem ι₀_eq_ιInf_iff (x₀ : X₀ K t) (xi : XInf K t) :
    (ι₀ K t).base x₀ = (ιInf K t).base xi ↔
      ∃ u : XOverlap K t, (f₀ K t).base u = x₀ ∧ (fInf K t).base u = xi
theorem

range_fInf

L482 ↗
AlgebraicCurve.CurveModel.range_fInf
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Overlap
variable [Fact (t ≠ 0)]
Lean source · statement
theorem range_fInf : Set.range (fInf K t).base =
    ((PrimeSpectrum.basicOpen (tInvChart K t) :
        TopologicalSpace.Opens (PrimeSpectrum (chartRing K ({t⁻¹} : Set L)))) :
      Set (PrimeSpectrum (chartRing K ({t⁻¹} : Set L))))
theorem

range_f₀

L491 ↗
AlgebraicCurve.CurveModel.range_f₀
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Overlap
variable [Fact (t ≠ 0)]
Lean source · statement
theorem range_f₀ : Set.range (f₀ K t).base =
    ((PrimeSpectrum.basicOpen (tChart K t) :
        TopologicalSpace.Opens (PrimeSpectrum (chartRing K ({t} : Set L)))) :
      Set (PrimeSpectrum (chartRing K ({t} : Set L))))
theorem

ιInf_mem_range_ι₀_iff

L500 ↗
AlgebraicCurve.CurveModel.ιInf_mem_range_ι₀_iff
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Overlap
variable [Fact (t ≠ 0)]
Lean source · statement
theorem ιInf_mem_range_ι₀_iff (xi : XInf K t) :
    (ιInf K t).base xi ∈ Set.range (ι₀ K t).base ↔ tInvChart K t ∉ xi.asIdeal
theorem

ι₀_mem_range_ιInf_iff

L513 ↗
AlgebraicCurve.CurveModel.ι₀_mem_range_ιInf_iff
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section Overlap
variable [Fact (t ≠ 0)]
Lean source · statement
theorem ι₀_mem_range_ιInf_iff (x₀ : X₀ K t) :
    (ι₀ K t).base x₀ ∈ Set.range (ιInf K t).base ↔ tChart K t ∉ x₀.asIdeal
instance

stalkAlgebra_spec

L539 ↗
AlgebraicCurve.CurveModel.stalkAlgebra_spec
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section StalkRange
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L]
variable (A : Subalgebra K L) (i : A →ₐ[K] chartRing K ({t, t⁻¹} : Set L))
  (hi : ∀ a : A, (i a : L) = a)
  (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
  (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
omit [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
instance stalkAlgebra_spec (p : PrimeSpectrum A) :
    Algebra A ((Spec (CommRingCat.of A)).presheaf.stalk p)
instance

isLocalization_stalk_spec

L545 ↗
AlgebraicCurve.CurveModel.isLocalization_stalk_spec
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section StalkRange
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L]
variable (A : Subalgebra K L) (i : A →ₐ[K] chartRing K ({t, t⁻¹} : Set L))
  (hi : ∀ a : A, (i a : L) = a)
  (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
  (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
omit [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
instance isLocalization_stalk_spec (p : PrimeSpectrum A) :
    IsLocalization.AtPrime ((Spec (CommRingCat.of A)).presheaf.stalk p) p.asIdeal
theorem

specMap_genericPoint

L551 ↗
AlgebraicCurve.CurveModel.specMap_genericPoint
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section StalkRange
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L]
variable (A : Subalgebra K L) (i : A →ₐ[K] chartRing K ({t, t⁻¹} : Set L))
  (hi : ∀ a : A, (i a : L) = a)
  (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
  (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
omit [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem specMap_genericPoint :
    (Spec.map (CommRingCat.ofHom i.toRingHom)).base (genericPoint (XOverlap K t)) =
      genericPoint (Spec (CommRingCat.of A))
def

thetaHom

L557 ↗
AlgebraicCurve.CurveModel.thetaHom
Documentation

The homomorphism from an affine chart stalk to the given function field.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section StalkRange
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L]
variable (A : Subalgebra K L) (i : A →ₐ[K] chartRing K ({t, t⁻¹} : Set L))
  (hi : ∀ a : A, (i a : L) = a)
  (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
  (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
Lean source · statement
def thetaHom (p : PrimeSpectrum A) :
    (Spec (CommRingCat.of A)).presheaf.stalk (schemePoint p) →+* L
theorem

thetaHom_toStalk

L566 ↗
AlgebraicCurve.CurveModel.thetaHom_toStalk
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section StalkRange
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L]
variable (A : Subalgebra K L) (i : A →ₐ[K] chartRing K ({t, t⁻¹} : Set L))
  (hi : ∀ a : A, (i a : L) = a)
  (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
  (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
include hi in
omit [Fact (t ≠ 0)] in
Lean source · statement
theorem thetaHom_toStalk (p : PrimeSpectrum A) (a : A) :
    thetaHom K t A i p (StructureSheaf.toStalk A p a) = a
theorem

thetaHom_mk'

L582 ↗
AlgebraicCurve.CurveModel.thetaHom_mk'
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section StalkRange
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L]
variable (A : Subalgebra K L) (i : A →ₐ[K] chartRing K ({t, t⁻¹} : Set L))
  (hi : ∀ a : A, (i a : L) = a)
  (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
  (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
include hi in
omit [Fact (t ≠ 0)] in
Lean source · statement
theorem thetaHom_mk' (p : PrimeSpectrum A) (a : A) (b : p.asIdeal.primeCompl) :
    thetaHom K t A i p (IsLocalization.mk' _ a b) = (a : L) * ((b : A) : L)⁻¹
theorem

range_thetaHom

L598 ↗
AlgebraicCurve.CurveModel.range_thetaHom
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section StalkRange
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L]
variable (A : Subalgebra K L) (i : A →ₐ[K] chartRing K ({t, t⁻¹} : Set L))
  (hi : ∀ a : A, (i a : L) = a)
  (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
  (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
include hi in
omit [Fact (t ≠ 0)] in
Lean source · statement
theorem range_thetaHom (p : PrimeSpectrum A) :
    Set.range (thetaHom K t A i p) =
      {y : L | ∃ a b : A, b ∉ p.asIdeal ∧ y = (a : L) * ((b : A) : L)⁻¹}
theorem

ffEquiv_symm_algebraMap_stalk

L612 ↗
AlgebraicCurve.CurveModel.ffEquiv_symm_algebraMap_stalk
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section StalkRange
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L]
variable (A : Subalgebra K L) (i : A →ₐ[K] chartRing K ({t, t⁻¹} : Set L))
  (hi : ∀ a : A, (i a : L) = a)
  (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
  (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
include comm in
omit [IsOpenImmersion ιA] in
Lean source · statement
theorem ffEquiv_symm_algebraMap_stalk (p : Spec (CommRingCat.of A))
    (s : (glued K t).presheaf.stalk (ιA.base p)) :
    (gluedFunctionFieldEquiv K t).symm
        (algebraMap ((glued K t).presheaf.stalk (ιA.base p)) (glued K t).functionField s) =
      thetaHom K t A i (specPoint p) ((ιA.stalkMap p) s)
theorem

range_ffEquiv_symm_comp_algebraMap_stalk

L649 ↗
AlgebraicCurve.CurveModel.range_ffEquiv_symm_comp_algebraMap_stalk
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section StalkRange
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L]
variable (A : Subalgebra K L) (i : A →ₐ[K] chartRing K ({t, t⁻¹} : Set L))
  (hi : ∀ a : A, (i a : L) = a)
  (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
  (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
include hi comm in
Lean source · statement
theorem range_ffEquiv_symm_comp_algebraMap_stalk (p : Spec (CommRingCat.of A)) :
    (((gluedFunctionFieldEquiv K t).symm : (glued K t).functionField ≃+* L).toRingHom.comp
        (algebraMap ((glued K t).presheaf.stalk (ιA.base p)) (glued K t).functionField)).range =
      {y : L | ∃ a b : A, b ∉ p.asIdeal ∧ y = (a : L) * ((b : A) : L)⁻¹}
theorem

transcendental_inv

L673 ↗
AlgebraicCurve.CurveModel.transcendental_inv
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem transcendental_inv (ht : Transcendental K t) : Transcendental K t⁻¹
def

primeOfι₀

L677 ↗
AlgebraicCurve.CurveModel.primeOfι₀
Documentation

The height-one prime associated to a closed point in the finite chart.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
def primeOfι₀ (ht : Transcendental K t) (x₀ : X₀ K t)
    (hx : (ι₀ K t).base x₀ ∈ closedPoints (glued K t)) :
    HeightOneSpectrum (chartRing K ({t} : Set L))
def

primeOfιInf

L687 ↗
AlgebraicCurve.CurveModel.primeOfιInf
Documentation

The height-one prime associated to a closed point in the infinite chart.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
def primeOfιInf (ht : Transcendental K t) (xi : XInf K t)
    (hx : (ιInf K t).base xi ∈ closedPoints (glued K t)) :
    HeightOneSpectrum (chartRing K ({t⁻¹} : Set L))
theorem

primeOfι₀_asIdeal

L697 ↗
AlgebraicCurve.CurveModel.primeOfι₀_asIdeal
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem primeOfι₀_asIdeal (ht : Transcendental K t) (x₀ : X₀ K t) (hx) :
    (primeOfι₀ K t ht x₀ hx).asIdeal = x₀.asIdeal
theorem

primeOfιInf_asIdeal

L702 ↗
AlgebraicCurve.CurveModel.primeOfιInf_asIdeal
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem primeOfιInf_asIdeal (ht : Transcendental K t) (xi : XInf K t) (hx) :
    (primeOfιInf K t ht xi hx).asIdeal = xi.asIdeal
theorem

mem_range_ιInf_of_not_mem_range_ι₀

L708 ↗
AlgebraicCurve.CurveModel.mem_range_ιInf_of_not_mem_range_ι₀
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem mem_range_ιInf_of_not_mem_range_ι₀ {x : glued K t}
    (h : x ∉ Set.range (ι₀ K t).base) : x ∈ Set.range (ιInf K t).base
def

gluedPlaceOfPoint

L714 ↗
AlgebraicCurve.CurveModel.gluedPlaceOfPoint
Documentation

The place of a closed point obtained from a chart containing it.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
open scoped Classical in
Lean source · statement
def gluedPlaceOfPoint (ht : Transcendental K t) (x : closedPoints (glued K t)) : Place K L
theorem

gluedPlaceOfPoint_ι₀

L723 ↗
AlgebraicCurve.CurveModel.gluedPlaceOfPoint_ι₀
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem gluedPlaceOfPoint_ι₀ (ht : Transcendental K t) (x₀ : X₀ K t)
    (hx : (ι₀ K t).base x₀ ∈ closedPoints (glued K t)) :
    gluedPlaceOfPoint K t ht ⟨(ι₀ K t).base x₀, hx⟩ =
      Place.ofHeightOneSpectrum (K := K) (primeOfι₀ K t ht x₀ hx)
theorem

gluedPlaceOfPoint_of_not_mem

L736 ↗
AlgebraicCurve.CurveModel.gluedPlaceOfPoint_of_not_mem
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · full declaration
theorem gluedPlaceOfPoint_of_not_mem (ht : Transcendental K t) (x : closedPoints (glued K t))
    (h : x.1 ∉ Set.range (ι₀ K t).base) (xi : XInf K t)
    (hxi : (ιInf K t).base xi = x.1) :
    gluedPlaceOfPoint K t ht x =
      Place.ofHeightOneSpectrum (K := K) (primeOfιInf K t ht xi (by rw [hxi]; exact x.2)) := by
  have hc : Classical.choose (mem_range_ιInf_of_not_mem_range_ι₀ K t h) = xi :=
    (ιInf K t).isOpenEmbedding.injective
      ((Classical.choose_spec (mem_range_ιInf_of_not_mem_range_ι₀ K t h)).trans hxi.symm)
  have key : ∀ (y : XInf K t) (hy) (_ : y = xi),
      primeOfιInf K t ht y hy = primeOfιInf K t ht xi (by rw [hxi]; exact x.2) := by
    rintro y hy rfl; rfl
  unfold gluedPlaceOfPoint
  rw [dite_eq_right h, key _ _ hc]
theorem

t_mem_of_ι₀

L750 ↗
AlgebraicCurve.CurveModel.t_mem_of_ι₀
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem t_mem_of_ι₀ (ht : Transcendental K t) (x₀ : X₀ K t) (hx) :
    t ∈ (Place.ofHeightOneSpectrum (K := K) (primeOfι₀ K t ht x₀ hx)).toValuationSubring
theorem

t_not_mem_of_ιInf

L754 ↗
AlgebraicCurve.CurveModel.t_not_mem_of_ιInf
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem t_not_mem_of_ιInf (ht : Transcendental K t) (xi : XInf K t) (hx)
    (hxi : tInvChart K t ∈ xi.asIdeal) :
    t ∉ (Place.ofHeightOneSpectrum (K := K) (primeOfιInf K t ht xi hx)).toValuationSubring
theorem

tInvChart_mem_of_not_mem_range

L775 ↗
AlgebraicCurve.CurveModel.tInvChart_mem_of_not_mem_range
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem tInvChart_mem_of_not_mem_range (xi : XInf K t)
    (h : (ιInf K t).base xi ∉ Set.range (ι₀ K t).base) : tInvChart K t ∈ xi.asIdeal
theorem

gluedPlaceOfPoint_injective

L780 ↗
AlgebraicCurve.CurveModel.gluedPlaceOfPoint_injective
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem gluedPlaceOfPoint_injective (ht : Transcendental K t) :
    Function.Injective (gluedPlaceOfPoint K t ht)
theorem

gluedPlaceOfPoint_surjective

L814 ↗
AlgebraicCurve.CurveModel.gluedPlaceOfPoint_surjective
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem gluedPlaceOfPoint_surjective (ht : Transcendental K t) :
    Function.Surjective (gluedPlaceOfPoint K t ht)
theorem

gluedPlaceOfPoint_bijective

L855 ↗
AlgebraicCurve.CurveModel.gluedPlaceOfPoint_bijective
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem gluedPlaceOfPoint_bijective (ht : Transcendental K t) :
    Function.Bijective (gluedPlaceOfPoint K t ht)
theorem

range_stalk_eq_gluedPlaceOfPoint

L859 ↗
AlgebraicCurve.CurveModel.range_stalk_eq_gluedPlaceOfPoint
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
section PlaceMap
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem range_stalk_eq_gluedPlaceOfPoint (ht : Transcendental K t) (x : closedPoints (glued K t)) :
    (((gluedFunctionFieldEquiv K t).symm : (glued K t).functionField ≃+* L).toRingHom.comp
        (algebraMap ((glued K t).presheaf.stalk x.1) (glued K t).functionField)).range =
      (gluedPlaceOfPoint K t ht x).toValuationSubring.toSubring
instance

compactSpace_glued

L903 ↗
AlgebraicCurve.CurveModel.compactSpace_glued
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Compact
variable [Fact (t ≠ 0)]
Lean source · statement
instance compactSpace_glued : CompactSpace (glued K t)
instance

quasiCompact_gluedToBase

L911 ↗
AlgebraicCurve.CurveModel.quasiCompact_gluedToBase
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Compact
variable [Fact (t ≠ 0)]
Lean source · statement
instance quasiCompact_gluedToBase : QuasiCompact (gluedToBase K t)
instance

isLocallyNoetherian_glued

L936 ↗
AlgebraicCurve.CurveModel.isLocallyNoetherian_glued
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Noetherian
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
instance isLocallyNoetherian_glued : IsLocallyNoetherian (glued K t)
instance

quasiSeparated_gluedToBase

L951 ↗
AlgebraicCurve.CurveModel.quasiSeparated_gluedToBase
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Noetherian
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
instance quasiSeparated_gluedToBase : QuasiSeparated (gluedToBase K t)
def

liftOfRange

L961 ↗
AlgebraicCurve.CurveModel.liftOfRange
Documentation

The lift of a ring homomorphism through an injective map containing its image.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section RingLemmas
variable {B R F : Type*} [CommRing B] [CommRing R] [CommRing F]
Lean source · statement
def liftOfRange (j : R →+* F) (hj : Function.Injective j) (g : B →+* F)
    (h : ∀ b, g b ∈ j.range) : B →+* R
theorem

liftOfRange_spec

L967 ↗
AlgebraicCurve.CurveModel.liftOfRange_spec
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section RingLemmas
variable {B R F : Type*} [CommRing B] [CommRing R] [CommRing F]
Lean source · statement
theorem liftOfRange_spec (j : R →+* F) (hj : Function.Injective j) (g : B →+* F)
    (h : ∀ b, g b ∈ j.range) (b : B) : j (liftOfRange j hj g h b) = g b
theorem

comp_liftOfRange

L974 ↗
AlgebraicCurve.CurveModel.comp_liftOfRange
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section RingLemmas
variable {B R F : Type*} [CommRing B] [CommRing R] [CommRing F]
Lean source · statement
theorem comp_liftOfRange (j : R →+* F) (hj : Function.Injective j) (g : B →+* F)
    (h : ∀ b, g b ∈ j.range) : j.comp (liftOfRange j hj g h) = g
theorem

SpecMap_cancel

L982 ↗
AlgebraicCurve.CurveModel.SpecMap_cancel
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section SpecLemmas
Lean source · statement
theorem SpecMap_cancel {R F Y : CommRingCat.{u}} (j : R ⟶ F) (hj : Function.Injective j)
    (u v : Spec R ⟶ Spec Y) (h : Spec.map j ≫ u = Spec.map j ≫ v) : u = v
theorem

fromSpecStalk_comp

L990 ↗
AlgebraicCurve.CurveModel.fromSpecStalk_comp
Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section SpecLemmas
Lean source · statement
theorem fromSpecStalk_comp {X : Scheme.{u}} {A : CommRingCat.{u}} (f : X ⟶ Spec A) (x : X) :
    X.fromSpecStalk x ≫ f =
      Spec.map (StructureSheaf.toStalk A (specPoint (f.base x)) ≫ f.stalkMap x)
theorem

exists_eq_SpecMap_comp_fromSpecStalk

L1011 ↗
AlgebraicCurve.CurveModel.exists_eq_SpecMap_comp_fromSpecStalk
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section LiftLemma
variable [Fact (t ≠ 0)]
Lean source · statement
theorem exists_eq_SpecMap_comp_fromSpecStalk {F : Type u} [Field F] (f : Spec (.of F) ⟶ glued K t)
    {x : glued K t} (hx : f.base (closedPoint F) = x) :
    ∃ φ : (glued K t).presheaf.stalk x ⟶ CommRingCat.of F,
      IsLocalHom φ.hom ∧ f = Spec.map φ ≫ (glued K t).fromSpecStalk x
theorem

hasLift_of_range

L1018 ↗
AlgebraicCurve.CurveModel.hasLift_of_range
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section LiftLemma
variable [Fact (t ≠ 0)]
Lean source · statement
theorem hasLift_of_range (S : ValuativeCommSq (gluedToBase K t)) {x P : glued K t} (hsp : x ⤳ P)
    (φ : (glued K t).presheaf.stalk x ⟶ CommRingCat.of S.K)
    (h₁ : S.i₁ = Spec.map φ ≫ (glued K t).fromSpecStalk x)
    (hrange : ∀ s : (glued K t).presheaf.stalk P,
      φ ((glued K t).presheaf.stalkSpecializes hsp s) ∈ (algebraMap S.R S.K).range) :
    S.commSq.HasLift
theorem

ringCompat

L1039 ↗
AlgebraicCurve.CurveModel.ringCompat
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section LiftLemma
variable [Fact (t ≠ 0)]
Lean source · statement
theorem ringCompat (S : ValuativeCommSq (gluedToBase K t)) {x : glued K t}
    (φ : (glued K t).presheaf.stalk x ⟶ CommRingCat.of S.K)
    (h₁ : S.i₁ = Spec.map φ ≫ (glued K t).fromSpecStalk x) :
    (StructureSheaf.toStalk (CommRingCat.of K) ((gluedToBase K t).base x) ≫
        (gluedToBase K t).stalkMap x) ≫ φ =
      Spec.preimage S.i₂ ≫ CommRingCat.ofHom (algebraMap S.R S.K)
theorem

stalkMap_toStalk_genericPoint

L1057 ↗
AlgebraicCurve.CurveModel.stalkMap_toStalk_genericPoint
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Generic
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem stalkMap_toStalk_genericPoint (a : K) :
    (gluedToBase K t).stalkMap (genericPoint (glued K t))
        (StructureSheaf.toStalk (CommRingCat.of K) _ a) =
      baseToFunctionField (gluedToBase K t) a
def

gL

L1071 ↗
AlgebraicCurve.CurveModel.gL
Documentation

The function field map to the fraction field in the valuative diagram.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Generic
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (S : ValuativeCommSq (gluedToBase K t))
  (φ : (glued K t).presheaf.stalk (genericPoint (glued K t)) ⟶ CommRingCat.of S.K)
Lean source · statement
def gL : L →+* S.K
theorem

gL_ffEquiv_symm

L1074 ↗
AlgebraicCurve.CurveModel.gL_ffEquiv_symm
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Generic
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (S : ValuativeCommSq (gluedToBase K t))
  (φ : (glued K t).presheaf.stalk (genericPoint (glued K t)) ⟶ CommRingCat.of S.K)
omit [CharZero K] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem gL_ffEquiv_symm (y : (glued K t).functionField) :
    gL K t S φ ((gluedFunctionFieldEquiv K t).symm y) = φ y
def

pullbackVS

L1079 ↗
AlgebraicCurve.CurveModel.pullbackVS
Documentation

The valuation subring pulled back along the function field map.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Generic
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (S : ValuativeCommSq (gluedToBase K t))
  (φ : (glued K t).presheaf.stalk (genericPoint (glued K t)) ⟶ CommRingCat.of S.K)
Lean source · full declaration
def pullbackVS : ValuationSubring L where
  toSubring := (algebraMap S.R S.K).range.comap (gL K t S φ)
  mem_or_inv_mem' y := by
    rcases ValuationRing.isInteger_or_isInteger S.R (gL K t S φ y) with ⟨r, hr⟩ | ⟨r, hr⟩
    · exact Or.inl ⟨r, hr⟩
    · exact Or.inr ⟨r, by rw [map_inv₀]; exact hr⟩
theorem

mem_pullbackVS_iff

L1087 ↗
AlgebraicCurve.CurveModel.mem_pullbackVS_iff
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Generic
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (S : ValuativeCommSq (gluedToBase K t))
  (φ : (glued K t).presheaf.stalk (genericPoint (glued K t)) ⟶ CommRingCat.of S.K)
omit [CharZero K] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem mem_pullbackVS_iff (y : L) :
    y ∈ pullbackVS K t S φ ↔ gL K t S φ y ∈ (algebraMap S.R S.K).range
theorem

algebraMap_mem_pullbackVS

L1091 ↗
AlgebraicCurve.CurveModel.algebraMap_mem_pullbackVS
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Generic
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (S : ValuativeCommSq (gluedToBase K t))
  (φ : (glued K t).presheaf.stalk (genericPoint (glued K t)) ⟶ CommRingCat.of S.K)
omit [CharZero K] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem algebraMap_mem_pullbackVS
    (h₁ : S.i₁ = Spec.map φ ≫ (glued K t).fromSpecStalk (genericPoint (glued K t))) (a : K) :
    algebraMap K L a ∈ pullbackVS K t S φ
theorem

hasLift_generic_top

L1105 ↗
AlgebraicCurve.CurveModel.hasLift_generic_top
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Generic
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (S : ValuativeCommSq (gluedToBase K t))
  (φ : (glued K t).presheaf.stalk (genericPoint (glued K t)) ⟶ CommRingCat.of S.K)
omit [CharZero K] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem hasLift_generic_top
    (h₁ : S.i₁ = Spec.map φ ≫ (glued K t).fromSpecStalk (genericPoint (glued K t)))
    (hO : pullbackVS K t S φ = ⊤) : S.commSq.HasLift
theorem

hasLift_generic_centre

L1115 ↗
AlgebraicCurve.CurveModel.hasLift_generic_centre
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Generic
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (S : ValuativeCommSq (gluedToBase K t))
  (φ : (glued K t).presheaf.stalk (genericPoint (glued K t)) ⟶ CommRingCat.of S.K)
omit [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem hasLift_generic_centre (s : L) [FiniteDimensional K⟮s⟯ L]
    (i : chartRing K ({s} : Set L) →ₐ[K] chartRing K ({t, t⁻¹} : Set L))
    (hi : ∀ a : chartRing K ({s} : Set L), (i a : L) = a)
    (ιA : Spec (CommRingCat.of (chartRing K ({s} : Set L))) ⟶ glued K t) [IsOpenImmersion ιA]
    [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
    (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
    (h₁ : S.i₁ = Spec.map φ ≫ (glued K t).fromSpecStalk (genericPoint (glued K t)))
    (hO : pullbackVS K t S φ ≠ ⊤) (hs : s ∈ pullbackVS K t S φ) : S.commSq.HasLift
theorem

hasLift_generic

L1145 ↗
AlgebraicCurve.CurveModel.hasLift_generic
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Generic
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (S : ValuativeCommSq (gluedToBase K t))
  (φ : (glued K t).presheaf.stalk (genericPoint (glued K t)) ⟶ CommRingCat.of S.K)
Lean source · statement
theorem hasLift_generic (hgen : S.i₁.base (closedPoint S.K) = genericPoint (glued K t)) :
    S.commSq.HasLift
def

stalkChartEquiv

L1168 ↗
AlgebraicCurve.CurveModel.stalkChartEquiv
Documentation

The stalk identification induced by an open affine chart.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Closed
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
Lean source · statement
def stalkChartEquiv :
    (glued K t).presheaf.stalk (ιA.base p) ≃+* (Spec (CommRingCat.of A)).presheaf.stalk p
def

φA

L1173 ↗
AlgebraicCurve.CurveModel.φA
Documentation

The chart stalk map to the fraction field in the valuative diagram.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Closed
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
Lean source · statement
def φA : (Spec (CommRingCat.of A)).presheaf.stalk p →+* S.K
def

gA

L1177 ↗
AlgebraicCurve.CurveModel.gA
Documentation

The map on the affine chart ring induced by the given stalk map.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Closed
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
Lean source · statement
def gA : A →+* S.K
theorem

φA_stalkMap

L1180 ↗
AlgebraicCurve.CurveModel.φA_stalkMap
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Closed
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem φA_stalkMap (y : (glued K t).presheaf.stalk (ιA.base p)) :
    φA K t A ιA S p φ (ιA.stalkMap p y) = φ y
theorem

stalkMap_chart_toStalk

L1187 ↗
AlgebraicCurve.CurveModel.stalkMap_chart_toStalk
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Closed
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] [IsOpenImmersion ιA] in
include ιA_toBase in
Lean source · statement
theorem stalkMap_chart_toStalk (a : K) :
    ιA.stalkMap p ((gluedToBase K t).stalkMap (ιA.base p)
        (StructureSheaf.toStalk (CommRingCat.of K) _ a)) =
      StructureSheaf.toStalk A p (algebraMap K A a)
theorem

gA_algebraMap

L1209 ↗
AlgebraicCurve.CurveModel.gA_algebraMap
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Closed
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
include ιA_toBase in
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem gA_algebraMap (h₁ : S.i₁ = Spec.map φ ≫ (glued K t).fromSpecStalk (ιA.base p)) (a : K) :
    gA K t A ιA S p φ (algebraMap K A a) =
      algebraMap S.R S.K ((Spec.preimage S.i₂).hom a)
theorem

gA_eq_zero

L1222 ↗
AlgebraicCurve.CurveModel.gA_eq_zero
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Closed
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
variable [hmax : p.asIdeal.IsMaximal]
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] hmax in
Lean source · statement
theorem gA_eq_zero [IsLocalHom φ.hom] (m : A) (hm : m ∈ p.asIdeal) : gA K t A ιA S p φ m = 0
theorem

gA_mem_range

L1240 ↗
AlgebraicCurve.CurveModel.gA_mem_range
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Closed
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
variable [hmax : p.asIdeal.IsMaximal]
include ιA_toBase in
omit [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem gA_mem_range [Algebra.FiniteType K A] [IsLocalHom φ.hom]
    (h₁ : S.i₁ = Spec.map φ ≫ (glued K t).fromSpecStalk (ιA.base p)) (a : A) :
    gA K t A ιA S p φ a ∈ (algebraMap S.R S.K).range
theorem

exists_gA_mul_gA_eq_one

L1266 ↗
AlgebraicCurve.CurveModel.exists_gA_mul_gA_eq_one
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Closed
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
variable [hmax : p.asIdeal.IsMaximal]
omit [CharZero K] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem exists_gA_mul_gA_eq_one [IsLocalHom φ.hom] (b : A) (hb : b ∉ p.asIdeal) :
    ∃ c : A, gA K t A ιA S p φ b * gA K t A ιA S p φ c = 1
theorem

φ_mem_range

L1281 ↗
AlgebraicCurve.CurveModel.φ_mem_range
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Closed
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
variable (A : Subalgebra K L) (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
  (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
  (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
  (φ : (glued K t).presheaf.stalk (ιA.base p) ⟶ CommRingCat.of S.K)
variable [hmax : p.asIdeal.IsMaximal]
include ιA_toBase in
omit [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem φ_mem_range [Algebra.FiniteType K A] [IsLocalHom φ.hom]
    (h₁ : S.i₁ = Spec.map φ ≫ (glued K t).fromSpecStalk (ιA.base p))
    (s : (glued K t).presheaf.stalk (ιA.base p)) : φ s ∈ (algebraMap S.R S.K).range
theorem

hasLift_closed

L1315 ↗
AlgebraicCurve.CurveModel.hasLift_closed
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section ClosedLift
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
omit [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L] in
Lean source · statement
theorem hasLift_closed (A : Subalgebra K L) [Algebra.FiniteType K A]
    (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
    (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
    (S : ValuativeCommSq (gluedToBase K t)) (p : Spec (CommRingCat.of A))
    (hp : S.i₁.base (closedPoint S.K) = ιA.base p) (hmax : p.asIdeal.IsMaximal) :
    S.commSq.HasLift
theorem

valuativeCriterion_existence

L1327 ↗
AlgebraicCurve.CurveModel.valuativeCriterion_existence
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section ClosedLift
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
theorem valuativeCriterion_existence : ValuativeCriterion.Existence (gluedToBase K t)
theorem

range_subset_of_closedPoint_mem

L1353 ↗
AlgebraicCurve.CurveModel.range_subset_of_closedPoint_mem
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Uniqueness
variable [Fact (t ≠ 0)]
Lean source · statement
theorem range_subset_of_closedPoint_mem {R : Type u} [CommRing R] [IsLocalRing R]
    (l : Spec (CommRingCat.of R) ⟶ glued K t) {X : Scheme.{u}} (ι : X ⟶ glued K t)
    [IsOpenImmersion ι] (h : l.base (closedPoint R) ∈ Set.range ι.base) :
    Set.range l.base ⊆ Set.range ι.base
theorem

liftStruct_eq_of_mem_range

L1362 ↗
AlgebraicCurve.CurveModel.liftStruct_eq_of_mem_range
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Uniqueness
variable [Fact (t ≠ 0)]
Lean source · statement
theorem liftStruct_eq_of_mem_range {A : Type u} [CommRing A]
    (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
    (S : ValuativeCommSq (gluedToBase K t)) (l₁ l₂ : S.commSq.LiftStruct)
    (h₁ : l₁.l.base (closedPoint S.R) ∈ Set.range ιA.base)
    (h₂ : l₂.l.base (closedPoint S.R) ∈ Set.range ιA.base) : l₁ = l₂
theorem

incl₀_tChart_mul_inclInf_tInvChart

L1386 ↗
AlgebraicCurve.CurveModel.incl₀_tChart_mul_inclInf_tInvChart
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Uniqueness
variable [Fact (t ≠ 0)]
Lean source · statement
theorem incl₀_tChart_mul_inclInf_tInvChart :
    incl₀ K t (tChart K t) * inclInf K t (tInvChart K t) = 1
theorem

false_of_liftStruct_cross

L1392 ↗
AlgebraicCurve.CurveModel.false_of_liftStruct_cross
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Uniqueness
variable [Fact (t ≠ 0)]
Lean source · statement
theorem false_of_liftStruct_cross (S : ValuativeCommSq (gluedToBase K t))
    (l₁ l₂ : S.commSq.LiftStruct)
    (h₁ : l₁.l.base (closedPoint S.R) ∈ Set.range (ι₀ K t).base)
    (h₁' : l₁.l.base (closedPoint S.R) ∉ Set.range (ιInf K t).base)
    (h₂ : l₂.l.base (closedPoint S.R) ∈ Set.range (ιInf K t).base)
    (h₂' : l₂.l.base (closedPoint S.R) ∉ Set.range (ι₀ K t).base) : False
theorem

valuativeCriterion_uniqueness

L1463 ↗
AlgebraicCurve.CurveModel.valuativeCriterion_uniqueness
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Uniqueness
variable [Fact (t ≠ 0)]
Lean source · statement
theorem valuativeCriterion_uniqueness : ValuativeCriterion.Uniqueness (gluedToBase K t)
instance

isProper_gluedToBase

L1486 ↗
AlgebraicCurve.CurveModel.isProper_gluedToBase
Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
section Proper
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
instance isProper_gluedToBase : IsProper (gluedToBase K t)
def

secTop

L1500 ↗
AlgebraicCurve.CurveModel.secTop
Documentation

An affine ring element regarded as a global section of its spectrum.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section ChartGerms
variable (A : Subalgebra K L)
Lean source · statement
def secTop (r : A) : Γ(Spec (CommRingCat.of A), ⊤)
theorem

mem_basicOpen_secTop

L1502 ↗
AlgebraicCurve.CurveModel.mem_basicOpen_secTop
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section ChartGerms
variable (A : Subalgebra K L)
Lean source · statement
theorem mem_basicOpen_secTop (r : A) (p : Spec (CommRingCat.of A)) :
    p ∈ (Spec (CommRingCat.of A)).basicOpen (secTop K A r) ↔ r ∉ p.asIdeal
theorem

germ_res_secTop

L1507 ↗
AlgebraicCurve.CurveModel.germ_res_secTop
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section ChartGerms
variable (A : Subalgebra K L)
Lean source · statement
theorem germ_res_secTop (r : A) (V : (Spec (CommRingCat.of A)).Opens) (p : Spec (CommRingCat.of A))
    (hp : p ∈ V) :
    (Spec (CommRingCat.of A)).presheaf.germ V p hp
        ((Spec (CommRingCat.of A)).presheaf.map (homOfLE (le_top : V ≤ ⊤)).op (secTop K A r)) =
      StructureSheaf.toStalk A (specPoint p) r
theorem

stalkMap_germ_appIso_inv

L1517 ↗
AlgebraicCurve.CurveModel.stalkMap_germ_appIso_inv
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section ChartGerms
variable (A : Subalgebra K L)
variable [Fact (t ≠ 0)] (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
Lean source · statement
theorem stalkMap_germ_appIso_inv (V : (Spec (CommRingCat.of A)).Opens)
    (τ : Γ(Spec (CommRingCat.of A), V)) (p : Spec (CommRingCat.of A)) (hp : p ∈ V) :
    ιA.stalkMap p ((glued K t).presheaf.germ (ιA ''ᵁ V) (ιA.base p) ⟨p, hp, rfl⟩
        ((ιA.appIso V).inv τ)) = (Spec (CommRingCat.of A)).presheaf.germ V p hp τ
def

cSec

L1534 ↗
AlgebraicCurve.CurveModel.cSec
Documentation

A base-field element regarded as a section on an open of the glued scheme.

Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section ChartGerms
variable (A : Subalgebra K L)
variable [Fact (t ≠ 0)] (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
Lean source · statement
def cSec (a : K) (W : (glued K t).Opens) : Γ(glued K t, W)
theorem

stalkMap_germ_cSec

L1539 ↗
AlgebraicCurve.CurveModel.stalkMap_germ_cSec
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section ChartGerms
variable (A : Subalgebra K L)
variable [Fact (t ≠ 0)] (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
omit [IsOpenImmersion ιA] in
Lean source · statement
theorem stalkMap_germ_cSec
    (ιA_toBase : ιA ≫ gluedToBase K t = Spec.map (CommRingCat.ofHom (algebraMap K A)))
    (a : K) (W : (glued K t).Opens) (p : Spec (CommRingCat.of A)) (hp : ιA.base p ∈ W) :
    ιA.stalkMap p ((glued K t).presheaf.germ W (ιA.base p) hp (cSec K t a W)) =
      StructureSheaf.toStalk A (specPoint p) (algebraMap K A a)
theorem

isUnit_stalkMap_iff

L1553 ↗
AlgebraicCurve.CurveModel.isUnit_stalkMap_iff
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section ChartGerms
variable (A : Subalgebra K L)
variable [Fact (t ≠ 0)] (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
Lean source · statement
theorem isUnit_stalkMap_iff (p : Spec (CommRingCat.of A))
    (y : (glued K t).presheaf.stalk (ιA.base p)) : IsUnit (ιA.stalkMap p y) ↔ IsUnit y
theorem

thetaHom_algebraMap

L1565 ↗
AlgebraicCurve.CurveModel.thetaHom_algebraMap
Source context 16 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section ChartGerms
variable (A : Subalgebra K L)
variable [Fact (t ≠ 0)] (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
variable [FiniteDimensional K⟮t⟯ L]
variable (i : A →ₐ[K] chartRing K ({t, t⁻¹} : Set L)) (hi : ∀ a : A, (i a : L) = a)
  [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
  (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
include hi in
omit [Fact (t ≠ 0)] [IsOpenImmersion ιA] in
Lean source · statement
theorem thetaHom_algebraMap (p : Spec (CommRingCat.of A)) (r : A) :
    thetaHom K t A i (specPoint p)
      (StructureSheaf.toStalk A (specPoint p) r) = r
theorem

ffEquiv_symm_germ_appIso_inv

L1571 ↗
AlgebraicCurve.CurveModel.ffEquiv_symm_germ_appIso_inv
Source context 15 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section ChartGerms
variable (A : Subalgebra K L)
variable [Fact (t ≠ 0)] (ιA : Spec (CommRingCat.of A) ⟶ glued K t) [IsOpenImmersion ιA]
variable [FiniteDimensional K⟮t⟯ L]
variable (i : A →ₐ[K] chartRing K ({t, t⁻¹} : Set L)) (hi : ∀ a : A, (i a : L) = a)
  [IsOpenImmersion (Spec.map (CommRingCat.ofHom i.toRingHom))]
  (comm : Spec.map (CommRingCat.ofHom i.toRingHom) ≫ ιA = ιU K t)
include hi comm in
Lean source · statement
theorem ffEquiv_symm_germ_appIso_inv (V : (Spec (CommRingCat.of A)).Opens)
    (τ : Γ(Spec (CommRingCat.of A), V)) (p : Spec (CommRingCat.of A)) (hp : p ∈ V)
    (hη : genericPoint (glued K t) ∈ ιA ''ᵁ V) :
    (gluedFunctionFieldEquiv K t).symm
        ((glued K t).presheaf.germ (ιA ''ᵁ V) (genericPoint (glued K t)) hη ((ιA.appIso V).inv τ)) =
      thetaHom K t A i p ((Spec (CommRingCat.of A)).presheaf.germ V p hp τ)
def

tma

L1596 ↗
AlgebraicCurve.CurveModel.tma
Documentation

The finite chart coordinate minus a base-field scalar.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
def tma : chartRing K ({t} : Set L)
def

gInf

L1599 ↗
AlgebraicCurve.CurveModel.gInf
Documentation

One minus the base-field scalar times the infinite chart coordinate.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
def gInf : chartRing K ({t⁻¹} : Set L)
theorem

coe_tma

L1601 ↗
AlgebraicCurve.CurveModel.coe_tma
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
theorem coe_tma : (tma K t a : L) = t - algebraMap K L a
theorem

coe_gInf

L1604 ↗
AlgebraicCurve.CurveModel.coe_gInf
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
theorem coe_gInf : (gInf K t a : L) = 1 - algebraMap K L a * t⁻¹
theorem

incl₀_tma

L1608 ↗
AlgebraicCurve.CurveModel.incl₀_tma
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
theorem incl₀_tma [Fact (t ≠ 0)] :
    incl₀ K t (tma K t a) = incl₀ K t (tChart K t) * inclInf K t (gInf K t a)
theorem

gInf_add

L1614 ↗
AlgebraicCurve.CurveModel.gInf_add
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
theorem gInf_add : gInf K t a + algebraMap K _ a * tInvChart K t = 1
theorem

tma_add

L1617 ↗
AlgebraicCurve.CurveModel.tma_add
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
theorem tma_add : tma K t a + algebraMap K _ a = tChart K t
def

U₁

L1621 ↗
AlgebraicCurve.CurveModel.U₁
Documentation

The basic open where the shifted finite-chart coordinate is invertible.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
def U₁ : (X₀ K t).Opens
def

U₂

L1624 ↗
AlgebraicCurve.CurveModel.U₂
Documentation

The basic open where the corresponding infinite-chart function is invertible.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
def U₂ : (XInf K t).Opens
theorem

mem_U₁_iff

L1627 ↗
AlgebraicCurve.CurveModel.mem_U₁_iff
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
theorem mem_U₁_iff (p : X₀ K t) : p ∈ U₁ K t a ↔ tma K t a ∉ p.asIdeal
theorem

mem_U₂_iff

L1630 ↗
AlgebraicCurve.CurveModel.mem_U₂_iff
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
theorem mem_U₂_iff (q : XInf K t) : q ∈ U₂ K t a ↔ gInf K t a ∉ q.asIdeal
theorem

isUnit_res_tma

L1633 ↗
AlgebraicCurve.CurveModel.isUnit_res_tma
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
theorem isUnit_res_tma : IsUnit ((Spec (CommRingCat.of (chartRing K ({t} : Set L)))).presheaf.map
    (homOfLE ((X₀ K t).basicOpen_le (secTop K (chartRing K ({t} : Set L)) (tma K t a)))).op
    (secTop K (chartRing K ({t} : Set L)) (tma K t a)))
theorem

isUnit_res_gInf

L1638 ↗
AlgebraicCurve.CurveModel.isUnit_res_gInf
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
theorem isUnit_res_gInf : IsUnit ((Spec (CommRingCat.of (chartRing K ({t⁻¹} : Set L)))).presheaf.map
    (homOfLE ((XInf K t).basicOpen_le (secTop K (chartRing K ({t⁻¹} : Set L)) (gInf K t a)))).op
    (secTop K (chartRing K ({t⁻¹} : Set L)) (gInf K t a)))
def

σ₁

L1644 ↗
AlgebraicCurve.CurveModel.σ₁
Documentation

The inverse of the shifted finite-chart coordinate on its basic open.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
def σ₁ : Γ(X₀ K t, U₁ K t a)
def

σ₂

L1647 ↗
AlgebraicCurve.CurveModel.σ₂
Documentation

The inverse coordinate divided by the corresponding infinite-chart function.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
def σ₂ : Γ(XInf K t, U₂ K t a)
theorem

germ_σ₁_mul

L1653 ↗
AlgebraicCurve.CurveModel.germ_σ₁_mul
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
theorem germ_σ₁_mul (p : PrimeSpectrum (chartRing K ({t} : Set L))) (hp : p ∈ U₁ K t a) :
    (Spec (CommRingCat.of (chartRing K ({t} : Set L)))).presheaf.germ
      (U₁ K t a) (topPoint p) hp (σ₁ K t a) *
      algebraMap _ ((Spec (CommRingCat.of (chartRing K ({t} : Set L)))).presheaf.stalk (topPoint p))
        (tma K t a) = 1
theorem

germ_σ₂_mul

L1674 ↗
AlgebraicCurve.CurveModel.germ_σ₂_mul
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section LocalSections
variable (a : K)
Lean source · statement
theorem germ_σ₂_mul (q : PrimeSpectrum (chartRing K ({t⁻¹} : Set L))) (hq : q ∈ U₂ K t a) :
    (Spec (CommRingCat.of (chartRing K ({t⁻¹} : Set L)))).presheaf.germ
      (U₂ K t a) (topPoint q) hq (σ₂ K t a) *
      algebraMap _ ((Spec (CommRingCat.of (chartRing K ({t⁻¹} : Set L)))).presheaf.stalk (topPoint
        q))
        (gInf K t a) =
    algebraMap _ ((Spec (CommRingCat.of (chartRing K ({t⁻¹} : Set L)))).presheaf.stalk (topPoint q))
      (tInvChart K t)
def

V₁

L1713 ↗
AlgebraicCurve.CurveModel.V₁
Documentation

The image of the chosen finite-chart open in the glued scheme.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
Lean source · statement
def V₁ : (glued K t).Opens
def

V₂

L1716 ↗
AlgebraicCurve.CurveModel.V₂
Documentation

The image of the chosen infinite-chart open in the glued scheme.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
Lean source · statement
def V₂ : (glued K t).Opens
def

Ua

L1719 ↗
AlgebraicCurve.CurveModel.Ua
Documentation

The union of the chosen finite and infinite chart opens.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
Lean source · statement
def Ua : (glued K t).Opens
theorem

isAffineOpen_V₁

L1721 ↗
AlgebraicCurve.CurveModel.isAffineOpen_V₁
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
Lean source · statement
theorem isAffineOpen_V₁ : IsAffineOpen (V₁ K t a)
theorem

isAffineOpen_V₂

L1724 ↗
AlgebraicCurve.CurveModel.isAffineOpen_V₂
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
Lean source · statement
theorem isAffineOpen_V₂ : IsAffineOpen (V₂ K t a)
def

f₁'

L1728 ↗
AlgebraicCurve.CurveModel.f₁'
Documentation

The section transported from the finite chart to its image in the glued scheme.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
Lean source · statement
def f₁' : Γ(glued K t, V₁ K t a)
def

f₂'

L1731 ↗
AlgebraicCurve.CurveModel.f₂'
Documentation

The section transported from the infinite chart to its image in the glued scheme.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
Lean source · statement
def f₂' : Γ(glued K t, V₂ K t a)
theorem

one_sub_ne_zero

L1737 ↗
AlgebraicCurve.CurveModel.one_sub_ne_zero
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
variable (ha : (t - algebraMap K L a) ≠ 0)
include ha in
omit [Fact (t ≠ 0)] in
Lean source · statement
theorem one_sub_ne_zero [Fact (t ≠ 0)] : (1 - algebraMap K L a * t⁻¹) ≠ 0
theorem

genericPoint_mem_U₁

L1746 ↗
AlgebraicCurve.CurveModel.genericPoint_mem_U₁
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
variable (ha : (t - algebraMap K L a) ≠ 0)
include ha in
omit [Fact (t ≠ 0)] in
Lean source · statement
theorem genericPoint_mem_U₁ : genericPoint (X₀ K t) ∈ U₁ K t a
theorem

genericPoint_mem_U₂

L1755 ↗
AlgebraicCurve.CurveModel.genericPoint_mem_U₂
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
variable (ha : (t - algebraMap K L a) ≠ 0)
include ha in
Lean source · statement
theorem genericPoint_mem_U₂ : genericPoint (XInf K t) ∈ U₂ K t a
theorem

genericPoint_mem

L1764 ↗
AlgebraicCurve.CurveModel.genericPoint_mem
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
variable (ha : (t - algebraMap K L a) ≠ 0)
include ha in
Lean source · statement
theorem genericPoint_mem : genericPoint (glued K t) ∈ V₁ K t a ⊓ V₂ K t a
theorem

val_f₁'

L1773 ↗
AlgebraicCurve.CurveModel.val_f₁'
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
variable (ha : (t - algebraMap K L a) ≠ 0)
variable [FiniteDimensional K⟮t⟯ L]
include ha in
Lean source · statement
theorem val_f₁' (hη : genericPoint (glued K t) ∈ V₁ K t a) :
    (gluedFunctionFieldEquiv K t).symm
        ((glued K t).presheaf.germ (V₁ K t a) (genericPoint (glued K t)) hη (f₁' K t a)) =
      (t - algebraMap K L a)⁻¹
theorem

val_f₂'

L1807 ↗
AlgebraicCurve.CurveModel.val_f₂'
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
variable (ha : (t - algebraMap K L a) ≠ 0)
variable [FiniteDimensional K⟮t⟯ L]
include ha in
Lean source · statement
theorem val_f₂' (hη : genericPoint (glued K t) ∈ V₂ K t a) :
    (gluedFunctionFieldEquiv K t).symm
        ((glued K t).presheaf.germ (V₂ K t a) (genericPoint (glued K t)) hη (f₂' K t a)) =
      t⁻¹ * (1 - algebraMap K L a * t⁻¹)⁻¹
theorem

res_f₁'_eq_res_f₂'

L1848 ↗
AlgebraicCurve.CurveModel.res_f₁'_eq_res_f₂'
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
variable (ha : (t - algebraMap K L a) ≠ 0)
variable [FiniteDimensional K⟮t⟯ L]
include ha in
Lean source · statement
theorem res_f₁'_eq_res_f₂' (W : (glued K t).Opens) (h₁ : W ≤ V₁ K t a) (h₂ : W ≤ V₂ K t a)
    (hη : genericPoint (glued K t) ∈ W) :
    (glued K t).presheaf.map (homOfLE h₁).op (f₁' K t a) =
    (glued K t).presheaf.map (homOfLE h₂).op (f₂' K t a)
def

cover

L1859 ↗
AlgebraicCurve.CurveModel.cover
Documentation

The chosen two-open covering indexed by a Boolean.

Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
variable (ha : (t - algebraMap K L a) ≠ 0)
variable [FiniteDimensional K⟮t⟯ L]
Lean source · statement
def cover : Bool → (glued K t).Opens
theorem

exists_glued_section

L1862 ↗
AlgebraicCurve.CurveModel.exists_glued_section
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Values
variable [Fact (t ≠ 0)] (a : K)
variable (ha : (t - algebraMap K L a) ≠ 0)
variable [FiniteDimensional K⟮t⟯ L]
include ha in
Lean source · statement
theorem exists_glued_section : ∃ f : Γ(glued K t, Ua K t a),
    (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a ∧
    (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a
theorem

f₀_appTop_secTop

L1891 ↗
AlgebraicCurve.CurveModel.f₀_appTop_secTop
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
omit [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem f₀_appTop_secTop (r : chartRing K ({t} : Set L)) :
    (f₀ K t).appTop (secTop K _ r) = secTop K _ (incl₀ K t r)
theorem

fInf_appTop_secTop

L1898 ↗
AlgebraicCurve.CurveModel.fInf_appTop_secTop
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
omit [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem fInf_appTop_secTop (r : chartRing K ({t⁻¹} : Set L)) :
    (fInf K t).appTop (secTop K _ r) = secTop K _ (inclInf K t r)
theorem

tma_not_mem_iff

L1905 ↗
AlgebraicCurve.CurveModel.tma_not_mem_iff
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem tma_not_mem_iff (p : X₀ K t) (q : XInf K t) (h : (ι₀ K t).base p = (ιInf K t).base q) :
    tma K t a ∉ p.asIdeal ↔ gInf K t a ∉ q.asIdeal
def

fTwo

L1930 ↗
AlgebraicCurve.CurveModel.fTwo
Documentation

One plus the base-field scalar times the glued reciprocal section.

Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
Lean source · statement
def fTwo : Γ(glued K t, Ua K t a)
theorem

span_eq_top

L1933 ↗
AlgebraicCurve.CurveModel.span_eq_top
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem span_eq_top : Ideal.span ({f, fTwo K t a f} : Set Γ(glued K t, Ua K t a)) = ⊤
theorem

stalkMap_germ_f_V₁

L1939 ↗
AlgebraicCurve.CurveModel.stalkMap_germ_f_V₁
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
include hf₁ in
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem stalkMap_germ_f_V₁ (p : X₀ K t) (hp : p ∈ U₁ K t a) :
    (ι₀ K t).stalkMap p ((glued K t).presheaf.germ (Ua K t a) ((ι₀ K t).base p)
        (le_sup_left (α := (glued K t).Opens) ⟨p, hp, rfl⟩) f) =
      (Spec (CommRingCat.of (chartRing K ({t} : Set L)))).presheaf.germ
        (U₁ K t a) p hp (σ₁ K t a)
theorem

stalkMap_germ_f_V₂

L1954 ↗
AlgebraicCurve.CurveModel.stalkMap_germ_f_V₂
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
include hf₂ in
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem stalkMap_germ_f_V₂ (q : XInf K t) (hq : q ∈ U₂ K t a) :
    (ιInf K t).stalkMap q ((glued K t).presheaf.germ (Ua K t a) ((ιInf K t).base q)
        (le_sup_right (α := (glued K t).Opens) ⟨q, hq, rfl⟩) f) =
      (Spec (CommRingCat.of (chartRing K ({t⁻¹} : Set L)))).presheaf.germ
        (U₂ K t a) q hq (σ₂ K t a)
theorem

stalkMap_germ_fTwo_V₁

L1969 ↗
AlgebraicCurve.CurveModel.stalkMap_germ_fTwo_V₁
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
include hf₁ in
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem stalkMap_germ_fTwo_V₁ (p : PrimeSpectrum (chartRing K ({t} : Set L)))
    (hp : p ∈ U₁ K t a) :
    (ι₀ K t).stalkMap (schemePoint p)
      ((glued K t).presheaf.germ (Ua K t a) ((ι₀ K t).base (schemePoint p))
        (le_sup_left (α := (glued K t).Opens) ⟨schemePoint p, hp, rfl⟩) (fTwo K t a f)) =
      1 + algebraMap (chartRing K ({t} : Set L))
          ((Spec (CommRingCat.of (chartRing K ({t} : Set L)))).presheaf.stalk (topPoint p))
          (algebraMap K _ a) *
        (Spec (CommRingCat.of (chartRing K ({t} : Set L)))).presheaf.germ
          (U₁ K t a) (topPoint p) hp (σ₁ K t a)
theorem

stalkMap_germ_fTwo_V₂

L1987 ↗
AlgebraicCurve.CurveModel.stalkMap_germ_fTwo_V₂
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
include hf₂ in
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem stalkMap_germ_fTwo_V₂ (q : PrimeSpectrum (chartRing K ({t⁻¹} : Set L)))
    (hq : q ∈ U₂ K t a) :
    (ιInf K t).stalkMap (schemePoint q)
      ((glued K t).presheaf.germ (Ua K t a) ((ιInf K t).base (schemePoint q))
        (le_sup_right (α := (glued K t).Opens) ⟨schemePoint q, hq, rfl⟩) (fTwo K t a f)) =
      1 + algebraMap (chartRing K ({t⁻¹} : Set L))
          ((Spec (CommRingCat.of (chartRing K ({t⁻¹} : Set L)))).presheaf.stalk (topPoint q))
          (algebraMap K _ a) *
        (Spec (CommRingCat.of (chartRing K ({t⁻¹} : Set L)))).presheaf.germ
          (U₂ K t a) (topPoint q) hq (σ₂ K t a)
theorem

basicOpen_f

L2005 ↗
AlgebraicCurve.CurveModel.basicOpen_f
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
include hf₁ hf₂ in
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem basicOpen_f : (glued K t).basicOpen f = V₁ K t a
theorem

basicOpen_fTwo

L2051 ↗
AlgebraicCurve.CurveModel.basicOpen_fTwo
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
include hf₁ hf₂ in
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem basicOpen_fTwo : (glued K t).basicOpen (fTwo K t a f) = V₂ K t a
theorem

isAffineOpen_Ua_of

L2100 ↗
AlgebraicCurve.CurveModel.isAffineOpen_Ua_of
Source context 14 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
include hf₁ hf₂ in
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem isAffineOpen_Ua_of : IsAffineOpen (Ua K t a)
theorem

isAffineOpen_Ua

L2108 ↗
AlgebraicCurve.CurveModel.isAffineOpen_Ua
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
include ha in
Lean source · statement
theorem isAffineOpen_Ua : IsAffineOpen (Ua K t a)
theorem

ιInf_mem_Ua

L2113 ↗
AlgebraicCurve.CurveModel.ιInf_mem_Ua
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem ιInf_mem_Ua (q : XInf K t) (hq : gInf K t a ∉ q.asIdeal) : (ιInf K t).base q ∈ Ua K t a
theorem

ι₀_mem_Ua

L2117 ↗
AlgebraicCurve.CurveModel.ι₀_mem_Ua
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem ι₀_mem_Ua (p : X₀ K t) (hp : tma K t a ∉ p.asIdeal) : (ι₀ K t).base p ∈ Ua K t a
theorem

subsingleton_gInf_mem

L2121 ↗
AlgebraicCurve.CurveModel.subsingleton_gInf_mem
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
omit [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem subsingleton_gInf_mem (q : XInf K t) : {a : K | gInf K t a ∈ q.asIdeal}.Subsingleton
theorem

finite_setOf_not_mem_Ua

L2139 ↗
AlgebraicCurve.CurveModel.finite_setOf_not_mem_Ua
Source context 13 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Affine
variable [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] (a : K) (ha : (t - algebraMap K L a) ≠ 0)
variable (f : Γ(glued K t, Ua K t a))
  (hf₁ : (glued K t).presheaf.map (homOfLE (le_sup_left : V₁ K t a ≤ Ua K t a)).op f = f₁' K t a)
  (hf₂ : (glued K t).presheaf.map (homOfLE (le_sup_right : V₂ K t a ≤ Ua K t a)).op f = f₂' K t a)
omit [FiniteDimensional K⟮t⟯ L] in
Lean source · statement
theorem finite_setOf_not_mem_Ua (x : glued K t) : {a : K | x ∉ Ua K t a}.Finite
theorem

finset_subset_affineOpen_glued

L2168 ↗
AlgebraicCurve.CurveModel.finset_subset_affineOpen_glued
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Packaging
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L]
Lean source · statement
theorem finset_subset_affineOpen_glued :
    ∀ F : Finset (glued K t), ∃ U : (glued K t).Opens, IsAffineOpen U ∧ ∀ x ∈ F, x ∈ U
def

ofGenerator

L2189 ↗
AlgebraicCurve.CurveModel.ofGenerator
Documentation

The curve model constructed from a transcendental coordinate and its two charts.

Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section Packaging
variable [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L]
variable [FiniteDimensional K⟮t⁻¹⟯ L]
Lean source · statement
def ofGenerator (ht : Transcendental K t) : CurveModel K L
def

towerGenerator

L2207 ↗
AlgebraicCurve.CurveModel.towerGenerator
Documentation

The image of the rational-function variable in the extension field.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section TowerPack
variable [Algebra (RatFunc K) L] [IsScalarTower K (RatFunc K) L]
Lean source · statement
def towerGenerator : L
theorem

towerGenerator_ne_zero

L2210 ↗
AlgebraicCurve.CurveModel.towerGenerator_ne_zero
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section TowerPack
variable [Algebra (RatFunc K) L] [IsScalarTower K (RatFunc K) L]
omit [Algebra K L] [IsScalarTower K (RatFunc K) L] in
Lean source · statement
theorem towerGenerator_ne_zero : towerGenerator K (L := L) ≠ 0
theorem

transcendental_towerGenerator

L2214 ↗
AlgebraicCurve.CurveModel.transcendental_towerGenerator
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section TowerPack
variable [Algebra (RatFunc K) L] [IsScalarTower K (RatFunc K) L]
Lean source · statement
theorem transcendental_towerGenerator : Transcendental K (towerGenerator K (L := L))
theorem

coe_algEquivOfTranscendental_towerGenerator

L2218 ↗
AlgebraicCurve.CurveModel.coe_algEquivOfTranscendental_towerGenerator
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section TowerPack
variable [Algebra (RatFunc K) L] [IsScalarTower K (RatFunc K) L]
Lean source · statement
theorem coe_algEquivOfTranscendental_towerGenerator (u : RatFunc K) :
    ((RatFunc.algEquivOfTranscendental (towerGenerator K (L := L))
        (transcendental_towerGenerator K) u : K⟮towerGenerator K (L := L)⟯) : L) =
      algebraMap (RatFunc K) L u
theorem

adjoin_simple_inv_eq

L2241 ↗
AlgebraicCurve.CurveModel.adjoin_simple_inv_eq
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section TowerPack
variable [Algebra (RatFunc K) L] [IsScalarTower K (RatFunc K) L]
omit [Algebra (RatFunc K) L] [IsScalarTower K (RatFunc K) L] in
Lean source · statement
theorem adjoin_simple_inv_eq (x : L) : K⟮x⁻¹⟯ = K⟮x⟯
theorem

finiteDimensional_congr

L2246 ↗
AlgebraicCurve.CurveModel.finiteDimensional_congr
Source context 12 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section TowerPack
variable [Algebra (RatFunc K) L] [IsScalarTower K (RatFunc K) L]
omit [Algebra (RatFunc K) L] [IsScalarTower K (RatFunc K) L] in
Lean source · statement
theorem finiteDimensional_congr {F F' : IntermediateField K L} (h : F = F')
    [hF : FiniteDimensional F L] : FiniteDimensional F' L
theorem

finiteDimensional_adjoin_towerGenerator

L2250 ↗
AlgebraicCurve.CurveModel.finiteDimensional_adjoin_towerGenerator
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section TowerPack
variable [Algebra (RatFunc K) L] [IsScalarTower K (RatFunc K) L]
Lean source · statement
theorem finiteDimensional_adjoin_towerGenerator [FiniteDimensional (RatFunc K) L] :
    FiniteDimensional K⟮towerGenerator K (L := L)⟯ L ∧
      FiniteDimensional K⟮(towerGenerator K (L := L))⁻¹⟯ L
theorem

nonempty_body

L2263 ↗
AlgebraicCurve.CurveModel.nonempty_body
Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IntermediateField IsDedekindDomain
open Topology TopCat
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
open IsLocalRing
open TopologicalSpace
section TowerPack
variable [Algebra (RatFunc K) L] [IsScalarTower K (RatFunc K) L]
Lean source · statement
theorem nonempty_body (K L : Type u) [Field K] [IsAlgClosed K] [CharZero K] [Field L]
    [Algebra K L] [Algebra (RatFunc K) L] [IsScalarTower K (RatFunc K) L]
    [FiniteDimensional (RatFunc K) L] : Nonempty (CurveModel K L)

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