Module

OpenCurveResidues.lean

Nyll.AnabelianGeometry.WeightFiltration.OpenCurveResidues

10 declarations indexed from sourceView source ↗

Module documentation

The residue sequence on actual open-curve cohomology

The residue map is defined on genuine derived étale H¹ through the proved comparison with actual Kummer covers. Its kernel is the proper divisorial Kummer quotient, and its image is the sum-zero boundary module. The comparison of the first map with geometric pullback, inverse-limit exactness, and arithmetic equivariance are separate steps.

Imports3

Imported by2

abbrev

FiniteKummerH1

L29 ↗

AnabelianGeometry.WeightFiltration.FiniteKummerH1

Documentation

Actual finite-coefficient derived cohomology with constant roots of unity.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve
open scoped BigOperators
namespace AnabelianGeometry.WeightFiltration

Lean source · statement

abbrev FiniteKummerH1 (K : Type) [Field K] (X : Scheme) (n : ℕ+)

def

finiteResidue

L41 ↗

AnabelianGeometry.WeightFiltration.finiteResidue

Documentation

Boundary residues of an actual étale cohomology class.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve
open scoped BigOperators
namespace AnabelianGeometry.WeightFiltration
variable {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · statement

def finiteResidue :
    FiniteKummerH1 K X n →+ (M.openBoundaryPlaces j → ZMod (n : ℕ))

def

properKummerToFiniteH1

L47 ↗

AnabelianGeometry.WeightFiltration.properKummerToFiniteH1

Documentation

Proper divisorial Kummer classes, regarded as actual classes on the open curve.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve
open scoped BigOperators
namespace AnabelianGeometry.WeightFiltration
variable {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · statement

def properKummerToFiniteH1 :
    Additive (Pic0.kummerUnits K F n ⧸ Pic0.kummerPowers K F n) →+
      FiniteKummerH1 K X n

theorem

finiteResidue_comparison

L54 ↗

AnabelianGeometry.WeightFiltration.finiteResidue_comparison

Documentation

The residue map retains the valuation formula of the actual cover.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve
open scoped BigOperators
namespace AnabelianGeometry.WeightFiltration
variable {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · statement

theorem finiteResidue_comparison
    (q : Additive (Pic0.openKummerUnits K F (M.openBoundaryPlaces j) n ⧸
      Pic0.openKummerPowers K F (M.openBoundaryPlaces j) n)) :
    finiteResidue M n j hj hn xi
      (CurveModel.OpenKummer.quotientCohomologyEquiv M n j hj hn xi q) =
        Multiplicative.toAdd
          (Pic0.openKummerResidueQuotient (M.openBoundaryPlaces j) n q.toMul)

theorem

properKummerToFiniteH1_injective

L68 ↗

AnabelianGeometry.WeightFiltration.properKummerToFiniteH1_injective

Documentation

The proper Kummer term embeds into actual open-curve H¹.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve
open scoped BigOperators
namespace AnabelianGeometry.WeightFiltration
variable {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · statement

theorem properKummerToFiniteH1_injective :
    Function.Injective (properKummerToFiniteH1 M n j hj hn xi)

theorem

finiteResidue_eq_zero_iff

L74 ↗

AnabelianGeometry.WeightFiltration.finiteResidue_eq_zero_iff

Documentation

Exactness at actual open-curve H¹, not at an assumed cohomology model.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve
open scoped BigOperators
namespace AnabelianGeometry.WeightFiltration
variable {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · statement

theorem finiteResidue_eq_zero_iff (x : FiniteKummerH1 K X n) :
    finiteResidue M n j hj hn xi x = 0 ↔
      ∃ q, properKummerToFiniteH1 M n j hj hn xi q = x

theorem

properKummerToFiniteH1_range

L102 ↗

AnabelianGeometry.WeightFiltration.properKummerToFiniteH1_range

Documentation

The image of the proper term is exactly the residue kernel.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve
open scoped BigOperators
namespace AnabelianGeometry.WeightFiltration
variable {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · statement

theorem properKummerToFiniteH1_range :
    (@AddMonoidHom.range
      (Additive (Pic0.kummerUnits K F n ⧸ Pic0.kummerPowers K F n)) inferInstance
      (FiniteKummerH1 K X n) inferInstance (properKummerToFiniteH1 M n j hj hn xi)) =
      (finiteResidue M n j hj hn xi).ker

theorem

sum_finiteResidue_eq_zero

L113 ↗

AnabelianGeometry.WeightFiltration.sum_finiteResidue_eq_zero

Documentation

Residues of every actual open-curve H¹ class satisfy the sum relation.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve
open scoped BigOperators
namespace AnabelianGeometry.WeightFiltration
variable {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)
variable [IsCurveOver K F] [Fintype (M.openBoundaryPlaces j)]

Lean source · statement

theorem sum_finiteResidue_eq_zero (x : FiniteKummerH1 K X n) :
    ∑ v, finiteResidue M n j hj hn xi x v = 0

theorem

exists_finiteH1_of_sum_eq_zero

L124 ↗

AnabelianGeometry.WeightFiltration.exists_finiteH1_of_sum_eq_zero

Documentation

Every sum-zero boundary vector is the residue of an actual class. A boundary point is needed here; the empty-boundary sequence is different.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve
open scoped BigOperators
namespace AnabelianGeometry.WeightFiltration
variable {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)
variable [IsCurveOver K F] [Fintype (M.openBoundaryPlaces j)]

Lean source · statement

theorem exists_finiteH1_of_sum_eq_zero
    (ε : NeronModelInfra.SchemeHomOver (𝟙 (Spec (.of K))) M.toBase)
    (v₀ : M.openBoundaryPlaces j)
    (a : M.openBoundaryPlaces j → ZMod (n : ℕ)) (ha : ∑ v, a v = 0) :
    ∃ x : FiniteKummerH1 K X n, finiteResidue M n j hj hn xi x = a

theorem

finiteResidue_range

L137 ↗

AnabelianGeometry.WeightFiltration.finiteResidue_range

Documentation

Exactness at the boundary term of the actual finite-coefficient sequence.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve
open scoped BigOperators
namespace AnabelianGeometry.WeightFiltration
variable {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)
variable [IsCurveOver K F] [Fintype (M.openBoundaryPlaces j)]

Lean source · statement

theorem finiteResidue_range
    (ε : NeronModelInfra.SchemeHomOver (𝟙 (Spec (.of K))) M.toBase)
    (v₀ : M.openBoundaryPlaces j) :
    (finiteResidue M n j hj hn xi).range =
      JacobianVarieties.Kummer.boundaryResidueGroup (M.openBoundaryPlaces j) n

Module documentation

The residue sequence on actual open-curve cohomology

Declarations