Module

PullbackAlong.lean

Nyll.JacobianVarieties.Pic0.PullbackAlong

4 declarations indexed from sourceView source ↗

Module documentation

Pullback of degree-zero divisor classes

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

Imports1

Nyll.AlgebraicCurves.Divisors.Correspondences

Imported by2

def

pullbackAlongDegZeroHom

L34 ↗

AlgebraicCurve.Pic0.pullbackAlongDegZeroHom

Documentation

Pull back degree-zero divisors along the given embedding of function fields.

Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
open Divisor
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
variable (hFI : FundamentalIdentityAlong K φ hφ)

Lean source · statement

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

theorem

coe_pullbackAlongDegZeroHom

L40 ↗

AlgebraicCurve.Pic0.coe_pullbackAlongDegZeroHom

Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
open Divisor
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
variable (hFI : FundamentalIdentityAlong K φ hφ)

Lean source · statement

theorem coe_pullbackAlongDegZeroHom (D : Divisor.degZero (K := K) (F := F)) :
    (pullbackAlongDegZeroHom φ hφ hFI D : Divisor K F') =
      Divisor.pullbackAlong φ hφ (D : Divisor K F)

def

pullbackAlongHom

L46 ↗

AlgebraicCurve.Pic0.pullbackAlongHom

Documentation

The induced pullback homomorphism on degree-zero divisor classes.

Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
open Divisor
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
variable (hFI : FundamentalIdentityAlong K φ hφ)

Lean source · statement

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

theorem

pullbackAlongHom_mk

L52 ↗

AlgebraicCurve.Pic0.pullbackAlongHom_mk

Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
open Divisor
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
variable (hFI : FundamentalIdentityAlong K φ hφ)

Lean source · statement

theorem pullbackAlongHom_mk (D : Divisor.degZero (K := K) (F := F)) :
    pullbackAlongHom φ hφ hFI (mk D) = mk (pullbackAlongDegZeroHom φ hφ hFI D)

Module documentation

Pullback of degree-zero divisor classes

Declarations

pullbackAlongDegZeroHom

coe_pullbackAlongDegZeroHom

pullbackAlongHom

pullbackAlongHom_mk