Module

CurveModel_exists_finite_flat_hom_of_algHom.lean

Nyll.AlgebraicCurves.Models.CurveModel_exists_finite_flat_hom_of_algHom

66 declarations indexed from sourceView source ↗

Module documentation

Curve Model exists finite flat hom of alg Hom

Imports8

Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Mathlib.AlgebraicGeometry.Birational.RationalMap
Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Mathlib.AlgebraicGeometry.ValuativeCriterion
Mathlib.AlgebraicGeometry.Noetherian
Mathlib.RingTheory.Flat.TorsionFree
Nyll.AlgebraicCurves.Models.Basic
Nyll.AlgebraicCurves.Divisors.Correspondences

Imported by3

theorem

fromSpecStalkOfMem_eq_of_specializes

L44 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
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

L51 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
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

L59 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
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

L67 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
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

L73 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
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

L117 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
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

L128 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
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

L145 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section LocalRings

Lean source · statement

theorem isPrincipalIdealRing_mvPolynomial_fin_one (K : Type*) [Field K] :
    IsPrincipalIdealRing (MvPolynomial (Fin 1) K)

theorem

valuationRing_stalk

L150 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.valuationRing_stalk

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
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

L188 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.ffHom

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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.presheaf.stalk (genericPoint M.C) ⟶ M'.C.presheaf.stalk (genericPoint M'.C)

abbrev

genericHom

L192 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.genericHom

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L196 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L219 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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' φ).hom.comp (baseToFunctionField M.toBase) = baseToFunctionField M'.toBase

theorem

genericHom_comp_toBase

L227 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L239 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L243 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L249 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L290 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L299 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L325 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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)) ≫
        ffHom M M' φ

theorem

algebraMap_stalkMap_apply

L337 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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'

L346 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.valuationRing_stalk'

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L350 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Generic
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L366 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.stalkRange

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L370 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.stalkRange_closedPoint

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L374 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L379 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.stalkRange_genericPoint

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L388 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L405 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L411 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L448 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L465 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L470 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L482 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L488 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L501 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L510 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

finite_of_isClosed_of_forall_isClosed_singleton

L526 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.finite_of_isClosed_of_forall_isClosed_singleton

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

Lean source · statement

theorem finite_of_isClosed_of_forall_isClosed_singleton {X : Type*} [TopologicalSpace X]
    [TopologicalSpace.NoetherianSpace X] [QuasiSober X] {s : Set X} (hs : IsClosed s)
    (hpt : ∀ x ∈ s, IsClosed ({x} : Set X)) : s.Finite

theorem

isNoetherian

L543 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.isNoetherian

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

Lean source · statement

theorem isNoetherian (M : CurveModel K F) : IsNoetherian M.C

theorem

finite_preimage_singleton

L548 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.finite_preimage_singleton

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Places
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

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

L579 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.isProper

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L584 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.locallyOfFiniteType

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L589 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.locallyQuasiFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

Lean source · statement

theorem locallyQuasiFinite (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

L599 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.isFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

Lean source · statement

theorem isFinite (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

L608 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.stalkMap_injective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L618 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L631 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.flat_stalkMap

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L639 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.flat

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L649 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L653 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.isLocallyNoetherian

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

Lean source · statement

theorem isLocallyNoetherian (M : CurveModel K F) : IsLocallyNoetherian M.C

theorem

locallyOfFinitePresentation

L656 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.locallyOfFinitePresentation

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L668 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

Lean source · statement

theorem finrank_eq_finrank_genericPoint (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

L680 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L696 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L705 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.algebraMap_germ

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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)) :
    let _ : 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
  let _ : 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

L716 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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)) :
    let _ : Nonempty U := ⟨⟨_, hη⟩⟩
    let _ : 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
  let _ : Nonempty U := ⟨⟨_, hη⟩⟩
  have hη' : genericPoint M'.C ∈ π ⁻¹ᵁ U := genericPoint_mem_preimage M M' φ π hd hη
  have hx : π.base (genericPoint M'.C) ∈ U := hη'
  let _ : 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

L747 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.injective_app

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L758 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.isPullback_fromSpec

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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

L773 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.finite_app

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

Lean source · statement

theorem finite_app (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

L784 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.flat_app

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

Lean source · statement

theorem flat_app (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

L796 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.fromSpec_bot

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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) :
    let _ : Nonempty U := ⟨⟨_, hη⟩⟩
    hU.fromSpec (⊥ : PrimeSpectrum Γ(M.C, U)) = genericPoint M.C := by
  let _ : 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

L805 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

Lean source · full declaration

theorem finrank_genericPoint_eq_ringHom_finrank (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) :
    let _ : Nonempty U := ⟨⟨_, hη⟩⟩
    π.finrank (genericPoint M.C) = (π.app U).hom.finrank (⊥ : PrimeSpectrum Γ(M.C, U)) := by
  let _ : Nonempty U := ⟨⟨_, hη⟩⟩
  let _ := isFinite M M' φ hφ hfin π ha hd
  let _ := 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

L823 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.finrank_functionField

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [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') :
    let _ := (ffHom M M' φ).hom.toAlgebra
    Module.finrank M.C.functionField M'.C.functionField = finrankAlong K φ := by
  let _ := (ffHom M M' φ).hom.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
  change φ (M.ffEquiv.symm x) = M'.ffEquiv.symm (M'.ffEquiv (φ (M.ffEquiv.symm x)))
  exact (M'.ffEquiv.symm_apply_apply _).symm

theorem

finrank_genericPoint

L834 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom.FUNC1.finrank_genericPoint

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

Lean source · statement

theorem finrank_genericPoint (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_finite_flat_hom_of_algHom.FUNC1.finrank_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
namespace FUNC1
section Rank
variable {K : Type u} [Field K] {F : Type v} {F' : Type w} [Field F] [Algebra K F] [Field F']
  [Algebra K F']

Lean source · statement

theorem finrank_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' φ)
    (x : M.C) : π.finrank x = finrankAlong K φ

theorem

exists_finite_flat_hom_of_algHom

L878 ↗

AlgebraicCurve.CurveModel.exists_finite_flat_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_finite_flat_hom_of_algHom

-- Rewrites through `Spec.map` identify the generic stalk with the function field.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v w
open AlgebraicCurve.CurveModel FUNC1 in

Lean source · statement

theorem _root_.AlgebraicCurve.CurveModel.exists_finite_flat_hom_of_algHom {K : Type u} [Field K]
    {F : Type v} {F' : Type w} [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) ≫ π → π' = π

Module documentation

Curve Model exists finite flat hom of alg Hom

Declarations