NYLL
Module

Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.lean

Nyll.JacobianVarieties.Pic0.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
18 declarations indexed from sourceView source ↗

Module documentation

Picard groups under equivalences of function fields

Transport places, divisor classes, and scalar actions along the given field equivalence.

Imports2
Imported by1

Declarations

theorem

mapDomain_apply

L39 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.mapDomain_apply
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Divisors
variable (Φ : Place K F ≃ Place K' F')
Lean source · statement
theorem mapDomain_apply (D : Divisor K F) (w : Place K' F') :
    Finsupp.mapDomain Φ D w = D (Φ.symm w)
theorem

mapDomain_symm_mapDomain

L43 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.mapDomain_symm_mapDomain
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Divisors
variable (Φ : Place K F ≃ Place K' F')
Lean source · statement
theorem mapDomain_symm_mapDomain (D : Divisor K F) :
    Finsupp.mapDomain Φ.symm (Finsupp.mapDomain Φ D) = D
theorem

mapDomain_mapDomain_symm

L47 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.mapDomain_mapDomain_symm
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Divisors
variable (Φ : Place K F ≃ Place K' F')
Lean source · statement
theorem mapDomain_mapDomain_symm (D' : Divisor K' F') :
    Finsupp.mapDomain Φ (Finsupp.mapDomain Φ.symm D') = D'
theorem

degree_mapDomain

L51 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.degree_mapDomain
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Divisors
variable (Φ : Place K F ≃ Place K' F')
Lean source · statement
theorem degree_mapDomain (hdeg : ∀ v : Place K F, (Φ v).deg = v.deg) (D : Divisor K F) :
    Divisor.degree (Finsupp.mapDomain Φ D) = Divisor.degree D
theorem

isPrincipal_mapDomain

L60 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.isPrincipal_mapDomain
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Divisors
variable (Φ : Place K F ≃ Place K' F')
Lean source · statement
theorem isPrincipal_mapDomain (φ : F ≃+* F')
    (hord : ∀ (v : Place K F) (f : F), (Φ v).ord (φ f) = v.ord f)
    {D : Divisor K F} (hD : Divisor.IsPrincipal D) :
      Divisor.IsPrincipal (Finsupp.mapDomain Φ D)
theorem

isPrincipal_mapDomain_symm

L68 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.isPrincipal_mapDomain_symm
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Divisors
variable (Φ : Place K F ≃ Place K' F')
Lean source · statement
theorem isPrincipal_mapDomain_symm (φ : F ≃+* F')
    (hord : ∀ (v : Place K F) (f : F), (Φ v).ord (φ f) = v.ord f)
    {D' : Divisor K' F'} (hD : Divisor.IsPrincipal D') :
      Divisor.IsPrincipal (Finsupp.mapDomain Φ.symm D')
def

degZeroMap

L78 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.degZeroMap
Documentation

Transport degree-zero divisors along a degree-preserving equivalence of places.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Divisors
variable (Φ : Place K F ≃ Place K' F')
Lean source · statement
def degZeroMap (hdeg : ∀ v : Place K F, (Φ v).deg = v.deg) :
    Divisor.degZero (K := K) (F := F) →+ Divisor.degZero (K := K') (F := F')
theorem

coe_degZeroMap

L86 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.coe_degZeroMap
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Divisors
variable (Φ : Place K F ≃ Place K' F')
Lean source · statement
theorem coe_degZeroMap (hdeg : ∀ v : Place K F, (Φ v).deg = v.deg)
    (D : Divisor.degZero (K := K) (F := F)) :
    (degZeroMap Φ hdeg D : Divisor K' F') = Finsupp.mapDomain Φ (D : Divisor K F)
def

degZeroMapSymm

L91 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.degZeroMapSymm
Documentation

Transport degree-zero divisors back along the inverse equivalence of places.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Divisors
variable (Φ : Place K F ≃ Place K' F')
Lean source · statement
def degZeroMapSymm (hdeg : ∀ v : Place K F, (Φ v).deg = v.deg) :
    Divisor.degZero (K := K') (F := F') →+ Divisor.degZero (K := K) (F := F)
theorem

coe_degZeroMapSymm

L100 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.coe_degZeroMapSymm
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Divisors
variable (Φ : Place K F ≃ Place K' F')
Lean source · statement
theorem coe_degZeroMapSymm (hdeg : ∀ v : Place K F, (Φ v).deg = v.deg)
    (D' : Divisor.degZero (K := K') (F := F')) :
    (degZeroMapSymm Φ hdeg D' : Divisor K F) = Finsupp.mapDomain Φ.symm (D' : Divisor K' F')
def

picMap

L113 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.picMap
Documentation

The homomorphism on Picard groups induced by transporting places and principal divisors.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Pic
variable (Φ : Place K F ≃ Place K' F') (φ : F ≃+* F')
  (hord : ∀ (v : Place K F) (f : F), (Φ v).ord (φ f) = v.ord f)
  (hdeg : ∀ v : Place K F, (Φ v).deg = v.deg)
Lean source · statement
def picMap : Pic0 K F →+ Pic0 K' F'
def

picMapSymm

L120 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.picMapSymm
Documentation

The inverse homomorphism on Picard groups induced by the inverse equivalence of places.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Pic
variable (Φ : Place K F ≃ Place K' F') (φ : F ≃+* F')
  (hord : ∀ (v : Place K F) (f : F), (Φ v).ord (φ f) = v.ord f)
  (hdeg : ∀ v : Place K F, (Φ v).deg = v.deg)
Lean source · statement
def picMapSymm : Pic0 K' F' →+ Pic0 K F
theorem

picMap_mk

L126 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.picMap_mk
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Pic
variable (Φ : Place K F ≃ Place K' F') (φ : F ≃+* F')
  (hord : ∀ (v : Place K F) (f : F), (Φ v).ord (φ f) = v.ord f)
  (hdeg : ∀ v : Place K F, (Φ v).deg = v.deg)
Lean source · statement
theorem picMap_mk (D : Divisor.degZero (K := K) (F := F)) :
    picMap Φ φ hord hdeg (Pic0.mk D) = Pic0.mk (degZeroMap Φ hdeg D)
theorem

picMapSymm_mk

L129 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.picMapSymm_mk
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Pic
variable (Φ : Place K F ≃ Place K' F') (φ : F ≃+* F')
  (hord : ∀ (v : Place K F) (f : F), (Φ v).ord (φ f) = v.ord f)
  (hdeg : ∀ v : Place K F, (Φ v).deg = v.deg)
Lean source · statement
theorem picMapSymm_mk (D' : Divisor.degZero (K := K') (F := F')) :
    picMapSymm Φ φ hord hdeg (Pic0.mk D') = Pic0.mk (degZeroMapSymm Φ hdeg D')
def

picEquiv

L133 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.picEquiv
Documentation

The additive equivalence of Picard groups induced by the given equivalence of places.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Pic
variable (Φ : Place K F ≃ Place K' F') (φ : F ≃+* F')
  (hord : ∀ (v : Place K F) (f : F), (Φ v).ord (φ f) = v.ord f)
  (hdeg : ∀ v : Place K F, (Φ v).deg = v.deg)
Lean source · statement
def picEquiv : Pic0 K F ≃+ Pic0 K' F'
theorem

picEquiv_mk

L146 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.picEquiv_mk
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Pic
variable (Φ : Place K F ≃ Place K' F') (φ : F ≃+* F')
  (hord : ∀ (v : Place K F) (f : F), (Φ v).ord (φ f) = v.ord f)
  (hdeg : ∀ v : Place K F, (Φ v).deg = v.deg)
Lean source · statement
theorem picEquiv_mk (D : Divisor.degZero (K := K) (F := F)) :
    picEquiv Φ φ hord hdeg (Pic0.mk D) = Pic0.mk (degZeroMap Φ hdeg D)
theorem

map_smul

L157 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv.Pic0Transport.map_smul
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace Pic0Transport
variable {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
section Equivariance
variable (φ : F ≃+* F') (Φ : Place K F ≃ Place K' F')
  (hcomap : ∀ v : Place K F, (Φ v).toValuationSubring = v.toValuationSubring.comap φ.symm.toRingHom)
include hcomap in
Lean source · statement
theorem map_smul (σ : F ≃ₐ[K] F) (σ' : F' ≃ₐ[K'] F') (hσ : ∀ f : F, φ (σ f) = σ' (φ f))
    (v : Place K F) :
    Φ (σ • v) = σ' • Φ v
theorem

exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv

L183 ↗
AlgebraicCurve.Pic0.exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
open AlgebraicCurve
open scoped Pointwise
open Pic0Transport in
Lean source · statement
theorem _root_.AlgebraicCurve.Pic0.exists_equiv_addEquiv_mk_eq_and_smul_of_ringEquiv
    {K K' F F' : Type} [Field K] [Field K'] [Field F] [Field F'] [Algebra K F] [Algebra K' F']
    (e : K ≃+* K') (φ : F ≃+* F') (hφ : ∀ a : K, φ (algebraMap K F a) = algebraMap K' F' (e a)) :
    ∃ (Φ : Place K F ≃ Place K' F') (Ψ : Pic0 K F ≃+ Pic0 K' F'),
      (∀ v : Place K F, (Φ v).toValuationSubring = v.toValuationSubring.comap φ.symm.toRingHom) ∧
      (∀ D : Divisor.degZero (K := K) (F := F),
        ∃ hD : Finsupp.mapDomain Φ (D : Divisor K F) ∈ Divisor.degZero (K := K') (F := F'),
          Ψ (Pic0.mk D) = Pic0.mk ⟨_, hD⟩) ∧
      (∀ (σ : F ≃ₐ[K] F) (σ' : F' ≃ₐ[K'] F'), (∀ f : F, φ (σ f) = σ' (φ f)) →
        ∀ x : Pic0 K F, Ψ (σ • x) = σ' • Ψ x)

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