Module

PushforwardAlong.lean

Nyll.JacobianVarieties.Pic0.PushforwardAlong

5 declarations indexed from sourceView source ↗

Module documentation

Pushforward of degree-zero divisor classes

The pushforward of divisors descends to the degree-zero Picard group.

Imports1

Nyll.AlgebraicCurves.Divisors.Correspondences

Imported by7

theorem

deg_restrictAlong_mul_inertiaDegAlong

L28 ↗

AlgebraicCurve.Place.deg_restrictAlong_mul_inertiaDegAlong

Source context 3 commands

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

noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

theorem Place.deg_restrictAlong_mul_inertiaDegAlong (φ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (w : Place K F') :
    (w.restrictAlong φ hφ).deg * w.inertiaDegAlong φ hφ = w.deg

def

pushforwardAlongDegZero

L42 ↗

AlgebraicCurve.Pic0.pushforwardAlongDegZero

Documentation

Push forward degree-zero divisors along the given embedding of function fields.

Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
namespace Pic0
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
variable (hfin : FiniteAlong K φ) (hN : NormFormulaAlong K φ hfin)

Lean source · statement

def pushforwardAlongDegZero :
    Divisor.degZero (K := K) (F := F') →+ Divisor.degZero (K := K) (F := F)

theorem

coe_pushforwardAlongDegZero

L49 ↗

AlgebraicCurve.Pic0.coe_pushforwardAlongDegZero

Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
namespace Pic0
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
variable (hfin : FiniteAlong K φ) (hN : NormFormulaAlong K φ hfin)

Lean source · statement

theorem coe_pushforwardAlongDegZero (D : Divisor.degZero (K := K) (F := F')) :
    (pushforwardAlongDegZero φ hφ D : Divisor K F) =
      Divisor.pushforwardAlong φ hφ (D : Divisor K F')

def

pushforwardAlongHom

L55 ↗

AlgebraicCurve.Pic0.pushforwardAlongHom

Documentation

The induced pushforward homomorphism on degree-zero divisor classes.

Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
namespace Pic0
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
variable (hfin : FiniteAlong K φ) (hN : NormFormulaAlong K φ hfin)

Lean source · statement

def pushforwardAlongHom : Pic0 K F' →+ Pic0 K F

theorem

pushforwardAlongHom_mk

L61 ↗

AlgebraicCurve.Pic0.pushforwardAlongHom_mk

Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
namespace Pic0
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
variable (hfin : FiniteAlong K φ) (hN : NormFormulaAlong K φ hfin)

Lean source · statement

theorem pushforwardAlongHom_mk (D : Divisor.degZero (K := K) (F := F')) :
    pushforwardAlongHom φ hφ hfin hN (mk D) = mk (pushforwardAlongDegZero φ hφ D)

Module documentation

Pushforward of degree-zero divisor classes

Declarations

deg_restrictAlong_mul_inertiaDegAlong

pushforwardAlongDegZero

coe_pushforwardAlongDegZero

pushforwardAlongHom

pushforwardAlongHom_mk