NYLL
Module

CurveCoverCharacter.lean

Nyll.JacobianVarieties.Kummer.CurveCoverCharacter
6 declarations indexed from sourceView source ↗

Module documentation

The actual monodromy character and cohomology class of a Kummer cover

The character comes from the proved root-scaling torsor structure on the original finite etale cover. The actual derived H¹ comparison then constructs a degree-one etale cohomology class. Its vanishing is equivalent to splitting of that cover, and hence to vanishing of the actual divided divisor class.

Imports6
Imported by6

Declarations

def

kummerMonodromyCharacter

L41 ↗
AlgebraicCurve.CurveModel.kummerMonodromyCharacter
Documentation

The displacement character of monodromy on the actual normalized Kummer cover, with the discrete topology on its roots of unity.

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ M.C)
Lean source · full declaration
def kummerMonodromyCharacter :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    Aut (FiniteEtale.fiber ξ) →ₜ* rootsOfUnity (n : ℕ) K := by
  let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
  let T := M.kummerGeometricRootTorsor n u hn ξ
  have := M.kummerGeometricRootAction_commutes n u hn ξ
  exact torsorCharacter (G := Aut (FiniteEtale.fiber ξ)) (Classical.choice T.nonempty)
theorem

kummerMonodromyCharacter_eq_torsorCharacter

L50 ↗
AlgebraicCurve.CurveModel.kummerMonodromyCharacter_eq_torsorCharacter
Documentation

Every point of the original fiber computes the same displacement character.

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ M.C)
Lean source · full declaration
theorem kummerMonodromyCharacter_eq_torsorCharacter
    (x : (FiniteEtale.fiber ξ).obj (M.kummerCover n hn u)) :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    let := M.kummerGeometricRootTorsor n u hn ξ
    let := M.kummerGeometricRootAction_commutes n u hn ξ
    M.kummerMonodromyCharacter n u hn ξ = torsorCharacter x := by
  let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
  let T := M.kummerGeometricRootTorsor n u hn ξ
  have := M.kummerGeometricRootAction_commutes n u hn ξ
  exact torsorCharacter_eq (Classical.choice T.nonempty) x
theorem

kummerMonodromyCharacter_eq_one_iff_exists_section

L63 ↗
AlgebraicCurve.CurveModel.kummerMonodromyCharacter_eq_one_iff_exists_section
Documentation

Triviality of the actual Kummer monodromy character is equivalent to a section of the original cover, including when that cover is disconnected.

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ M.C)
Lean source · full declaration
theorem kummerMonodromyCharacter_eq_one_iff_exists_section :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    M.kummerMonodromyCharacter n u hn ξ = 1 ↔
      ∃ s : M.C ⟶ (M.kummerCover n hn u).left,
        s ≫ (M.kummerCover n hn u).hom = 𝟙 M.C := by
  let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
  let T := M.kummerGeometricRootTorsor n u hn ξ
  have := M.kummerGeometricRootAction_commutes n u hn ξ
  rw [FiniteEtale.exists_section_iff_exists_fiber_fixed ξ (M.kummerCover n hn u)]
  constructor
  · intro h
    let x := Classical.choice T.nonempty
    refine ⟨x, ?_⟩
    apply (torsorCharacter_eq_one_iff x).mp
    exact (M.kummerMonodromyCharacter_eq_torsorCharacter n u hn ξ x).symm.trans h
  · rintro ⟨x, hx⟩
    exact (M.kummerMonodromyCharacter_eq_torsorCharacter n u hn ξ x).trans
      ((torsorCharacter_eq_one_iff x).mpr hx)
def

kummerEtaleClass

L84 ↗
AlgebraicCurve.CurveModel.kummerEtaleClass
Documentation

The genuine derived degree-one etale cohomology class of the actual Kummer covering torsor, using the proved finite-coefficient H¹ comparison.

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ M.C)
Lean source · statement
def kummerEtaleClass :
    Sheaf.H.{u} ((constantSheaf M.C.smallEtaleTopology AddCommGrpCat.{u}).obj
      (AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K)))) 1
theorem

kummerEtaleClass_eq_zero_iff_character_eq_one

L97 ↗
AlgebraicCurve.CurveModel.kummerEtaleClass_eq_zero_iff_character_eq_one
Documentation

Vanishing of the actual cohomology class detects the actual Kummer character; the cohomology group here is Sheaf.H, not a divisor-group alias.

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ M.C)
Lean source · full declaration
theorem kummerEtaleClass_eq_zero_iff_character_eq_one :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    M.kummerEtaleClass n u hn ξ = 0 ↔ M.kummerMonodromyCharacter n u hn ξ = 1 := by
  let A := AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K))
  have : NeZero (n : ℕ) := ⟨n.ne_zero⟩
  have : NeZero ((n : ℕ) : K) := ⟨hn.ne_zero⟩
  let : TopologicalSpace (Multiplicative A) := ⊥
  have : DiscreteTopology (Multiplicative A) := ⟨rfl⟩
  change (finiteH1CharacterEquiv A ξ).symm
    (Additive.ofMul (M.kummerMonodromyCharacter n u hn ξ)) = 0 ↔ _
  exact (finiteH1CharacterEquiv A ξ).symm.map_eq_zero_iff
theorem

kummerEtaleClass_eq_zero_iff_kummerClass_eq_one

L111 ↗
AlgebraicCurve.CurveModel.kummerEtaleClass_eq_zero_iff_kummerClass_eq_one
Documentation

Over algebraically closed constants, vanishing of the genuine Kummer H¹ class agrees with vanishing of the actual divided principal-divisor class.

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ M.C)
Lean source · statement
theorem kummerEtaleClass_eq_zero_iff_kummerClass_eq_one [IsAlgClosed K]
    [Algebra.EssFiniteType K F] [IsCurveOver K F] :
    M.kummerEtaleClass n u hn ξ = 0 ↔ Pic0.kummerClass n u = 1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.