Module

ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div

62 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring exists aeval div eq aeval div add aeval inv div

Imports21

Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Mathlib.Algebra.Order.Antidiag.Prod
Mathlib.Algebra.Order.GroupWithZero.Basic
Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.Algebra.Polynomial.Basic
Mathlib.Algebra.Polynomial.Degree.Defs
Mathlib.Algebra.Polynomial.Degree.Operations
Mathlib.Algebra.Polynomial.Eval.Defs
Mathlib.Algebra.Polynomial.Roots
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.RingTheory.Algebraic.Basic
Mathlib.RingTheory.Valuation.Basic
Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.Tactic.Choose
Mathlib.Tactic.FieldSimp
Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.Push
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.SplitIfs
Mathlib.Algebra.Polynomial.Inductions

Imported by2

def

ACoeff

L51 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff

Documentation

The condition that all coefficients of a polynomial belong to the valuation ring.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

def ACoeff (p : L[X]) : Prop

theorem

zero

L53 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff.zero

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem ACoeff.zero : ACoeff A (0 : L[X])

theorem

one

L55 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff.one

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem ACoeff.one : ACoeff A (1 : L[X])

theorem

C

L58 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff.C

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem ACoeff.C {a : L} (ha : a ∈ A) : ACoeff A (C a)

theorem

X

L61 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff.X

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem ACoeff.X : ACoeff A (X : L[X])

theorem

add

L64 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff.add

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem ACoeff.add {p q : L[X]} (hp : ACoeff A p) (hq : ACoeff A q) : ACoeff A (p + q)

theorem

neg

L67 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff.neg

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem ACoeff.neg {p : L[X]} (hp : ACoeff A p) : ACoeff A (-p)

theorem

sub

L70 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff.sub

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem ACoeff.sub {p q : L[X]} (hp : ACoeff A p) (hq : ACoeff A q) : ACoeff A (p - q)

theorem

mul

L73 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff.mul

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem ACoeff.mul {p q : L[X]} (hp : ACoeff A p) (hq : ACoeff A q) : ACoeff A (p * q)

theorem

multiset_prod

L79 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff.multiset_prod

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem ACoeff.multiset_prod {ι : Type*} (s : Multiset ι) (g : ι → L[X])
    (hg : ∀ i ∈ s, ACoeff A (g i)) : ACoeff A (s.map g).prod

theorem

divX

L88 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff.divX

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem ACoeff.divX {p : L[X]} (hp : ACoeff A p) : ACoeff A (divX p)

theorem

valuation_le

L91 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.ACoeff.valuation_le

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem ACoeff.valuation_le {p : L[X]} (hp : ACoeff A p) (j : ℕ) :
    A.valuation (p.coeff j) ≤ 1

theorem

acoeff_of_valuation_le

L95 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.acoeff_of_valuation_le

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem acoeff_of_valuation_le {p : L[X]} (hp : ∀ j, A.valuation (p.coeff j) ≤ 1) :
    ACoeff A p

def

IsGood

L99 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsGood

Documentation

A polynomial with unit-valued constant coefficient and strictly smaller other coefficients.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

def IsGood (t : L[X]) : Prop

theorem

valuation_le

L102 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsGood.valuation_le

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem IsGood.valuation_le {t : L[X]} (ht : IsGood A t) (j : ℕ) :
    A.valuation (t.coeff j) ≤ 1

theorem

acoeff

L108 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsGood.acoeff

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem IsGood.acoeff {t : L[X]} (ht : IsGood A t) : ACoeff A t

theorem

coeff_zero_ne

L111 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsGood.coeff_zero_ne

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem IsGood.coeff_zero_ne {t : L[X]} (ht : IsGood A t) : t.coeff 0 ≠ 0

theorem

ne_zero

L114 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsGood.ne_zero

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem IsGood.ne_zero {t : L[X]} (ht : IsGood A t) : t ≠ 0

theorem

one

L117 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsGood.one

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem IsGood.one : IsGood A (1 : L[X])

theorem

one_sub

L121 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsGood.one_sub

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem IsGood.one_sub {c : L} (hc : A.valuation c < 1) :
    IsGood A (1 - Polynomial.C c * Polynomial.X : L[X])

theorem

mul

L130 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsGood.mul

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem IsGood.mul {t s : L[X]} (ht : IsGood A t) (hs : IsGood A s) : IsGood A (t * s)

theorem

multiset_prod_one_sub

L147 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsGood.multiset_prod_one_sub

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · full declaration

theorem IsGood.multiset_prod_one_sub (rs : Multiset L) (hrs : ∀ r ∈ rs, A.valuation r < 1) :
    IsGood A (rs.map fun r => (1 - Polynomial.C r * Polynomial.X : L[X])).prod := by
  induction rs using Multiset.induction_on with
  | empty => simpa using IsGood.one A
  | cons a s ih =>
    rw [Multiset.map_cons, Multiset.prod_cons]
    exact IsGood.mul A (IsGood.one_sub A (hrs a (Multiset.mem_cons_self _ _)))
      (ih fun r hr => hrs r (Multiset.mem_cons_of_mem hr))

theorem

coeff_zero_multiset_prod_one_sub

L156 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.coeff_zero_multiset_prod_one_sub

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · full declaration

theorem coeff_zero_multiset_prod_one_sub (rs : Multiset L) :
    ((rs.map fun r => (1 - Polynomial.C r * Polynomial.X : L[X])).prod).coeff 0 = 1 := by
  induction rs using Multiset.induction_on with
  | empty => simp
  | cons a s ih => rw [Multiset.map_cons, Multiset.prod_cons, mul_coeff_zero, ih]; simp

theorem

one_lt_valuation_of_isRoot

L162 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsGood.one_lt_valuation_of_isRoot

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem IsGood.one_lt_valuation_of_isRoot {t : L[X]} (ht : IsGood A t) {ρ : L}
    (hρ : t.IsRoot ρ) : 1 < A.valuation ρ

theorem

valuation_ne_one_of_isRoot

L184 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.valuation_ne_one_of_isRoot

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem valuation_ne_one_of_isRoot {t : L[X]} {d : ℕ} (hd : A.valuation (t.coeff d) = 1)
    (ht : ∀ j, j ≠ d → A.valuation (t.coeff j) < 1) {ρ : L} (hρ : t.IsRoot ρ) :
    A.valuation ρ ≠ 1

theorem

prod_X_sub_C_eq_C_mul_prod_one_sub

L210 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.prod_X_sub_C_eq_C_mul_prod_one_sub

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · full declaration

theorem prod_X_sub_C_eq_C_mul_prod_one_sub (s : Multiset L) (hs : ∀ ρ ∈ s, ρ ≠ 0) :
    (s.map fun ρ => (X - C ρ : L[X])).prod =
      C (s.map fun ρ => -ρ).prod * ((s.map fun ρ => ρ⁻¹).map fun r => (1 - C r * X : L[X])).prod :=
        by
  rw [map_multiset_prod C, Multiset.map_map, Multiset.map_map, ← Multiset.prod_map_mul]
  refine congr_arg _ (Multiset.map_congr rfl fun ρ hρ => ?_)
  simp only [Function.comp_apply]
  have hρ0 : ρ ≠ 0 := hs ρ hρ
  have : C (-ρ) * (1 - C ρ⁻¹ * X) = X - C ρ := by
    have h1 : C ρ * C ρ⁻¹ = (1 : L[X]) := by rw [← C_mul, mul_inv_cancel₀ hρ0, C_1]
    rw [C_neg]
    linear_combination X * h1
  exact this.symm

theorem

exists_eq_C_mul_prod

L226 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsGood.exists_eq_C_mul_prod

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]

Lean source · full declaration

theorem IsGood.exists_eq_C_mul_prod {s : L[X]} (hs : IsGood A s) :
    ∃ rs : Multiset L, (∀ r ∈ rs, A.valuation r < 1) ∧
      s = C (s.coeff 0) * (rs.map fun r => (1 - C r * X : L[X])).prod := by
  classical
  have hs0 := hs.ne_zero A
  have hsplit : C s.leadingCoeff * (s.roots.map fun a => X - C a).prod = s :=
    C_leadingCoeff_mul_prod_multiset_X_sub_C IsAlgClosed.card_roots_eq_natDegree
  have hroots : ∀ ρ ∈ s.roots, 1 < A.valuation ρ := fun ρ hρ =>
    hs.one_lt_valuation_of_isRoot A ((mem_roots hs0).mp hρ)
  have hroots0 : ∀ ρ ∈ s.roots, ρ ≠ 0 := by
    intro ρ hρ h; have := hroots ρ hρ; rw [h, map_zero] at this
    exact absurd this (not_lt.mpr zero_le)
  refine ⟨s.roots.map fun ρ => ρ⁻¹, ?_, ?_⟩
  · intro r hr
    rw [Multiset.mem_map] at hr
    obtain ⟨ρ, hρ, rfl⟩ := hr
    have h1 := hroots ρ hρ
    rw [map_inv₀]
    exact inv_lt_one_of_one_lt₀ h1
  · set P := ((s.roots.map fun ρ => ρ⁻¹).map fun r => (1 - C r * X : L[X])).prod with hP
    have hfac : s = C (s.leadingCoeff * (s.roots.map fun ρ => -ρ).prod) * P := by
      conv_lhs => rw [← hsplit]
      rw [prod_X_sub_C_eq_C_mul_prod_one_sub s.roots hroots0, ← mul_assoc, ← C_mul]
    have hc0 : s.coeff 0 = s.leadingCoeff * (s.roots.map fun ρ => -ρ).prod := by
      conv_lhs => rw [hfac]
      rw [coeff_C_mul, hP, coeff_zero_multiset_prod_one_sub, mul_one]
    rw [hc0]
    exact hfac

theorem

exists_eq_C_mul_prod_mul_prod

L255 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.exists_eq_C_mul_prod_mul_prod

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]

Lean source · full declaration

theorem exists_eq_C_mul_prod_mul_prod {t : L[X]} {d : ℕ} (hd : A.valuation (t.coeff d) = 1)
    (ht : ∀ j, j ≠ d → A.valuation (t.coeff j) < 1) :
    ∃ (u : L) (sm : Multiset L) (cs : Multiset L),
      u ≠ 0 ∧ 1 ≤ A.valuation u ∧ (∀ ρ ∈ sm, A.valuation ρ < 1) ∧ (∀ c ∈ cs, A.valuation c < 1) ∧
      t = C u * (sm.map fun ρ => (X - C ρ : L[X])).prod *
        (cs.map fun c => (1 - C c * X : L[X])).prod := by
  classical
  have htd : t.coeff d ≠ 0 := by
    intro h; rw [h, map_zero] at hd; exact zero_ne_one hd
  have ht0 : t ≠ 0 := fun h => htd (by rw [h, coeff_zero])
  have hsplit : C t.leadingCoeff * (t.roots.map fun a => X - C a).prod = t :=
    C_leadingCoeff_mul_prod_multiset_X_sub_C IsAlgClosed.card_roots_eq_natDegree
  set sm := t.roots.filter fun ρ => A.valuation ρ < 1 with hsm
  set lg := t.roots.filter fun ρ => ¬ A.valuation ρ < 1 with hlg
  have hsplit2 : t.roots = sm + lg := (Multiset.filter_add_not _ _).symm
  have hlg1 : ∀ ρ ∈ lg, 1 < A.valuation ρ := by
    intro ρ hρ
    rw [hlg, Multiset.mem_filter] at hρ
    have hne := valuation_ne_one_of_isRoot A hd ht ((mem_roots ht0).mp hρ.1)
    exact lt_of_le_of_ne (not_lt.mp hρ.2) (Ne.symm hne)
  have hlg0 : ∀ ρ ∈ lg, ρ ≠ 0 := by
    intro ρ hρ h; have := hlg1 ρ hρ; rw [h, map_zero] at this
    exact absurd this (not_lt.mpr zero_le)
  set u : L := t.leadingCoeff * (lg.map fun ρ => -ρ).prod with hu
  set cs : Multiset L := lg.map fun ρ => ρ⁻¹ with hcs
  have hcs1 : ∀ c ∈ cs, A.valuation c < 1 := by
    intro c hc
    rw [hcs, Multiset.mem_map] at hc
    obtain ⟨ρ, hρ, rfl⟩ := hc
    rw [map_inv₀]
    exact inv_lt_one_of_one_lt₀ (hlg1 ρ hρ)
  have hsm1 : ∀ ρ ∈ sm, A.valuation ρ < 1 := by
    intro ρ hρ; rw [hsm, Multiset.mem_filter] at hρ; exact hρ.2
  set P : L[X] := (sm.map fun ρ => (X - C ρ : L[X])).prod *
    (cs.map fun c => (1 - C c * X : L[X])).prod with hP
  have hfac : t = C u * P := by
    conv_lhs => rw [← hsplit, hsplit2, Multiset.map_add, Multiset.prod_add,
      prod_X_sub_C_eq_C_mul_prod_one_sub lg hlg0]
    rw [hP, hu, hcs, C_mul]
    ring
  have hu0 : u ≠ 0 := by
    intro h; apply ht0; rw [hfac, h, C_0, zero_mul]
  have hPA : ACoeff A P := by
    apply ACoeff.mul
    · apply ACoeff.multiset_prod
      intro ρ hρ
      exact ACoeff.sub A (ACoeff.X A) (ACoeff.C A ((A.valuation_le_one_iff _).mp (hsm1 ρ hρ).le))
    · exact (IsGood.multiset_prod_one_sub A cs hcs1).acoeff A
  have hu1 : 1 ≤ A.valuation u := by
    have h1 : t.coeff d = u * P.coeff d := by
      conv_lhs => rw [hfac]
      rw [coeff_C_mul]
    have h2 : A.valuation (t.coeff d) ≤ A.valuation u * 1 := by
      rw [h1, map_mul]
      gcongr
      exact hPA.valuation_le A d
    rw [hd, mul_one] at h2
    exact h2
  exact ⟨u, sm, cs, hu0, hu1, hsm1, hcs1, by rw [hfac, hP, mul_assoc]⟩

theorem

aeval_ne_zero_of_isGood

L318 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.aeval_ne_zero_of_isGood

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
omit [IsAlgClosed L] in

Lean source · statement

theorem aeval_ne_zero_of_isGood {F : Type*} [Field F] [Algebra L F] {g : F}
    (hg : Transcendental L g) {t : L[X]} (ht : IsGood A t) : aeval g t ≠ 0

def

IsLam

L326 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsLam

Documentation

The condition of admitting a polynomial fraction with a good denominator at the given element.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]

Lean source · statement

def IsLam (g x : F) : Prop

def

InM

L330 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM

Documentation

The condition of being a sum of fractions regular in the element and its inverse.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]

Lean source · statement

def InM (g x : F) : Prop

theorem

isLam_aeval

L333 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.isLam_aeval

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem isLam_aeval (g : F) {p : L[X]} (hp : ACoeff A p) : IsLam A g (aeval g p)

theorem

isLam_algebraMap

L336 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.isLam_algebraMap

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem isLam_algebraMap (g : F) {a : L} (ha : a ∈ A) : IsLam A g (algebraMap L F a)

theorem

isLam_zero

L340 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.isLam_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem isLam_zero (g : F) : IsLam A g 0

theorem

isLam_one

L344 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.isLam_one

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem isLam_one (g : F) : IsLam A g 1

theorem

add

L348 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsLam.add

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem IsLam.add {g x y : F} (hx : IsLam A g x) (hy : IsLam A g y) : IsLam A g (x + y)

theorem

mul

L357 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsLam.mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem IsLam.mul {g x y : F} (hx : IsLam A g x) (hy : IsLam A g y) : IsLam A g (x * y)

theorem

mul_self

L364 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsLam.mul_self

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem IsLam.mul_self {g x : F} (hx : IsLam A g x) : IsLam A g (g * x)

theorem

exists_eq_add_mul

L370 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsLam.exists_eq_add_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem IsLam.exists_eq_add_mul {g x : F} (hg : Transcendental L g) (hx : IsLam A g x) :
    ∃ a ∈ A, ∃ x', IsLam A g x' ∧ x = algebraMap L F a + g * x'

theorem

exists_mul_one_sub_eq

L394 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.IsLam.exists_mul_one_sub_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem IsLam.exists_mul_one_sub_eq {g x : F} (hg : Transcendental L g) (hx : IsLam A g x)
    {c : L} (hc : A.valuation c < 1) :
    ∃ x', IsLam A g x' ∧ x' * (1 - algebraMap L F c * g) = x

theorem

isLam_of_mul_prod_eq

L409 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.isLam_of_mul_prod_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · full declaration

theorem isLam_of_mul_prod_eq {g x : F} (rs : Multiset L) (hrs : ∀ r ∈ rs, A.valuation r < 1)
    {q : L[X]} (hq : ACoeff A q)
    (h : x * (rs.map fun r => 1 - algebraMap L F r * g).prod = aeval g q) : IsLam A g x := by
  refine ⟨q, (rs.map fun r => (1 - Polynomial.C r * X : L[X])).prod, hq,
    IsGood.multiset_prod_one_sub A rs hrs, ?_⟩
  rw [← h, map_multiset_prod, Multiset.map_map]
  congr 2
  refine Multiset.map_congr rfl fun r _ => ?_
  simp

theorem

inM_symm

L419 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.inM_symm

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem inM_symm {g x : F} : InM A g x ↔ InM A g⁻¹ x

theorem

of_isLam

L424 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.of_isLam

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem InM.of_isLam {g x : F} (hx : IsLam A g x) : InM A g x

theorem

of_isLam_inv

L427 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.of_isLam_inv

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem InM.of_isLam_inv {g x : F} (hx : IsLam A g⁻¹ x) : InM A g x

theorem

inM_zero

L430 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.inM_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem inM_zero (g : F) : InM A g 0

theorem

add

L432 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.add

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem InM.add {g x y : F} (hx : InM A g x) (hy : InM A g y) : InM A g (x + y)

theorem

smul

L437 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.smul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem InM.smul {g x : F} (hx : InM A g x) {a : L} (ha : a ∈ A) : InM A g (algebraMap L F a * x)

theorem

sum

L442 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.sum

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem InM.sum {g : F} {ι : Type*} (s : Finset ι) (x : ι → F) (hx : ∀ i ∈ s, InM A g (x i)) :
    InM A g (∑ i ∈ s, x i)

theorem

mul_self

L452 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.mul_self

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem InM.mul_self {g x : F} (hg : Transcendental L g) (hg0 : g ≠ 0) (hx : InM A g x) :
    InM A g (g * x)

theorem

mul_inv_self

L462 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.mul_inv_self

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem InM.mul_inv_self {g x : F} (hg : Transcendental L g) (hg0 : g ≠ 0) (hx : InM A g x) :
    InM A g (g⁻¹ * x)

theorem

mul_pow

L468 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.mul_pow

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem InM.mul_pow {g x : F} (hg : Transcendental L g) (hg0 : g ≠ 0) (hx : InM A g x) (n : ℕ) :
    InM A g (g ^ n * x)

theorem

mul_inv_pow

L474 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.mul_inv_pow

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem InM.mul_inv_pow {g x : F} (hg : Transcendental L g) (hg0 : g ≠ 0) (hx : InM A g x) (n : ℕ) :
    InM A g (g⁻¹ ^ n * x)

theorem

mul_aeval

L480 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.mul_aeval

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem InM.mul_aeval {g x : F} (hg : Transcendental L g) (hg0 : g ≠ 0) (hx : InM A g x)
    {p : L[X]} (hp : ACoeff A p) : InM A g (aeval g p * x)

theorem

aeval_prod_one_sub

L487 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.aeval_prod_one_sub

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · full declaration

theorem aeval_prod_one_sub (g : F) (rs : Multiset L) :
    aeval g ((rs.map fun r => (1 - Polynomial.C r * X : L[X])).prod) =
      (rs.map fun r => 1 - algebraMap L F r * g).prod := by
  rw [map_multiset_prod, Multiset.map_map]
  congr 1
  refine Multiset.map_congr rfl fun r _ => ?_
  simp

theorem

exists_inM_mul_one_sub_eq_inv_pow

L495 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.exists_inM_mul_one_sub_eq_inv_pow

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · statement

theorem exists_inM_mul_one_sub_eq_inv_pow {g : F} (hg : Transcendental L g) (hg0 : g ≠ 0)
    {c : L} (hc : A.valuation c < 1) (j : ℕ) :
    ∃ w, InM A g w ∧ w * (1 - algebraMap L F c * g) = g⁻¹ ^ j

theorem

exists_inM_mul_one_sub_eq_of_fac

L507 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.exists_inM_mul_one_sub_eq_of_fac

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]
omit [IsAlgClosed L] in

Lean source · full declaration

theorem exists_inM_mul_one_sub_eq_of_fac {g : F} (hg : Transcendental L g) (hg0 : g ≠ 0)
    {c : L} (hc : A.valuation c < 1) (rs : Multiset L) :
    ∀ (z : F) (q : L[X]), (∀ r ∈ rs, A.valuation r < 1) → ACoeff A q →
      z * (rs.map fun r => 1 - algebraMap L F r * g⁻¹).prod = aeval g⁻¹ q →
      ∃ z'', InM A g z'' ∧ z'' * (1 - algebraMap L F c * g) = z := by
  induction rs using Multiset.induction_on with
  | empty =>
    intro z q _ hq h
    simp only [Multiset.map_zero, Multiset.prod_zero, mul_one] at h
    choose w hw hwe using fun j => exists_inM_mul_one_sub_eq_inv_pow A hg hg0 hc j
    refine ⟨∑ j ∈ Finset.range (q.natDegree + 1), algebraMap L F (q.coeff j) * w j,
      InM.sum A _ _ fun j _ => (hw j).smul A (hq j), ?_⟩
    rw [h, aeval_eq_sum_range, Finset.sum_mul]
    refine Finset.sum_congr rfl fun j _ => ?_
    rw [mul_assoc, hwe, Algebra.smul_def]
  | cons r rs ih =>
    intro z q hrs hq h
    have hgi : Transcendental L g⁻¹ := fun h => hg (IsAlgebraic.inv_iff.mp h)
    have hr : A.valuation r < 1 := hrs r (Multiset.mem_cons_self _ _)
    have hrs' : ∀ r' ∈ rs, A.valuation r' < 1 := fun r' hr' => hrs r' (Multiset.mem_cons_of_mem hr')
    have hzL : IsLam A g⁻¹ z := isLam_of_mul_prod_eq A (r ::ₘ rs) hrs hq h
    obtain ⟨z₁, hz₁⟩ : ∃ z₁ : F, z₁ = z * (1 - algebraMap L F r * g⁻¹) := ⟨_, rfl⟩
    have hz₁e : z₁ * (rs.map fun r => 1 - algebraMap L F r * g⁻¹).prod = aeval g⁻¹ q := by
      rw [← h, Multiset.map_cons, Multiset.prod_cons, hz₁]
      ring
    obtain ⟨z₁'', hz₁'', hz₁''e⟩ := ih z₁ q hrs' hq hz₁e
    have hrc : A.valuation (r * c) < 1 := by
      rw [map_mul]
      calc A.valuation r * A.valuation c ≤ 1 * A.valuation c := mul_le_mul_left hr.le _
        _ < 1 := by rw [one_mul]; exact hc
    have h1rc : A.valuation (1 - r * c) = 1 := Valuation.map_one_sub_of_lt _ hrc
    have h1rc0 : (1 - r * c) ≠ 0 := by
      intro h0; rw [h0, map_zero] at h1rc; exact zero_ne_one h1rc
    set Q : L := (1 - r * c)⁻¹ with hQ
    have hQA : Q ∈ A := by
      rw [← A.valuation_le_one_iff, hQ, map_inv₀, h1rc, inv_one]
    have hrQA : r * Q ∈ A := by
      rw [← A.valuation_le_one_iff, map_mul]
      calc A.valuation r * A.valuation Q ≤ 1 * 1 :=
            mul_le_mul' hr.le ((A.valuation_le_one_iff _).mpr hQA)
        _ = 1 := one_mul 1
    have hQe : algebraMap L F Q * (1 - algebraMap L F r * algebraMap L F c) = 1 := by
      rw [← map_mul, ← map_one (algebraMap L F), ← map_sub, ← map_mul, hQ,
        inv_mul_cancel₀ h1rc0]
    have hginv : g⁻¹ * g = 1 := inv_mul_cancel₀ hg0
    refine ⟨algebraMap L F Q * z₁'' + algebraMap L F (r * Q) * (g⁻¹ * z),
      (hz₁''.smul A hQA).add A ((InM.of_isLam_inv A (hzL.mul_self A)).smul A hrQA), ?_⟩
    rw [map_mul]
    rw [hz₁] at hz₁''e
    linear_combination (algebraMap L F Q) * hz₁''e
      - (algebraMap L F r * algebraMap L F Q * algebraMap L F c * z) * hginv + z * hQe

theorem

exists_mul_one_sub_eq

L559 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.exists_mul_one_sub_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]

Lean source · statement

theorem InM.exists_mul_one_sub_eq {g x : F} (hg : Transcendental L g) (hg0 : g ≠ 0)
    (hx : InM A g x) {c : L} (hc : A.valuation c < 1) :
    ∃ x', InM A g x' ∧ x' * (1 - algebraMap L F c * g) = x

theorem

exists_mul_one_sub_inv_eq

L584 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.exists_mul_one_sub_inv_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]

Lean source · statement

theorem InM.exists_mul_one_sub_inv_eq {g x : F} (hg : Transcendental L g) (hg0 : g ≠ 0)
    (hx : InM A g x) {r : L} (hr : A.valuation r < 1) :
    ∃ x', InM A g x' ∧ x' * (1 - algebraMap L F r * g⁻¹) = x

theorem

exists_mul_prod_eq

L592 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.exists_mul_prod_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]

Lean source · full declaration

theorem InM.exists_mul_prod_eq {g x : F} (hg : Transcendental L g) (hg0 : g ≠ 0)
    (hx : InM A g x) (cs : Multiset L) (hcs : ∀ c ∈ cs, A.valuation c < 1) :
    ∃ x', InM A g x' ∧ x' * (cs.map fun c => 1 - algebraMap L F c * g).prod = x := by
  induction cs using Multiset.induction_on with
  | empty => exact ⟨x, hx, by simp⟩
  | cons c cs ih =>
    obtain ⟨x₁, hx₁, hx₁e⟩ := ih fun c' hc' => hcs c' (Multiset.mem_cons_of_mem hc')
    obtain ⟨x₂, hx₂, hx₂e⟩ := hx₁.exists_mul_one_sub_eq A hg hg0 (hcs c (Multiset.mem_cons_self _
      _))
    refine ⟨x₂, hx₂, ?_⟩
    rw [Multiset.map_cons, Multiset.prod_cons, ← mul_assoc, hx₂e, hx₁e]

theorem

exists_mul_prod_inv_eq

L604 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.InM.exists_mul_prod_inv_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]

Lean source · full declaration

theorem InM.exists_mul_prod_inv_eq {g x : F} (hg : Transcendental L g) (hg0 : g ≠ 0)
    (hx : InM A g x) (rs : Multiset L) (hrs : ∀ r ∈ rs, A.valuation r < 1) :
    ∃ x', InM A g x' ∧ x' * (rs.map fun r => 1 - algebraMap L F r * g⁻¹).prod = x := by
  induction rs using Multiset.induction_on with
  | empty => exact ⟨x, hx, by simp⟩
  | cons r rs ih =>
    obtain ⟨x₁, hx₁, hx₁e⟩ := ih fun r' hr' => hrs r' (Multiset.mem_cons_of_mem hr')
    obtain ⟨x₂, hx₂, hx₂e⟩ := hx₁.exists_mul_one_sub_inv_eq A hg hg0
      (hrs r (Multiset.mem_cons_self _ _))
    refine ⟨x₂, hx₂, ?_⟩
    rw [Multiset.map_cons, Multiset.prod_cons, ← mul_assoc, hx₂e, hx₁e]

theorem

inM_aeval_div

L616 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div.P1aSol.inM_aeval_div

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
namespace P1aSol
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]
section Charts
variable {F : Type*} [Field F] [Algebra L F]

Lean source · statement

theorem inM_aeval_div {f : F} (hf : Transcendental L f) {p t : L[X]} (hp : ACoeff A p)
    {d : ℕ} (hd : A.valuation (t.coeff d) = 1) (ht : ∀ j, j ≠ d → A.valuation (t.coeff j) < 1) :
    InM A f (aeval f p / aeval f t)

theorem

exists_aeval_div_eq_aeval_div_add_aeval_inv_div

L670 ↗

ValuationSubring.exists_aeval_div_eq_aeval_div_add_aeval_inv_div

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
open Polynomial
open P1aSol in

Lean source · statement

theorem _root_.ValuationSubring.exists_aeval_div_eq_aeval_div_add_aeval_inv_div
    {L : Type*} [Field L] [IsAlgClosed L] (A : ValuationSubring L)
    {F : Type*} [Field F] [Algebra L F] {f : F} (hf : Transcendental L f)
    (p t : L[X]) (hp : ∀ j, p.coeff j ∈ A)
    (ht : ∃ d, A.valuation (t.coeff d) = 1 ∧ ∀ j, j ≠ d → A.valuation (t.coeff j) < 1) :
    ∃ p₁ t₁ q s : L[X],
      (∀ j, p₁.coeff j ∈ A) ∧ (∀ j, q.coeff j ∈ A) ∧
      (A.valuation (t₁.coeff 0) = 1 ∧ ∀ j, j ≠ 0 → A.valuation (t₁.coeff j) < 1) ∧
      (A.valuation (s.coeff 0) = 1 ∧ ∀ j, j ≠ 0 → A.valuation (s.coeff j) < 1) ∧
      aeval f p / aeval f t = aeval f p₁ / aeval f t₁ + aeval f⁻¹ q / aeval f⁻¹ s

Module documentation

Valuation Subring exists aeval div eq aeval div add aeval inv div

Declarations