Module

GeometricGenusBaseChange.lean

Nyll.AlgebraicCurves.Geometry.Curves.GeometricGenusBaseChange

2 declarations indexed from sourceView source ↗

Module documentation

Geometric genus after a finite field extension

A finite extension embeds in an algebraic closure of the original field. Actual Cech cohomology and the function-field isomorphism of the two iterated pullbacks then compare the genera. The auxiliary rational point is only used to construct a two-affine cover of the extended curve.

Imports7

Nyll.AlgebraicCurves.Geometry.Curves.GeometricGenus
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_exists_twoAffineOpenCover_of_section
Nyll.AlgebraicCurves.Geometry.Nonempty_algEquiv_functionField_of_iso
Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_eq_of_algEquiv
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Mathlib.Algebra.Algebra.Tower

Imported by2

theorem

finrank_H1_eq_genusFF_baseChange

L35 ↗

AlgebraicGeometry.SmoothProperCurve.finrank_H1_eq_genusFF_baseChange

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
open NeronModelInfra
open scoped TensorProduct
namespace AlgebraicGeometry.SmoothProperCurve

Lean source · full declaration

theorem finrank_H1_eq_genusFF_baseChange
    (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (𝒱 : C.TwoAffineOpenCover) (Ω : Type u) [Field Ω] [Algebra K Ω] [IsAlgClosed Ω] :
    let := (AlgebraicCurve.baseToFunctionField (baseChange K c Ω)).toAlgebra
    Module.finrank K (𝒱.structureSheafSections c).H1 =
      AlgebraicCurve.genusFF Ω (pullback c (specMap K Ω)).functionField := by
  intro a
  let d := (𝒱.structureSheafSections c).cechDiff
  have hex : Function.Exact d (LinearMap.range d).mkQ :=
    LinearMap.exact_map_mkQ_range d
  have hsurj : Function.Surjective (LinearMap.range d).mkQ :=
    Submodule.mkQ_surjective (LinearMap.range d)
  have hexΩ : Function.Exact (d.baseChange Ω)
      ((LinearMap.range d).mkQ.baseChange Ω) := by
    have ht := lTensor_exact Ω hex hsurj
    rwa [← LinearMap.baseChange_eq_ltensor, ← LinearMap.baseChange_eq_ltensor] at ht
  let e := hexΩ.linearEquivOfSurjective (LinearMap.baseChange_surjective Ω hsurj)
  calc
    Module.finrank K (𝒱.structureSheafSections c).H1 =
        Module.finrank Ω (Ω ⊗[K] (𝒱.structureSheafSections c).H1) :=
      Module.finrank_baseChange.symm
    _ = Module.finrank Ω ((Ω ⊗[K] (𝒱.cover c).A01) ⧸
        LinearMap.range (d.baseChange Ω)) := e.finrank_eq.symm
    _ = AlgebraicCurve.genusFF Ω (pullback c (specMap K Ω)).functionField :=
      (𝒱.finrank_cechDiff_baseChange_of_isAlgClosed c Ω).2.2

theorem

geometricGenus_baseChange_of_finite_of_section

L64 ↗

AlgebraicGeometry.SmoothProperCurve.geometricGenus_baseChange_of_finite_of_section

Documentation

A finite extension with a point does not change the point-independent genus. No separability assumption is needed.