NYLL
Module

ValuationSubring_exists_smul_mem_of_transcendental_residue.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_smul_mem_of_transcendental_residue
10 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring exists smul mem of transcendental residue

Imports19
  • Mathlib.Algebra.MonoidAlgebra.Defs
  • Mathlib.Algebra.Order.Monoid.Unbundled.Pow
  • Mathlib.Algebra.Polynomial.AlgebraMap
  • Mathlib.Algebra.Polynomial.Basic
  • Mathlib.Algebra.Polynomial.Degree.Defs
  • Mathlib.Algebra.Polynomial.Degree.Operations
  • Mathlib.Algebra.Polynomial.Eval.Defs
  • Mathlib.Data.Finset.Max
  • Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
  • Mathlib.FieldTheory.IsAlgClosed.Basic
  • Mathlib.LinearAlgebra.Finsupp.LinearCombination
  • Mathlib.LinearAlgebra.LinearIndependent.Defs
  • Mathlib.RingTheory.Algebraic.Defs
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  • Mathlib.RingTheory.LocalRing.ResidueField.Defs
  • Mathlib.RingTheory.Valuation.Basic
  • Mathlib.RingTheory.Valuation.ValuationSubring
  • Mathlib.Tactic.Push
Imported by1

Declarations

theorem

aeval_eq_linearCombination

L49 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_mem_of_transcendental_residue.ValuationSubring.A36FE.aeval_eq_linearCombination
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_mem_of_transcendental_residue
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace A36FE
open _root_.ValuationSubring
Lean source · full declaration
theorem aeval_eq_linearCombination {K B : Type*} [CommRing K] [Ring B] [Algebra K B]
    (x : B) (p : Polynomial K) :
    Polynomial.aeval x p = Finsupp.linearCombination K (fun j : ℕ => x ^ j) p.toFinsupp.coeff := by
  rcases p with ⟨q⟩
  simp only [Polynomial.aeval_def, Polynomial.eval₂_eq_sum, Polynomial.sum_def,
    Polynomial.support_ofFinsupp, Polynomial.coeff_ofFinsupp, Finsupp.linearCombination_apply,
    Finsupp.sum, Algebra.smul_def]
theorem

linearIndependent_pow_of_transcendental

L57 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_mem_of_transcendental_residue.ValuationSubring.A36FE.linearIndependent_pow_of_transcendental
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_mem_of_transcendental_residue
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace A36FE
open _root_.ValuationSubring
Lean source · full declaration
theorem linearIndependent_pow_of_transcendental {K B : Type*} [Field K] [Ring B] [Algebra K B]
    {x : B} (hx : Transcendental K x) : LinearIndependent K (fun j : ℕ => x ^ j) := by
  rw [linearIndependent_iff]
  rw [transcendental_iff] at hx
  intro l hl
  have := hx ⟨.ofCoeff l⟩ (by rw [aeval_eq_linearCombination]; exact hl)
  exact AddMonoidAlgebra.ofCoeff_eq_zero.mp (Polynomial.ofFinsupp_eq_zero.mp this)
theorem

valuation_eq_one_of_residue_ne_zero

L76 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_mem_of_transcendental_residue.ValuationSubring.A36FE.valuation_eq_one_of_residue_ne_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_mem_of_transcendental_residue
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace A36FE
open _root_.ValuationSubring
variable {L : Type*} [Field L] {A : ValuationSubring L}
  {F : Type*} [Field F] [Algebra L F]
  {O : ValuationSubring F} (hO : ∀ x : L, algebraMap L F x ∈ O ↔ x ∈ A)
  {Fbar : Type*} [Field Fbar] [Algebra (IsLocalRing.ResidueField A) Fbar]
  {ρ : O →+* Fbar} (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
  (hρ : ∀ a : A, ρ ⟨algebraMap L F a, (hO a).mpr a.2⟩ =
      algebraMap (IsLocalRing.ResidueField A) Fbar (IsLocalRing.residue A a))
  {f : F} {hf : f ∈ O}
  (htr : Transcendental (IsLocalRing.ResidueField A) (ρ ⟨f, hf⟩))
include hker in
Lean source · statement
theorem valuation_eq_one_of_residue_ne_zero (x : O) (hx : ρ x ≠ 0) :
    O.valuation (x : F) = 1
theorem

residue_ne_zero_of_valuation_eq_one

L83 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_mem_of_transcendental_residue.ValuationSubring.A36FE.residue_ne_zero_of_valuation_eq_one
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_mem_of_transcendental_residue
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace A36FE
open _root_.ValuationSubring
variable {L : Type*} [Field L] {A : ValuationSubring L}
  {F : Type*} [Field F] [Algebra L F]
  {O : ValuationSubring F} (hO : ∀ x : L, algebraMap L F x ∈ O ↔ x ∈ A)
  {Fbar : Type*} [Field Fbar] [Algebra (IsLocalRing.ResidueField A) Fbar]
  {ρ : O →+* Fbar} (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
  (hρ : ∀ a : A, ρ ⟨algebraMap L F a, (hO a).mpr a.2⟩ =
      algebraMap (IsLocalRing.ResidueField A) Fbar (IsLocalRing.residue A a))
  {f : F} {hf : f ∈ O}
  (htr : Transcendental (IsLocalRing.ResidueField A) (ρ ⟨f, hf⟩))
include hker in
Lean source · statement
theorem residue_ne_zero_of_valuation_eq_one (x : O) (hx : O.valuation (x : F) = 1) :
    ρ x ≠ 0
theorem

algebraMap_mem_of_valuation_le

L89 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_mem_of_transcendental_residue.ValuationSubring.A36FE.algebraMap_mem_of_valuation_le
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_mem_of_transcendental_residue
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace A36FE
open _root_.ValuationSubring
variable {L : Type*} [Field L] {A : ValuationSubring L}
  {F : Type*} [Field F] [Algebra L F]
  {O : ValuationSubring F} (hO : ∀ x : L, algebraMap L F x ∈ O ↔ x ∈ A)
  {Fbar : Type*} [Field Fbar] [Algebra (IsLocalRing.ResidueField A) Fbar]
  {ρ : O →+* Fbar} (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
  (hρ : ∀ a : A, ρ ⟨algebraMap L F a, (hO a).mpr a.2⟩ =
      algebraMap (IsLocalRing.ResidueField A) Fbar (IsLocalRing.residue A a))
  {f : F} {hf : f ∈ O}
  (htr : Transcendental (IsLocalRing.ResidueField A) (ρ ⟨f, hf⟩))
include hO in
Lean source · statement
theorem algebraMap_mem_of_valuation_le {x y : L} (hy : y ≠ 0)
    (hle : O.valuation (algebraMap L F x) ≤ O.valuation (algebraMap L F y)) :
    y⁻¹ * x ∈ A
theorem

exists_valuation_aeval_eq

L100 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_mem_of_transcendental_residue.ValuationSubring.A36FE.exists_valuation_aeval_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_mem_of_transcendental_residue
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace A36FE
open _root_.ValuationSubring
variable {L : Type*} [Field L] {A : ValuationSubring L}
  {F : Type*} [Field F] [Algebra L F]
  {O : ValuationSubring F} (hO : ∀ x : L, algebraMap L F x ∈ O ↔ x ∈ A)
  {Fbar : Type*} [Field Fbar] [Algebra (IsLocalRing.ResidueField A) Fbar]
  {ρ : O →+* Fbar} (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
  (hρ : ∀ a : A, ρ ⟨algebraMap L F a, (hO a).mpr a.2⟩ =
      algebraMap (IsLocalRing.ResidueField A) Fbar (IsLocalRing.residue A a))
  {f : F} {hf : f ∈ O}
  (htr : Transcendental (IsLocalRing.ResidueField A) (ρ ⟨f, hf⟩))
include hO hker hρ htr in
Lean source · statement
theorem exists_valuation_aeval_eq (r : L[X]) (hr : r ≠ 0) :
    ∃ d : L, d ≠ 0 ∧ O.valuation (aeval f r) = O.valuation (algebraMap L F d)
theorem

exists_valuation_eq_of_mem_adjoin

L159 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_mem_of_transcendental_residue.ValuationSubring.A36FE.exists_valuation_eq_of_mem_adjoin
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_mem_of_transcendental_residue
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace A36FE
open _root_.ValuationSubring
variable {L : Type*} [Field L] {A : ValuationSubring L}
  {F : Type*} [Field F] [Algebra L F]
  {O : ValuationSubring F} (hO : ∀ x : L, algebraMap L F x ∈ O ↔ x ∈ A)
  {Fbar : Type*} [Field Fbar] [Algebra (IsLocalRing.ResidueField A) Fbar]
  {ρ : O →+* Fbar} (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
  (hρ : ∀ a : A, ρ ⟨algebraMap L F a, (hO a).mpr a.2⟩ =
      algebraMap (IsLocalRing.ResidueField A) Fbar (IsLocalRing.residue A a))
  {f : F} {hf : f ∈ O}
  (htr : Transcendental (IsLocalRing.ResidueField A) (ρ ⟨f, hf⟩))
include hO hker hρ htr in
Lean source · statement
theorem exists_valuation_eq_of_mem_adjoin {y : F}
    (hy : y ∈ IntermediateField.adjoin L ({f} : Set F)) (hy0 : y ≠ 0) :
    ∃ d : L, d ≠ 0 ∧ O.valuation y = O.valuation (algebraMap L F d)
theorem

exists_smul_of_valuation_eq

L175 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_mem_of_transcendental_residue.ValuationSubring.A36FE.exists_smul_of_valuation_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_mem_of_transcendental_residue
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace A36FE
open _root_.ValuationSubring
variable {L : Type*} [Field L] {A : ValuationSubring L}
  {F : Type*} [Field F] [Algebra L F]
  {O : ValuationSubring F} (hO : ∀ x : L, algebraMap L F x ∈ O ↔ x ∈ A)
  {Fbar : Type*} [Field Fbar] [Algebra (IsLocalRing.ResidueField A) Fbar]
  {ρ : O →+* Fbar} (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
  (hρ : ∀ a : A, ρ ⟨algebraMap L F a, (hO a).mpr a.2⟩ =
      algebraMap (IsLocalRing.ResidueField A) Fbar (IsLocalRing.residue A a))
  {f : F} {hf : f ∈ O}
  (htr : Transcendental (IsLocalRing.ResidueField A) (ρ ⟨f, hf⟩))
include hO hker hρ htr in
Lean source · statement
theorem exists_smul_of_valuation_eq [IsAlgClosed L] {h : F} (hh : h ≠ 0) {i j : ℕ} (hij : i < j)
    {ci cj : F} (hci : ci ∈ IntermediateField.adjoin L ({f} : Set F))
    (hcj : cj ∈ IntermediateField.adjoin L ({f} : Set F)) (hci0 : ci ≠ 0) (hcj0 : cj ≠ 0)
    (heq : O.valuation (ci * h ^ i) = O.valuation (cj * h ^ j)) :
    ∃ c : L, ∃ hc : c • h ∈ O, ρ ⟨c • h, hc⟩ ≠ 0
theorem

exists_smul_mem

L207 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_mem_of_transcendental_residue.ValuationSubring.A36FE.exists_smul_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_mem_of_transcendental_residue
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace A36FE
open _root_.ValuationSubring
variable {L : Type*} [Field L] {A : ValuationSubring L}
  {F : Type*} [Field F] [Algebra L F]
  {O : ValuationSubring F} (hO : ∀ x : L, algebraMap L F x ∈ O ↔ x ∈ A)
  {Fbar : Type*} [Field Fbar] [Algebra (IsLocalRing.ResidueField A) Fbar]
  {ρ : O →+* Fbar} (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
  (hρ : ∀ a : A, ρ ⟨algebraMap L F a, (hO a).mpr a.2⟩ =
      algebraMap (IsLocalRing.ResidueField A) Fbar (IsLocalRing.residue A a))
  {f : F} {hf : f ∈ O}
  (htr : Transcendental (IsLocalRing.ResidueField A) (ρ ⟨f, hf⟩))
include hO hker hρ htr in
Lean source · statement
theorem exists_smul_mem [IsAlgClosed L]
    [Algebra.IsAlgebraic (IntermediateField.adjoin L ({f} : Set F)) F]
    (h : F) (hh : h ≠ 0) :
    ∃ c : L, ∃ hc : c • h ∈ O, ρ ⟨c • h, hc⟩ ≠ 0
theorem

exists_smul_mem_of_transcendental_residue

L260 ↗
ValuationSubring.exists_smul_mem_of_transcendental_residue
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_mem_of_transcendental_residue
open Polynomial
Lean source · statement
theorem _root_.ValuationSubring.exists_smul_mem_of_transcendental_residue
    {L : Type*} [Field L] [IsAlgClosed L] (A : ValuationSubring L)
    {F : Type*} [Field F] [Algebra L F]
    (O : ValuationSubring F) (hO : ∀ x : L, algebraMap L F x ∈ O ↔ x ∈ A)
    {Fbar : Type*} [Field Fbar] [Algebra (IsLocalRing.ResidueField A) Fbar]
    (ρ : O →+* Fbar) (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ a : A, ρ ⟨algebraMap L F a, (hO a).mpr a.2⟩ =
      algebraMap (IsLocalRing.ResidueField A) Fbar (IsLocalRing.residue A a))
    (f : F) (hf : f ∈ O)
    (htr : Transcendental (IsLocalRing.ResidueField A) (ρ ⟨f, hf⟩))
    [Algebra.IsAlgebraic (IntermediateField.adjoin L ({f} : Set F)) F]
    (h : F) (hh : h ≠ 0) :
    ∃ c : L, ∃ hc : c • h ∈ O, ρ ⟨c • h, hc⟩ ≠ 0

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