Module

GenusFF_eq_of_constantFieldExtension_of_finite_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_eq_of_constantFieldExtension_of_finite_of_isAlgClosed

56 declarations indexed from sourceView source ↗

Module documentation

Genus FF eq of constant Field Extension of finite of is Alg Closed

Imports19

Imported by1

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.All

theorem

finiteDimensional_lSpace_zero_of_constantsAreBase

L78 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.finiteDimensional_lSpace_zero_of_constantsAreBase

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Genus
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finiteDimensional_lSpace_zero_of_constantsAreBase (hC : ConstantsAreBase K F) :
    FiniteDimensional K (LSpace (0 : Divisor K F))

theorem

genusFF_eq_of_riemannGenusReachedAt

L82 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.genusFF_eq_of_riemannGenusReachedAt

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Genus
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem genusFF_eq_of_riemannGenusReachedAt [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))] (hC : ConstantsAreBase K F)
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) : (genusFF K F : ℤ) = γ

theorem

exists_riemannGenusReachedAt_genusFF

L91 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.exists_riemannGenusReachedAt_genusFF

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Genus
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_riemannGenusReachedAt_genusFF [PerfectField K] [Algebra.EssFiniteType K F]
    [IsCurveOver K F] (hC : ConstantsAreBase K F) :
    Nonempty (Place K F) ∧ ∃ D₀ : Divisor K F, RiemannGenusReachedAt (genusFF K F : ℤ) D₀

theorem

mem_of_combinations_mem

L106 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.mem_of_combinations_mem

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section LinAlg
variable {R V : Type*} [Field R] [AddCommGroup V] [Module R V]

Lean source · statement

theorem mem_of_combinations_mem {n : Type*} [Fintype n] [DecidableEq n] (N : Matrix n n R)
    (hN : N.det ≠ 0) (S : Submodule R V) (u : n → V) (h : ∀ j, ∑ i, N j i • u i ∈ S) (i : n) :
    u i ∈ S

theorem

algebraMap_mem_lSpace_pullbackConstants

L137 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.algebraMap_mem_lSpace_pullbackConstants

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Compare
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']

Lean source · statement

theorem algebraMap_mem_lSpace_pullbackConstants {D : Divisor K F} {y : F} (hy : y ∈ LSpace D) :
    algebraMap F F' y ∈ LSpace (Divisor.pullbackConstants K' F' D)

theorem

mem_lSpace_of_algebraMap_mem

L148 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.mem_lSpace_of_algebraMap_mem

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Compare
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']

Lean source · statement

theorem mem_lSpace_of_algebraMap_mem
    (hsurj : ∀ v : Place K F, ∃ w : Place K' F', Place.restrictConstants F (K := K) w = v)
    {D : Divisor K F} {y : F}
    (hy : algebraMap F F' y ∈ LSpace (Divisor.pullbackConstants K' F' D)) : y ∈ LSpace D

theorem

ell_le_ell_pullbackConstants

L170 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.ell_le_ell_pullbackConstants

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Compare
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']

Lean source · full declaration

theorem ell_le_ell_pullbackConstants
    (hLD : ∀ (n : ℕ) (b : Fin n → F), LinearIndependent K b →
      LinearIndependent K' (fun i => algebraMap F F' (b i)))
    (D : Divisor K F) [FiniteDimensional K (LSpace D)]
    [FiniteDimensional K' (LSpace (Divisor.pullbackConstants K' F' D))] :
    ell D ≤ ell (Divisor.pullbackConstants K' F' D) := by
  set b := Module.finBasis K (LSpace D)
  have hb : LinearIndependent K (fun i => (b i : F)) :=
    b.linearIndependent.map' (LSpace D).subtype (Submodule.ker_subtype _)
  have hb' := hLD _ _ hb
  let c : Fin (Module.finrank K (LSpace D)) → LSpace (Divisor.pullbackConstants K' F' D) :=
    fun i => ⟨algebraMap F F' (b i), algebraMap_mem_lSpace_pullbackConstants (b i).2⟩
  have hc : LinearIndependent K' c :=
    LinearIndependent.of_comp (LSpace (Divisor.pullbackConstants K' F' D)).subtype hb'
  simpa [ell] using hc.fintype_card_le_finrank

theorem

pullbackConstants_apply_smul

L186 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.pullbackConstants_apply_smul

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Compare
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']

Lean source · statement

theorem pullbackConstants_apply_smul {g : SemilinearAut K' F'}
    (hg : ∀ y : F, g • algebraMap F F' y = algebraMap F F' y) (D : Divisor K F)
    (w : Place K' F') :
    Divisor.pullbackConstants K' F' D (g • w) = Divisor.pullbackConstants K' F' D w

theorem

smul_mem_lSpace_pullbackConstants

L209 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.smul_mem_lSpace_pullbackConstants

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Compare
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']

Lean source · statement

theorem smul_mem_lSpace_pullbackConstants {g : SemilinearAut K' F'}
    (hg : ∀ y : F, g • algebraMap F F' y = algebraMap F F' y) {D : Divisor K F} {z : F'}
    (hz : z ∈ LSpace (Divisor.pullbackConstants K' F' D)) :
    g • z ∈ LSpace (Divisor.pullbackConstants K' F' D)

theorem

exists_eq_sum_basis

L222 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.exists_eq_sum_basis

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Compare
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']
omit [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F'] in

Lean source · statement

theorem exists_eq_sum_basis [Algebra.IsAlgebraic K K']
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤) (z : F') :
    ∃ (E : IntermediateField K K') (_ : FiniteDimensional K E)
      (y : Fin (Module.finrank K E) → F),
      z = ∑ i, algebraMap F F' (y i) * algebraMap K' F' (Module.finBasis K E i)

theorem

lSpace_pullbackConstants_le_span

L272 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.lSpace_pullbackConstants_le_span

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Compare
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']

Lean source · statement

theorem lSpace_pullbackConstants_le_span [PerfectField K] [IsAlgClosed K']
    [Algebra.IsAlgebraic K K']
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hsurj : ∀ v : Place K F, ∃ w : Place K' F', Place.restrictConstants F (K := K) w = v)
    (hAut : ∀ σ : K' ≃ₐ[K] K', ∃ g : SemilinearAut K' F',
      (∀ a : K', SemilinearAut.baseAut g a = σ a) ∧
        ∀ y : F, g • algebraMap F F' y = algebraMap F F' y)
    (D : Divisor K F) :
    LSpace (Divisor.pullbackConstants K' F' D)
      ≤ Submodule.span K' (algebraMap F F' '' (LSpace D : Set F))

theorem

ell_pullbackConstants_le_ell

L330 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.ell_pullbackConstants_le_ell

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Compare
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']

Lean source · statement

theorem ell_pullbackConstants_le_ell [PerfectField K] [IsAlgClosed K']
    [Algebra.IsAlgebraic K K']
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hsurj : ∀ v : Place K F, ∃ w : Place K' F', Place.restrictConstants F (K := K) w = v)
    (hAut : ∀ σ : K' ≃ₐ[K] K', ∃ g : SemilinearAut K' F',
      (∀ a : K', SemilinearAut.baseAut g a = σ a) ∧
        ∀ y : F, g • algebraMap F F' y = algebraMap F F' y)
    (D : Divisor K F) [FiniteDimensional K (LSpace D)] :
    ell (Divisor.pullbackConstants K' F' D) ≤ ell D

theorem

exists_le_pullbackConstants

L362 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.exists_le_pullbackConstants

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Compare
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']

Lean source · statement

theorem exists_le_pullbackConstants (D' : Divisor K' F') :
    ∃ D : Divisor K F, D' ≤ Divisor.pullbackConstants K' F' D

theorem

genusFF_eq_of_perfectField

L392 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.genusFF_eq_of_perfectField

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Engine
open _root_.Polynomial
open _root_.IntermediateField
open _root_.AlgebraicCurve
section Compare
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F']
omit [HasPrincipalDivisors K' F'] in

Lean source · full declaration

theorem genusFF_eq_of_perfectField [PerfectField K] [IsAlgClosed K'] [Algebra.IsAlgebraic K K']
    [Algebra.EssFiniteType K F] [IsCurveOver K F]
    [Algebra.EssFiniteType K' F'] [IsCurveOver K' F']
    (hC : ConstantsAreBase K F) (hC' : ConstantsAreBase K' F')
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (hLD : ∀ (n : ℕ) (b : Fin n → F), LinearIndependent K b →
      LinearIndependent K' (fun i => algebraMap F F' (b i)))
    (hAut : ∀ σ : K' ≃ₐ[K] K', ∃ g : SemilinearAut K' F',
      (∀ a : K', SemilinearAut.baseAut g a = σ a) ∧
        ∀ y : F, g • algebraMap F F' y = algebraMap F F' y) :
    genusFF K F = genusFF K' F' := by
  have : Algebra.IsSeparable K K' := Algebra.IsAlgebraic.isSeparable_of_perfectField
  have := finiteDimensional_lSpace_zero_of_constantsAreBase hC
  have := finiteDimensional_lSpace_zero_of_constantsAreBase hC'
  obtain ⟨hne, D₀, hR⟩ := exists_riemannGenusReachedAt_genusFF hC
  obtain ⟨hne', D₀', hR'⟩ := exists_riemannGenusReachedAt_genusFF hC'
  have := hne
  have := hne'
  have : ConstantFieldDegreeFormula K K' F F' :=
    constantFieldDegreeFormula_of_isConstantFieldExtension_of_isCurveOver hgen hconst
  have hsurj : ∀ v : Place K F, ∃ w : Place K' F', Place.restrictConstants F (K := K) w = v :=
    fun v => Place.exists_forgetConstants_restrict_eq_of_isConstantFieldExtension
      hgen hconst (M := F) v
  have hdeg := ConstantFieldDegreeFormula.degree_pullbackConstants (K := K) (K' := K')
    (F := F) (F' := F')
  apply le_antisymm
  · have h1 := hR.eq
    have h2 := hR'.isMax (Divisor.pullbackConstants K' F' D₀)
    have := finiteDimensional_lSpace (K := K) (F := F) D₀
    have h3 : (ell (Divisor.pullbackConstants K' F' D₀) : ℤ) ≤ ell D₀ := by
      exact_mod_cast ell_pullbackConstants_le_ell hgen hsurj hAut D₀
    rw [hdeg] at h2
    have : (genusFF K F : ℤ) ≤ genusFF K' F' := by linarith
    exact_mod_cast this
  · obtain ⟨D, hD⟩ := exists_le_pullbackConstants (K := K) (F := F) D₀'
    have := finiteDimensional_lSpace (K := K') (F := F') (Divisor.pullbackConstants K' F' D)
    have := finiteDimensional_lSpace (K := K) (F := F) D
    have h1 := hR'.eq
    have h2 := ell_sub_ell_le_degree_sub_degree hD
    have h3 := hR.isMax D
    have h4 : (ell D : ℤ) ≤ ell (Divisor.pullbackConstants K' F' D) := by
      exact_mod_cast ell_le_ell_pullbackConstants hLD D
    rw [hdeg] at h2
    have : (genusFF K' F' : ℤ) ≤ genusFF K F := by linarith
    exact_mod_cast this

theorem

exists_constantEmbedding

L448 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.exists_constantEmbedding

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Constants
variable {k K F₀ F : Type*} [Field k] [Finite k] [Field K] [IsAlgClosed K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]

Lean source · statement

theorem exists_constantEmbedding :
    ∃ j : k →+* K, ∀ a : k, algebraMap K F (j a) = algebraMap F₀ F (algebraMap k F₀ a)

theorem

mem_range_algebraMap_of_pow_card_eq

L480 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.mem_range_algebraMap_of_pow_card_eq

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Constants
variable {k K F₀ F : Type*} [Field k] [Finite k] [Field K] [IsAlgClosed K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
omit [IsAlgClosed K] [Algebra K F] [Algebra F₀ F] in

Lean source · statement

theorem mem_range_algebraMap_of_pow_card_eq {L : Type*} [Field L] [Algebra k L] {y : L}
    (hy : y ^ Nat.card k = y) : y ∈ Set.range (algebraMap k L)

theorem

linearDisjoint

L513 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.linearDisjoint

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Constants
variable {k K F₀ F : Type*} [Field k] [Finite k] [Field K] [IsAlgClosed K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
variable [Algebra k K]
variable [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]

Lean source · statement

theorem linearDisjoint (φ : F →ₐ[K] F)
    (hφ : ∀ x : F₀, φ (algebraMap F₀ F x) = algebraMap F₀ F (x ^ Nat.card k)) :
    ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0

theorem

essFiniteType_of_gen

L622 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.essFiniteType_of_gen

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Upstairs
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]

Lean source · statement

theorem essFiniteType_of_gen
    (hfg : ∃ s : Finset F₀, IntermediateField.adjoin k (s : Set F₀) = ⊤)
    (hgen : IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤) :
    Algebra.EssFiniteType K F

def

AA

L658 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.AA

Documentation

The image of the base function field as a subalgebra of the ambient field.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)

Lean source · statement

def AA : Subalgebra k F

def

BB

L661 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.BB

Documentation

The image of the chosen constant field as a subalgebra of the ambient field.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)

Lean source · statement

def BB : Subalgebra k F

theorem

algebraMap_mem_AA

L664 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.algebraMap_mem_AA

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
omit [IsScalarTower k K F] in

Lean source · statement

theorem algebraMap_mem_AA (y : F₀) : algebraMap F₀ F y ∈ AA (k := k) (F₀ := F₀) (F := F)

theorem

algebraMap_mem_BB

L667 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.algebraMap_mem_BB

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)

Lean source · statement

theorem algebraMap_mem_BB (ω : Ω) : algebraMap Ω F ω ∈ BB (F := F) Ω

def

compSubalg

L670 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.compSubalg

Documentation

The compositum of the two image subalgebras, regarded as an algebra over the function field.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)

Lean source · full declaration

def compSubalg : Subalgebra F₀ F where
  carrier := (AA (k := k) (F₀ := F₀) (F := F) ⊔ BB (F := F) Ω : Subalgebra k F)
  mul_mem' ha hb := Subalgebra.mul_mem _ ha hb
  add_mem' ha hb := Subalgebra.add_mem _ ha hb
  algebraMap_mem' y := Algebra.mem_sup_left (algebraMap_mem_AA (k := k) y)

theorem

mem_compSubalg_iff

L676 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.mem_compSubalg_iff

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)

Lean source · statement

theorem mem_compSubalg_iff {x : F} :
    x ∈ compSubalg (k := k) (F₀ := F₀) (F := F) Ω ↔
      x ∈ (AA (k := k) (F₀ := F₀) (F := F) ⊔ BB (F := F) Ω : Subalgebra k F)

theorem

isIntegral_algebraMap_of_mem_Ω

L682 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.isIntegral_algebraMap_of_mem_Ω

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

theorem isIntegral_algebraMap_of_mem_Ω (ω : Ω) : IsIntegral F₀ (algebraMap Ω F ω)

theorem

isIntegral_of_mem_compSubalg

L693 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.isIntegral_of_mem_compSubalg

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

theorem isIntegral_of_mem_compSubalg {x : F}
    (hx : x ∈ compSubalg (k := k) (F₀ := F₀) (F := F) Ω) : IsIntegral F₀ x

def

FΩ

L709 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.FΩ

Documentation

The intermediate field generated by the function field and the chosen constant field.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

def FΩ : IntermediateField F₀ F

theorem

mem_FΩ_iff

L714 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.mem_FΩ_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

theorem mem_FΩ_iff {x : F} :
    x ∈ FΩ (k := k) (F₀ := F₀) (F := F) Ω ↔
      x ∈ (AA (k := k) (F₀ := F₀) (F := F) ⊔ BB (F := F) Ω : Subalgebra k F)

instance

isIntegral_FΩ

L718 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.isIntegral_FΩ

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

instance isIntegral_FΩ : Algebra.IsIntegral F₀ (FΩ (k := k) (F₀ := F₀) (F := F) Ω)

instance

algΩ

L722 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.algΩ

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

instance algΩ : Algebra Ω (FΩ (k := k) (F₀ := F₀) (F := F) Ω)

theorem

coe_algebraMap_Ω

L730 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.coe_algebraMap_Ω

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

theorem coe_algebraMap_Ω (ω : Ω) :
    ((algebraMap Ω (FΩ (k := k) (F₀ := F₀) (F := F) Ω) ω : FΩ (k := k) (F₀ := F₀) (F := F) Ω) : F)
      = algebraMap Ω F ω

instance

towerΩ

L734 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.towerΩ

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

instance towerΩ : IsScalarTower Ω (FΩ (k := k) (F₀ := F₀) (F := F) Ω) F

instance

towerkΩ

L737 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.towerkΩ

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

instance towerkΩ : IsScalarTower k Ω (FΩ (k := k) (F₀ := F₀) (F := F) Ω)

theorem

coe_algebraMap_F₀

L746 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.coe_algebraMap_F₀

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

theorem coe_algebraMap_F₀ (y : F₀) :
    ((algebraMap F₀ (FΩ (k := k) (F₀ := F₀) (F := F) Ω) y : FΩ (k := k) (F₀ := F₀) (F := F) Ω) : F)
      = algebraMap F₀ F y

theorem

mem_FΩ_iff_adjoin

L750 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.mem_FΩ_iff_adjoin

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

theorem mem_FΩ_iff_adjoin {x : F} :
    x ∈ FΩ (k := k) (F₀ := F₀) (F := F) Ω ↔
      x ∈ Algebra.adjoin k ((AA (k := k) (F₀ := F₀) (F := F) : Set F) ∪ (BB (F := F) Ω : Set F))

theorem

mem_adjoin_range_algebraMap_Ω

L756 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.mem_adjoin_range_algebraMap_Ω

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

theorem mem_adjoin_range_algebraMap_Ω (x : F) (hx : x ∈ FΩ (k := k) (F₀ := F₀) (F := F) Ω) :
    (⟨x, hx⟩ : FΩ (k := k) (F₀ := F₀) (F := F) Ω)
      ∈ Algebra.adjoin F₀ (Set.range (algebraMap Ω (FΩ (k := k) (F₀ := F₀) (F := F) Ω)))

theorem

adjoin_range_algebraMap_Ω_eq_top

L791 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.adjoin_range_algebraMap_Ω_eq_top

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Compositum
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

theorem adjoin_range_algebraMap_Ω_eq_top :
    Algebra.adjoin F₀ (Set.range (algebraMap Ω (FΩ (k := k) (F₀ := F₀) (F := F) Ω))) = ⊤

theorem

linearDisjoint_AA_BB

L808 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.linearDisjoint_AA_BB

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Semilinear
open TensorProduct
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)

Lean source · statement

theorem linearDisjoint_AA_BB
    (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0) :
    (AA (k := k) (F₀ := F₀) (F := F)).LinearDisjoint (BB (F := F) Ω)

def

mulEquiv

L860 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.mulEquiv

Documentation

The tensor-product description of the compositum supplied by linear disjointness.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Semilinear
open TensorProduct
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)

Lean source · statement

def mulEquiv : (AA (k := k) (F₀ := F₀) (F := F)) ⊗[k] (BB (F := F) Ω) ≃ₐ[k]
    ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F) Ω))

theorem

coe_mulEquiv_tmul

L865 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.coe_mulEquiv_tmul

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Semilinear
open TensorProduct
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)

Lean source · statement

theorem coe_mulEquiv_tmul (a : AA (k := k) (F₀ := F₀) (F := F)) (b : BB (F := F) Ω) :
    ((mulEquiv Ω hLD (a ⊗ₜ[k] b) : ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F) Ω))) : F)
      = (a : F) * (b : F)

def

eB

L871 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.eB

Documentation

Identify the constant field with its image subalgebra in the ambient field.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Semilinear
open TensorProduct
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)

Lean source · statement

def eB : Ω ≃ₐ[k] BB (F := F) Ω

theorem

coe_eB

L873 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.coe_eB

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Semilinear
open TensorProduct
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)

Lean source · statement

theorem coe_eB (ω : Ω) : ((eB (F := F) Ω ω : BB (F := F) Ω) : F) = algebraMap Ω F ω

def

supAut

L879 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.supAut

Documentation

Extend a constant-field automorphism to the compositum through the tensor-product description.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Semilinear
open TensorProduct
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)

Lean source · statement

def supAut (σ : Ω ≃ₐ[k] Ω) :
    ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F) Ω)) ≃ₐ[k]
      ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F) Ω))

theorem

supAut_algebraMap_F₀

L886 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.supAut_algebraMap_F₀

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Semilinear
open TensorProduct
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)

Lean source · statement

theorem supAut_algebraMap_F₀ (σ : Ω ≃ₐ[k] Ω) (y : F₀)
    (hy : algebraMap F₀ F y ∈ (AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F) Ω)) :
    ((supAut Ω hLD σ ⟨algebraMap F₀ F y, hy⟩ : ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F)
      Ω))) : F)
      = algebraMap F₀ F y

theorem

supAut_algebraMap_Ω

L909 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.supAut_algebraMap_Ω

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Semilinear
open TensorProduct
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)

Lean source · statement

theorem supAut_algebraMap_Ω (σ : Ω ≃ₐ[k] Ω) (ω : Ω)
    (hω : algebraMap Ω F ω ∈ (AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F) Ω)) :
    ((supAut Ω hLD σ ⟨algebraMap Ω F ω, hω⟩ : ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F)
      Ω))) : F)
      = algebraMap Ω F (σ ω)

def

ringAutFΩ

L934 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.ringAutFΩ

Documentation

The ring automorphism of the intermediate compositum induced by a constant-field automorphism.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Semilinear
open TensorProduct
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)
variable [Algebra.IsAlgebraic k Ω]

Lean source · full declaration

def ringAutFΩ (σ : Ω ≃ₐ[k] Ω) : (FΩ (k := k) (F₀ := F₀) (F := F) Ω) ≃+* (FΩ (k := k) (F₀ := F₀) (F
  := F) Ω) where
  toFun x := ⟨supAut Ω hLD σ ⟨x.1, x.2⟩, (supAut Ω hLD σ ⟨x.1, x.2⟩).2⟩
  invFun x := ⟨(supAut Ω hLD σ).symm ⟨x.1, x.2⟩, ((supAut Ω hLD σ).symm ⟨x.1, x.2⟩).2⟩
  left_inv x := by
    apply Subtype.ext
    exact congrArg
      (fun z : ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F) Ω)) => (z : F))
      ((supAut Ω hLD σ).symm_apply_apply ⟨x.1, x.2⟩)
  right_inv x := by
    apply Subtype.ext
    exact congrArg
      (fun z : ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F) Ω)) => (z : F))
      ((supAut Ω hLD σ).apply_symm_apply ⟨x.1, x.2⟩)
  map_mul' x y := by
    apply Subtype.ext
    change ((supAut Ω hLD σ ⟨x.1 * y.1, _⟩ : ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F)
      Ω))) : F) = _
    rw [show (⟨x.1 * y.1, (x * y).2⟩ : ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F) Ω)))
        = ⟨x.1, x.2⟩ * ⟨y.1, y.2⟩ from rfl, map_mul]
    rfl
  map_add' x y := by
    apply Subtype.ext
    change ((supAut Ω hLD σ ⟨x.1 + y.1, _⟩ : ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F)
      Ω))) : F) = _
    rw [show (⟨x.1 + y.1, (x + y).2⟩ : ↥((AA (k := k) (F₀ := F₀) (F := F)) ⊔ (BB (F := F) Ω)))
        = ⟨x.1, x.2⟩ + ⟨y.1, y.2⟩ from rfl, map_add]
    rfl

theorem

coe_ringAutFΩ_apply

L963 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.coe_ringAutFΩ_apply

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Semilinear
open TensorProduct
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)
variable [Algebra.IsAlgebraic k Ω]

Lean source · statement

theorem coe_ringAutFΩ_apply (σ : Ω ≃ₐ[k] Ω) (x : FΩ (k := k) (F₀ := F₀) (F := F) Ω) :
    ((ringAutFΩ Ω hLD σ x : FΩ (k := k) (F₀ := F₀) (F := F) Ω) : F) = (supAut Ω hLD σ ⟨x.1, x.2⟩ :
      F)

theorem

exists_semilinearAut

L968 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.exists_semilinearAut

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Semilinear
open TensorProduct
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K)
variable (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)
variable [Algebra.IsAlgebraic k Ω]
include hLD in

Lean source · statement

theorem exists_semilinearAut (σ : Ω ≃ₐ[k] Ω) :
    ∃ g : SemilinearAut Ω (FΩ (k := k) (F₀ := F₀) (F := F) Ω),
      (∀ a : Ω, SemilinearAut.baseAut g a = σ a) ∧
        ∀ y : F₀, g • algebraMap F₀ (FΩ (k := k) (F₀ := F₀) (F := F) Ω) y
          = algebraMap F₀ (FΩ (k := k) (F₀ := F₀) (F := F) Ω) y

def

ψ

L996 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.ψ

Documentation

The algebra map from the base function field into the compositum.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Curve
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K) [Algebra.IsAlgebraic k Ω]
variable (F) in

Lean source · statement

def ψ : F₀ →ₐ[k] FΩ (k := k) (F₀ := F₀) (F := F) Ω

theorem

ψ_apply

L998 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.ψ_apply

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Curve
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K) [Algebra.IsAlgebraic k Ω]
variable (F) in

Lean source · statement

theorem ψ_apply (y : F₀) : ψ F Ω y = algebraMap F₀ (FΩ (k := k) (F₀ := F₀) (F := F)
  Ω) y

theorem

isIntegral_adjoin_ψ

L1001 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.isIntegral_adjoin_ψ

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Curve
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K) [Algebra.IsAlgebraic k Ω]
variable (F) in

Lean source · statement

theorem isIntegral_adjoin_ψ {t y : F₀}
    (hy : IsIntegral (IntermediateField.adjoin k ({t} : Set F₀)) y) :
    IsIntegral (IntermediateField.adjoin Ω ({ψ F Ω t} : Set (FΩ (k := k) (F₀ := F₀) (F := F) Ω)))
      (ψ F Ω y)

theorem

mem_range_of_isAlgebraic

L1056 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.mem_range_of_isAlgebraic

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Curve
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K) [Algebra.IsAlgebraic k Ω]
variable (F) in
variable (φ : F →ₐ[K] F) [Finite k]
  (hφ : ∀ x : F₀, φ (algebraMap F₀ F x) = algebraMap F₀ F (x ^ Nat.card k))
include hφ in
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] [Algebra.IsAlgebraic
  k Ω] in

Lean source · statement

theorem mem_range_of_isAlgebraic [IsAlgClosed K] {t : F₀}
    (ht : IsAlgebraic K (algebraMap F₀ F t)) : t ∈ Set.range (algebraMap k F₀)

theorem

transcendental_ψ

L1069 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.transcendental_ψ

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Curve
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K) [Algebra.IsAlgebraic k Ω]
variable (F) in
variable (φ : F →ₐ[K] F) [Finite k]
  (hφ : ∀ x : F₀, φ (algebraMap F₀ F x) = algebraMap F₀ F (x ^ Nat.card k))
include hφ in

Lean source · statement

theorem transcendental_ψ [IsAlgClosed K] {t : F₀} (ht : Transcendental k t) :
    Transcendental Ω (ψ F Ω t : FΩ (k := k) (F₀ := F₀) (F := F) Ω)

theorem

adjoin_image_ψ_eq_top

L1082 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.adjoin_image_ψ_eq_top

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Curve
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K) [Algebra.IsAlgebraic k Ω]
variable (F) in
variable (φ : F →ₐ[K] F) [Finite k]
  (hφ : ∀ x : F₀, φ (algebraMap F₀ F x) = algebraMap F₀ F (x ^ Nat.card k))
omit [Finite k] in

Lean source · statement

theorem adjoin_image_ψ_eq_top {s : Set F₀}
    (hs : IntermediateField.adjoin k s = ⊤) :
    IntermediateField.adjoin Ω (ψ F Ω '' s : Set (FΩ (k := k) (F₀ := F₀) (F := F) Ω)) = ⊤

theorem

finiteDimensional_adjoin_ψ

L1127 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed.AlgebraicCurve.GenusFinToAlgClosedG.finiteDimensional_adjoin_ψ

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenusFinToAlgClosedG
open _root_.AlgebraicCurve
section Curve
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  (Ω : IntermediateField k K) [Algebra.IsAlgebraic k Ω]
variable (F) in
variable (φ : F →ₐ[K] F) [Finite k]
  (hφ : ∀ x : F₀, φ (algebraMap F₀ F x) = algebraMap F₀ F (x ^ Nat.card k))
omit [Finite k] in

Lean source · statement

theorem finiteDimensional_adjoin_ψ {t : F₀}
    (hfd : FiniteDimensional (IntermediateField.adjoin k ({t} : Set F₀)) F₀)
    (hfg : ∃ s : Finset F₀, IntermediateField.adjoin k (s : Set F₀) = ⊤) :
    FiniteDimensional (IntermediateField.adjoin Ω ({ψ F Ω t} : Set (FΩ (k := k) (F₀ := F₀) (F :=
      F) Ω)))
      (FΩ (k := k) (F₀ := F₀) (F := F) Ω)

theorem

genusFF_eq_of_constantFieldExtension_of_finite_of_isAlgClosed

L1162 ↗

AlgebraicCurve.genusFF_eq_of_constantFieldExtension_of_finite_of_isAlgClosed

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
  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 _root_.AlgebraicCurve AlgebraicCurve AlgebraicCurve.GenusFinToAlgClosedG in

Lean source · statement

theorem _root_.AlgebraicCurve.genusFF_eq_of_constantFieldExtension_of_finite_of_isAlgClosed
    (k K F₀ F : Type*) [Field k] [Finite k] [Field K] [IsAlgClosed K] [Field F₀] [Field F]
    [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
    [AlgebraicCurve.IsCurveOver k F₀] [AlgebraicCurve.IsCurveOver K F]
    (hfg : ∃ s : Finset F₀, IntermediateField.adjoin k (s : Set F₀) = ⊤)
    (hgen : IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤)
    (φ : F →ₐ[K] F)
    (hφ : ∀ x : F₀, φ (algebraMap F₀ F x) = algebraMap F₀ F (x ^ Nat.card k))
    (hC : AlgebraicCurve.ConstantsAreBase k F₀) :
    AlgebraicCurve.genusFF K F = AlgebraicCurve.genusFF k F₀

Module documentation

Genus FF eq of constant Field Extension of finite of is Alg Closed

Declarations