NYLL
Module

ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
16 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring exists eq algebra Map of forall valuation Subring mul aeval mem

Imports22
  • Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  • Mathlib.Algebra.Order.GroupWithZero.Basic
  • Mathlib.Algebra.Polynomial.AlgebraMap
  • Mathlib.Algebra.Polynomial.Basic
  • Mathlib.Algebra.Polynomial.Degree.SmallDegree
  • Mathlib.Algebra.Polynomial.Eval.Defs
  • Mathlib.Algebra.Polynomial.Roots
  • Mathlib.Algebra.Ring.GeomSum
  • Mathlib.Algebra.Ring.Subring.Basic
  • Mathlib.FieldTheory.IsAlgClosed.Basic
  • Mathlib.FieldTheory.Minpoly.Basic
  • Mathlib.FieldTheory.Minpoly.Field
  • Mathlib.RingTheory.Algebraic.Basic
  • Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
  • Mathlib.RingTheory.Valuation.Basic
  • Mathlib.RingTheory.Valuation.LocalSubring
  • Mathlib.RingTheory.Valuation.ValuationSubring
  • Mathlib.Tactic.FieldSimp
  • Mathlib.Tactic.GCongr.Core
  • Mathlib.Tactic.LinearCombination
  • Mathlib.Tactic.Push
  • Mathlib.Tactic.Ring.RingNF
Imported by1

Declarations

def

IsGood

L52 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.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_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
variable {L : Type*} [Field L] (A : ValuationSubring L)
Lean source · statement
def IsGood (t : L[X]) : Prop
theorem

valuation_le

L55 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.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_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
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

coeff_mem

L61 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.IsGood.coeff_mem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
variable {L : Type*} [Field L] (A : ValuationSubring L)
Lean source · statement
theorem IsGood.coeff_mem {t : L[X]} (ht : IsGood A t) (j : ℕ) : t.coeff j ∈ A
theorem

coeff_zero_ne

L64 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.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_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
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

L67 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.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_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
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

valuation_eval_eq_one

L70 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.IsGood.valuation_eval_eq_one
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
variable {L : Type*} [Field L] (A : ValuationSubring L)
Lean source · statement
theorem IsGood.valuation_eval_eq_one {t : L[X]} (ht : IsGood A t) {c : L}
    (hc : A.valuation c < 1) : A.valuation (t.eval c) = 1
theorem

one_lt_valuation_of_isRoot

L84 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.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_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
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

prod_X_sub_C_eq_C_mul_prod_one_sub

L106 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.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_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
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

L120 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.IsGood.exists_eq_C_mul_prod
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
variable {L : Type*} [Field L] (A : ValuationSubring L)
Lean source · full declaration
theorem IsGood.exists_eq_C_mul_prod [IsAlgClosed L] {t : L[X]} (ht : IsGood A t) :
    ∃ (u : L) (cs : Multiset L), u ≠ 0 ∧ (∀ c ∈ cs, A.valuation c < 1) ∧
      t = C u * (cs.map fun c => (1 - C c * X : L[X])).prod := by
  classical
  have ht0 := ht.ne_zero A
  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
  have hroots : ∀ ρ ∈ t.roots, 1 < A.valuation ρ := fun ρ hρ =>
    ht.one_lt_valuation_of_isRoot A ((mem_roots ht0).mp hρ)
  have hroots0 : ∀ ρ ∈ t.roots, ρ ≠ 0 := by
    intro ρ hρ h; have := hroots ρ hρ; rw [h, map_zero] at this
    exact absurd this (not_lt.mpr zero_le)
  refine ⟨t.leadingCoeff * (t.roots.map fun ρ => -ρ).prod, t.roots.map fun ρ => ρ⁻¹, ?_, ?_, ?_⟩
  · refine mul_ne_zero (leadingCoeff_ne_zero.mpr ht0) ?_
    rw [ne_eq, Multiset.prod_eq_zero_iff, Multiset.mem_map]
    rintro ⟨ρ, hρ, h⟩
    exact hroots0 ρ hρ (neg_eq_zero.mp h)
  · intro r hr
    rw [Multiset.mem_map] at hr
    obtain ⟨ρ, hρ, rfl⟩ := hr
    rw [map_inv₀]
    exact inv_lt_one_of_one_lt₀ (hroots ρ hρ)
  · conv_lhs => rw [← hsplit, prod_X_sub_C_eq_C_mul_prod_one_sub t.roots hroots0]
    rw [C_mul, mul_assoc]
theorem

valuation_algebraMap_eq_one

L150 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.valuation_algebraMap_eq_one
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
variable {L : Type*} [Field L] (A : ValuationSubring L)
section Field
variable {F : Type*} [Field F] [Algebra L F]
omit A in
Lean source · statement
theorem valuation_algebraMap_eq_one (V : ValuationSubring F) (hV : ∀ c : L, algebraMap L F c ∈ V)
    {c : L} (hc : c ≠ 0) : V.valuation (algebraMap L F c) = 1
theorem

valuation_algebraMap_le_one

L166 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.valuation_algebraMap_le_one
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
variable {L : Type*} [Field L] (A : ValuationSubring L)
section Field
variable {F : Type*} [Field F] [Algebra L F]
omit A in
Lean source · statement
theorem valuation_algebraMap_le_one (V : ValuationSubring F) (hV : ∀ c : L, algebraMap L F c ∈ V)
    (c : L) : V.valuation (algebraMap L F c) ≤ 1
theorem

valuation_aeval_eq_one_of_lt

L170 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.valuation_aeval_eq_one_of_lt
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
variable {L : Type*} [Field L] (A : ValuationSubring L)
section Field
variable {F : Type*} [Field F] [Algebra L F]
Lean source · statement
theorem valuation_aeval_eq_one_of_lt (V : ValuationSubring F) (hV : ∀ c : L, algebraMap L F c ∈ V)
    {g : F} (hg : V.valuation g < 1) {t : L[X]} (ht : IsGood A t) :
    V.valuation (aeval g t) = 1
theorem

valuation_aeval_eq_one_of_sub_lt

L187 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.valuation_aeval_eq_one_of_sub_lt
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
variable {L : Type*} [Field L] (A : ValuationSubring L)
section Field
variable {F : Type*} [Field F] [Algebra L F]
Lean source · statement
theorem valuation_aeval_eq_one_of_sub_lt (V : ValuationSubring F)
    (hV : ∀ c : L, algebraMap L F c ∈ V) {g : F} {c : L} (hc : A.valuation c < 1)
    (hgc : V.valuation (g - algebraMap L F c) < 1) {t : L[X]} (ht : IsGood A t) :
    V.valuation (aeval g t) = 1
theorem

mem_of_forall

L234 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.mem_of_forall
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
variable {L : Type*} [Field L] (A : ValuationSubring L)
section Field
variable {F : Type*} [Field F] [Algebra L F]
Lean source · statement
theorem mem_of_forall [IsAlgClosed L] {f : F} (hf : Transcendental L f) {t t' : L[X]}
    (ht : IsGood A t) (ht' : IsGood A t') {x : F}
    (hx : ∀ V : ValuationSubring F, (∀ c : L, algebraMap L F c ∈ V) → f ∈ V → x * aeval f t ∈ V)
    (hx' : ∀ V : ValuationSubring F, (∀ c : L, algebraMap L F c ∈ V) → f⁻¹ ∈ V →
      x * aeval f⁻¹ t' ∈ V)
    (V : ValuationSubring F) (hV : ∀ c : L, algebraMap L F c ∈ V) : x ∈ V
theorem

exists_eq_algebraMap_of_forall_mem

L284 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem.E1Sol.exists_eq_algebraMap_of_forall_mem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
namespace E1Sol
variable {L : Type*} [Field L] (A : ValuationSubring L)
section Field
variable {F : Type*} [Field F] [Algebra L F]
omit A in
Lean source · statement
theorem exists_eq_algebraMap_of_forall_mem [IsAlgClosed L] {x : F}
    (hx : ∀ V : ValuationSubring F, (∀ c : L, algebraMap L F c ∈ V) → x ∈ V) :
    ∃ c : L, x = algebraMap L F c
theorem

exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem

L326 ↗
ValuationSubring.exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
open Polynomial
open E1Sol in
Lean source · statement
theorem _root_.ValuationSubring.exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
    {L : Type*} [Field L] [IsAlgClosed L] (A : ValuationSubring L)
    {F : Type*} [Field F] [Algebra L F] {f : F} (hf : Transcendental L f)
    (t t' : L[X])
    (ht : A.valuation (t.coeff 0) = 1 ∧ ∀ j, j ≠ 0 → A.valuation (t.coeff j) < 1)
    (ht' : A.valuation (t'.coeff 0) = 1 ∧ ∀ j, j ≠ 0 → A.valuation (t'.coeff j) < 1)
    (x : F)
    (hx : ∀ V : ValuationSubring F, (∀ c : L, algebraMap L F c ∈ V) → f ∈ V → x * aeval f t ∈ V)
    (hx' : ∀ V : ValuationSubring F, (∀ c : L, algebraMap L F c ∈ V) → f⁻¹ ∈ V →
      x * aeval f⁻¹ t' ∈ V) :
    ∃ c : L, x = algebraMap L F c

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