Module

Place_exists_algHom_laurentSeries_order_eq_ord.lean

Nyll.AlgebraicCurves.Places.Place_exists_algHom_laurentSeries_order_eq_ord

28 declarations indexed from sourceView source ↗

Module documentation

Place exists alg Hom laurent Series order eq ord

Imports2

Imported by1

Nyll.AlgebraicCurves.Places.All

def

resEquiv

L39 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.resEquiv

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def resEquiv (w : Place K F) (hw : w.deg = 1) : K ≃+* w.ResidueField

theorem

resEquiv_apply

L43 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.resEquiv_apply

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resEquiv_apply (w : Place K F) (hw : w.deg = 1) (a : K) :
    resEquiv w hw a = algebraMap K w.ResidueField a

theorem

residue_algebraMap

L46 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.residue_algebraMap

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem residue_algebraMap (w : Place K F) (a : K) :
    residue w.toValuationSubring (algebraMap K w.toValuationSubring a)
      = algebraMap K w.ResidueField a

def

resCoeff

L52 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.resCoeff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def resCoeff (w : Place K F) (hw : w.deg = 1) (y : w.toValuationSubring) : K

theorem

residue_sub_algebraMap_resCoeff

L55 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.residue_sub_algebraMap_resCoeff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem residue_sub_algebraMap_resCoeff (w : Place K F) (hw : w.deg = 1)
    (y : w.toValuationSubring) :
    residue w.toValuationSubring (y - algebraMap K w.toValuationSubring (resCoeff w hw y))
      = 0

theorem

exists_sub_resCoeff_eq_mul

L64 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.exists_sub_resCoeff_eq_mul

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_sub_resCoeff_eq_mul (w : Place K F) (hw : w.deg = 1)
    {π : w.toValuationSubring} (hπ : Irreducible π) (y : w.toValuationSubring) :
    ∃ z : w.toValuationSubring,
      y - algebraMap K w.toValuationSubring (resCoeff w hw y) = π * z

def

remSeq

L72 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.remSeq

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def remSeq (w : Place K F) (hw : w.deg = 1) {π : w.toValuationSubring}
    (hπ : Irreducible π) (y : w.toValuationSubring) : ℕ → w.toValuationSubring
  | 0 => y
  | n + 1 => (exists_sub_resCoeff_eq_mul w hw hπ (remSeq w hw hπ y n)).choose

theorem

remSeq_spec

L77 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.remSeq_spec

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem remSeq_spec (w : Place K F) (hw : w.deg = 1) {π : w.toValuationSubring}
    (hπ : Irreducible π) (y : w.toValuationSubring) (n : ℕ) :
    remSeq w hw hπ y n
        - algebraMap K w.toValuationSubring (resCoeff w hw (remSeq w hw hπ y n))
      = π * remSeq w hw hπ y (n + 1)

def

expCoeff

L84 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.expCoeff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def expCoeff (w : Place K F) (hw : w.deg = 1) {π : w.toValuationSubring}
    (hπ : Irreducible π) (y : w.toValuationSubring) (n : ℕ) : K

theorem

remSeq_sum

L88 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.remSeq_sum

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem remSeq_sum (w : Place K F) (hw : w.deg = 1) {π : w.toValuationSubring}
    (hπ : Irreducible π) (y : w.toValuationSubring) (M : ℕ) :
    y = (∑ n ∈ Finset.range M,
          algebraMap K w.toValuationSubring (expCoeff w hw hπ y n) * π ^ n)
        + π ^ M * remSeq w hw hπ y M

theorem

remSeq_shift

L108 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.remSeq_shift

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem remSeq_shift (w : Place K F) (hw : w.deg = 1) {π : w.toValuationSubring}
    (hπ : Irreducible π) (y : w.toValuationSubring) :
    ∀ n : ℕ, remSeq w hw hπ y (n + 1) = remSeq w hw hπ (remSeq w hw hπ y 1) n
  | 0 => rfl
  | n + 1 => by
      change (exists_sub_resCoeff_eq_mul w hw hπ (remSeq w hw hπ y (n + 1))).choose
        = remSeq w hw hπ (remSeq w hw hπ y 1) (n + 1)
      rw [remSeq_shift w hw hπ y n]
      rfl

theorem

expCoeff_eq_of_eq_sum

L118 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.expCoeff_eq_of_eq_sum

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem expCoeff_eq_of_eq_sum (w : Place K F) (hw : w.deg = 1)
    {π : w.toValuationSubring} (hπ : Irreducible π) :
    ∀ (M : ℕ) (y : w.toValuationSubring) (b : ℕ → K) (r : w.toValuationSubring),
      y = (∑ n ∈ Finset.range M, algebraMap K w.toValuationSubring (b n) * π ^ n)
          + π ^ M * r →
      ∀ n < M, expCoeff w hw hπ y n = b n

theorem

sum_single_coeff

L168 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.sum_single_coeff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem sum_single_coeff (w : Place K F) {π : w.toValuationSubring} (M j : ℕ)
    (hj : j < M) (a : K) :
    (∑ k ∈ Finset.range M,
        algebraMap K w.toValuationSubring (if k = j then a else 0) * π ^ k)
      = algebraMap K w.toValuationSubring a * π ^ j := by
  rw [Finset.sum_eq_single j]
  · rw [ite_eq_left rfl]
  · intro k _ hk
    rw [ite_eq_right hk, map_zero, zero_mul]
  · intro hj'
    exact absurd (Finset.mem_range.mpr hj) hj'

def

expPS

L180 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.expPS

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def expPS (w : Place K F) (hw : w.deg = 1) {π : w.toValuationSubring}
    (hπ : Irreducible π) : w.toValuationSubring →+* PowerSeries K where
  toFun y := PowerSeries.mk (expCoeff w hw hπ y)
  map_one' := by
    ext n
    rw [PowerSeries.coeff_mk, PowerSeries.coeff_one]
    have hident : (1 : w.toValuationSubring)
        = (∑ k ∈ Finset.range (n + 1),
            algebraMap K w.toValuationSubring (if k = 0 then (1 : K) else 0) * π ^ k)
          + π ^ (n + 1) * 0 := by
      rw [mul_zero, add_zero, sum_single_coeff w (n + 1) 0 n.succ_pos 1, map_one, pow_zero,
        mul_one]
    exact expCoeff_eq_of_eq_sum w hw hπ (n + 1) 1
      (fun j => if j = 0 then (1 : K) else 0) 0 hident n n.lt_succ_self
  map_mul' y z := by
    ext n
    rw [PowerSeries.coeff_mk]
    have hprod : ∀ d < n + 1,
        (PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ y))
            * PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ z))).coeff d
          = PowerSeries.coeff d
              (PowerSeries.mk (expCoeff w hw hπ y) * PowerSeries.mk (expCoeff w hw hπ z)) := by
      intro d hd
      rw [Polynomial.coeff_mul, PowerSeries.coeff_mul]
      refine Finset.sum_congr rfl fun x hx => ?_
      rw [Finset.HasAntidiagonal.mem_antidiagonal] at hx
      rw [PowerSeries.coeff_trunc, PowerSeries.coeff_trunc, ite_eq_left (by omega),
        ite_eq_left (by omega)]
    obtain ⟨Q, hQ⟩ : ∃ Q : Polynomial K,
        PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ y))
            * PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ z))
          = PowerSeries.trunc (n + 1)
              (PowerSeries.mk (expCoeff w hw hπ y) * PowerSeries.mk (expCoeff w hw hπ z))
            + Polynomial.X ^ (n + 1) * Q := by
      have hdvd : Polynomial.X ^ (n + 1) ∣
          (PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ y))
              * PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ z))
            - PowerSeries.trunc (n + 1)
                (PowerSeries.mk (expCoeff w hw hπ y)
                  * PowerSeries.mk (expCoeff w hw hπ z))) := by
        rw [Polynomial.X_pow_dvd_iff]
        intro d hd
        rw [Polynomial.coeff_sub, hprod d hd, PowerSeries.coeff_trunc, ite_eq_left hd, sub_self]
      obtain ⟨Q, hQ⟩ := hdvd
      refine ⟨Q, ?_⟩
      rw [← hQ]
      ring
    have hyev : y = Polynomial.eval₂ (algebraMap K w.toValuationSubring) π
          (PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ y)))
        + π ^ (n + 1) * remSeq w hw hπ y (n + 1) := by
      rw [PowerSeries.eval₂_trunc_eq_sum_range]
      simp only [PowerSeries.coeff_mk]
      exact remSeq_sum w hw hπ y (n + 1)
    have hzev : z = Polynomial.eval₂ (algebraMap K w.toValuationSubring) π
          (PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ z)))
        + π ^ (n + 1) * remSeq w hw hπ z (n + 1) := by
      rw [PowerSeries.eval₂_trunc_eq_sum_range]
      simp only [PowerSeries.coeff_mk]
      exact remSeq_sum w hw hπ z (n + 1)
    have hAB : Polynomial.eval₂ (algebraMap K w.toValuationSubring) π
          (PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ y)))
        * Polynomial.eval₂ (algebraMap K w.toValuationSubring) π
            (PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ z)))
        = (∑ k ∈ Finset.range (n + 1),
            algebraMap K w.toValuationSubring
                (PowerSeries.coeff k
                  (PowerSeries.mk (expCoeff w hw hπ y)
                    * PowerSeries.mk (expCoeff w hw hπ z)))
              * π ^ k)
          + π ^ (n + 1) * Polynomial.eval₂ (algebraMap K w.toValuationSubring) π Q := by
      rw [← Polynomial.eval₂_mul, hQ, Polynomial.eval₂_add, Polynomial.eval₂_mul,
        Polynomial.eval₂_X_pow, PowerSeries.eval₂_trunc_eq_sum_range]
    set p := π ^ (n + 1)
    set A := Polynomial.eval₂ (algebraMap K w.toValuationSubring) π
      (PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ y)))
    set B := Polynomial.eval₂ (algebraMap K w.toValuationSubring) π
      (PowerSeries.trunc (n + 1) (PowerSeries.mk (expCoeff w hw hπ z)))
    set ry := remSeq w hw hπ y (n + 1)
    set rz := remSeq w hw hπ z (n + 1)
    set EQ := Polynomial.eval₂ (algebraMap K w.toValuationSubring) π Q
    have hident : y * z
        = (∑ k ∈ Finset.range (n + 1),
            algebraMap K w.toValuationSubring
                (PowerSeries.coeff k
                  (PowerSeries.mk (expCoeff w hw hπ y)
                    * PowerSeries.mk (expCoeff w hw hπ z)))
              * π ^ k)
          + p * (EQ + (A * rz + ry * B + p * (ry * rz))) := by
      conv_lhs => rw [hyev, hzev]
      rw [show (A + p * ry) * (B + p * rz)
          = A * B + p * (A * rz + ry * B + p * (ry * rz)) from by ring, hAB]
      ring
    exact expCoeff_eq_of_eq_sum w hw hπ (n + 1) (y * z)
      (fun j => PowerSeries.coeff j
        (PowerSeries.mk (expCoeff w hw hπ y) * PowerSeries.mk (expCoeff w hw hπ z)))
      (EQ + (A * rz + ry * B + p * (ry * rz))) hident n n.lt_succ_self
  map_zero' := by
    ext n
    rw [PowerSeries.coeff_mk, map_zero]
    have hident : (0 : w.toValuationSubring)
        = (∑ k ∈ Finset.range (n + 1),
            algebraMap K w.toValuationSubring ((0 : K)) * π ^ k)
          + π ^ (n + 1) * 0 := by
      simp
    exact expCoeff_eq_of_eq_sum w hw hπ (n + 1) 0 (fun _ => (0 : K)) 0 hident n
      n.lt_succ_self
  map_add' y z := by
    ext n
    rw [PowerSeries.coeff_mk, map_add, PowerSeries.coeff_mk, PowerSeries.coeff_mk]
    have hident : y + z
        = (∑ k ∈ Finset.range (n + 1),
            algebraMap K w.toValuationSubring
                (expCoeff w hw hπ y k + expCoeff w hw hπ z k) * π ^ k)
          + π ^ (n + 1) * (remSeq w hw hπ y (n + 1) + remSeq w hw hπ z (n + 1)) := by
      conv_lhs => rw [remSeq_sum w hw hπ y (n + 1), remSeq_sum w hw hπ z (n + 1)]
      simp only [map_add, add_mul, Finset.sum_add_distrib, mul_add]
      ring
    exact expCoeff_eq_of_eq_sum w hw hπ (n + 1) (y + z)
      (fun j => expCoeff w hw hπ y j + expCoeff w hw hπ z j)
      _ hident n n.lt_succ_self

theorem

coeff_expPS

L301 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.coeff_expPS

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem coeff_expPS (w : Place K F) (hw : w.deg = 1) {π : w.toValuationSubring}
    (hπ : Irreducible π) (y : w.toValuationSubring) (n : ℕ) :
    PowerSeries.coeff n (expPS w hw hπ y) = expCoeff w hw hπ y n

theorem

expPS_algebraMap

L306 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.expPS_algebraMap

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem expPS_algebraMap (w : Place K F) (hw : w.deg = 1) {π : w.toValuationSubring}
    (hπ : Irreducible π) (a : K) :
    expPS w hw hπ (algebraMap K w.toValuationSubring a) = PowerSeries.C a

theorem

expPS_self

L319 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.expPS_self

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem expPS_self (w : Place K F) (hw : w.deg = 1) {π : w.toValuationSubring}
    (hπ : Irreducible π) : expPS w hw hπ π = PowerSeries.X

theorem

ord_coe_nonneg

L337 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.ord_coe_nonneg

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ord_coe_nonneg (w : Place K F) {y : w.toValuationSubring} (hy : y ≠ 0) :
    0 ≤ w.ord (y : F)

theorem

exists_unit_mul_pow

L360 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.exists_unit_mul_pow

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_unit_mul_pow (w : Place K F) {y : w.toValuationSubring} (hy : y ≠ 0)
    {π : w.toValuationSubring} (hπ : Irreducible π) :
    ∃ u : w.toValuationSubringˣ,
      y = (u : w.toValuationSubring) * π ^ (w.ord (y : F)).toNat

theorem

expCoeff_eq_zero_of_lt_ord

L372 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.expCoeff_eq_zero_of_lt_ord

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem expCoeff_eq_zero_of_lt_ord (w : Place K F) (hw : w.deg = 1)
    {π : w.toValuationSubring} (hπ : Irreducible π) {y : w.toValuationSubring} (hy : y ≠ 0)
    {n : ℕ} (hn : (n : ℤ) < w.ord (y : F)) : expCoeff w hw hπ y n = 0

theorem

expCoeff_ord_toNat_ne_zero

L384 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.expCoeff_ord_toNat_ne_zero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem expCoeff_ord_toNat_ne_zero (w : Place K F) (hw : w.deg = 1)
    {π : w.toValuationSubring} (hπ : Irreducible π) {y : w.toValuationSubring} (hy : y ≠ 0) :
    expCoeff w hw hπ y ((w.ord (y : F)).toNat) ≠ 0

theorem

ofPowerSeries_expPS_ne_zero

L413 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.ofPowerSeries_expPS_ne_zero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ofPowerSeries_expPS_ne_zero (w : Place K F) (hw : w.deg = 1)
    {π : w.toValuationSubring} (hπ : Irreducible π) {y : w.toValuationSubring} (hy : y ≠ 0) :
    HahnSeries.ofPowerSeries ℤ K (expPS w hw hπ y) ≠ 0

theorem

order_ofPowerSeries_expPS

L422 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.order_ofPowerSeries_expPS

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem order_ofPowerSeries_expPS (w : Place K F) (hw : w.deg = 1)
    {π : w.toValuationSubring} (hπ : Irreducible π) {y : w.toValuationSubring} (hy : y ≠ 0) :
    (HahnSeries.ofPowerSeries ℤ K (expPS w hw hπ y)).order = w.ord (y : F)

theorem

exists_irreducible_coe_of_ord_eq_one

L455 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.exists_irreducible_coe_of_ord_eq_one

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_irreducible_coe_of_ord_eq_one (w : Place K F) {t : F}
    (ht : w.ord t = 1) :
    ∃ tO : w.toValuationSubring, (tO : F) = t ∧ Irreducible tO

theorem

exists_algHom_laurentSeries_of_irreducible

L470 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.exists_algHom_laurentSeries_of_irreducible

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_algHom_laurentSeries_of_irreducible (w : Place K F) (hw : w.deg = 1)
    {π : w.toValuationSubring} (hπ : Irreducible π) :
    ∃ φ : F →ₐ[K] LaurentSeries K,
      φ (π : F) = HahnSeries.single (1 : ℤ) (1 : K) ∧ ∀ x : F, (φ x).order = w.ord x

theorem

exists_algHom_laurentSeries_of_deg_eq_one

L516 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.exists_algHom_laurentSeries_of_deg_eq_one

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in

Lean source · statement

theorem AlgebraicCurve.Place.exists_algHom_laurentSeries_of_deg_eq_one
    {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F) (hw : w.deg = 1)
    (t : F) (ht : w.ord t = 1) :
    ∃ φ : F →ₐ[K] LaurentSeries K,
      φ t = HahnSeries.single (1 : ℤ) (1 : K) ∧ ∀ x : F, (φ x).order = w.ord x

theorem

exists_algHom_laurentSeries_order_eq_ord_aux

L525 ↗

AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord.AlgebraicCurve.Place.exists_algHom_laurentSeries_order_eq_ord_aux

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
open _root_.ModularCurve
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in

Lean source · statement

theorem AlgebraicCurve.Place.exists_algHom_laurentSeries_order_eq_ord_aux
    {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F) (hw : w.deg = 1) :
    ∃ φ : F →ₐ[K] LaurentSeries K, ∀ x : F, (φ x).order = w.ord x

theorem

exists_algHom_laurentSeries_order_eq_ord

L535 ↗

AlgebraicCurve.Place.exists_algHom_laurentSeries_order_eq_ord

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algHom_laurentSeries_order_eq_ord
open _root_.AlgebraicCurve AlgebraicCurve ModularCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.exists_algHom_laurentSeries_order_eq_ord {K F : Type*} [Field
  K] [Field F] [Algebra K F] (w : Place K F) (hw : w.deg = 1) :
    ∃ φ : F →ₐ[K] LaurentSeries K, ∀ x : F, (φ x).order = w.ord x

Module documentation

Place exists alg Hom laurent Series order eq ord

Declarations