Module

GenusFF_eq_of_constantFieldExtension_of_finiteDimensional.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_eq_of_constantFieldExtension_of_finiteDimensional

41 declarations indexed from sourceView source ↗

Module documentation

Genus FF eq of constant Field Extension of finite Dimensional

Imports9

Mathlib.RingTheory.Adjoin.PowerBasis
Mathlib.RingTheory.Polynomial.IsIntegral
Nyll.AlgebraicCurves.FunctionFields.CurveOver
Nyll.AlgebraicCurves.Cohomology.Adelic.Index
Nyll.AlgebraicCurves.Divisors.ConstantExtension
Nyll.AlgebraicCurves.Places.OverDVR
Nyll.AlgebraicCurves.Places.Rational.Basic
Nyll.AlgebraicCurves.Places.Place_exists_forall_ord_eq
Mathlib.Data.Fintype.EquivFin

Imported by2

theorem

minpoly_algebraMap_eq_map

L41 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.minpoly_algebraMap_eq_map

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']

Lean source · statement

theorem minpoly_algebraMap_eq_map [FiniteDimensional K K']
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range) (θ : K') :
    minpoly F (algebraMap K' F' θ) = (minpoly K θ).map (algebraMap K F)

theorem

adjoin_gen_eq_top

L73 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.adjoin_gen_eq_top

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
omit [FiniteDimensional K K'] [Algebra.IsSeparable K K'] in

Lean source · statement

theorem adjoin_gen_eq_top (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (pb : PowerBasis K K') :
    Algebra.adjoin F {algebraMap K' F' pb.gen} = ⊤

theorem

isIntegral_algebraMap'

L89 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.isIntegral_algebraMap'

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
include K in
omit [Algebra.IsSeparable K K'] in

Lean source · statement

theorem isIntegral_algebraMap' (θ : K') : IsIntegral F (algebraMap K' F' θ)

def

pbF

L93 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.pbF

Documentation

The power basis of the function-field extension induced by a constant-field power basis.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']

Lean source · statement

def pbF (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (pb : PowerBasis K K') : PowerBasis F F'

theorem

pbF_gen

L99 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.pbF_gen

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
omit [Algebra.IsSeparable K K'] in

Lean source · statement

theorem pbF_gen (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (pb : PowerBasis K K') : (pbF hgen pb).gen = algebraMap K' F' pb.gen

theorem

pbF_dim

L104 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.pbF_dim

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
omit [Algebra.IsSeparable K K'] in

Lean source · statement

theorem pbF_dim (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (pb : PowerBasis K K') : (pbF hgen pb).dim = pb.dim

theorem

finiteDimensional'

L111 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.finiteDimensional'

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
include K in

Lean source · statement

theorem finiteDimensional' (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤) :
    FiniteDimensional F F'

theorem

finrank_eq'

L115 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.finrank_eq'

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']

Lean source · statement

theorem finrank_eq' (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range) :
    Module.finrank F F' = Module.finrank K K'

theorem

isSeparable'

L121 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.isSeparable'

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']

Lean source · statement

theorem isSeparable' (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range) :
    Algebra.IsSeparable F F'

def

bF

L140 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.bF

Documentation

The induced function-field basis reindexed by the dimension of the constant-field power basis.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']

Lean source · statement

def bF (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (pb : PowerBasis K K') : Module.Basis (Fin pb.dim) F F'

theorem

bF_apply

L146 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.bF_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
omit [Algebra.IsSeparable K K'] in

Lean source · statement

theorem bF_apply (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (pb : PowerBasis K K') (i : Fin pb.dim) :
    bF hgen hconst pb i = algebraMap K' F' (pb.basis i)

theorem

bF_repr_algebraMap

L154 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.bF_repr_algebraMap

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']
omit [Algebra.IsSeparable K K'] in

Lean source · statement

theorem bF_repr_algebraMap (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (pb : PowerBasis K K') (k : K') (i : Fin pb.dim) :
    (bF hgen hconst pb).repr (algebraMap K' F' k) i = algebraMap K F (pb.basis.repr k i)

theorem

trace_algebraMap'

L167 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.trace_algebraMap'

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']

Lean source · statement

theorem trace_algebraMap' (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range) (k : K') :
    Algebra.trace F F' (algebraMap K' F' k) = algebraMap K F (Algebra.trace K K' k)

theorem

dualBasis_bF_apply

L179 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.dualBasis_bF_apply

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
namespace GenusCFE
section
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']
variable [FiniteDimensional K K'] [Algebra.IsSeparable K K']

Lean source · statement

theorem dualBasis_bF_apply (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (pb : PowerBasis K K') (j : Fin pb.dim) :
    (Algebra.traceForm F F').dualBasis (traceForm_nondegenerate F F') (bF hgen hconst pb) j =
      algebraMap K' F' ((Algebra.traceForm K K').dualBasis (traceForm_nondegenerate K K')
        pb.basis j)

theorem

mem_integralClosureAt_of_forall_mem

L211 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.mem_integralClosureAt_of_forall_mem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
namespace GenusCFE
section
variable {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']

Lean source · statement

theorem mem_integralClosureAt_of_forall_mem (v : Place K F) (x : F')
    (hx : ∀ w : Place K F', w.restrict F = v → x ∈ w.toValuationSubring) :
    x ∈ integralClosure v.toValuationSubring F'

theorem

isScalarTower_valuationSubring

L225 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.isScalarTower_valuationSubring

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
namespace GenusCFE
section
variable {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
omit [FiniteDimensional F F'] [Algebra.IsSeparable F F'] in

Lean source · statement

theorem isScalarTower_valuationSubring (v : Place K F) :
    IsScalarTower K v.toValuationSubring F'

theorem

repr_mem_valuationSubring

L242 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.repr_mem_valuationSubring

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
namespace GenusCFE
section
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']
    [FiniteDimensional K K']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']

Lean source · statement

theorem repr_mem_valuationSubring {ι : Type*} [Finite ι] [DecidableEq ι]
    (b : Module.Basis ι F F') (e : ι → K') (hb : ∀ i, b i = algebraMap K' F' (e i))
    (d : ι → K')
    (hd : ∀ j, (Algebra.traceForm F F').dualBasis (traceForm_nondegenerate F F') b j =
      algebraMap K' F' (d j))
    (hrepr : ∀ (k : K') (i : ι), b.repr (algebraMap K' F' k) i ∈ (algebraMap K F).range)
    (v : Place K F) (x : F')
    (hx : ∀ w : Place K F', w.restrict F = v → x ∈ w.toValuationSubring) (i : ι) :
    b.repr x i ∈ v.toValuationSubring

theorem

finite_setOf_not_le_one_const

L280 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.finite_setOf_not_le_one_const

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finite_setOf_not_le_one_const [HasPrincipalDivisors K F] (f : F) :
    {v : Place K F | ¬ v.adicValuation f ≤ 1}.Finite

theorem

finite_setOf_not_le_one

L290 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.finite_setOf_not_le_one

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finite_setOf_not_le_one [HasPrincipalDivisors K F] {α : Place K F → F}
    (hα : α ∈ repartitions K F) :
    {v : Place K F | ¬ v.adicValuation (α v) ≤ 1}.Finite

theorem

exists_sub_le_one

L311 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.exists_sub_le_one

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_sub_le_one (S : Finset (Place K F)) (a : Place K F → F) :
    ∃ y : F, ∀ w ∈ S, w.adicValuation (y - a w) ≤ 1

theorem

mem_repartitionsOf_zero_iff

L367 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.mem_repartitionsOf_zero_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_repartitionsOf_zero_iff {α : ↥(repartitions K F)} :
    α ∈ repartitionsOf (0 : Divisor K F) ↔
      ∀ v : Place K F, v.adicValuation ((α : Place K F → F) v) ≤ 1

structure

GoodBasis

L374 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis

Documentation

A basis from constant-field elements whose coordinates preserve the stated local integrality.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

structure GoodBasis (K K' F F' : Type*) [Field K] [Field K'] [Field F] [Field F']
    [Algebra K' F'] [Algebra K F] [Algebra F F'] [Algebra K F'] [IsScalarTower K F F']
    [Algebra.IsIntegral F F'] (ι : Type*) where
  /-- The basis of the function-field extension. -/
  basis : Module.Basis ι F F'
  /-- The constant-field elements giving the basis vectors. -/
  elt : ι → K'
  /-- Each basis vector is the image of its chosen constant-field element. -/
  basis_eq : ∀ i, basis i = algebraMap K' F' (elt i)
  /-- Integrality above a place implies integrality of every basis coordinate at that place. -/
  repr_mem : ∀ (v : Place K F) (x : F'),
    (∀ w : Place K F', w.restrict F = v → x ∈ w.toValuationSubring) →
      ∀ i, basis.repr x i ∈ v.toValuationSubring

theorem

mem_restrictConstants_iff

L395 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.mem_restrictConstants_iff

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]

Lean source · statement

theorem mem_restrictConstants_iff (w : Place K' F') (f : F) :
    f ∈ (Place.restrictConstants F (K := K) w).toValuationSubring ↔
      algebraMap F F' f ∈ w.toValuationSubring

theorem

restrictConstants_extendConstants

L400 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.restrictConstants_extendConstants

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]

Lean source · statement

theorem restrictConstants_extendConstants [Algebra.IsIntegral K K'] (w : Place K F') :
    Place.restrictConstants F (K := K) (Place.extendConstants K' w) = w.restrict F

def

psi

L410 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.psi

Documentation

Combine the restricted repartition components using the chosen basis.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)

Lean source · statement

def psi (α : ι → Place K F → F) (w : Place K' F') : F'

theorem

psi_mem

L413 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.psi_mem

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)

Lean source · statement

theorem psi_mem (α : ι → Place K F → F) (w : Place K' F')
    (h : ∀ i, α i (Place.restrictConstants F (K := K) w) ∈
      (Place.restrictConstants F (K := K) w).toValuationSubring) :
    B.psi α w ∈ w.toValuationSubring

theorem

adicValuation_psi_le_one

L420 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.adicValuation_psi_le_one

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)

Lean source · statement

theorem adicValuation_psi_le_one (α : ι → Place K F → F) (w : Place K' F')
    (h : ∀ i, (Place.restrictConstants F (K := K) w).adicValuation
      (α i (Place.restrictConstants F (K := K) w)) ≤ 1) :
    w.adicValuation (B.psi α w) ≤ 1

theorem

sub_repr_mem

L427 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.sub_repr_mem

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)

Lean source · statement

theorem sub_repr_mem [Algebra.IsIntegral K K'] (α : ι → Place K F → F) (β : Place K' F' → F')
    (y : F') (hβ : ∀ w : Place K' F', w.adicValuation (β w) ≤ 1)
    (h : ∀ w, B.psi α w = β w + y) (i : ι) (v : Place K F) :
    α i v - B.basis.repr y i ∈ v.toValuationSubring

theorem

psi_mem_repartitions

L452 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.psi_mem_repartitions

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem psi_mem_repartitions (α : ι → Place K F → F)
    (hα : ∀ i, {v : Place K F | ¬ v.adicValuation (α i v) ≤ 1}.Finite) :
    B.psi α ∈ repartitions K' F'

def

Psi

L467 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.Psi

Documentation

The linear map on repartitions obtained by combining components in the chosen basis.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']

Lean source · full declaration

def Psi : (ι → ↥(repartitions K F)) →ₗ[K] ↥(repartitions K' F') where
  toFun α := ⟨B.psi (fun i => (α i : Place K F → F)),
    B.psi_mem_repartitions _ fun i => finite_setOf_not_le_one (α i).2⟩
  map_add' α β := by
    ext w
    simp only [psi, Pi.add_apply, Subalgebra.coe_add, map_add, add_mul,
      Finset.sum_add_distrib]
  map_smul' c α := by
    ext w
    simp only [psi, Pi.smul_apply, Subalgebra.coe_smul, RingHom.id_apply]
    simp only [Algebra.smul_def, map_mul, Finset.mul_sum, ← IsScalarTower.algebraMap_apply K F F',
      mul_assoc]

theorem

coe_Psi

L480 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.coe_Psi

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']

Lean source · full declaration

theorem coe_Psi (α : ι → ↥(repartitions K F)) :
    ((B.Psi α : ↥(repartitions K' F')) : Place K' F' → F') =
      B.psi fun i => (α i : Place K F → F) :=
  rfl

theorem

Psi_mem_iff

L485 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.Psi_mem_iff

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']

Lean source · statement

theorem Psi_mem_iff [Algebra.IsIntegral K K'] (α : ι → ↥(repartitions K F)) :
    B.Psi α ∈ repartitionsOf (0 : Divisor K' F') ⊔ principalRepartitions K' F' ↔
      ∀ i, α i ∈ repartitionsOf (0 : Divisor K F) ⊔ principalRepartitions K F

theorem

exists_sub_Psi_mem

L520 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.exists_sub_Psi_mem

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']

Lean source · statement

theorem exists_sub_Psi_mem (α' : ↥(repartitions K' F')) :
    ∃ α : ι → ↥(repartitions K F), α' - B.Psi α ∈ repartitionsOf (0 : Divisor K' F')

def

Phi

L555 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.Phi

Documentation

The cohomology class of the repartition obtained from the chosen basis.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']

Lean source · statement

def Phi : (ι → ↥(repartitions K F)) →ₗ[K] H1 (0 : Divisor K' F')

theorem

Phi_apply

L559 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.Phi_apply

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']

Lean source · statement

theorem Phi_apply (α : ι → ↥(repartitions K F)) :
    B.Phi α = Submodule.Quotient.mk (B.Psi α)

theorem

Phi_surjective

L562 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.Phi_surjective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']

Lean source · statement

theorem Phi_surjective : Function.Surjective B.Phi

theorem

ker_Phi

L572 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.ker_Phi

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']
variable [Algebra.IsIntegral K K']

Lean source · full declaration

theorem ker_Phi : LinearMap.ker B.Phi = Submodule.pi Set.univ
    fun _ : ι => repartitionsOf (0 : Divisor K F) ⊔ principalRepartitions K F := by
  ext α
  rw [LinearMap.mem_ker, Submodule.mem_pi, Phi_apply, Submodule.Quotient.mk_eq_zero, Psi_mem_iff]
  simp

def

H1Equiv

L582 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.H1Equiv

Documentation

Identify cohomology after constant-field extension with a family of base-field cohomology classes.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']
variable [Algebra.IsIntegral K K']

Lean source · statement

def H1Equiv [DecidableEq ι] :
    H1 (0 : Divisor K' F') ≃ₗ[K] (ι → H1 (0 : Divisor K F))

theorem

finrank_H1_eq

L588 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.finrank_H1_eq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']
variable [Algebra.IsIntegral K K']
include B in

Lean source · statement

theorem finrank_H1_eq :
    Module.finrank K (H1 (0 : Divisor K' F')) =
      Fintype.card ι * Module.finrank K (H1 (0 : Divisor K F))

theorem

genusFF_eq

L598 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim.GenusCFE.GoodBasis.genusFF_eq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
namespace GenusCFE
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Compare
variable {K' F' : Type*} [Field K'] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
    {ι : Type*} [Fintype ι]
namespace GoodBasis
variable (B : GoodBasis K K' F F' ι)
variable [HasPrincipalDivisors K F] [HasPrincipalDivisors K' F']
variable [Algebra.IsIntegral K K']
include B in

Lean source · statement

theorem genusFF_eq [FiniteDimensional K K']
    (hcard : Fintype.card ι = Module.finrank K K') :
    genusFF K' F' = genusFF K F

theorem

genusFF_eq_of_constantFieldExtension_of_finiteDimensional

L613 ↗

AlgebraicCurve.genusFF_eq_of_constantFieldExtension_of_finiteDimensional

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFFConstantsFiniteDim
open Polynomial
open AlgebraicCurve IsDedekindDomain
open AlgebraicCurve WithZero
open AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.genusFF_eq_of_constantFieldExtension_of_finiteDimensional
    {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']
    [FiniteDimensional K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
    [AlgebraicCurve.IsCurveOver K F] [Algebra.EssFiniteType K F]
    [AlgebraicCurve.IsCurveOver K' F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range) :
    AlgebraicCurve.genusFF K' F' = AlgebraicCurve.genusFF K F

Module documentation

Genus FF eq of constant Field Extension of finite Dimensional

Declarations