Module

OpenDivisorCohomologyInjection.lean

Nyll.JacobianVarieties.Kummer.OpenDivisorCohomologyInjection

7 declarations indexed from sourceView source ↗

Module documentation

Actual open divisorial Kummer classes inject into derived H¹

The constructed cover supplies the map; multiplication is checked on actual generic roots, and its kernel is exactly the actual subgroup of powers. Surjectivity requires the converse interior valuation calculation.

Imports3

Nyll.JacobianVarieties.Kummer.OpenCurveCoverCharacterProduct
Nyll.JacobianVarieties.Kummer.OpenCurveCoverSplitting
Mathlib.GroupTheory.QuotientGroup.Defs

Imported by2

theorem

kummerMonodromyHom_ker

L38 ↗

AlgebraicCurve.CurveModel.OpenKummer.kummerMonodromyHom_ker

Documentation

The actual character kernel is exactly the subgroup of actual powers.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology TopologicalSpace
namespace AlgebraicCurve.CurveModel.OpenKummer
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
  {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hinterior : ∀ (y : X) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · full declaration

theorem kummerMonodromyHom_ker :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    let : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
    (kummerMonodromyHom M S n j hj hinterior hn xi).ker =
      Pic0.openKummerPowers K F S n := by
  let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
  have : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
  apply Subgroup.ext
  intro w
  change kummerMonodromyCharacter M S n w j hj hinterior hn xi = 1 ↔
    w ∈ Pic0.openKummerPowers K F S n
  exact (kummerMonodromyCharacter_eq_one_iff_exists_section
    M S n w j hj hinterior hn xi).trans
      (mem_openKummerPowers_iff_exists_section M S n w j hj hinterior hn).symm

def

quotientCharacter

L54 ↗

AlgebraicCurve.CurveModel.OpenKummer.quotientCharacter

Documentation

Actual functions modulo actual powers determine actual characters.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology TopologicalSpace
namespace AlgebraicCurve.CurveModel.OpenKummer
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
  {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hinterior : ∀ (y : X) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · full declaration

def quotientCharacter :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    let : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
    (Pic0.openKummerUnits K F S n ⧸ Pic0.openKummerPowers K F S n) →*
      (Aut (FiniteEtale.fiber xi) →ₜ* rootsOfUnity (n : ℕ) K) := by
  let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
  have : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
  exact QuotientGroup.lift (Pic0.openKummerPowers K F S n)
    (kummerMonodromyHom M S n j hj hinterior hn xi)
    (kummerMonodromyHom_ker M S n j hj hinterior hn xi).ge

theorem

quotientCharacter_injective

L66 ↗

AlgebraicCurve.CurveModel.OpenKummer.quotientCharacter_injective

Documentation

Distinct open divisorial Kummer classes have distinct actual characters.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology TopologicalSpace
namespace AlgebraicCurve.CurveModel.OpenKummer
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
  {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hinterior : ∀ (y : X) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · full declaration

theorem quotientCharacter_injective :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    let : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
    Function.Injective (quotientCharacter M S n j hj hinterior hn xi) := by
  let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
  have : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
  exact (QuotientGroup.injective_lift_iff (Pic0.openKummerPowers K F S n)
    (kummerMonodromyHom M S n j hj hinterior hn xi)
    (kummerMonodromyHom_ker M S n j hj hinterior hn xi).ge).mpr
      (kummerMonodromyHom_ker M S n j hj hinterior hn xi).symm

theorem

quotientCharacter_mk

L78 ↗

AlgebraicCurve.CurveModel.OpenKummer.quotientCharacter_mk

Documentation

The quotient character is the character of its original normalized 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 TopologicalSpace
namespace AlgebraicCurve.CurveModel.OpenKummer
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
  {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hinterior : ∀ (y : X) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · full declaration

theorem quotientCharacter_mk (w : Pic0.openKummerUnits K F S n) :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    let : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
    quotientCharacter M S n j hj hinterior hn xi (QuotientGroup.mk w) =
      kummerMonodromyCharacter M S n w j hj hinterior hn xi := rfl

def

quotientCohomology

L85 ↗

AlgebraicCurve.CurveModel.OpenKummer.quotientCohomology

Documentation

The actual quotient maps additively to genuine derived étale H¹.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology TopologicalSpace
namespace AlgebraicCurve.CurveModel.OpenKummer
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
  {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hinterior : ∀ (y : X) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · statement

def quotientCohomology :
    Additive (Pic0.openKummerUnits K F S n ⧸ Pic0.openKummerPowers K F S n) →+
      Sheaf.H.{u} ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
        (AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K)))) 1

theorem

quotientCohomology_injective

L100 ↗

AlgebraicCurve.CurveModel.OpenKummer.quotientCohomology_injective

Documentation

No nonzero actual open divisorial Kummer class maps to zero in derived H¹.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology TopologicalSpace
namespace AlgebraicCurve.CurveModel.OpenKummer
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
  {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hinterior : ∀ (y : X) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · statement

theorem quotientCohomology_injective :
    Function.Injective (quotientCohomology M S n j hj hinterior hn xi)

theorem

quotientCohomology_mk

L113 ↗

AlgebraicCurve.CurveModel.OpenKummer.quotientCohomology_mk

Documentation

The additive map retains the genuine class 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 TopologicalSpace
namespace AlgebraicCurve.CurveModel.OpenKummer
variable {K : Type u} [Field K] [IsSepClosed K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
  {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hinterior : ∀ (y : X) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · statement

theorem quotientCohomology_mk (w : Pic0.openKummerUnits K F S n) :
    quotientCohomology M S n j hj hinterior hn xi
      (Additive.ofMul (QuotientGroup.mk w)) =
        kummerEtaleClass M S n w j hj hinterior hn xi

Module documentation

Actual open divisorial Kummer classes inject into derived H¹

Declarations

kummerMonodromyHom_ker

quotientCharacter

quotientCharacter_injective

quotientCharacter_mk

quotientCohomology

quotientCohomology_injective

quotientCohomology_mk