NYLL
Module

CurveModel_exists_curveModel_ratFunc.lean

Nyll.AlgebraicCurves.Models.CurveModel_exists_curveModel_ratFunc
13 declarations indexed from sourceView source ↗

Module documentation

Curve Model exists curve Model rat Func

Imports3
Imported by2

Declarations

theorem

ratFunc_transcendental_X

L40 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.ratFunc_transcendental_X
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section InstanceFacts
variable (κ : Type u) [Field κ]
Lean source · statement
theorem ratFunc_transcendental_X : Transcendental κ (RatFunc.X : RatFunc κ)
theorem

ratFunc_adjoin_X_eq_top

L43 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.ratFunc_adjoin_X_eq_top
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section InstanceFacts
variable (κ : Type u) [Field κ]
Lean source · statement
theorem ratFunc_adjoin_X_eq_top : κ⟮(RatFunc.X : RatFunc κ)⟯ = ⊤
theorem

mem_ratFunc_adjoin_X

L45 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.mem_ratFunc_adjoin_X
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section InstanceFacts
variable (κ : Type u) [Field κ]
Lean source · statement
theorem mem_ratFunc_adjoin_X (f : RatFunc κ) : f ∈ κ⟮(RatFunc.X : RatFunc κ)⟯
instance

ratFunc_finiteDimensional_adjoin_X

L48 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.ratFunc_finiteDimensional_adjoin_X
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section InstanceFacts
variable (κ : Type u) [Field κ]
Lean source · statement
instance ratFunc_finiteDimensional_adjoin_X :
    FiniteDimensional κ⟮(RatFunc.X : RatFunc κ)⟯ (RatFunc κ)
instance

ratFunc_isSeparable_adjoin_X

L57 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.ratFunc_isSeparable_adjoin_X
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section InstanceFacts
variable (κ : Type u) [Field κ]
Lean source · statement
instance ratFunc_isSeparable_adjoin_X :
    Algebra.IsSeparable κ⟮(RatFunc.X : RatFunc κ)⟯ (RatFunc κ)
theorem

ratFunc_isProper_smooth_places_affineCover_glued

L71 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.ratFunc_isProper_smooth_places_affineCover_glued
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Model
variable (κ : Type u) [Field κ] [IsAlgClosed κ] [Fact ((RatFunc.X : RatFunc κ) ≠ 0)]
Lean source · statement
theorem ratFunc_isProper_smooth_places_affineCover_glued :
    IsProper (CurveModel.gluedToBase κ (RatFunc.X : RatFunc κ)) ∧
    SmoothOfRelativeDimension 1 (CurveModel.gluedToBase κ (RatFunc.X : RatFunc κ)) ∧
    (∃ P : closedPoints (CurveModel.glued κ (RatFunc.X : RatFunc κ)) → Place κ (RatFunc κ),
      Function.Bijective P ∧
      ∀ x : closedPoints (CurveModel.glued κ (RatFunc.X : RatFunc κ)),
        (((CurveModel.gluedFunctionFieldEquiv κ (RatFunc.X : RatFunc κ)).symm :
              (CurveModel.glued κ (RatFunc.X : RatFunc κ)).functionField ≃+* RatFunc
                κ).toRingHom.comp
            (algebraMap ((CurveModel.glued κ (RatFunc.X : RatFunc κ)).presheaf.stalk x.1)
              (CurveModel.glued κ (RatFunc.X : RatFunc κ)).functionField)).range =
          (P x).toValuationSubring.toSubring) ∧
    (∀ F : Finset (CurveModel.glued κ (RatFunc.X : RatFunc κ)),
      ∃ U : (CurveModel.glued κ (RatFunc.X : RatFunc κ)).Opens, IsAffineOpen U ∧ ∀ x ∈ F, x ∈ U)
instance

ratFunc_isProper_gluedToBase

L88 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.ratFunc_isProper_gluedToBase
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Model
variable (κ : Type u) [Field κ] [IsAlgClosed κ] [Fact ((RatFunc.X : RatFunc κ) ≠ 0)]
Lean source · statement
instance ratFunc_isProper_gluedToBase :
    IsProper (CurveModel.gluedToBase κ (RatFunc.X : RatFunc κ))
instance

ratFunc_smoothOfRelativeDimension_one_gluedToBase

L92 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.ratFunc_smoothOfRelativeDimension_one_gluedToBase
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Model
variable (κ : Type u) [Field κ] [IsAlgClosed κ] [Fact ((RatFunc.X : RatFunc κ) ≠ 0)]
Lean source · statement
instance ratFunc_smoothOfRelativeDimension_one_gluedToBase :
    SmoothOfRelativeDimension 1 (CurveModel.gluedToBase κ (RatFunc.X : RatFunc κ))
def

ratFuncCurveModel

L98 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.ratFuncCurveModel
Documentation

The smooth proper curve model of the rational function field assembled from the two affine charts associated to RatFunc.X.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Model
variable (κ : Type u) [Field κ] [IsAlgClosed κ] [Fact ((RatFunc.X : RatFunc κ) ≠ 0)]
Lean source · full declaration
def ratFuncCurveModel : CurveModel κ (RatFunc κ) where
  C := CurveModel.glued κ (RatFunc.X : RatFunc κ)
  toBase := CurveModel.gluedToBase κ (RatFunc.X : RatFunc κ)
  ffEquiv := CurveModel.gluedFunctionFieldEquiv κ (RatFunc.X : RatFunc κ)
  ffEquiv_algebraMap := CurveModel.gluedFunctionFieldEquiv_algebraMap κ (RatFunc.X : RatFunc κ)
  placeOfPoint := (ratFunc_isProper_smooth_places_affineCover_glued κ).2.2.1.choose
  placeOfPoint_bijective := (ratFunc_isProper_smooth_places_affineCover_glued κ).2.2.1.choose_spec.1
  range_stalk_eq := (ratFunc_isProper_smooth_places_affineCover_glued κ).2.2.1.choose_spec.2
  finset_subset_affineOpen := (ratFunc_isProper_smooth_places_affineCover_glued κ).2.2.2
theorem

ratFuncCurveModel_C

L108 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.ratFuncCurveModel_C
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Model
variable (κ : Type u) [Field κ] [IsAlgClosed κ] [Fact ((RatFunc.X : RatFunc κ) ≠ 0)]
Lean source · statement
theorem ratFuncCurveModel_C :
    (ratFuncCurveModel κ).C = CurveModel.glued κ (RatFunc.X : RatFunc κ)
theorem

ratFuncCurveModel_toBase

L111 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.ratFuncCurveModel_toBase
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Model
variable (κ : Type u) [Field κ] [IsAlgClosed κ] [Fact ((RatFunc.X : RatFunc κ) ≠ 0)]
Lean source · statement
theorem ratFuncCurveModel_toBase :
    (ratFuncCurveModel κ).toBase = CurveModel.gluedToBase κ (RatFunc.X : RatFunc κ)
theorem

ratFuncCurveModel_ffEquiv

L114 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc.AlgebraicCurve.ratFuncCurveModel_ffEquiv
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Model
variable (κ : Type u) [Field κ] [IsAlgClosed κ] [Fact ((RatFunc.X : RatFunc κ) ≠ 0)]
Lean source · statement
theorem ratFuncCurveModel_ffEquiv :
    (ratFuncCurveModel κ).ffEquiv = CurveModel.gluedFunctionFieldEquiv κ (RatFunc.X : RatFunc κ)
theorem

exists_curveModel_ratFunc

L124 ↗
AlgebraicCurve.CurveModel.exists_curveModel_ratFunc
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_ratFunc
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField
universe u
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.CurveModel.exists_curveModel_ratFunc
    (κ : Type u) [Field κ] [IsAlgClosed κ] [Fact ((RatFunc.X : RatFunc κ) ≠ 0)] :
    ∃ (M : CurveModel κ (RatFunc κ)) (e : M.C ≅ CurveModel.glued κ (RatFunc.X : RatFunc κ)),
      e.hom ≫ CurveModel.gluedToBase κ (RatFunc.X : RatFunc κ) = M.toBase

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