NYLL
Module

CurveModel_exists_hom_pointEquivPlace_restrict_eq.lean

Nyll.AlgebraicCurves.Models.CurveModel_exists_hom_pointEquivPlace_restrict_eq
5 declarations indexed from sourceView source ↗

Module documentation

Curve Model exists hom point Equiv Place restrict eq

Imports4
Imported by1

Declarations

theorem

isIntegral_toAlgHom

L47 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_pointEquivPlace_restrict_eq.HG1ACor.isIntegral_toAlgHom
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_pointEquivPlace_restrict_eq
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1ACor
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem isIntegral_toAlgHom [Module.Finite F F'] :
    (IsScalarTower.toAlgHom K F F').toRingHom.IsIntegral
theorem

algebraAlong_toAlgHom

L51 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_pointEquivPlace_restrict_eq.HG1ACor.algebraAlong_toAlgHom
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_pointEquivPlace_restrict_eq
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1ACor
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem algebraAlong_toAlgHom :
    algebraAlong (IsScalarTower.toAlgHom K F F') = (inferInstance : Algebra F F')
theorem

finiteAlong_toAlgHom

L55 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_pointEquivPlace_restrict_eq.HG1ACor.finiteAlong_toAlgHom
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_pointEquivPlace_restrict_eq
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1ACor
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem finiteAlong_toAlgHom [Module.Finite F F'] :
    FiniteAlong K (IsScalarTower.toAlgHom K F F')
theorem

finrankAlong_toAlgHom

L60 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_pointEquivPlace_restrict_eq.HG1ACor.finrankAlong_toAlgHom
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_pointEquivPlace_restrict_eq
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
universe u
namespace HG1ACor
variable {K : Type u} [Field K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem finrankAlong_toAlgHom :
    finrankAlong K (IsScalarTower.toAlgHom K F F') = Module.finrank F F'
theorem

exists_hom_pointEquivPlace_restrict_eq

L68 ↗
AlgebraicCurve.CurveModel.exists_hom_pointEquivPlace_restrict_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_hom_pointEquivPlace_restrict_eq
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
universe u
open HG1ACor in
open AlgebraicCurve.CurveModel in
Lean source · statement
theorem _root_.AlgebraicCurve.CurveModel.exists_hom_pointEquivPlace_restrict_eq {K : Type u} [Field
  K] [IsAlgClosed K]
    [CharZero K] {F F' : Type u} [Field F] [Algebra K F] [Field F'] [Algebra K F']
    [Algebra F F'] [IsScalarTower K F F'] [Module.Finite F F']
    (M : CurveModel K F) (M' : CurveModel K F') :
    ∃ π : M'.C ⟶ M.C,
      π ≫ M.toBase = M'.toBase ∧
      IsFinite π ∧ Flat π ∧ LocallyOfFinitePresentation π ∧
      (∀ x : M.C, π.finrank x = Module.finrank F F') ∧
      M'.C.fromSpecStalk (genericPoint M'.C) ≫ π =
        Spec.map (CommRingCat.ofHom
          (M'.ffEquiv.toRingHom.comp ((algebraMap F F').comp M.ffEquiv.symm.toRingHom))) ≫
          M.C.fromSpecStalk (genericPoint M.C) ∧
      (∀ (y : {q : Spec (CommRingCat.of K) ⟶ M'.C // q ≫ M'.toBase = 𝟙 _})
          (x : {q : Spec (CommRingCat.of K) ⟶ M.C // q ≫ M.toBase = 𝟙 _}),
        y.1 ≫ π = x.1 → (M'.pointEquivPlace y).restrict F = M.pointEquivPlace x) ∧
      ∀ π' : M'.C ⟶ M.C,
        M'.C.fromSpecStalk (genericPoint M'.C) ≫ π' =
          M'.C.fromSpecStalk (genericPoint M'.C) ≫ π → π' = π

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