Module

DivisorClassCohomologyInjection.lean

Nyll.JacobianVarieties.Kummer.DivisorClassCohomologyInjection

7 declarations indexed from sourceView source ↗

Module documentation

Torsion divisor classes inject into actual etale H¹

The actual Kummer character is multiplicative and has exactly the subgroup of powers as its kernel. It therefore descends injectively through the proved divisorial Kummer quotient. The proved finite H¹ comparison then supplies an injective additive map to actual derived etale cohomology. Surjectivity is not asserted here.

Imports6

Imported by2

theorem

kummerMonodromyHom_ker

L40 ↗

AlgebraicCurve.CurveModel.kummerMonodromyHom_ker

Documentation

The actual Kummer-character kernel consists precisely of actual powers of functions, as detected by splitting of the original cover.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsAlgClosed K]
  {F : Type v} [Field F] [Algebra K F] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  (M : CurveModel K F) (n : ℕ+) (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ M.C)

Lean source · full declaration

theorem kummerMonodromyHom_ker :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    let : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
    (M.kummerMonodromyHom n hn xi).ker = Pic0.kummerPowers K F n := by
  let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
  have : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
  rw [← Pic0.kummerClass_ker]
  apply Subgroup.ext
  intro u
  change M.kummerMonodromyCharacter n u hn xi = 1 ↔ Pic0.kummerClass n u = 1
  exact (M.kummerMonodromyCharacter_eq_one_iff_exists_section n u hn xi).trans
    (M.kummerClass_eq_one_iff_exists_section n hn u).symm

def

kummerTorsionCharacter

L55 ↗

AlgebraicCurve.CurveModel.kummerTorsionCharacter

Documentation

The actual torsion divisor class determines a continuous character of the actual fundamental group, via its proved Kummer representative quotient.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsAlgClosed K]
  {F : Type v} [Field F] [Algebra K F] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  (M : CurveModel K F) (n : ℕ+) (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ M.C)

Lean source · full declaration

def kummerTorsionCharacter :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    let : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
    Multiplicative (Pic0.torsion K F n) →*
      (Aut (FiniteEtale.fiber xi) →ₜ* rootsOfUnity (n : ℕ) K) := by
  let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
  have : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
  exact (QuotientGroup.lift (Pic0.kummerPowers K F n) (M.kummerMonodromyHom n hn xi)
    (M.kummerMonodromyHom_ker n hn xi).ge).comp
      (Pic0.kummerDivisorEquiv K F n).symm.toMonoidHom

theorem

kummerTorsionCharacter_injective

L67 ↗

AlgebraicCurve.CurveModel.kummerTorsionCharacter_injective

Documentation

No nonzero actual torsion divisor class has trivial Kummer monodromy.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsAlgClosed K]
  {F : Type v} [Field F] [Algebra K F] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  (M : CurveModel K F) (n : ℕ+) (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ M.C)

Lean source · full declaration

theorem kummerTorsionCharacter_injective :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    let : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
    Function.Injective (M.kummerTorsionCharacter n hn xi) := by
  let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
  have : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
  exact ((QuotientGroup.injective_lift_iff (Pic0.kummerPowers K F n)
    (M.kummerMonodromyHom n hn xi) (M.kummerMonodromyHom_ker n hn xi).ge).mpr
      (M.kummerMonodromyHom_ker n hn xi).symm).comp
        (Pic0.kummerDivisorEquiv K F n).symm.injective

theorem

kummerTorsionCharacter_kummerClass

L80 ↗

AlgebraicCurve.CurveModel.kummerTorsionCharacter_kummerClass

Documentation

Evaluation on an actual represented divisor class is the character of the original normalized Kummer cover for that function.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsAlgClosed K]
  {F : Type v} [Field F] [Algebra K F] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  (M : CurveModel K F) (n : ℕ+) (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ M.C)

Lean source · full declaration

theorem kummerTorsionCharacter_kummerClass (u : Pic0.kummerUnits K F n) :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    let : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
    M.kummerTorsionCharacter n hn xi (Pic0.kummerClass n u) =
      M.kummerMonodromyCharacter n u hn xi := by
  let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
  have : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
  rw [← Pic0.kummerDivisorEquiv_mk]
  change QuotientGroup.lift (Pic0.kummerPowers K F n) (M.kummerMonodromyHom n hn xi)
    (M.kummerMonodromyHom_ker n hn xi).ge
      ((Pic0.kummerDivisorEquiv K F n).symm
        ((Pic0.kummerDivisorEquiv K F n) (QuotientGroup.mk u))) = _
  rw [MulEquiv.symm_apply_apply, QuotientGroup.lift_mk']
  rfl

def

kummerTorsionCohomology

L99 ↗

AlgebraicCurve.CurveModel.kummerTorsionCohomology

Documentation

Actual torsion divisor classes map to the actual derived etale H¹ with constant roots-of-unity coefficients.

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsAlgClosed K]
  {F : Type v} [Field F] [Algebra K F] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  (M : CurveModel K F) (n : ℕ+) (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ M.C)
include xi

Lean source · statement

def kummerTorsionCohomology :
    Pic0.torsion K F n →+
      Sheaf.H.{u} ((constantSheaf M.C.smallEtaleTopology AddCommGrpCat.{u}).obj
        (AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K)))) 1

theorem

kummerTorsionCohomology_injective

L116 ↗

AlgebraicCurve.CurveModel.kummerTorsionCohomology_injective

Documentation

The map from actual torsion divisor classes to genuine etale H¹ is injective.

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsAlgClosed K]
  {F : Type v} [Field F] [Algebra K F] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  (M : CurveModel K F) (n : ℕ+) (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ M.C)
include xi

Lean source · statement

theorem kummerTorsionCohomology_injective :
    Function.Injective (M.kummerTorsionCohomology n hn xi)

theorem

kummerTorsionCohomology_kummerClass

L130 ↗

AlgebraicCurve.CurveModel.kummerTorsionCohomology_kummerClass

Documentation

The descended H¹ map retains the actual Kummer covering class on every represented 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
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] [IsAlgClosed K]
  {F : Type v} [Field F] [Algebra K F] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  (M : CurveModel K F) (n : ℕ+) (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ M.C)
include xi

Lean source · statement

theorem kummerTorsionCohomology_kummerClass (u : Pic0.kummerUnits K F n) :
    M.kummerTorsionCohomology n hn xi (Multiplicative.toAdd (Pic0.kummerClass n u)) =
      M.kummerEtaleClass n u hn xi

Module documentation

Torsion divisor classes inject into actual etale H¹

Declarations

kummerMonodromyHom_ker

kummerTorsionCharacter

kummerTorsionCharacter_injective

kummerTorsionCharacter_kummerClass

kummerTorsionCohomology

kummerTorsionCohomology_injective

kummerTorsionCohomology_kummerClass