Module

Cohomology.lean

Nyll.JacobianVarieties.Autoduality.Cohomology

51 declarations indexed from sourceView source ↗

Module documentation

Picard cohomology and pairing data

Picard groups, degree-zero classes, torsion characters, and transport of supplied perfect pairings.

Imports3

Nyll.AlgebraicCurves.Divisors.ClassGroup
Mathlib.GroupTheory.QuotientGroup.Defs
Mathlib.Algebra.Group.AddChar

Imported by7

theorem

principal_le_degZero

L36 ↗

AlgebraicCurve.Divisor.principal_le_degZero

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Divisor
variable {K F}

Lean source · statement

theorem principal_le_degZero [HasPrincipalDivisors K F] :
    Divisor.principal (K := K) (F := F) ≤ Divisor.degZero (K := K) (F := F)

theorem

degree_eq_zero_of_isPrincipal

L43 ↗

AlgebraicCurve.Divisor.degree_eq_zero_of_isPrincipal

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Divisor
variable {K F}

Lean source · statement

theorem degree_eq_zero_of_isPrincipal [HasPrincipalDivisors K F] {D : Divisor K F}
    (hD : D.IsPrincipal) : Divisor.degree D = 0

abbrev

H1Gm

L50 ↗

AlgebraicCurve.H1Gm

Documentation

The Picard group, used here as the model of first cohomology with coefficients in Gm.

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev H1Gm : Type _

abbrev

mk

L57 ↗

AlgebraicCurve.H1Gm.mk

Documentation

The cohomology class represented by a divisor.

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1Gm
variable {K F}

Lean source · statement

abbrev mk (D : Divisor K F) : H1Gm K F

theorem

mk_surjective

L59 ↗

AlgebraicCurve.H1Gm.mk_surjective

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1Gm
variable {K F}

Lean source · statement

theorem mk_surjective : Function.Surjective (mk (K := K) (F := F))

def

ofPic0

L65 ↗

AlgebraicCurve.H1Gm.ofPic0

Documentation

The homomorphism from degree-zero divisor classes to the full Picard group.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1Gm
variable {K F}
variable (K F)

Lean source · statement

def ofPic0 : Pic0 K F →+ H1Gm K F

theorem

ofPic0_mk

L71 ↗

AlgebraicCurve.H1Gm.ofPic0_mk

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1Gm
variable {K F}
variable (K F)
variable {K F} in

Lean source · statement

theorem ofPic0_mk (D : Divisor.degZero (K := K) (F := F)) :
    ofPic0 K F (Pic0.mk D) = mk (D : Divisor K F)

theorem

ofPic0_injective

L74 ↗

AlgebraicCurve.H1Gm.ofPic0_injective

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1Gm
variable {K F}
variable (K F)
variable {K F} in

Lean source · statement

theorem ofPic0_injective : Function.Injective (ofPic0 K F)

def

degree

L86 ↗

AlgebraicCurve.H1Gm.degree

Documentation

The degree homomorphism on divisor classes.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1Gm
variable {K F}
variable (K F)
variable {K F} in
variable [HasPrincipalDivisors K F]

Lean source · statement

def degree : H1Gm K F →+ ℤ

theorem

degree_mk

L91 ↗

AlgebraicCurve.H1Gm.degree_mk

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1Gm
variable {K F}
variable (K F)
variable {K F} in
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem degree_mk (D : Divisor K F) : degree K F (mk D) = Divisor.degree D

theorem

degree_ofPic0

L94 ↗

AlgebraicCurve.H1Gm.degree_ofPic0

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1Gm
variable {K F}
variable (K F)
variable {K F} in
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem degree_ofPic0 (x : Pic0 K F) : degree K F (ofPic0 K F x) = 0

theorem

exact_ofPic0_degree

L98 ↗

AlgebraicCurve.H1Gm.exact_ofPic0_degree

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1Gm
variable {K F}
variable (K F)
variable {K F} in
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem exact_ofPic0_degree :
    (ofPic0 K F).range = (degree K F).ker

def

ofPic0Equiv

L109 ↗

AlgebraicCurve.H1Gm.ofPic0Equiv

Documentation

Identify the degree-zero Picard group with the kernel of the degree homomorphism.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1Gm
variable {K F}
variable (K F)
variable {K F} in
variable [HasPrincipalDivisors K F]

Lean source · statement

def ofPic0Equiv : Pic0 K F ≃+ (degree K F).ker

abbrev

H1mu

L121 ↗

AlgebraicCurve.H1mu

Documentation

The n-torsion subgroup of the degree-zero Picard group.

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev H1mu (n : ℕ) : Type _

theorem

mem_iff

L127 ↗

AlgebraicCurve.H1mu.mem_iff

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1mu
variable {K F}

Lean source · statement

theorem mem_iff {n : ℕ} {x : Pic0 K F} :
    x ∈ Pic0.torsion K F n ↔ (n : ℤ) • x = 0

theorem

ofPic0_nsmul_eq_zero_iff

L133 ↗

AlgebraicCurve.H1mu.ofPic0_nsmul_eq_zero_iff

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace H1mu
variable {K F}
variable (K F)

Lean source · statement

theorem ofPic0_nsmul_eq_zero_iff {n : ℕ} (x : Pic0 K F) :
    (n : ℤ) • H1Gm.ofPic0 K F x = 0 ↔ (n : ℤ) • x = 0

abbrev

HomPic0Gm

L142 ↗

AlgebraicCurve.HomPic0Gm

Documentation

Multiplicative characters on the n-torsion Picard group with values in the base field.

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev HomPic0Gm (n : ℕ) : Type _

theorem

nsmul_eq_zero

L148 ↗

AlgebraicCurve.HomPic0Gm.nsmul_eq_zero

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace HomPic0Gm
variable {K F}

Lean source · statement

theorem nsmul_eq_zero {n : ℕ} (x : Pic0.torsion K F n) : n • x = 0

theorem

apply_pow_eq_one

L154 ↗

AlgebraicCurve.HomPic0Gm.apply_pow_eq_one

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace HomPic0Gm
variable {K F}

Lean source · statement

theorem apply_pow_eq_one {n : ℕ} (χ : HomPic0Gm K F n) (x : Pic0.torsion K F n) :
    χ x ^ n = 1

def

map

L159 ↗

AlgebraicCurve.HomPic0Gm.map

Documentation

Pull back a torsion character along a homomorphism of torsion Picard groups.

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace HomPic0Gm
variable {K F}

Lean source · statement

def map {F' : Type*} [Field F'] [Algebra K F'] {n : ℕ}
    (f : Pic0.torsion K F n →+ Pic0.torsion K F' n) :
    HomPic0Gm K F' n → HomPic0Gm K F n

theorem

map_apply

L165 ↗

AlgebraicCurve.HomPic0Gm.map_apply

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace HomPic0Gm
variable {K F}

Lean source · statement

theorem map_apply {F' : Type*} [Field F'] [Algebra K F'] {n : ℕ}
    (f : Pic0.torsion K F n →+ Pic0.torsion K F' n) (χ : HomPic0Gm K F' n)
    (x : Pic0.torsion K F n) :
    map f χ x = χ (f x)

theorem

map_one

L171 ↗

AlgebraicCurve.HomPic0Gm.map_one

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace HomPic0Gm
variable {K F}

Lean source · statement

theorem map_one {F' : Type*} [Field F'] [Algebra K F'] {n : ℕ}
    (f : Pic0.torsion K F n →+ Pic0.torsion K F' n) :
    map f (1 : HomPic0Gm K F' n) = 1

theorem

map_mul

L176 ↗

AlgebraicCurve.HomPic0Gm.map_mul

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace HomPic0Gm
variable {K F}

Lean source · statement

theorem map_mul {F' : Type*} [Field F'] [Algebra K F'] {n : ℕ}
    (f : Pic0.torsion K F n →+ Pic0.torsion K F' n) (χ χ' : HomPic0Gm K F' n) :
    map f (χ * χ') = map f χ * map f χ'

theorem

map_id

L182 ↗

AlgebraicCurve.HomPic0Gm.map_id

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace HomPic0Gm
variable {K F}

Lean source · statement

theorem map_id {n : ℕ} (χ : HomPic0Gm K F n) :
    map (AddMonoidHom.id (Pic0.torsion K F n)) χ = χ

theorem

map_comp

L186 ↗

AlgebraicCurve.HomPic0Gm.map_comp

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace HomPic0Gm
variable {K F}

Lean source · statement

theorem map_comp {F' F'' : Type*} [Field F'] [Field F''] [Algebra K F'] [Algebra K F''] {n : ℕ}
    (f : Pic0.torsion K F n →+ Pic0.torsion K F' n)
    (g : Pic0.torsion K F' n →+ Pic0.torsion K F'' n) (χ : HomPic0Gm K F'' n) :
    map (g.comp f) χ = map f (map (F := F') g χ)

structure

WeilPairingData

L195 ↗

AlgebraicCurve.WeilPairingData

Documentation

A given perfect pairing, presented as an isomorphism to the group of torsion characters.

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · full declaration

structure WeilPairingData (n : ℕ) where

  /-- The homomorphism sending a torsion class to its pairing character. -/
  toHom : Pic0.torsion K F n →+ Additive (HomPic0Gm K F n)

  /-- The supplied nondegeneracy condition. -/
  bijective : Function.Bijective toHom

def

eval

L208 ↗

AlgebraicCurve.WeilPairingData.eval

Documentation

Evaluate the supplied pairing on two torsion classes.

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {K F}

Lean source · statement

def eval {n : ℕ} (e : WeilPairingData K F n) (x y : Pic0.torsion K F n) : K

theorem

eval_pow_eq_one

L211 ↗

AlgebraicCurve.WeilPairingData.eval_pow_eq_one

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {K F}

Lean source · statement

theorem eval_pow_eq_one {n : ℕ} (e : WeilPairingData K F n) (x y : Pic0.torsion K F n) :
    e.eval x y ^ n = 1

theorem

eval_add_left

L215 ↗

AlgebraicCurve.WeilPairingData.eval_add_left

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {K F}

Lean source · statement

theorem eval_add_left {n : ℕ} (e : WeilPairingData K F n) (x x' y : Pic0.torsion K F n) :
    e.eval (x + x') y = e.eval x y * e.eval x' y

theorem

eval_add_right

L220 ↗

AlgebraicCurve.WeilPairingData.eval_add_right

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {K F}

Lean source · statement

theorem eval_add_right {n : ℕ} (e : WeilPairingData K F n) (x y y' : Pic0.torsion K F n) :
    e.eval x (y + y') = e.eval x y * e.eval x y'

theorem

eq_zero_of_forall_eval_eq_one

L224 ↗

AlgebraicCurve.WeilPairingData.eq_zero_of_forall_eval_eq_one

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {K F}

Lean source · statement

theorem eq_zero_of_forall_eval_eq_one {n : ℕ} (e : WeilPairingData K F n)
    {x : Pic0.torsion K F n} (h : ∀ y, e.eval x y = 1) : x = 0

def

autodualityEquiv

L244 ↗

AlgebraicCurve.WeilPairingData.autodualityEquiv

Documentation

The additive equivalence determined by the supplied perfect pairing.

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

def autodualityEquiv : Pic0.torsion K F n ≃+ Additive (HomPic0Gm K F n)

theorem

autodualityEquiv_apply

L248 ↗

AlgebraicCurve.WeilPairingData.autodualityEquiv_apply

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem autodualityEquiv_apply (x : Pic0.torsion K F n) :
    e.autodualityEquiv x = e.toHom x

theorem

toMul_autodualityEquiv_apply

L251 ↗

AlgebraicCurve.WeilPairingData.toMul_autodualityEquiv_apply

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem toMul_autodualityEquiv_apply (x y : Pic0.torsion K F n) :
    Additive.toMul (e.autodualityEquiv x) y = e.eval x y

theorem

autodualityEquiv_symm_apply

L254 ↗

AlgebraicCurve.WeilPairingData.autodualityEquiv_symm_apply

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem autodualityEquiv_symm_apply (χ : Additive (HomPic0Gm K F n)) :
    e.toHom (e.autodualityEquiv.symm χ) = χ

theorem

eval_zero_left

L259 ↗

AlgebraicCurve.WeilPairingData.eval_zero_left

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem eval_zero_left (y : Pic0.torsion K F n) : e.eval 0 y = 1

theorem

eval_zero_right

L263 ↗

AlgebraicCurve.WeilPairingData.eval_zero_right

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem eval_zero_right (x : Pic0.torsion K F n) : e.eval x 0 = 1

theorem

eval_neg_left

L267 ↗

AlgebraicCurve.WeilPairingData.eval_neg_left

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem eval_neg_left (x y : Pic0.torsion K F n) :
    e.eval (-x) y = (e.eval x y)⁻¹

theorem

eval_neg_right

L272 ↗

AlgebraicCurve.WeilPairingData.eval_neg_right

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem eval_neg_right (x y : Pic0.torsion K F n) :
    e.eval x (-y) = (e.eval x y)⁻¹

theorem

eval_nsmul_left

L276 ↗

AlgebraicCurve.WeilPairingData.eval_nsmul_left

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem eval_nsmul_left (k : ℕ) (x y : Pic0.torsion K F n) :
    e.eval (k • x) y = e.eval x y ^ k

theorem

eval_nsmul_right

L280 ↗

AlgebraicCurve.WeilPairingData.eval_nsmul_right

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem eval_nsmul_right (k : ℕ) (x y : Pic0.torsion K F n) :
    e.eval x (k • y) = e.eval x y ^ k

theorem

eval_zsmul_left

L284 ↗

AlgebraicCurve.WeilPairingData.eval_zsmul_left

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem eval_zsmul_left (k : ℤ) (x y : Pic0.torsion K F n) :
    e.eval (k • x) y = e.eval x y ^ k

theorem

eval_zsmul_right

L288 ↗

AlgebraicCurve.WeilPairingData.eval_zsmul_right

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem eval_zsmul_right (k : ℤ) (x y : Pic0.torsion K F n) :
    e.eval x (k • y) = e.eval x y ^ k

def

evalAddChar

L294 ↗

AlgebraicCurve.WeilPairingData.evalAddChar

Documentation

The character obtained by fixing the second argument of the pairing.

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · full declaration

def evalAddChar (y : Pic0.torsion K F n) : AddChar (Pic0.torsion K F n) K where
  toFun x := e.eval x y
  map_zero_eq_one' := e.eval_zero_left y
  map_add_eq_mul' x x' := e.eval_add_left x x' y

theorem

evalAddChar_add

L299 ↗

AlgebraicCurve.WeilPairingData.evalAddChar_add

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem evalAddChar_add (y y' : Pic0.torsion K F n) :
    e.evalAddChar (y + y') = e.evalAddChar y * e.evalAddChar y'

theorem

evalAddChar_zero

L304 ↗

AlgebraicCurve.WeilPairingData.evalAddChar_zero

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem evalAddChar_zero : e.evalAddChar 0 = 1

def

congrHom

L307 ↗

AlgebraicCurve.WeilPairingData.congrHom

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · full declaration

def congrHom {F' : Type*} [Field F'] [Algebra K F']
    (φ : Pic0.torsion K F n ≃+ Pic0.torsion K F' n) :
    Pic0.torsion K F' n →+ Additive (HomPic0Gm K F' n) where
  toFun x' := Additive.ofMul ((Additive.toMul (e.toHom (φ.symm x'))).compAddMonoidHom
    φ.symm.toAddMonoidHom)
  map_zero' := by
    ext y'
    change (Additive.toMul (e.toHom (φ.symm 0))) (φ.symm y') = 1
    rw [map_zero, map_zero]; rfl
  map_add' x₁ x₂ := by
    ext y'
    change (Additive.toMul (e.toHom (φ.symm (x₁ + x₂)))) (φ.symm y')
        = (Additive.toMul (e.toHom (φ.symm x₁))) (φ.symm y')
          * (Additive.toMul (e.toHom (φ.symm x₂))) (φ.symm y')
    rw [map_add, map_add, toMul_add, AddChar.mul_apply]

theorem

congrHom_apply

L323 ↗

AlgebraicCurve.WeilPairingData.congrHom_apply

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem congrHom_apply {F' : Type*} [Field F'] [Algebra K F']
    (φ : Pic0.torsion K F n ≃+ Pic0.torsion K F' n) (x' y' : Pic0.torsion K F' n) :
    Additive.toMul (e.congrHom φ x') y' = e.eval (φ.symm x') (φ.symm y')

def

congr

L328 ↗

AlgebraicCurve.WeilPairingData.congr

Documentation

Transport the supplied perfect pairing along an additive equivalence of torsion groups.

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · full declaration

def congr {F' : Type*} [Field F'] [Algebra K F']
    (φ : Pic0.torsion K F n ≃+ Pic0.torsion K F' n) :
    WeilPairingData K F' n where
  toHom := e.congrHom φ
  bijective := by
    refine ⟨fun a b h => ?_, fun χ => ?_⟩
    · apply φ.symm.injective
      apply e.bijective.injective
      ext y
      have h' := DFunLike.congr_fun (congrArg Additive.toMul h) (φ y)
      rwa [e.congrHom_apply, e.congrHom_apply, AddEquiv.symm_apply_apply] at h'
    · obtain ⟨x, hx⟩ :=
        e.bijective.surjective (Additive.ofMul
          ((Additive.toMul χ).compAddMonoidHom φ.toAddMonoidHom))
      refine ⟨φ x, ?_⟩
      ext y'
      rw [e.congrHom_apply, AddEquiv.symm_apply_apply]
      have hx' := DFunLike.congr_fun (congrArg Additive.toMul hx) (φ.symm y')
      rw [show Additive.toMul (e.toHom x) (φ.symm y') = e.eval x (φ.symm y') from rfl] at hx'
      rw [hx']
      change ((Additive.toMul χ).compAddMonoidHom φ.toAddMonoidHom) (φ.symm y')
          = Additive.toMul χ y'
      rw [AddChar.compAddMonoidHom_apply, AddEquiv.toAddMonoidHom_eq_coe,
        AddMonoidHom.coe_ofClass, AddEquiv.apply_symm_apply]

theorem

congr_eval

L354 ↗

AlgebraicCurve.WeilPairingData.congr_eval

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilPairingData
variable {n : ℕ} (e : WeilPairingData K F n)

Lean source · statement

theorem congr_eval {F' : Type*} [Field F'] [Algebra K F']
    (φ : Pic0.torsion K F n ≃+ Pic0.torsion K F' n)
    (x y : Pic0.torsion K F n) :
    (e.congr φ).eval (φ x) (φ y) = e.eval x y

structure

PrincipalPolarization

L364 ↗

AlgebraicCurve.PrincipalPolarization

Documentation

Perfect pairing data with the alternating condition for a principal polarization.

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

structure PrincipalPolarization (K F : Type*) [Field K] [Field F] [Algebra K F]
    (n : ℕ) extends WeilPairingData K F n where

  /-- The pairing of every class with itself is one. -/
  alternating : ∀ x : Pic0.torsion K F n, toWeilPairingData.eval x x = 1

Module documentation

Picard cohomology and pairing data

Declarations