NYLL
Module

Pic0_exists_injective_addMonoidHom_torsion_dlog.lean

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

Module documentation

Logarithmic differentials of torsion divisor classes

A torsion class admits a degree-zero divisor representative whose multiple is principal. The logarithmic differential of a witnessing function is independent of this choice, is additive, and is injective under the stated separability and nonvanishing hypotheses.

Imports4
Imported by1

Declarations

theorem

dlog_algebraMap

L45 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.dlog_algebraMap
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem dlog_algebraMap (a : K) : kw_hwcd_dlog K (algebraMap K F a) = 0
theorem

dlog_eq_zero_iff

L48 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.dlog_eq_zero_iff
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem dlog_eq_zero_iff {f : F} (hf : f ≠ 0) : kw_hwcd_dlog K f = 0 ↔ D K F f = 0
theorem

dlog_eq_of_forall_ord_eq

L51 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.dlog_eq_of_forall_ord_eq
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem dlog_eq_of_forall_ord_eq [IsAlgClosed K] (t : F) (ht : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F]
    {f f' : F} (hf : f ≠ 0) (hf' : f' ≠ 0) (h : ∀ v : Place K F, v.ord f = v.ord f') :
    kw_hwcd_dlog K f = kw_hwcd_dlog K f'
theorem

dlog_mul_pow_char

L62 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.dlog_mul_pow_char
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem dlog_mul_pow_char (p : ℕ) [CharP F p] {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) :
    kw_hwcd_dlog K (f * g ^ p) = kw_hwcd_dlog K f
theorem

exists_witness

L70 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.exists_witness
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Witness
variable (p : ℕ)
Lean source · statement
theorem exists_witness (c : Pic0.torsion K F p) :
    ∃ (Dv : Divisor.degZero (K := K) (F := F)) (f : F), Pic0.mk Dv = (c : Pic0 K F) ∧ f ≠ 0 ∧
      ∀ v : Place K F, v.ord f = (p : ℤ) * (Dv : Divisor K F) v
def

repr

L82 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.repr
Documentation

A degree-zero divisor representing the torsion class, from the principal-multiple witness.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Witness
variable (p : ℕ)
Lean source · statement
def repr (c : Pic0.torsion K F p) : Divisor.degZero (K := K) (F := F)
def

fn

L86 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.fn
Documentation

A nonzero function whose divisor is the stated multiple of the chosen representative.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Witness
variable (p : ℕ)
Lean source · statement
def fn (c : Pic0.torsion K F p) : F
theorem

mk_repr

L89 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.mk_repr
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Witness
variable (p : ℕ)
Lean source · statement
theorem mk_repr (c : Pic0.torsion K F p) : Pic0.mk (repr p c) = (c : Pic0 K F)
theorem

fn_ne_zero

L92 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.fn_ne_zero
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Witness
variable (p : ℕ)
Lean source · statement
theorem fn_ne_zero (c : Pic0.torsion K F p) : fn p c ≠ 0
theorem

ord_fn

L95 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.ord_fn
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Witness
variable (p : ℕ)
Lean source · statement
theorem ord_fn (c : Pic0.torsion K F p) (v : Place K F) :
    v.ord (fn p c) = (p : ℤ) * (repr p c : Divisor K F) v
theorem

dlog_eq_of_mk_eq

L105 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.dlog_eq_of_mk_eq
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Map
variable [IsAlgClosed K]
Lean source · statement
theorem dlog_eq_of_mk_eq (p : ℕ) [CharP F p] (t : F) (ht : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F]
    {D₁ D₂ : Divisor.degZero (K := K) (F := F)} {f₁ f₂ : F}
    (hmk : Pic0.mk D₁ = Pic0.mk D₂) (hf₁ : f₁ ≠ 0) (hf₂ : f₂ ≠ 0)
    (h₁ : ∀ v : Place K F, v.ord f₁ = (p : ℤ) * (D₁ : Divisor K F) v)
    (h₂ : ∀ v : Place K F, v.ord f₂ = (p : ℤ) * (D₂ : Divisor K F) v) :
    kw_hwcd_dlog K f₁ = kw_hwcd_dlog K f₂
def

dlogFun

L126 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.dlogFun
Documentation

The logarithmic differential of the witnessing function for a torsion class.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Map
variable [IsAlgClosed K]
Lean source · statement
def dlogFun (p : ℕ) (c : Pic0.torsion K F p) : Ω[F⁄K]
theorem

dlogFun_eq

L128 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.dlogFun_eq
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Map
variable [IsAlgClosed K]
Lean source · statement
theorem dlogFun_eq (p : ℕ) [CharP F p] (t : F) (ht : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F]
    (c : Pic0.torsion K F p) {Dv : Divisor.degZero (K := K) (F := F)} {f : F}
    (hmk : Pic0.mk Dv = (c : Pic0 K F)) (hf : f ≠ 0)
    (h : ∀ v : Place K F, v.ord f = (p : ℤ) * (Dv : Divisor K F) v) :
    dlogFun p c = kw_hwcd_dlog K f
theorem

dlogFun_add

L136 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.dlogFun_add
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Map
variable [IsAlgClosed K]
Lean source · statement
theorem dlogFun_add (p : ℕ) [CharP F p] (t : F) (ht : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F] (c₁ c₂ : Pic0.torsion K F p) :
    dlogFun p (c₁ + c₂) = dlogFun p c₁ + dlogFun p c₂
def

dlogHom

L152 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.dlogHom
Documentation

The additive map from torsion classes to differentials defined by logarithmic differentiation.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Map
variable [IsAlgClosed K]
Lean source · statement
def dlogHom (p : ℕ) [CharP F p] (t : F) (ht : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F] :
      Pic0.torsion K F p →+ Ω[F⁄K]
theorem

dlogHom_apply

L157 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.dlogHom_apply
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Map
variable [IsAlgClosed K]
Lean source · statement
theorem dlogHom_apply (p : ℕ) [CharP F p] (t : F) (ht : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F] (c : Pic0.torsion K F p) :
    dlogHom p t ht c = kw_hwcd_dlog K (fn p c)
theorem

dlogHom_injective

L161 ↗
JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog.P2mWs11R4.dlogHom_injective
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R4
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Map
variable [IsAlgClosed K]
Lean source · statement
theorem dlogHom_injective (p : ℕ) [Fact p.Prime] [CharP F p] (t : F) (ht : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F]
    (hsepK : Algebra.IsSeparable (IntermediateField.adjoin K ({t} : Set F)) F)
    (hdt : KaehlerDifferential.D K F t ≠ 0) :
    Function.Injective (dlogHom (K := K) (F := F) p t ht)
theorem

exists_injective_addMonoidHom_torsion_dlog

L192 ↗
AlgebraicCurve.Pic0.exists_injective_addMonoidHom_torsion_dlog
Source context 6 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_injective_addMonoidHom_torsion_dlog
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve KaehlerDifferential
open P2mWs11R4 in
Lean source · statement
theorem _root_.AlgebraicCurve.Pic0.exists_injective_addMonoidHom_torsion_dlog
    (K F : Type*) [Field K] [Field F] [Algebra K F] [IsAlgClosed K]
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (t : F) (ht : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F]
    (hsepK : Algebra.IsSeparable (IntermediateField.adjoin K ({t} : Set F)) F)
    (hdt : KaehlerDifferential.D K F t ≠ 0) :
    ∃ φ : AlgebraicCurve.Pic0.torsion K F p →+ Ω[F⁄K], Function.Injective φ ∧
      ∀ c, ∃ f : F, f ≠ 0 ∧ (∀ v : AlgebraicCurve.Place K F, (p : ℤ) ∣ v.ord f) ∧
        φ c = f⁻¹ • KaehlerDifferential.D K F f

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