NYLL
Module

Pic0_exists_injective_conorm_of_constantFieldExtension_of_isAlgClosed.lean

Nyll.JacobianVarieties.Pic0.Pic0_exists_injective_conorm_of_constantFieldExtension_of_isAlgClosed
28 declarations indexed from sourceView source ↗

Module documentation

Injectivity of conorm under algebraically closed constant extension

Lifts places uniquely, extends divisors, and descends principal divisors through the corresponding spaces of rational functions to obtain an injective map on Picard groups.

Imports7
Imported by4

Declarations

theorem

ord_eq_zero_of_mem_of_inv_mem

L56 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.ord_eq_zero_of_mem_of_inv_mem
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
omit [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
  [Field K] [Algebra K F] [Field F] in
Lean source · statement
theorem ord_eq_zero_of_mem_of_inv_mem {L E : Type*} [Field L] [Field E] [Algebra L E]
    (w : Place L E) {x : E} (hx : x ∈ w.toValuationSubring) (hx' : x⁻¹ ∈ w.toValuationSubring)
    (hx0 : x ≠ 0) : w.ord x = 0
theorem

mem_of_forall_comap_ne

L68 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.mem_of_forall_comap_ne
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
Lean source · statement
theorem mem_of_forall_comap_ne
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (v' : Place K' F')
    (hv' : ∀ v : Place K F, v'.toValuationSubring.comap (algebraMap F F') ≠ v.toValuationSubring)
    (f : F) : algebraMap F F' f ∈ v'.toValuationSubring
theorem

ord_eq_zero_of_forall_comap_ne

L90 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.ord_eq_zero_of_forall_comap_ne
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
Lean source · statement
theorem ord_eq_zero_of_forall_comap_ne
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (v' : Place K' F')
    (hv' : ∀ v : Place K F, v'.toValuationSubring.comap (algebraMap F F') ≠ v.toValuationSubring)
    {f : F} (hf : f ≠ 0) : v'.ord (algebraMap F F' f) = 0
def

lift

L111 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.lift
Documentation

The unique place above the given place under this constant-field extension.

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
def lift (P : Place K F) : Place K' F'
theorem

lift_spec

L116 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.lift_spec
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem lift_spec (P : Place K F) :
    (lift hfg hfg' hgen P).toValuationSubring.comap (algebraMap F F') = P.toValuationSubring ∧
      (∀ f : F, (lift hfg hfg' hgen P).ord (algebraMap F F' f) = P.ord f) ∧
      ∀ Q' : Place K' F',
        Q'.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring →
          Q' = lift hfg hfg' hgen P
theorem

comap_lift

L126 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.comap_lift
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem comap_lift (P : Place K F) :
    (lift hfg hfg' hgen P).toValuationSubring.comap (algebraMap F F') = P.toValuationSubring
theorem

ord_lift

L130 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.ord_lift
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem ord_lift (P : Place K F) (f : F) :
    (lift hfg hfg' hgen P).ord (algebraMap F F' f) = P.ord f
theorem

eq_lift_of_comap_eq

L134 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.eq_lift_of_comap_eq
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem eq_lift_of_comap_eq {P : Place K F} {Q' : Place K' F'}
    (h : Q'.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring) :
    Q' = lift hfg hfg' hgen P
theorem

lift_injective

L139 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.lift_injective
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem lift_injective : Function.Injective (lift (K' := K') (F' := F') hfg hfg' hgen)
theorem

lift_new

L144 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.lift_new
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem lift_new (v' : Place K' F') (hv' : ∀ v, lift hfg hfg' hgen v ≠ v') (v : Place K F) :
    v'.toValuationSubring.comap (algebraMap F F') ≠ v.toValuationSubring
theorem

exists_lift_eq_of_comap_eq

L148 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.exists_lift_eq_of_comap_eq
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem exists_lift_eq_of_comap_eq {v' : Place K' F'} {v : Place K F}
    (h : v'.toValuationSubring.comap (algebraMap F F') = v.toValuationSubring) :
    lift hfg hfg' hgen v = v'
def

con

L154 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.con
Documentation

The divisor obtained by sending each place to its unique lift.

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
def con (D : Divisor K F) : Divisor K' F'
theorem

con_apply_lift

L156 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.con_apply_lift
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem con_apply_lift (D : Divisor K F) (v : Place K F) :
    con hfg hfg' hgen D (lift hfg hfg' hgen v) = D v
theorem

con_apply_of_forall_ne

L160 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.con_apply_of_forall_ne
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem con_apply_of_forall_ne (D : Divisor K F) (v' : Place K' F')
    (hv' : ∀ v, lift hfg hfg' hgen v ≠ v') : con hfg hfg' hgen D v' = 0
theorem

eq_con

L164 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.eq_con
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem eq_con {D : Divisor K F} {D' : Divisor K' F'}
    (hD'over : ∀ (v' : Place K' F') (v : Place K F),
      v'.toValuationSubring.comap (algebraMap F F') = v.toValuationSubring → D' v' = D v)
    (hD'off : ∀ v' : Place K' F',
      (∀ v : Place K F, v'.toValuationSubring.comap (algebraMap F F') ≠ v.toValuationSubring) →
        D' v' = 0) :
    D' = con hfg hfg' hgen D
def

conHom

L179 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.conHom
Documentation

The additive conorm map induced by the unique lifts of places.

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
def conHom : Divisor K F →+ Divisor K' F'
theorem

conHom_apply

L181 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.conHom_apply
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem conHom_apply (D : Divisor K F) : conHom hfg hfg' hgen D = con hfg hfg' hgen D
theorem

isPrincipal_con

L183 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.isPrincipal_con
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem isPrincipal_con {D : Divisor K F} (hD : D.IsPrincipal) :
    (con hfg hfg' hgen D).IsPrincipal
theorem

degree_eq_sum

L197 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.degree_eq_sum
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
variable [IsAlgClosed K'] [IsCurveOver K' F']
omit [IsAlgClosed K] [IsCurveOver K F] in
Lean source · full declaration
theorem degree_eq_sum {L E : Type*} [Field L] [Field E] [Algebra L E] [IsAlgClosed L]
    [IsCurveOver L E]
    (D : Divisor L E) : Divisor.degree D = D.sum fun _ n => n := by
  unfold Divisor.degree
  rw [Finsupp.liftAddHom_apply]
  refine Finsupp.sum_congr fun v _ => ?_
  rw [AddMonoidHom.mulRight_apply, IsCurveOver.deg_eq_one_of_isAlgClosed v, Nat.cast_one, mul_one]
theorem

degree_con

L205 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.degree_con
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
variable [IsAlgClosed K'] [IsCurveOver K' F']
Lean source · statement
theorem degree_con (D : Divisor K F) : Divisor.degree (con hfg hfg' hgen D) = Divisor.degree D
theorem

degree_eq_zero_of_isPrincipal

L210 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.degree_eq_zero_of_isPrincipal
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
variable [IsAlgClosed K'] [IsCurveOver K' F']
omit [IsAlgClosed K'] [IsAlgClosed K] [IsCurveOver K F] in
Lean source · statement
theorem degree_eq_zero_of_isPrincipal {L E : Type*} [Field L] [Field E] [Algebra L E]
    [HasPrincipalDivisors L E] {D : Divisor L E} (hD : D.IsPrincipal) : Divisor.degree D = 0
theorem

isPrincipal_of_isPrincipal_con

L217 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.isPrincipal_of_isPrincipal_con
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
variable [IsAlgClosed K'] [IsCurveOver K' F']
Lean source · statement
theorem isPrincipal_of_isPrincipal_con {D : Divisor K F} (hD : (con hfg hfg' hgen D).IsPrincipal) :
    D.IsPrincipal
def

conDegZero

L266 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.conDegZero
Documentation

The conorm map restricted to divisors of degree zero.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
variable [IsAlgClosed K'] [IsCurveOver K' F']
Lean source · statement
def conDegZero : Divisor.degZero (K := K) (F := F) →+ Divisor.degZero (K := K') (F := F')
theorem

coe_conDegZero

L273 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.coe_conDegZero
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
variable [IsAlgClosed K'] [IsCurveOver K' F']
Lean source · statement
theorem coe_conDegZero (D : Divisor.degZero (K := K) (F := F)) :
    (conDegZero hfg hfg' hgen D : Divisor K' F') = con hfg hfg' hgen (D : Divisor K F)
def

conPic0

L277 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.conPic0
Documentation

The conorm homomorphism on degree-zero divisor classes.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
variable [IsAlgClosed K'] [IsCurveOver K' F']
Lean source · statement
def conPic0 : Pic0 K F →+ Pic0 K' F'
theorem

conPic0_mk

L283 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.conPic0_mk
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
variable [IsAlgClosed K'] [IsCurveOver K' F']
Lean source · statement
theorem conPic0_mk (D : Divisor.degZero (K := K) (F := F)) :
    conPic0 hfg hfg' hgen (Pic0.mk D) = Pic0.mk (conDegZero hfg hfg' hgen D)
theorem

conPic0_injective

L286 ↗
JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc.conPic0_injective
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConDesc
open _root_.AlgebraicCurve
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
section Lift
variable [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
variable [IsAlgClosed K'] [IsCurveOver K' F']
Lean source · statement
theorem conPic0_injective : Function.Injective (conPic0 hfg hfg' hgen)
theorem

exists_injective_conorm_of_constantFieldExtension_of_isAlgClosed

L307 ↗
AlgebraicCurve.Pic0.exists_injective_conorm_of_constantFieldExtension_of_isAlgClosed
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConormInjectivity
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
noncomputable section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
  _root_.JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve
  AlgebraicCurve.ConDesc in
Lean source · statement
theorem _root_.AlgebraicCurve.Pic0.exists_injective_conorm_of_constantFieldExtension_of_isAlgClosed
    (K F K' F' : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [IsAlgClosed K] [IsAlgClosed K']
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    [IsCurveOver K F] [IsCurveOver K' F']
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤) :
    ∃ ι : Pic0 K F →+ Pic0 K' F', Function.Injective ι ∧
      ∀ (D : Divisor.degZero (K := K) (F := F)) (D' : Divisor.degZero (K := K') (F := F')),
        (∀ (v' : Place K' F') (v : Place K F),
          v'.toValuationSubring.comap (algebraMap F F') = v.toValuationSubring →
            (D' : Divisor K' F') v' = (D : Divisor K F) v) →
        (∀ v' : Place K' F',
          (∀ v : Place K F, v'.toValuationSubring.comap (algebraMap F F') ≠ v.toValuationSubring) →
            (D' : Divisor K' F') v' = 0) →
        ι (Pic0.mk D) = Pic0.mk D'

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