Module

WeilDifferentialRankOne_of_isCurveOver.lean

Nyll.AlgebraicCurves.Differentials.WeilDifferentialRankOne_of_isCurveOver

3 declarations indexed from sourceView source ↗

Module documentation

Weil Differential Rank One of is Curve Over

Imports10

Imported by3

theorem

stichtenothGenusExists_of_isCurveOver_port

L55 ↗

AlgebraicCurves.Differentials.Proofs.WeilDifferentialRankOneCurve.AlgebraicCurve.TowerFreePort.stichtenothGenusExists_of_isCurveOver_port

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.WeilDifferentialRankOneCurve
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open IntermediateField
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TowerFreePort
open _root_.AlgebraicCurve

Lean source · statement

theorem stichtenothGenusExists_of_isCurveOver_port {K : Type*} {F : Type*} [Field K] [Field F]
  [Algebra K F] [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F] (hC :
  ConstantsAreBase K F) :
    StichtenothGenusExists K F

theorem

solution

L79 ↗

AlgebraicCurves.Differentials.Proofs.WeilDifferentialRankOneCurve.AlgebraicCurve.TowerFreePort.solution

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.WeilDifferentialRankOneCurve
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open IntermediateField
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TowerFreePort
open _root_.AlgebraicCurve

Lean source · statement

theorem solution {K : Type*} {F : Type*} [Field K] [Field F] [Algebra K F] [PerfectField K]
  [Algebra.EssFiniteType K F] [IsCurveOver K F] (hC : ConstantsAreBase K F) :
    WeilDifferentialRankOne K F

theorem

weilDifferentialRankOne_of_isCurveOver

L89 ↗

AlgebraicCurve.weilDifferentialRankOne_of_isCurveOver

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.WeilDifferentialRankOneCurve
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open IntermediateField
open _root_.AlgebraicCurve
open IntermediateField _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Differentials.Proofs.WeilDifferentialRankOneCurve.AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.weilDifferentialRankOne_of_isCurveOver {K : Type*} {F : Type*}
  [Field K] [Field F] [Algebra K F] [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  (hC : ConstantsAreBase K F) :
    WeilDifferentialRankOne K F

Module documentation

Weil Differential Rank One of is Curve Over

Declarations

stichtenothGenusExists_of_isCurveOver_port

solution

weilDifferentialRankOne_of_isCurveOver