NYLL
Module

Exists_isFinite_hom_proj_of_isProper.lean

Nyll.AlgebraicCurves.Models.Exists_isFinite_hom_proj_of_isProper
33 declarations indexed from sourceView source ↗

Module documentation

Exists is Finite hom proj of is Proper

Imports10
Imported by2

Declarations

abbrev

A

L48 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.A
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section target
variable (K : Type u) [Field K]
Lean source · statement
abbrev A : Type u
abbrev

𝒜

L50 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.𝒜
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section target
variable (K : Type u) [Field K]
Lean source · statement
abbrev 𝒜 : ℕ → Submodule K (A K)
abbrev

P1

L52 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.P1
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section target
variable (K : Type u) [Field K]
Lean source · statement
abbrev P1 : Scheme.{u}
lemma

X_mem

L54 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.X_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section target
variable (K : Type u) [Field K]
Lean source · statement
lemma X_mem (i : Fin 2) : (MvPolynomial.X i : A K) ∈ 𝒜 K 1
instance

finiteType_gradeZero

L57 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.finiteType_gradeZero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section target
variable (K : Type u) [Field K]
Lean source · statement
instance finiteType_gradeZero : Algebra.FiniteType (𝒜 K 0) (A K)
def

ev0

L74 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.ev0
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section target
variable (K : Type u) [Field K]
Lean source · statement
def ev0 : 𝒜 K 0 →+* K
lemma

ev0_algebraMap

L76 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.ev0_algebraMap
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section target
variable (K : Type u) [Field K]
Lean source · statement
lemma ev0_algebraMap (r : K) : ev0 K (algebraMap K (𝒜 K 0) r) = r
lemma

ev0_surjective

L79 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.ev0_surjective
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section target
variable (K : Type u) [Field K]
Lean source · statement
lemma ev0_surjective : Function.Surjective (ev0 K)
def

sK

L81 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.sK
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section target
variable (K : Type u) [Field K]
Lean source · statement
def sK : Spec (.of K) ⟶ Spec (.of (𝒜 K 0))
instance

(anonymous instance)

L83 ↗
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section target
variable (K : Type u) [Field K]
Lean source · statement
instance : IsClosedImmersion (sK K)
def

κ

L91 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.κ
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
def κ : K →+* C.functionField
lemma

Spec_map_κ

L93 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.Spec_map_κ
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
omit [SmoothOfRelativeDimension 1 c] in
Lean source · statement
lemma Spec_map_κ : Spec.map (CommRingCat.ofHom (κ c)) = C.fromSpecStalk (genericPoint C) ≫
  c
def

g

L97 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.g
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
def g (f : C.functionField) : A K →+* C.functionField
lemma

isUnit_g_X0

L99 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.isUnit_g_X0
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
omit [SmoothOfRelativeDimension 1 c] in
Lean source · statement
lemma isUnit_g_X0 (f : C.functionField) : IsUnit (g c f (MvPolynomial.X 0))
def

ψ

L102 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.ψ
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
def ψ (f : C.functionField) : HomogeneousLocalization.Away (𝒜 K) (MvPolynomial.X 0 : A K)
  →+*
    C.functionField
def

p

L109 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.p
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
def p (f : C.functionField) : Spec C.functionField ⟶ P1 K
lemma

p_toSpecZero

L112 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.p_toSpecZero
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
omit [SmoothOfRelativeDimension 1 c] in
Lean source · statement
lemma p_toSpecZero (f : C.functionField) :
    p c f ≫ Proj.toSpecZero (𝒜 K) = C.fromSpecStalk (genericPoint C) ≫ c ≫ sK K
def

R

L145 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.R
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
def R (f : C.functionField) : C ⤏ P1 K
lemma

valuationRing_stalk

L149 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.valuationRing_stalk
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
include c in
Lean source · statement
lemma valuationRing_stalk (x : C) (hx : IsClosed ({x} : Set C)) :
    ValuationRing (C.presheaf.stalk x)
lemma

mem_domain

L166 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.mem_domain
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
lemma mem_domain (f : C.functionField) (x : C) (hx : IsClosed ({x} : Set C)) :
    x ∈ (R c f).domain
lemma

domain_eq_top

L210 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.domain_eq_top
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
lemma domain_eq_top (f : C.functionField) : (R c f).domain = ⊤
def

φ

L222 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.φ
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
def φ (f : C.functionField) : C ⟶ P1 K
lemma

ι_φ

L225 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.ι_φ
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
lemma ι_φ (f : C.functionField) :
    (R c f).toPartialMap.domain.ι ≫ φ c f = (R c f).toPartialMap.hom
lemma

fromSpecStalk_φ

L235 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.fromSpecStalk_φ
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
lemma fromSpecStalk_φ (f : C.functionField) :
    C.fromSpecStalk (genericPoint C) ≫ φ c f = p c f
lemma

φ_toSpecZero

L246 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.φ_toSpecZero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
lemma φ_toSpecZero (f : C.functionField) : φ c f ≫ Proj.toSpecZero (𝒜 K) = c ≫ sK K
instance

isProper_φ

L254 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.isProper_φ
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
instance isProper_φ [IsProper c] (f : C.functionField) : IsProper (φ c f)
lemma

exists_pole

L259 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.exists_pole
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
include c in
Lean source · statement
lemma exists_pole [IsProper c] : ∃ (f : C.functionField) (x : C), IsClosed ({x} : Set C) ∧
    f ∉ (algebraMap (C.presheaf.stalk x) C.functionField).range
def

tX

L274 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.tX
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
def tX : HomogeneousLocalization.Away (𝒜 K) (MvPolynomial.X 0 : A K)
lemma

ψ_tX

L278 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.ψ_tX
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
omit [SmoothOfRelativeDimension 1 c] in
Lean source · statement
lemma ψ_tX (f : C.functionField) : ψ c f tX = f
lemma

φ_genericPoint_mem

L285 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.φ_genericPoint_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
lemma φ_genericPoint_mem (f : C.functionField) :
    φ c f (genericPoint C) ∈ Proj.basicOpen (𝒜 K) (MvPolynomial.X 0 : A K)
lemma

φ_pole_not_mem

L298 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.φ_pole_not_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
lemma φ_pole_not_mem (f : C.functionField) (x₀ : C)
    (hf : f ∉ (algebraMap (C.presheaf.stalk x₀) C.functionField).range) :
    φ c f x₀ ∉ Proj.basicOpen (𝒜 K) (MvPolynomial.X 0 : A K)
lemma

finite_fibre

L336 ↗
AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper.AlgebraicCurve.FiniteMapToP1.finite_fibre
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FiniteMapToP1
open _root_.AlgebraicCurve
attribute [local instance] MvPolynomial.gradedAlgebra
section curve
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
  [IsIntegral C] [SmoothOfRelativeDimension 1 c]
Lean source · statement
lemma finite_fibre [IsProper c] (f : C.functionField) (x₀ : C) (hx₀ : IsClosed ({x₀} : Set
  C))
    (hf : f ∉ (algebraMap (C.presheaf.stalk x₀) C.functionField).range) (y : P1 K) :
    ((φ c f) ⁻¹' {y}).Finite
theorem

exists_isFinite_hom_proj_of_isProper

L371 ↗
AlgebraicCurve.exists_isFinite_hom_proj_of_isProper
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.Exists_isFinite_hom_proj_of_isProper
noncomputable section
open CategoryTheory AlgebraicGeometry
universe u
open AlgebraicCurve.FiniteMapToP1 in
Lean source · full declaration
theorem _root_.AlgebraicCurve.exists_isFinite_hom_proj_of_isProper {K : Type u} [Field K] {C :
  Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
    [IsIntegral C] [IsProper c] [SmoothOfRelativeDimension 1 c] :
    letI := MvPolynomial.gradedAlgebra (σ := Fin 2) (R := K)
    ∃ φ : C ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin 2) K), IsFinite φ := by
  let := MvPolynomial.gradedAlgebra (σ := Fin 2) (R := K)
  obtain ⟨f, x₀, hx₀, hf⟩ := exists_pole c
  have : LocallyQuasiFinite (φ c f) := .of_finite_preimage_singleton _ (finite_fibre c f x₀ hx₀ hf)
  exact ⟨φ c f, IsFinite.of_isProper_of_locallyQuasiFinite _⟩

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