Module

Pic0_pushforwardHom_pullbackHom.lean

Nyll.JacobianVarieties.Pic0.Pic0_pushforwardHom_pullbackHom

2 declarations indexed from sourceView source ↗

Module documentation

Pullback followed by pushforward on the Picard group is multiplication by the extension degree.

Imports2

Imported by1

Nyll.JacobianVarieties.Pic0.All

theorem

pushforwardHom_pullbackHom_s11

L36 ↗

JacobianVarieties.Pic0.Proofs.Pic0_pushforwardHom_pullbackHom.AlgebraicCurve.Pic0.pushforwardHom_pullbackHom_s11

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_pushforwardHom_pullbackHom
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Pic0
open _root_.AlgebraicCurve.Pic0
open _root_.AlgebraicCurve.Pic0
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F']
    [IsScalarTower K F F'] [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']

Lean source · statement

theorem pushforwardHom_pullbackHom_s11 [Module.Finite F F'] [SumRamificationInertia K F F']
    (H : Divisor.PushforwardNormFormula K F F') (x : Pic0 K F) :
    pushforwardHom K F F' H (pullbackHom F' x) = (Module.finrank F F' : ℤ) • x

theorem

pushforwardHom_pullbackHom

L47 ↗

AlgebraicCurve.Pic0.pushforwardHom_pullbackHom

Source context 3 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_pushforwardHom_pullbackHom
open _root_.AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Pic0.pushforwardHom_pullbackHom {K F F' : Type*} [Field K] [Field F]
    [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F'] [Module.Finite F F']
    [SumRamificationInertia K F F'] (H : Divisor.PushforwardNormFormula K F F')
    (x : Pic0 K F) : Pic0.pushforwardHom K F F' H (Pic0.pullbackHom F' x) =
    (Module.finrank F F' : ℤ) • x

Module documentation

Declarations

pushforwardHom_pullbackHom_s11

pushforwardHom_pullbackHom