Module

Finsum_ramificationIndexAlong_sub_one_eq.lean

Nyll.AlgebraicCurves.Places.Finsum_ramificationIndexAlong_sub_one_eq

16 declarations indexed from sourceView source ↗

Module documentation

Finsum ramification Index Along sub one eq

Imports31

Imported by2

theorem

transcendental_gen

L74 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.transcendental_gen

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Tower
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F}
omit [IsAlgClosed K] [CharZero K] in

Lean source · statement

theorem transcendental_gen (htr : Transcendental K f) :
    Transcendental K (⟨f, IntermediateField.mem_adjoin_simple_self K f⟩ :
      ↥(IntermediateField.adjoin K ({f} : Set F)))

theorem

generator_adjoin'

L87 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.generator_adjoin'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Tower
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F}
omit [IsAlgClosed K] [CharZero K] in

Lean source · statement

theorem generator_adjoin' (f : F) :
    ∀ y : ↥(IntermediateField.adjoin K ({f} : Set F)), ∃ pn pd : Polynomial K,
      y = Polynomial.aeval
          (⟨f, IntermediateField.mem_adjoin_simple_self K f⟩ :
            ↥(IntermediateField.adjoin K ({f} : Set F))) pn
        / Polynomial.aeval
          (⟨f, IntermediateField.mem_adjoin_simple_self K f⟩ :
            ↥(IntermediateField.adjoin K ({f} : Set F))) pd

theorem

finiteDimensional_top

L111 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.finiteDimensional_top

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Tower
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F}

Lean source · statement

theorem finiteDimensional_top (K' L : Type*) [Field K'] [Field L] [Algebra K' L] :
    FiniteDimensional (↥(⊤ : IntermediateField K' L)) L

theorem

finiteDimensional_adjoin_gen'

L122 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.finiteDimensional_adjoin_gen'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Tower
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F}
omit [IsAlgClosed K] [CharZero K] in

Lean source · statement

theorem finiteDimensional_adjoin_gen' (f : F) :
    FiniteDimensional
      (↥(IntermediateField.adjoin K
        ({(⟨f, IntermediateField.mem_adjoin_simple_self K f⟩ :
            ↥(IntermediateField.adjoin K ({f} : Set F)))} :
          Set (↥(IntermediateField.adjoin K ({f} : Set F))))))
      (↥(IntermediateField.adjoin K ({f} : Set F)))

theorem

transcendental_ratFunc_X

L147 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.transcendental_ratFunc_X

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Tower
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F}

Lean source · statement

theorem transcendental_ratFunc_X (K' : Type*) [Field K'] :
    Transcendental K' (RatFunc.X : RatFunc K')

theorem

adjoin_ratFunc_X_eq_top

L157 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.adjoin_ratFunc_X_eq_top

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Tower
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F}

Lean source · statement

theorem adjoin_ratFunc_X_eq_top (K' : Type*) [Field K'] :
    IntermediateField.adjoin K' ({(RatFunc.X : RatFunc K')} : Set (RatFunc K')) = ⊤

theorem

essFiniteType_ratFunc

L180 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.essFiniteType_ratFunc

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Tower
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F}

Lean source · statement

theorem essFiniteType_ratFunc (K' : Type*) [Field K'] :
    Algebra.EssFiniteType K' (RatFunc K')

def

adjoinEquivRatFunc

L188 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.adjoinEquivRatFunc

Documentation

Identifies the field generated by a transcendental element with the rational function field.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Tower
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F}

Lean source · statement

def adjoinEquivRatFunc (htr : Transcendental K f) :
    (↥(IntermediateField.adjoin K ({f} : Set F))) ≃ₐ[K] RatFunc K

theorem

isCurveOver_E

L228 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.isCurveOver_E

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Heads
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F} (htr : Transcendental K f)
local notation "E" => (IntermediateField.adjoin K (Set.singleton f) : Type _)
omit [IsAlgClosed K] in
include htr in

Lean source · statement

theorem isCurveOver_E : IsCurveOver K E

theorem

essFiniteType_E

L234 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.essFiniteType_E

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Heads
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F} (htr : Transcendental K f)
local notation "E" => (IntermediateField.adjoin K (Set.singleton f) : Type _)
omit [IsAlgClosed K] [CharZero K] in
include htr in

Lean source · statement

theorem essFiniteType_E : Algebra.EssFiniteType K E

theorem

hasCanonicalDivisor_E

L239 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.hasCanonicalDivisor_E

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Heads
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F} (htr : Transcendental K f)
local notation "E" => (IntermediateField.adjoin K (Set.singleton f) : Type _)
omit [IsAlgClosed K] in
include htr in

Lean source · full declaration

theorem hasCanonicalDivisor_E :
    haveI : IsCurveOver K E := isCurveOver_E htr
    HasCanonicalDivisor (K := K) (F := E) := by
  have : PerfectField K := PerfectField.ofCharZero
  have : IsCurveOver K E := isCurveOver_E htr
  have : Algebra.EssFiniteType K E := essFiniteType_E htr
  exact hasCanonicalDivisor_of_isCurveOver

theorem

genus_E_eq_zero

L247 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.RHEtower.genus_E_eq_zero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
namespace RHEtower
section Heads
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F]
variable {f : F} (htr : Transcendental K f)
local notation "E" => (IntermediateField.adjoin K (Set.singleton f) : Type _)
include htr in

Lean source · full declaration

theorem genus_E_eq_zero :
    haveI : IsCurveOver K E := isCurveOver_E htr
    haveI : HasCanonicalDivisor (K := K) (F := E) := hasCanonicalDivisor_E htr
    genus K E = 0 := by
  classical
  have : PerfectField K := PerfectField.ofCharZero
  have hIC : IsCurveOver K E := isCurveOver_E htr
  have hEF : Algebra.EssFiniteType K E := essFiniteType_E htr
  have hCD : HasCanonicalDivisor (K := K) (F := E) := hasCanonicalDivisor_E htr
  have hDC : ∀ v : Place K E, v.DCoordGenerates := dCoordGenerates_of_isCurveOver
  have hICr : IsCurveOver K (RatFunc K) := instIsCurveOverRatFunc K
  have hEFr : Algebra.EssFiniteType K (RatFunc K) := essFiniteType_ratFunc K
  have hCDr : HasCanonicalDivisor (K := K) (F := RatFunc K) :=
    instHasCanonicalDivisorRatFuncPerfectField K
  have hDCr : ∀ v : Place K (RatFunc K), v.DCoordGenerates := dCoordGenerates_of_isCurveOver
  let e := adjoinEquivRatFunc htr
  let : Algebra (RatFunc K) E := (e.symm.toAlgHom.toRingHom).toAlgebra
  have : IsScalarTower K (RatFunc K) E := IsScalarTower.of_algebraMap_eq' (by
    ext r
    exact congrArg Subtype.val ((e.symm.commutes r).symm))
  let eR : E ≃ₐ[RatFunc K] RatFunc K :=
    AlgEquiv.ofRingEquiv (f := e.toRingEquiv) (fun r => e.apply_symm_apply r)
  have : FiniteDimensional (RatFunc K) E := Module.Finite.equiv eR.symm.toLinearEquiv
  have : Algebra.IsSeparable (RatFunc K) E :=
    Algebra.IsSeparable.of_algHom _ _ eR.toAlgHom
  have hC_R : ConstantsAreBase K (RatFunc K) :=
    constantsAreBase_of_isAlgClosed K (RatFunc K)
  have hRR_R : FunctionFieldRiemannRoch K (RatFunc K) :=
    functionFieldRiemannRoch_of_isAlgClosed
  have hSG_R : StichtenothGenusExists K (RatFunc K) :=
    stichtenothGenusExists_of_isCurveOver hC_R
  have hWDA_R : WeilDualityAdelic K (RatFunc K) :=
    AlgebraicCurve.weilDualityAdelic_of_functionFieldRiemannRoch_of_stichtenothGenusExists hRR_R
    hSG_R
  have hC_E : ConstantsAreBase K E := constantsAreBase_of_isAlgClosed K E
  have hRR_E : FunctionFieldRiemannRoch K E := functionFieldRiemannRoch_of_isAlgClosed
  have hSG_E : StichtenothGenusExists K E := stichtenothGenusExists_of_isCurveOver hC_E
  have hWDA_E : WeilDualityAdelic K E :=
    AlgebraicCurve.weilDualityAdelic_of_functionFieldRiemannRoch_of_stichtenothGenusExists hRR_E
    hSG_E
  have h1 : genus K E = genusFF K E := AlgebraicCurve.genus_eq_genusFF hRR_E hWDA_E hC_E
  have h2 : genusFF K E = genusFF K (RatFunc K) := AlgebraicCurve.genusFF_eq_of_algEquiv e
  have h3 : genus K (RatFunc K) = genusFF K (RatFunc K) :=
    AlgebraicCurve.genus_eq_genusFF hRR_R hWDA_R hC_R
  have h4 : genus K (RatFunc K) = 0 := genus_ratFunc_eq_zero K
  omega

lemma

degree_canonicalDivisorOf_F

L312 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.SolRH.degree_canonicalDivisorOf_F

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
open AlgebraicCurve IntermediateField KaehlerDifferential
namespace SolRH
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F] [IsCurveOver K F] [Algebra.EssFiniteType K F]
variable [HasCanonicalDivisor (K := K) (F := F)]
variable {f : F} (htr : Transcendental K f)
  [FiniteDimensional (↥(adjoin K ({f} : Set F))) F]
include htr
local notation "E" => (adjoin K (Set.singleton f) : Type _)

Lean source · statement

lemma degree_canonicalDivisorOf_F {ω : Ω[F⁄K]} (hω : ω ≠ 0) :
    Divisor.degree (canonicalDivisorOf hω) = 2 * (genus K F : ℤ) - 2

lemma

degree_canonicalDivisorOf_E

L347 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.SolRH.degree_canonicalDivisorOf_E

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
open AlgebraicCurve IntermediateField KaehlerDifferential
namespace SolRH
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F] [IsCurveOver K F] [Algebra.EssFiniteType K F]
variable [HasCanonicalDivisor (K := K) (F := F)]
variable {f : F} (htr : Transcendental K f)
  [FiniteDimensional (↥(adjoin K ({f} : Set F))) F]
include htr
local notation "E" => (adjoin K (Set.singleton f) : Type _)
omit [IsCurveOver K F] [Algebra.EssFiniteType K F] [HasCanonicalDivisor (K := K) (F := F)]
  [FiniteDimensional (↥(adjoin K ({f} : Set F))) F] in

Lean source · full declaration

lemma degree_canonicalDivisorOf_E :
    haveI : IsCurveOver K E := RHEtower.isCurveOver_E htr
    haveI : HasCanonicalDivisor (K := K) (F := E) := RHEtower.hasCanonicalDivisor_E htr
    ∀ {ω : Ω[E⁄K]} (hω : ω ≠ 0),
      Divisor.degree (canonicalDivisorOf hω) = 2 * (genus K E : ℤ) - 2 := by
  have : IsCurveOver K E := RHEtower.isCurveOver_E htr
  have : Algebra.EssFiniteType K E := RHEtower.essFiniteType_E htr
  have : HasCanonicalDivisor (K := K) (F := E) := RHEtower.hasCanonicalDivisor_E htr
  intro ω hω
  have hgen := RHEtower.transcendental_gen htr
  have hfd : FiniteDimensional (↥(adjoin K ({AdjoinSimple.gen K f} : Set E))) E :=
    RHEtower.finiteDimensional_adjoin_gen' f
  exact @degree_canonicalDivisorOf_F K _ _ _ E _ _ _ _ _ _ hgen hfd _ hω

lemma

ramIdxAlong_eq_ramIdx

L363 ↗

AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq.SolRH.ramIdxAlong_eq_ramIdx

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
open AlgebraicCurve IntermediateField KaehlerDifferential
namespace SolRH
variable {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
variable {F : Type*} [Field F] [Algebra K F] [IsCurveOver K F] [Algebra.EssFiniteType K F]
variable [HasCanonicalDivisor (K := K) (F := F)]
variable {f : F} (htr : Transcendental K f)
  [FiniteDimensional (↥(adjoin K ({f} : Set F))) F]
include htr
local notation "E" => (adjoin K (Set.singleton f) : Type _)
omit [IsAlgClosed K] [CharZero K] [IsCurveOver K F] [Algebra.EssFiniteType K F] htr
  [HasCanonicalDivisor (K := K) (F := F)]
  [FiniteDimensional (↥(adjoin K ({f} : Set F))) F] in

Lean source · statement

lemma ramIdxAlong_eq_ramIdx (w : Place K F) :
    Place.ramificationIndexAlong (adjoin K ({f} : Set F)).val w = w.ramificationIndex E

theorem

finsum_ramificationIndexAlong_sub_one_eq

L371 ↗

AlgebraicCurve.finsum_ramificationIndexAlong_sub_one_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finsum_ramificationIndexAlong_sub_one_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve IntermediateField
open AlgebraicCurve IntermediateField KaehlerDifferential
open SolRH in

Lean source · statement

theorem _root_.AlgebraicCurve.finsum_ramificationIndexAlong_sub_one_eq
    {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
    {F : Type*} [Field F] [Algebra K F] [IsCurveOver K F] [Algebra.EssFiniteType K F]
    [HasCanonicalDivisor (K := K) (F := F)]
    {f : F} (htr : Transcendental K f)
    [FiniteDimensional (↥(adjoin K ({f} : Set F))) F] :
    (∑ᶠ w : Place K F, ((Place.ramificationIndexAlong (adjoin K ({f} : Set F)).val w : ℤ) - 1)) =
      2 * (Module.finrank K ↥(regularDifferentials K F) : ℤ) - 2 +
      2 * (Module.finrank (↥(adjoin K ({f} : Set F))) F : ℤ)

Module documentation

Finsum ramification Index Along sub one eq

Declarations