Module

Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Divisors.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed

23 declarations indexed from sourceView source ↗

Module documentation

Divisor deg Zero exists Unique conorm of constant Field Extension of is Alg Closed

Imports4

Imported by1

Nyll.AlgebraicCurves.Divisors.All

theorem

ord_eq_zero_of_mem_of_inv_mem

L40 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.ord_eq_zero_of_mem_of_inv_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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_mem_of_inv_mem {k L : Type*} [Field k] [Field L] [Algebra k L]
    (w : Place k L) {z : L} (hz : z ∈ w.toValuationSubring)
    (hzi : z⁻¹ ∈ w.toValuationSubring) : w.ord z = 0

theorem

ord_algebraMap_base

L49 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.ord_algebraMap_base

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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_algebraMap_base {k L : Type*} [Field k] [Field L] [Algebra k L]
    (w : Place k L) (a : k) : w.ord (algebraMap k L a) = 0

theorem

degree_eq_zero_of_forall_eq_ord

L57 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.degree_eq_zero_of_forall_eq_ord

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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 degree_eq_zero_of_forall_eq_ord {k L : Type*} [Field k] [Field L] [Algebra k L]
    [HasPrincipalDivisors k L] {f : L} (hf : f ≠ 0) {D : Divisor k L}
    (hD : ∀ v, D v = v.ord f) : Divisor.degree D = 0

theorem

mk_zsmul'

L65 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.mk_zsmul'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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 mk_zsmul' {k L : Type*} [Field k] [Field L] [Algebra k L] (n : ℤ)
    (D : Divisor.degZero (K := k) (F := L)) : Pic0.mk (n • D) = n • Pic0.mk D

theorem

mk_eq_zero_iff'

L69 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.mk_eq_zero_iff'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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 mk_eq_zero_iff' {k L : Type*} [Field k] [Field L] [Algebra k L]
    (D : Divisor.degZero (K := k) (F := L)) :
    Pic0.mk D = 0 ↔ (D : Divisor k L) ∈ (Divisor.principal : AddSubgroup (Divisor k L))

theorem

mk_eq_mk_iff'

L75 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.mk_eq_mk_iff'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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 mk_eq_mk_iff' {k L : Type*} [Field k] [Field L] [Algebra k L]
    (D E : Divisor.degZero (K := k) (F := L)) :
    Pic0.mk D = Pic0.mk E ↔
      -(D : Divisor k L) + E ∈ (Divisor.principal : AddSubgroup (Divisor k L))

theorem

natCast_mul_apply_eq_of_zsmul_mem_principal

L83 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.natCast_mul_apply_eq_of_zsmul_mem_principal

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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 natCast_mul_apply_eq_of_zsmul_mem_principal {k L : Type*} [Field k] [Field L]
    [Algebra k L] {n : ℕ} {D : Divisor.degZero (K := k) (F := L)}
    (h : ((n : ℤ) • D : Divisor.degZero (K := k) (F := L)) ∈
      (Divisor.principal : AddSubgroup (Divisor k L)).addSubgroupOf Divisor.degZero) :
    ∃ g : L, g ≠ 0 ∧ ∀ v : Place k L, (n : ℤ) * (D : Divisor k L) v = v.ord g

def

liftPlace

L103 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.liftPlace

Documentation

A chosen lift of the place along the constant-field extension.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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 liftPlace (P : Place K F) : Place K' F'

theorem

liftPlace_spec

L108 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.liftPlace_spec

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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 liftPlace_spec (P : Place K F) :
    (liftPlace hfg hfg' hgen P).toValuationSubring.comap (algebraMap F F') =
        P.toValuationSubring ∧
      (∀ f : F, (liftPlace 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' = liftPlace hfg hfg' hgen P

theorem

liftPlace_comap

L118 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.liftPlace_comap

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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 liftPlace_comap (P : Place K F) :
    (liftPlace hfg hfg' hgen P).toValuationSubring.comap (algebraMap F F') =
      P.toValuationSubring

theorem

ord_liftPlace

L123 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.ord_liftPlace

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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_liftPlace (P : Place K F) (f : F) :
    (liftPlace hfg hfg' hgen P).ord (algebraMap F F' f) = P.ord f

theorem

eq_liftPlace

L127 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.eq_liftPlace

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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_liftPlace {P : Place K F} {Q' : Place K' F'}
    (h : Q'.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring) :
    Q' = liftPlace hfg hfg' hgen P

theorem

liftPlace_injective

L132 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.liftPlace_injective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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 liftPlace_injective :
    Function.Injective (liftPlace (K := K) (F := F) (K' := K') (F' := F') hfg hfg' hgen)

theorem

ord_algebraMap_eq_zero_of_forall_ne

L138 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.ord_algebraMap_eq_zero_of_forall_ne

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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_algebraMap_eq_zero_of_forall_ne (w : Place K' F')
    (hw : ∀ P : Place K F, w ≠ liftPlace hfg hfg' hgen P) (f : F) :
    w.ord (algebraMap F F' f) = 0

def

conormDiv

L156 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.conormDiv

Documentation

The additive map of divisors induced by the chosen lifts of places.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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 conormDiv : Divisor K F →+ Divisor K' F'

theorem

conormDiv_apply_liftPlace

L159 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.conormDiv_apply_liftPlace

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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 conormDiv_apply_liftPlace (D : Divisor K F) (P : Place K F) :
    conormDiv hfg hfg' hgen D (liftPlace hfg hfg' hgen P) = D P

theorem

conormDiv_apply_of_forall_ne

L163 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.conormDiv_apply_of_forall_ne

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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 conormDiv_apply_of_forall_ne (D : Divisor K F) (w : Place K' F')
    (hw : ∀ P : Place K F, w ≠ liftPlace hfg hfg' hgen P) : conormDiv hfg hfg' hgen D w = 0

theorem

conormDiv_single

L167 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.conormDiv_single

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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 conormDiv_single (P : Place K F) (m : ℤ) :
    conormDiv hfg hfg' hgen (Finsupp.single P m) = Finsupp.single (liftPlace hfg hfg' hgen P) m

theorem

conormDiv_mem_principal

L171 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.conormDiv_mem_principal

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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 conormDiv_mem_principal {D : Divisor K F}
    (hD : D ∈ (Divisor.principal : AddSubgroup (Divisor K F))) :
    conormDiv hfg hfg' hgen D ∈ (Divisor.principal : AddSubgroup (Divisor K' F'))

theorem

degree_conormDiv

L185 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.degree_conormDiv

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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_conormDiv (D : Divisor K F) :
    Divisor.degree (conormDiv hfg hfg' hgen D) = Divisor.degree D

def

conormDegZero

L193 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.conormDegZero

Documentation

The conorm map restricted to the subgroups of degree-zero divisors.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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 conormDegZero :
    Divisor.degZero (K := K) (F := F) →+ Divisor.degZero (K := K') (F := F')

theorem

coe_conormDegZero

L199 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.HEXkit.coe_conormDegZero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HEXkit
open _root_.AlgebraicCurve
section Transfer
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] [CharZero 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_conormDegZero (D : Divisor.degZero (K := K) (F := F)) :
    (conormDegZero hfg hfg' hgen D : Divisor K' F') = conormDiv hfg hfg' hgen D

theorem

existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed

L209 ↗

AlgebraicCurve.Divisor.degZero.existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
open _root_.AlgebraicCurve
open AlgebraicCurve.HEXkit in

Lean source · statement

theorem
  _root_.AlgebraicCurve.Divisor.degZero.existsUnique_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] [CharZero 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')) = ⊤)
    (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)

Module documentation

Divisor deg Zero exists Unique conorm of constant Field Extension of is Alg Closed

Declarations