NYLL
Module

Divisor_pushforward_pullback_of_finite.lean

Nyll.AlgebraicCurves.Divisors.Divisor_pushforward_pullback_of_finite
4 declarations indexed from sourceView source ↗

Module documentation

Divisor pushforward pullback of finite

Imports1
Imported by3

Declarations

theorem

pushforward_pullback_single

L33 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforward_pullback_of_finite.AlgebraicCurve.Divisor.pushforward_pullback_single
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforward_pullback_of_finite
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Divisor
open _root_.AlgebraicCurve.Divisor
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 pushforward_pullback_single (v : Place K F) (n : ℤ) :
    pushforward F (pullback F' (Finsupp.single v n))
      = Finsupp.single v
          (n * ∑ w ∈ v.fiber F', (w.ramificationIndex F : ℤ) * (w.inertiaDeg F : ℤ))
theorem

pushforward_pullback_apply

L52 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforward_pullback_of_finite.AlgebraicCurve.Divisor.pushforward_pullback_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforward_pullback_of_finite
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Divisor
open _root_.AlgebraicCurve.Divisor
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 pushforward_pullback_apply (D : Divisor K F) (v : Place K F) :
    pushforward F (pullback F' D) v
      = (∑ w ∈ v.fiber F', (w.ramificationIndex F : ℤ) * (w.inertiaDeg F : ℤ)) * D v
theorem

pushforward_pullback_of_sumRam

L67 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforward_pullback_of_finite.AlgebraicCurve.Divisor.pushforward_pullback_of_sumRam
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforward_pullback_of_finite
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Divisor
open _root_.AlgebraicCurve.Divisor
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 pushforward_pullback_of_sumRam [SumRamificationInertia K F F'] (D : Divisor K F) :
    pushforward F (pullback F' D) = (Module.finrank F F' : ℤ) • D
theorem

pushforward_pullback_of_finite

L76 ↗
AlgebraicCurve.Divisor.pushforward_pullback_of_finite
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforward_pullback_of_finite
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Divisor.pushforward_pullback_of_finite {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'] (D : Divisor K F) : Divisor.pushforward F (Divisor.pullback F' D)
  = (Module.finrank F F' : ℤ) • D

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.