Module

CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.lean

Nyll.AlgebraicCurves.Models.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite

27 declarations indexed from sourceView source ↗

Module documentation

Curve Model exists alg Hom finite Along point Equiv Place restrict Along of is Finite

Imports3

Nyll.AlgebraicCurves.Models.Basic
Nyll.AlgebraicCurves.Divisors.Correspondences
Mathlib.AlgebraicGeometry.Morphisms.Finite

Imported by5

def

pull

L47 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.pull

Documentation

Pull a function-field element back through the specialization of generic points.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}

Lean source · statement

def pull [IrreducibleSpace X] [IrreducibleSpace Y] (f : X ⟶ Y)
    (h : f.base (genericPoint X) ⤳ genericPoint Y) : Y.functionField ⟶ X.functionField

theorem

pull_germ

L55 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.pull_germ

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
section
variable [IrreducibleSpace X] [IrreducibleSpace Y] [IrreducibleSpace Z]

Lean source · statement

theorem pull_germ (f : X ⟶ Y) (h : f.base (genericPoint X) ⤳ genericPoint Y)
    (U : Y.Opens) (hU : genericPoint Y ∈ U) (s : Γ(Y, U)) :
    pull f h (Y.presheaf.germ U (genericPoint Y) hU s) =
      X.presheaf.germ (f ⁻¹ᵁ U) (genericPoint X) (h.mem_open U.isOpen hU) (f.app U s)

theorem

pull_algebraMap

L62 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.pull_algebraMap

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
section
variable [IrreducibleSpace X] [IrreducibleSpace Y] [IrreducibleSpace Z]

Lean source · statement

theorem pull_algebraMap (f : X ⟶ Y) (h : f.base (genericPoint X) ⤳ genericPoint Y) (x : X)
    (a : Y.presheaf.stalk (f.base x)) :
    pull f h (algebraMap (Y.presheaf.stalk (f.base x)) Y.functionField a) =
      algebraMap (X.presheaf.stalk x) X.functionField (f.stalkMap x a)

theorem

pull_id

L72 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.pull_id

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
section
variable [IrreducibleSpace X] [IrreducibleSpace Y] [IrreducibleSpace Z]

Lean source · statement

theorem pull_id : pull (𝟙 X) (specializes_refl _) = 𝟙 _

theorem

pull_comp

L75 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.pull_comp

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
section
variable [IrreducibleSpace X] [IrreducibleSpace Y] [IrreducibleSpace Z]

Lean source · statement

theorem pull_comp (f : X ⟶ Y) (g : Y ⟶ Z) (hf : f.base (genericPoint X) ⤳ genericPoint Y)
    (hg : g.base (genericPoint Y) ⤳ genericPoint Z) :
    pull (f ≫ g) ((g.base.hom.map_specializes hf).trans hg) = pull g hg ≫ pull f hf

theorem

specializes_of_iso

L87 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.specializes_of_iso

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem specializes_of_iso (e : X ≅ Y) : e.hom.base (genericPoint X) ⤳ genericPoint Y

theorem

specializes_of_iso_inv

L90 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.specializes_of_iso_inv

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem specializes_of_iso_inv (e : X ≅ Y) : e.inv.base (genericPoint Y) ⤳ genericPoint X

def

equivOfIso

L94 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.equivOfIso

Documentation

The function-field equivalence induced by an isomorphism of integral schemes.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

def equivOfIso (e : X ≅ Y) : Y.functionField ≃+* X.functionField

theorem

equivOfIso_apply

L112 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.equivOfIso_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem equivOfIso_apply (e : X ≅ Y) (a : Y.functionField) :
    equivOfIso e a = pull e.hom (specializes_of_iso e) a

theorem

equivOfIso_symm_apply

L115 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.equivOfIso_symm_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem equivOfIso_symm_apply (e : X ≅ Y) (a : X.functionField) :
    (equivOfIso e).symm a = pull e.inv (specializes_of_iso_inv e) a

theorem

map_equivOfIso_range_stalk

L118 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.map_equivOfIso_range_stalk

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem map_equivOfIso_range_stalk (e : X ≅ Y) (x : X) :
    (algebraMap (Y.presheaf.stalk (e.hom.base x)) Y.functionField).range.map
        (equivOfIso e).toRingHom =
      (algebraMap (X.presheaf.stalk x) X.functionField).range

theorem

image_equivOfIso_range_stalk

L134 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.image_equivOfIso_range_stalk

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem image_equivOfIso_range_stalk (e : X ≅ Y) (x : X) :
    (equivOfIso e) ''
        ((algebraMap (Y.presheaf.stalk (e.hom.base x)) Y.functionField).range : Set _) =
      ((algebraMap (X.presheaf.stalk x) X.functionField).range : Set _)

theorem

image_equivOfIso_symm_range_stalk

L142 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.image_equivOfIso_symm_range_stalk

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem image_equivOfIso_symm_range_stalk (e : X ≅ Y) (x : X) :
    (equivOfIso e).symm '' ((algebraMap (X.presheaf.stalk x) X.functionField).range : Set _) =
      ((algebraMap (Y.presheaf.stalk (e.hom.base x)) Y.functionField).range : Set _)

theorem

pull_baseToFunctionField

L148 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.pull_baseToFunctionField

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem pull_baseToFunctionField {K : Type u} [Field K] (f : X ⟶ Y)
    (h : f.base (genericPoint X) ⤳ genericPoint Y)
    (cX : X ⟶ Spec (CommRingCat.of K)) (cY : Y ⟶ Spec (CommRingCat.of K)) (hf : f ≫ cY = cX)
    (a : K) :
    pull f h (baseToFunctionField cY a) = baseToFunctionField cX a

theorem

equivOfIso_baseToFunctionField

L160 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.FunctionFieldPull.equivOfIso_baseToFunctionField

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem equivOfIso_baseToFunctionField {K : Type u} [Field K] (e : X ≅ Y)
    (cX : X ⟶ Spec (CommRingCat.of K)) (cY : Y ⟶ Spec (CommRingCat.of K))
    (hf : e.hom ≫ cY = cX) (a : K) :
    equivOfIso e (baseToFunctionField cY a) = baseToFunctionField cX a

theorem

finite_of_isFractionRing_of_finite

L168 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.finite_of_isFractionRing_of_finite

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve

Lean source · full declaration

theorem finite_of_isFractionRing_of_finite {A B K L : Type*} [CommRing A] [IsDomain A] [CommRing B]
  [IsDomain B]
    [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L]
    (f : A →+* B) (hf : Function.Injective f) (hfin : f.Finite)
    (g : K →+* L) (hg : ∀ a, g (algebraMap A K a) = algebraMap B L (f a)) :
    letI := g.toAlgebra; Module.Finite K L := by
  let algAB : Algebra A B := f.toAlgebra
  let algKL : Algebra K L := g.toAlgebra
  let algAL : Algebra A L := ((algebraMap B L).comp f).toAlgebra
  have : IsScalarTower A B L := IsScalarTower.of_algebraMap_eq (fun _ => rfl)
  have : IsScalarTower A K L := IsScalarTower.of_algebraMap_eq (fun a => (hg a).symm)
  have : Module.Finite A B := hfin
  have : FaithfulSMul A B := (faithfulSMul_iff_algebraMap_injective A B).mpr hf
  have : Algebra.IsIntegral A B := Algebra.IsIntegral.of_finite A B
  have : Algebra.IsAlgebraic A B := Algebra.IsIntegral.isAlgebraic
  exact Module.Finite.of_isLocalization A B (Rₚ := K) (Sₚ := L) A⁰

theorem

isIntegral_of_isFractionRing_of_finite

L185 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.isIntegral_of_isFractionRing_of_finite

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve

Lean source · statement

theorem isIntegral_of_isFractionRing_of_finite {A B K L : Type*} [CommRing A] [IsDomain A]
  [CommRing B] [IsDomain B]
    [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L]
    (f : A →+* B) (hf : Function.Injective f) (hfin : f.Finite)
    (g : K →+* L) (hg : ∀ a, g (algebraMap A K a) = algebraMap B L (f a)) :
    g.IsIntegral

theorem

ofPrime_eq_top_or_eq_self

L197 ↗

ValuationSubring.ofPrime_eq_top_or_eq_self

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve

Lean source · statement

theorem _root_.ValuationSubring.ofPrime_eq_top_or_eq_self {F : Type*} [Field F] (A :
  ValuationSubring F)
    [IsPrincipalIdealRing ↥A] (P : Ideal ↥A) [hP : P.IsPrime] :
    A.ofPrime P = ⊤ ∨ A.ofPrime P = A

theorem

eq_of_le_of_ne_top

L213 ↗

AlgebraicCurve.Place.eq_of_le_of_ne_top

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Place.eq_of_le_of_ne_top {K F : Type*} [Field K] [Field F]
  [Algebra K F]
    (v : Place K F) (S : ValuationSubring F) (h : v.toValuationSubring ≤ S) (hS : S ≠ ⊤) :
    v.toValuationSubring = S

theorem

specializes_genericPoint

L232 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.specializes_genericPoint

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
open FunctionFieldPull
section Leg
variable (k : Type) [Field k] [IsAlgClosed k]
  {L L' : Type} [Field L] [Field L'] [Algebra k L] [Algebra k L']
  (M : CurveModel k L) (M' : CurveModel k L')
  (d : M'.C ⟶ M.C) (hd : d ≫ M.toBase = M'.toBase)
omit [IsAlgClosed k] in

Lean source · statement

theorem specializes_genericPoint (hsurj : Function.Surjective d.base) :
    d.base (genericPoint M'.C) ⤳ genericPoint M.C

def

phi

L244 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.phi

Documentation

The base-field algebra homomorphism induced by a surjective morphism of curve models.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
open FunctionFieldPull
section Leg
variable (k : Type) [Field k] [IsAlgClosed k]
  {L L' : Type} [Field L] [Field L'] [Algebra k L] [Algebra k L']
  (M : CurveModel k L) (M' : CurveModel k L')
  (d : M'.C ⟶ M.C) (hd : d ≫ M.toBase = M'.toBase)

Lean source · statement

def phi (hsurj : Function.Surjective d.base) : L →ₐ[k] L'

theorem

phi_apply

L254 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.phi_apply

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
open FunctionFieldPull
section Leg
variable (k : Type) [Field k] [IsAlgClosed k]
  {L L' : Type} [Field L] [Field L'] [Algebra k L] [Algebra k L']
  (M : CurveModel k L) (M' : CurveModel k L')
  (d : M'.C ⟶ M.C) (hd : d ≫ M.toBase = M'.toBase)
omit [IsAlgClosed k] in

Lean source · statement

theorem phi_apply (hsurj : Function.Surjective d.base) (x : L) :
    phi k M M' d hd hsurj x = M'.ffEquiv.symm (pull d (specializes_genericPoint k M M' d hsurj)
      (M.ffEquiv x))

theorem

phi_germ

L258 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.phi_germ

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
open FunctionFieldPull
section Leg
variable (k : Type) [Field k] [IsAlgClosed k]
  {L L' : Type} [Field L] [Field L'] [Algebra k L] [Algebra k L']
  (M : CurveModel k L) (M' : CurveModel k L')
  (d : M'.C ⟶ M.C) (hd : d ≫ M.toBase = M'.toBase)
omit [IsAlgClosed k] in

Lean source · statement

theorem phi_germ (hsurj : Function.Surjective d.base)
    (U : M.C.Opens) [Nonempty (Scheme.Opens.toScheme U)] [Nonempty (Scheme.Opens.toScheme (d ⁻¹ᵁ
      U))] (t : Γ(M.C, U)) :
    phi k M M' d hd hsurj (M.ffEquiv.symm (M.C.germToFunctionField U t)) =
      M'.ffEquiv.symm (M'.C.germToFunctionField (d ⁻¹ᵁ U) ((d.app U).hom t))

theorem

finiteAlong_phi

L267 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.finiteAlong_phi

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
open FunctionFieldPull
section Leg
variable (k : Type) [Field k] [IsAlgClosed k]
  {L L' : Type} [Field L] [Field L'] [Algebra k L] [Algebra k L']
  (M : CurveModel k L) (M' : CurveModel k L')
  (d : M'.C ⟶ M.C) (hd : d ≫ M.toBase = M'.toBase)
omit [IsAlgClosed k] in

Lean source · statement

theorem finiteAlong_phi [IsFinite d] (hsurj : Function.Surjective d.base) : FiniteAlong k (phi k M
  M' d hd hsurj)

theorem

isIntegral_phi

L304 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.isIntegral_phi

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
open FunctionFieldPull
section Leg
variable (k : Type) [Field k] [IsAlgClosed k]
  {L L' : Type} [Field L] [Field L'] [Algebra k L] [Algebra k L']
  (M : CurveModel k L) (M' : CurveModel k L')
  (d : M'.C ⟶ M.C) (hd : d ≫ M.toBase = M'.toBase)
omit [IsAlgClosed k] in

Lean source · statement

theorem isIntegral_phi [IsFinite d] (hsurj : Function.Surjective d.base) : (phi k M M' d hd
  hsurj).toRingHom.IsIntegral

theorem

point_compat

L310 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite.AlgebraicCurve.FFLeg.point_compat

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.TopologicalSpace
open scoped nonZeroDivisors
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FFLeg
open _root_.AlgebraicCurve
open FunctionFieldPull
section Leg
variable (k : Type) [Field k] [IsAlgClosed k]
  {L L' : Type} [Field L] [Field L'] [Algebra k L] [Algebra k L']
  (M : CurveModel k L) (M' : CurveModel k L')
  (d : M'.C ⟶ M.C) (hd : d ≫ M.toBase = M'.toBase)

Lean source · statement

theorem point_compat [IsFinite d] (hsurj : Function.Surjective d.base) (R : Place k L') :
    (M.pointEquivPlace.symm (R.restrictAlong (phi k M M' d hd hsurj) (isIntegral_phi k M M' d hd
      hsurj))).1 =
      (M'.pointEquivPlace.symm R).1 ≫ d

theorem

exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite

L387 ↗

AlgebraicCurve.CurveModel.exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurve
noncomputable section
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
open _root_.AlgebraicCurve _root_.TopologicalSpace
open scoped nonZeroDivisors
open _root_.AlgebraicCurves.Models.Proofs in
open CurveModel_exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite in
open AlgebraicCurve.FFLeg in

Lean source · statement

theorem CurveModel.exists_algHom_finiteAlong_pointEquivPlace_restrictAlong_of_isFinite
    (k : Type) [Field k] [IsAlgClosed k]
    {L L' : Type} [Field L] [Field L'] [Algebra k L] [Algebra k L']
    (M : CurveModel k L) (M' : CurveModel k L')
    (d : M'.C ⟶ M.C) (hd : d ≫ M.toBase = M'.toBase) [IsFinite d] (hsurj : Function.Surjective
      d.base) :
    ∃ (φ : L →ₐ[k] L') (_hfin : FiniteAlong k φ) (hint : φ.toRingHom.IsIntegral),
      (∀ (U : M.C.Opens) [Nonempty (Scheme.Opens.toScheme U)] [Nonempty (Scheme.Opens.toScheme (d
        ⁻¹ᵁ U))]
        (t : Γ(M.C, U)),
        φ (M.ffEquiv.symm (M.C.germToFunctionField U t)) =
          M'.ffEquiv.symm (M'.C.germToFunctionField (d ⁻¹ᵁ U) ((d.app U).hom t))) ∧
      ∀ R : Place k L',
        (M.pointEquivPlace.symm (R.restrictAlong φ hint)).1 = (M'.pointEquivPlace.symm R).1 ≫ d

Module documentation

Curve Model exists alg Hom finite Along point Equiv Place restrict Along of is Finite

Declarations