Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_TwoAffineOpenCover_finrank_cechDiff_baseChange_of_isAlgClosed

theorem

finrank_cechDiff_baseChange_of_isAlgClosed

AlgebraicGeometry.Scheme.TwoAffineOpenCover.finrank_cechDiff_baseChange_of_isAlgClosed

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_finrank_cechDiff_baseChange_of_isAlgClosed
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
  AlgebraicCurve.Place.instIsLocalHomRestrictInclusion AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint AlgebraicCurve.Divisor.mapRestrict_single
  AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
  AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
  AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
  AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
  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.placeInfty_toValuationSubring
  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.Place.differentialCoeff_zero AlgebraicCurve.Place.differentialCoeff_dCoord
  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
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
open Scheme_TwoAffineOpenCover_finrank_cechDiff_baseChange_of_isAlgClosed in
with_weak_namespace _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover

Lean source · full declaration

theorem finrank_cechDiff_baseChange_of_isAlgClosed
    {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (CommRingCat.of R)) (K : Type u) [Field K] [IsAlgClosed K] [Algebra R K]
    [IsIntegral (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K))]
    [IsProper (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))]
    [SmoothOfRelativeDimension 1 (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))] :
    letI := (AlgebraicCurve.baseToFunctionField
      (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))).toAlgebra
    Module.Finite K (LinearMap.ker ((𝒱.structureSheafSections c).cechDiff.baseChange K)) ∧
      Module.finrank K (LinearMap.ker ((𝒱.structureSheafSections c).cechDiff.baseChange K)) = 1 ∧
      Module.finrank K ((K ⊗[R] (𝒱.cover c).A01) ⧸
          LinearMap.range ((𝒱.structureSheafSections c).cechDiff.baseChange K)) =
        AlgebraicCurve.genusFF K (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R
          K)).functionField := by
  obtain ⟨e0, e1, e01, eH0, eH1, -⟩ :=
    Scheme.TwoAffineOpenCover.exists_baseChangeIsos_structureSheaf 𝒱 c K
  obtain ⟨hf0, hf1, h0, h1⟩ := AlgebraicCurve.finite_H0_H1_structureSheaf_of_isAlgClosed
    (𝒱.pullback c K) (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))
  refine ⟨?_, ?_, ?_⟩
  · exact Module.Finite.equiv eH0.symm
  · rw [eH0.finrank_eq]; exact h0
  · rw [eH1.finrank_eq]; exact h1

Scheme_TwoAffineOpenCover_finrank_cechDiff_baseChange_of_isAlgClosed.lean

Module documentation

finrank_cechDiff_baseChange_of_isAlgClosed

Module documentation

Declarations

finrank_cechDiff_baseChange_of_isAlgClosed