Module

Pic0_exists_mk_eq_forall_notMem_support.lean

Nyll.JacobianVarieties.Pic0.Pic0_exists_mk_eq_forall_notMem_support

2 declarations indexed from sourceView source ↗

Module documentation

Approximation of valuations moves a degree-zero divisor class away from finitely many places.

Imports2

Imported by4

theorem

exists_mk_eq_forall_notMem

L35 ↗

JacobianVarieties.Pic0.Proofs.Pic0_exists_mk_eq_forall_notMem_support.AlgebraicCurve.WC1bSolMV.exists_mk_eq_forall_notMem

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_mk_eq_forall_notMem_support
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC1bSolMV
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_mk_eq_forall_notMem [HasPrincipalDivisors K F]
    (x : Pic0 K F) (S : Finset (Place K F)) :
    ∃ D : Divisor.degZero (K := K) (F := F),
      Pic0.mk D = x ∧ ∀ v ∈ (D : Divisor K F).support, v ∉ S

theorem

exists_mk_eq_forall_notMem_support

L66 ↗

AlgebraicCurve.Pic0.exists_mk_eq_forall_notMem_support

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_mk_eq_forall_notMem_support
noncomputable section
open _root_.AlgebraicCurve in
open JacobianVarieties.Pic0.Proofs.Pic0_exists_mk_eq_forall_notMem_support.AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.Pic0.exists_mk_eq_forall_notMem_support
    {K F : Type*} [Field K] [Field F] [Algebra K F] [HasPrincipalDivisors K F]
    (x : Pic0 K F) (S : Finset (Place K F)) :
    ∃ D : Divisor.degZero (K := K) (F := F),
      Pic0.mk D = x ∧ ∀ v ∈ (D : Divisor K F).support, v ∉ S

Module documentation

Declarations

exists_mk_eq_forall_notMem

exists_mk_eq_forall_notMem_support