NYLL
Module

CurveModel_exists_hom_of_algHom.lean

Nyll.AlgebraicCurves.Models.CurveModel_exists_hom_of_algHom
65 declarations indexed from sourceView source ↗

Module documentation

Curve Model exists hom of alg Hom

Imports8
Imported by3

Declarations

theorem

fromSpecStalkOfMem_eq_of_specializes

L42 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.fromSpecStalkOfMem_eq_of_specializes
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Spread
variable {X Y S : Scheme.{u}}
Lean source · statement
theorem fromSpecStalkOfMem_eq_of_specializes (U : X.Opens) {ξ x : X} (h : ξ ⤳ x)
    (hx : x ∈ U) (hξ : ξ ∈ U) :
    U.fromSpecStalkOfMem ξ hξ =
      Spec.map (X.presheaf.stalkSpecializes h) ≫ U.fromSpecStalkOfMem x hx
theorem

partialMap_fromSpecStalkOfMem_eq_of_specializes

L49 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.partialMap_fromSpecStalkOfMem_eq_of_specializes
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Spread
variable {X Y S : Scheme.{u}}
Lean source · statement
theorem partialMap_fromSpecStalkOfMem_eq_of_specializes (f : X.PartialMap Y) {ξ x : X}
    (h : ξ ⤳ x) (hx : x ∈ f.domain) (hξ : ξ ∈ f.domain) :
    f.fromSpecStalkOfMem hξ =
      Spec.map (X.presheaf.stalkSpecializes h) ≫ f.fromSpecStalkOfMem hx
theorem

partialMap_fromFunctionField_eq_of_mem

L57 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.partialMap_fromFunctionField_eq_of_mem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Spread
variable {X Y S : Scheme.{u}}
Lean source · statement
theorem partialMap_fromFunctionField_eq_of_mem [IrreducibleSpace X] (f : X.PartialMap Y)
    {x : X} (hx : x ∈ f.domain) :
    f.fromFunctionField =
      Spec.map (X.presheaf.stalkSpecializes (genericPoint_specializes x)) ≫
        f.fromSpecStalkOfMem hx
theorem

ofHom_algebraMap_stalk_functionField

L65 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.ofHom_algebraMap_stalk_functionField
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Spread
variable {X Y S : Scheme.{u}}
Lean source · statement
theorem ofHom_algebraMap_stalk_functionField [IrreducibleSpace X] (x : X) :
    CommRingCat.ofHom (algebraMap (X.presheaf.stalk x) X.functionField) =
      X.presheaf.stalkSpecializes ((genericPoint_spec X).specializes trivial)
theorem

mem_domain_of_valuationRing

L71 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.mem_domain_of_valuationRing
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Spread
variable {X Y S : Scheme.{u}}
Lean source · statement
theorem mem_domain_of_valuationRing (sX : X ⟶ S) (sY : Y ⟶ S) [IsIntegral X]
    [LocallyOfFiniteType sY] (hY : ValuativeCriterion.Existence sY) (f : X.PartialMap Y)
    (hf : f.hom ≫ sY = f.domain.ι ≫ sX) (x : X) (hx : ValuationRing (X.presheaf.stalk x)) :
    x ∈ f.toRationalMap.domain
theorem

valuationRing_of_surjective

L115 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.valuationRing_of_surjective
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section LocalRings
Lean source · statement
theorem valuationRing_of_surjective {A B : Type*} [CommRing A] [IsDomain A]
    [ValuationRing A]
    [CommRing B] [IsDomain B] (f : A →+* B) (hf : Function.Surjective f) : ValuationRing B
theorem

valuationRing_localization_atPrime

L126 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.valuationRing_localization_atPrime
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section LocalRings
Lean source · statement
theorem valuationRing_localization_atPrime {R B : Type*} [CommRing R] [CommRing B]
    [Algebra R B] [IsDomain B] [IsNoetherianRing B] [Algebra.EssFiniteType R B]
    (q : Ideal B) [q.IsPrime] [Algebra.IsUnramifiedAt R q] (hp : (q.under R).IsPrincipal) :
    ValuationRing (Localization.AtPrime q)
theorem

isPrincipalIdealRing_mvPolynomial_fin_one

L143 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.isPrincipalIdealRing_mvPolynomial_fin_one
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section LocalRings
Lean source · statement
theorem isPrincipalIdealRing_mvPolynomial_fin_one (K : Type*) [Field K] :
    IsPrincipalIdealRing (MvPolynomial (Fin 1) K)
theorem

valuationRing_stalk

L148 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.valuationRing_stalk
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section LocalRings
Lean source · statement
theorem valuationRing_stalk {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsIntegral C] [SmoothOfRelativeDimension 1 c] (x : C) :
    ValuationRing (C.presheaf.stalk x)
abbrev

ffHom

L185 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.ffHom
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
abbrev ffHom (M : CurveModel K F) (M' : CurveModel K F') (φ : F →ₐ[K] F') :
    M.C.functionField →+* M'.C.functionField
abbrev

genericHom

L189 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.genericHom
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
abbrev genericHom (M : CurveModel K F) (M' : CurveModel K F') (φ : F →ₐ[K] F') :
    Spec M'.C.functionField ⟶ M.C
theorem

fromSpecStalk_genericPoint_comp_eq

L193 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.fromSpecStalk_genericPoint_comp_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem fromSpecStalk_genericPoint_comp_eq {C : Scheme.{u}} [IsIntegral C]
    (c : C ⟶ Spec (CommRingCat.of K)) :
    C.fromSpecStalk (genericPoint C) ≫ c =
      Spec.map (CommRingCat.ofHom (baseToFunctionField c))
theorem

ffHom_comp_baseToFunctionField

L216 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.ffHom_comp_baseToFunctionField
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem ffHom_comp_baseToFunctionField (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') :
    (ffHom M M' φ).comp (baseToFunctionField M.toBase) = baseToFunctionField M'.toBase
theorem

genericHom_comp_toBase

L224 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.genericHom_comp_toBase
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem genericHom_comp_toBase (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') :
    genericHom M M' φ ≫ M.toBase = M'.C.fromSpecStalk (genericPoint M'.C) ≫ M'.toBase
theorem

isSeparated_of_over

L246 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.isSeparated_of_over
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem isSeparated_of_over {Y : Scheme.{u}} (g : Y ⟶ Spec (CommRingCat.of K))
    [IsSeparated g] : Y.IsSeparated
theorem

existence_of_isProper

L250 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.existence_of_isProper
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem existence_of_isProper {Y T : Scheme.{u}} (g : Y ⟶ T) [IsProper g] :
    ValuativeCriterion.Existence g
theorem

exists_hom_comp_toBase_eq

L256 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.exists_hom_comp_toBase_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem exists_hom_comp_toBase_eq (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') :
    ∃ π : M'.C ⟶ M.C, π ≫ M.toBase = M'.toBase ∧
      M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ
theorem

isDominant_fromSpecStalk_genericPoint

L298 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.isDominant_fromSpecStalk_genericPoint
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem isDominant_fromSpecStalk_genericPoint (X : Scheme.{u}) [IsIntegral X] :
    IsDominant (X.fromSpecStalk (genericPoint X))
theorem

apply_genericPoint_eq

L307 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.apply_genericPoint_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem apply_genericPoint_eq (M : CurveModel K F) (M' : CurveModel K F') (φ : F →ₐ[K] F')
    (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) :
    π.base (genericPoint M'.C) = genericPoint M.C
theorem

stalkMap_comp_stalkSpecializes

L332 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.stalkMap_comp_stalkSpecializes
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem stalkMap_comp_stalkSpecializes (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) (x : M'.C) :
    π.stalkMap x ≫ M'.C.presheaf.stalkSpecializes (genericPoint_specializes x) =
      M.C.presheaf.stalkSpecializes (genericPoint_specializes (π.base x)) ≫
        CommRingCat.ofHom (ffHom M M' φ)
theorem

algebraMap_stalkMap_apply

L348 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.algebraMap_stalkMap_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem algebraMap_stalkMap_apply (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) (x : M'.C)
    (a : M.C.presheaf.stalk (π.base x)) :
    algebraMap (M'.C.presheaf.stalk x) M'.C.functionField ((π.stalkMap x).hom a) =
      ffHom M M' φ (algebraMap (M.C.presheaf.stalk (π.base x)) M.C.functionField a)
theorem

valuationRing_stalk'

L357 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.valuationRing_stalk'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem valuationRing_stalk' (M : CurveModel K F) (x : M.C) :
    ValuationRing (M.C.presheaf.stalk x)
theorem

eq_of_fromSpecStalk_comp_eq

L361 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.eq_of_fromSpecStalk_comp_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Generic
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem eq_of_fromSpecStalk_comp_eq (M : CurveModel K F) (M' : CurveModel K F')
    {π π' : M'.C ⟶ M.C}
    (h : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π' =
      M'.C.fromSpecStalk (genericPoint M'.C) ≫ π) :
    π' = π
def

stalkRange

L376 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.stalkRange
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
def stalkRange (M : CurveModel K F) (x : M.C) : Subring F
theorem

stalkRange_closedPoint

L380 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.stalkRange_closedPoint
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem stalkRange_closedPoint (M : CurveModel K F) (x : closedPoints M.C) :
    stalkRange M x.1 = (M.placeOfPoint x).toValuationSubring.toSubring
theorem

mem_stalkRange_closedPoint

L384 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.mem_stalkRange_closedPoint
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem mem_stalkRange_closedPoint (M : CurveModel K F) (x : closedPoints M.C) (f : F) :
    f ∈ stalkRange M x.1 ↔ f ∈ (M.placeOfPoint x).toValuationSubring
theorem

stalkRange_genericPoint

L389 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.stalkRange_genericPoint
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem stalkRange_genericPoint (M : CurveModel K F) :
    stalkRange M (genericPoint M.C) = ⊤
theorem

map_stalkRange_le

L398 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.map_stalkRange_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem map_stalkRange_le (M : CurveModel K F) (M' : CurveModel K F') (φ : F →ₐ[K] F')
    (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) (y : M'.C) :
    (stalkRange M (π.base y)).map φ.toRingHom ≤ stalkRange M' y
theorem

apply_mem_stalkRange

L413 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.apply_mem_stalkRange
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem apply_mem_stalkRange (M : CurveModel K F) (M' : CurveModel K F') (φ : F →ₐ[K] F')
    (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) (y : M'.C) {f : F}
    (hf : f ∈ stalkRange M (π.base y)) : φ f ∈ stalkRange M' y
theorem

eq_of_specializes

L419 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.eq_of_specializes
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem eq_of_specializes (M : CurveModel K F) (x₀ : closedPoints M.C) {a b : M.C}
    (ha : a ⤳ x₀.1) (hb : b ⤳ x₀.1) (ha' : a ≠ x₀.1) (hb' : b ≠ x₀.1) : a = b
theorem

mem_closedPoints_or_eq_genericPoint

L456 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.mem_closedPoints_or_eq_genericPoint
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem mem_closedPoints_or_eq_genericPoint (M : CurveModel K F) (x : M.C) :
    x ∈ closedPoints M.C ∨ x = genericPoint M.C
theorem

mem_restrictAlong_iff

L473 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.mem_restrictAlong_iff
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem mem_restrictAlong_iff (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (w : Place K F')
    (f : F) : f ∈ (w.restrictAlong φ hφ).toValuationSubring ↔ φ f ∈ w.toValuationSubring
theorem

apply_ne_genericPoint

L478 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.apply_ne_genericPoint
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem apply_ne_genericPoint (M : CurveModel K F) (M' : CurveModel K F') (φ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    (y : closedPoints M'.C) : π.base y.1 ≠ genericPoint M.C
theorem

apply_mem_closedPoints

L490 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.apply_mem_closedPoints
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem apply_mem_closedPoints (M : CurveModel K F) (M' : CurveModel K F') (φ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    (y : closedPoints M'.C) : π.base y.1 ∈ closedPoints M.C
theorem

ofPrime_eq_top_or_eq

L496 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.ofPrime_eq_top_or_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem ofPrime_eq_top_or_eq {A : ValuationSubring F} [IsDiscreteValuationRing A]
    (P : Ideal A)
    [P.IsPrime] : A.ofPrime P = ⊤ ∨ A.ofPrime P = A
theorem

place_eq_of_le

L509 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.place_eq_of_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem place_eq_of_le {v v' : Place K F}
    (h : v.toValuationSubring ≤ v'.toValuationSubring) : v = v'
theorem

exists_mem_closedPoints_placeOfPoint_eq

L518 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.exists_mem_closedPoints_placeOfPoint_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem exists_mem_closedPoints_placeOfPoint_eq (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    (y : closedPoints M'.C) :
    ∃ h : π.base y.1 ∈ closedPoints M.C,
      M.placeOfPoint ⟨π.base y.1, h⟩ = (M'.placeOfPoint y).restrictAlong φ hφ
theorem

restrictAlong_fiber_finite

L536 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.restrictAlong_fiber_finite
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
variable [CharZero K]
Lean source · statement
theorem restrictAlong_fiber_finite (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (hfin : FiniteAlong K φ) (v : Place K F) :
    {w : Place K F' | w.restrictAlong φ hφ = v}.Finite
theorem

finite_preimage_singleton

L545 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.finite_preimage_singleton
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Places
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
variable [CharZero K]
Lean source · statement
theorem finite_preimage_singleton (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    (x : M.C) : (π.base ⁻¹' {x}).Finite
theorem

isProper

L580 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.isProper
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem isProper (M : CurveModel K F) (M' : CurveModel K F')
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase) : IsProper π
theorem

locallyOfFiniteType

L585 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.locallyOfFiniteType
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem locallyOfFiniteType (M : CurveModel K F) (M' : CurveModel K F')
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase) : LocallyOfFiniteType π
theorem

locallyQuasiFinite

L590 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.locallyQuasiFinite
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem locallyQuasiFinite [CharZero K] (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) :
    LocallyQuasiFinite π
theorem

isFinite

L600 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.isFinite
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem isFinite [CharZero K] (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) :
    IsFinite π
theorem

stalkMap_injective

L609 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.stalkMap_injective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem stalkMap_injective (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) (x : M'.C) :
    Function.Injective (π.stalkMap x).hom
theorem

flat_of_injective_of_valuationRing

L619 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.flat_of_injective_of_valuationRing
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem flat_of_injective_of_valuationRing {A B : Type u} [CommRing A] [IsDomain A]
    [ValuationRing A] [CommRing B] [IsDomain B] (f : A →+* B) (hf : Function.Injective f) :
    f.Flat
theorem

flat_stalkMap

L632 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.flat_stalkMap
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem flat_stalkMap (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) (x : M'.C) :
    (π.stalkMap x).hom.Flat
theorem

flat

L640 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.flat
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem flat (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) :
    Flat π
theorem

locallyOfFinitePresentation_of_locallyOfFiniteType

L650 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.locallyOfFinitePresentation_of_locallyOfFiniteType
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem locallyOfFinitePresentation_of_locallyOfFiniteType {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsLocallyNoetherian Y] [LocallyOfFiniteType f] : LocallyOfFinitePresentation f
theorem

isLocallyNoetherian

L654 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.isLocallyNoetherian
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem isLocallyNoetherian (M : CurveModel K F) : IsLocallyNoetherian M.C
theorem

locallyOfFinitePresentation

L657 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.locallyOfFinitePresentation
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem locallyOfFinitePresentation (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) :
    LocallyOfFinitePresentation π
theorem

finrank_eq_finrank_genericPoint

L669 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.finrank_eq_finrank_genericPoint
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem finrank_eq_finrank_genericPoint [CharZero K] (M : CurveModel K F)
    (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) (x : M.C) :
    π.finrank x = π.finrank (genericPoint M.C)
theorem

rankAtStalk_bot_eq_finrank

L681 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.rankAtStalk_bot_eq_finrank
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem rankAtStalk_bot_eq_finrank {A B KA KB : Type u} [CommRing A] [IsDomain A]
    [CommRing B] [IsDomain B] [Algebra A B] [Module.Finite A B] [FaithfulSMul A B]
    [Field KA] [Algebra A KA] [IsFractionRing A KA] [Field KB] [Algebra B KB] [IsFractionRing B KB]
    [Algebra KA KB] [Algebra A KB] [IsScalarTower A B KB] [IsScalarTower A KA KB] :
    Module.rankAtStalk (R := A) B ⊥ = Module.finrank KA KB
theorem

genericPoint_mem_preimage

L697 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.genericPoint_mem_preimage
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem genericPoint_mem_preimage (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F')
    (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    {U : M.C.Opens} (hη : genericPoint M.C ∈ U) : genericPoint M'.C ∈ π ⁻¹ᵁ U
theorem

algebraMap_germ

L706 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.algebraMap_germ
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · full declaration
theorem algebraMap_germ (M : CurveModel K F) (U : M.C.Opens) (hη : genericPoint M.C ∈ U)
    (x : M.C) (hx : x ∈ U) (b : Γ(M.C, U)) :
    haveI : Nonempty U := ⟨⟨_, hη⟩⟩
    @algebraMap (M.C.presheaf.stalk x) M.C.functionField _ _ (stalkFunctionFieldAlgebra M.C x)
        ((M.C.presheaf.germ U x hx).hom b) =
      algebraMap Γ(M.C, U) M.C.functionField b := by
  have : Nonempty U := ⟨⟨_, hη⟩⟩
  change (M.C.presheaf.stalkSpecializes _).hom ((M.C.presheaf.germ U x hx).hom b) =
    (M.C.presheaf.germ U (genericPoint M.C) _).hom b
  rw [← RingHom.comp_apply, ← CommRingCat.hom_comp, TopCat.Presheaf.germ_stalkSpecializes]
theorem

algebraMap_app_apply

L717 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.algebraMap_app_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · full declaration
theorem algebraMap_app_apply (M : CurveModel K F) (M' : CurveModel K F') (φ : F →ₐ[K] F')
    (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    (U : M.C.Opens) (hη : genericPoint M.C ∈ U) (a : Γ(M.C, U)) :
    haveI : Nonempty U := ⟨⟨_, hη⟩⟩
    haveI : Nonempty (π ⁻¹ᵁ U) := ⟨⟨_, genericPoint_mem_preimage M M' φ π hd hη⟩⟩
    algebraMap Γ(M'.C, π ⁻¹ᵁ U) M'.C.functionField ((π.app U).hom a) =
      ffHom M M' φ (algebraMap Γ(M.C, U) M.C.functionField a) := by
  have : Nonempty U := ⟨⟨_, hη⟩⟩
  have hη' : genericPoint M'.C ∈ π ⁻¹ᵁ U := genericPoint_mem_preimage M M' φ π hd hη
  have hx : π.base (genericPoint M'.C) ∈ U := hη'
  have : Nonempty (π ⁻¹ᵁ U) := ⟨⟨_, hη'⟩⟩
  calc algebraMap Γ(M'.C, π ⁻¹ᵁ U) M'.C.functionField ((π.app U).hom a)
      = @algebraMap (M'.C.presheaf.stalk (genericPoint M'.C)) M'.C.functionField _ _
          (stalkFunctionFieldAlgebra M'.C (genericPoint M'.C))
          ((M'.C.presheaf.germ (π ⁻¹ᵁ U) (genericPoint M'.C) hη').hom ((π.app U).hom a)) :=
        (algebraMap_germ M' (π ⁻¹ᵁ U) hη' (genericPoint M'.C) hη' ((π.app U).hom a)).symm
    _ = @algebraMap (M'.C.presheaf.stalk (genericPoint M'.C)) M'.C.functionField _ _
          (stalkFunctionFieldAlgebra M'.C (genericPoint M'.C))
          ((π.stalkMap (genericPoint M'.C)).hom
            ((M.C.presheaf.germ U (π.base (genericPoint M'.C)) hx).hom a)) :=
        congrArg (@algebraMap (M'.C.presheaf.stalk (genericPoint M'.C)) M'.C.functionField
            _ _ (stalkFunctionFieldAlgebra M'.C (genericPoint M'.C)))
          (Scheme.Hom.germ_stalkMap_apply π U (genericPoint M'.C) hx a).symm
    _ = ffHom M M' φ (@algebraMap (M.C.presheaf.stalk (π.base (genericPoint M'.C)))
          M.C.functionField _ _ (stalkFunctionFieldAlgebra M.C (π.base (genericPoint M'.C)))
          ((M.C.presheaf.germ U (π.base (genericPoint M'.C)) hx).hom a)) :=
        algebraMap_stalkMap_apply M M' φ π hd (genericPoint M'.C) _
    _ = ffHom M M' φ (algebraMap Γ(M.C, U) M.C.functionField a) :=
        congrArg (ffHom M M' φ) (algebraMap_germ M U hη (π.base (genericPoint M'.C)) hx a)
theorem

injective_app

L748 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.injective_app
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem injective_app (M : CurveModel K F) (M' : CurveModel K F') (φ : F →ₐ[K] F')
    (π : M'.C ⟶ M.C)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    (U : M.C.Opens) (hη : genericPoint M.C ∈ U) : Function.Injective (π.app U).hom
theorem

isPullback_fromSpec

L759 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.isPullback_fromSpec
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem isPullback_fromSpec (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    (U : M.C.Opens) (hU : IsAffineOpen U) (hV : IsAffineOpen (π ⁻¹ᵁ U)) :
    IsPullback hV.fromSpec (Spec.map (π.app U)) π hU.fromSpec
theorem

finite_app

L774 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.finite_app
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem finite_app [CharZero K] (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    (U : M.C.Opens) (hU : IsAffineOpen U) : (π.app U).hom.Finite
theorem

flat_app

L785 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.flat_app
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem flat_app [CharZero K] (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    (U : M.C.Opens) (hU : IsAffineOpen U) : (π.app U).hom.Flat
theorem

fromSpec_bot

L797 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.fromSpec_bot
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · full declaration
theorem fromSpec_bot (M : CurveModel K F) (U : M.C.Opens) (hU : IsAffineOpen U)
    (hη : genericPoint M.C ∈ U) :
    haveI : Nonempty U := ⟨⟨_, hη⟩⟩
    hU.fromSpec (⊥ : PrimeSpectrum Γ(M.C, U)) = genericPoint M.C := by
  have : Nonempty U := ⟨⟨_, hη⟩⟩
  have h := hU.fromSpec_primeIdealOf ⟨genericPoint M.C, hη⟩
  rw [hU.primeIdealOf_genericPoint, genericPoint_eq_bot_of_affine] at h
  exact h
theorem

finrank_genericPoint_eq_ringHom_finrank

L806 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.finrank_genericPoint_eq_ringHom_finrank
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · full declaration
theorem finrank_genericPoint_eq_ringHom_finrank [CharZero K] (M : CurveModel K F)
    (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    (U : M.C.Opens) (hU : IsAffineOpen U) (hη : genericPoint M.C ∈ U) :
    haveI : Nonempty U := ⟨⟨_, hη⟩⟩
    π.finrank (genericPoint M.C) = (π.app U).hom.finrank (⊥ : PrimeSpectrum Γ(M.C, U)) := by
  have : Nonempty U := ⟨⟨_, hη⟩⟩
  have := isFinite M M' φ hφ hfin π ha hd
  have := flat M M' φ hφ hfin π ha hd
  have hb : hU.fromSpec (⊥ : PrimeSpectrum Γ(M.C, U)) = genericPoint M.C := fromSpec_bot M U hU hη
  have h1 := Scheme.Hom.finrank_of_isPullback _ _ _ _
    (isPullback_fromSpec M M' φ hφ hfin π ha hd U hU (hU.preimage π)) (⊥ : PrimeSpectrum Γ(M.C, U))
  rw [hb] at h1
  exact h1.symm.trans (congrFun (Scheme.Hom.finrank_SpecMap_eq_finrank
    (finite_app M M' φ hφ hfin π ha hd U hU) (flat_app M M' φ hφ hfin π ha hd U hU)) _)
theorem

finrank_functionField

L824 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.finrank_functionField
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · full declaration
theorem finrank_functionField (M : CurveModel K F) (M' : CurveModel K F') (φ : F →ₐ[K] F') :
    letI := (ffHom M M' φ).toAlgebra
    Module.finrank M.C.functionField M'.C.functionField = finrankAlong K φ := by
  let := (ffHom M M' φ).toAlgebra
  let := algebraAlong φ
  change Module.finrank M.C.functionField M'.C.functionField = Module.finrank F F'
  refine Algebra.finrank_eq_of_equiv_equiv M.ffEquiv.symm M'.ffEquiv.symm ?_
  ext x
  simp [ffHom, RingHom.algebraMap_toAlgebra]
theorem

finrank_genericPoint

L834 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.finrank_genericPoint
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem finrank_genericPoint [CharZero K] (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ) :
    π.finrank (genericPoint M.C) = finrankAlong K φ
theorem

finrank_eq

L865 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom.HG1A.finrank_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1A
section Rank
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
Lean source · statement
theorem finrank_eq [CharZero K] (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (π : M'.C ⟶ M.C) (ha : π ≫ M.toBase = M'.toBase)
    (hd : M'.C.fromSpecStalk (genericPoint M'.C) ≫ π = genericHom M M' φ)
    (x : M.C) : π.finrank x = finrankAlong K φ
theorem

exists_hom_of_algHom

L878 ↗
AlgebraicCurve.CurveModel.exists_hom_of_algHom
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_of_algHom
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u
open AlgebraicCurve.CurveModel HG1A in
Lean source · statement
theorem _root_.AlgebraicCurve.CurveModel.exists_hom_of_algHom {K : Type u} [Field K] [CharZero K]
    {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
    (M : CurveModel K F) (M' : CurveModel K F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ) :
    ∃ π : M'.C ⟶ M.C,
      π ≫ M.toBase = M'.toBase ∧
      IsFinite π ∧ Flat π ∧ LocallyOfFinitePresentation π ∧
      (∀ x : M.C, π.finrank x = finrankAlong K φ) ∧
      M'.C.fromSpecStalk (genericPoint M'.C) ≫ π =
        Spec.map (CommRingCat.ofHom
          (M'.ffEquiv.toRingHom.comp (φ.toRingHom.comp M.ffEquiv.symm.toRingHom))) ≫
          M.C.fromSpecStalk (genericPoint M.C) ∧
      (∀ y : closedPoints M'.C, ∃ h : π.base y.1 ∈ closedPoints M.C,
        M.placeOfPoint ⟨π.base y.1, h⟩ = (M'.placeOfPoint y).restrictAlong φ hφ) ∧
      ∀ π' : M'.C ⟶ M.C,
        M'.C.fromSpecStalk (genericPoint M'.C) ≫ π' =
          M'.C.fromSpecStalk (genericPoint M'.C) ≫ π → π' = π

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