Pic0_mk_eq_zero_iff_exists_pow.lean

theorem ord_algebraMap_aux {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
    (c : K) : v.ord (algebraMap K F c) = 0

theorem mk_eq_zero_iff_aux {K F : Type*} [Field K] [Field F] [Algebra K F]
    (D : Divisor.degZero (K := K) (F := F)) :
    Pic0.mk D = 0 ↔ Divisor.IsPrincipal (D : Divisor K F)

theorem ord_pow_aux {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F) (h : F)
    (n : ℕ) : v.ord (h ^ n) = n * v.ord h

theorem mk_eq_zero_of_eq_algebraMap_mul_pow {K F : Type*} [Field K] [Field F] [Algebra K F]
    {n : ℕ} (hn : n ≠ 0) {f : F} (hf : f ≠ 0)
    {D : Divisor.degZero (K := K) (F := F)}
    (hfD : ∀ v : Place K F, v.ord f = n * (D : Divisor K F) v) (c : K) (h : F)
    (hfch : f = algebraMap K F c * h ^ n) : Pic0.mk D = 0

theorem exists_algebraMap_mul_pow_of_mk_eq_zero {K F : Type*} [Field K] [Field F]
    [Algebra K F]
    (hconst : ∀ u : F, u ≠ 0 → (∀ v : Place K F, v.ord u = 0) → u ∈ (algebraMap K F).range)
    {n : ℕ} {f : F} (hf : f ≠ 0) {D : Divisor.degZero (K := K) (F := F)}
    (hfD : ∀ v : Place K F, v.ord f = n * (D : Divisor K F) v) (hD : Pic0.mk D = 0) :
    ∃ c : K, c ≠ 0 ∧ ∃ h : F, h ≠ 0 ∧ f = algebraMap K F c * h ^ n

theorem mk_eq_zero_of_eq_pow {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ}
    (hn : n ≠ 0) {f : F} (hf : f ≠ 0)
    {D : Divisor.degZero (K := K) (F := F)}
    (hfD : ∀ v : Place K F, v.ord f = n * (D : Divisor K F) v) (h : F) (hfh : f = h ^ n) :
    Pic0.mk D = 0

theorem exists_pow_of_mk_eq_zero {K F : Type*} [Field K] [Field F] [Algebra K F]
    [IsAlgClosed K]
    (hconst : ∀ u : F, u ≠ 0 → (∀ v : Place K F, v.ord u = 0) → u ∈ (algebraMap K F).range)
    {n : ℕ} (hn : n ≠ 0) {f : F} (hf : f ≠ 0) {D : Divisor.degZero (K := K) (F := F)}
    (hfD : ∀ v : Place K F, v.ord f = n * (D : Divisor K F) v) (hD : Pic0.mk D = 0) :
    ∃ h : F, h ≠ 0 ∧ f = h ^ n

theorem _root_.AlgebraicCurve.Pic0.mk_eq_zero_iff_exists_pow {K F : Type*} [Field K] [Field F]
    [Algebra K F] [IsAlgClosed K]
    (hconst : ∀ u : F, u ≠ 0 → (∀ v : Place K F, v.ord u = 0) → u ∈ (algebraMap K F).range)
    {n : ℕ} (hn : n ≠ 0) {f : F} (hf : f ≠ 0) {D : Divisor.degZero (K := K) (F := F)}
    (hfD : ∀ v : Place K F, v.ord f = n * (D : Divisor K F) v) :
    Pic0.mk D = 0 ↔ ∃ h : F, h ≠ 0 ∧ f = h ^ n