Module

Pic0_roof_package_of_surjective.lean

Nyll.JacobianVarieties.Pic0.Pic0_roof_package_of_surjective

2 declarations indexed from sourceView source ↗

Module documentation

Picard pullback along a surjective field morphism

A surjective morphism has degree one. Its divisor pullback and pushforward are inverse, and conjugating field automorphisms yields the corresponding Picard equivariance.

Imports8

Imported by1

Nyll.JacobianVarieties.Pic0.All

theorem

finiteAlong_and_finrankAlong_eq_one

L58 ↗

JacobianVarieties.Pic0.Proofs.Pic0_roof_package_of_surjective.ROOFID.finiteAlong_and_finrankAlong_eq_one

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_roof_package_of_surjective
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsPrimeCenter AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
namespace ROOFID
variable {K F₁ F₂ : Type} [Field K] [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]

Lean source · statement

theorem finiteAlong_and_finrankAlong_eq_one (ι : F₁ →ₐ[K] F₂) (hιs : Function.Surjective ι) :
    FiniteAlong K ι ∧ finrankAlong K ι = 1

theorem

roof_package_of_surjective

L74 ↗

AlgebraicCurve.Pic0.roof_package_of_surjective

Source context 7 commands