NYLL
Module

WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic.lean

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

Module documentation

Witt Vector exists valuation Subring residue Field equiv of is Algebraic

Imports25
  • Mathlib.Algebra.Algebra.Basic
  • Mathlib.Algebra.Polynomial.AlgebraMap
  • Mathlib.Algebra.Polynomial.Coeff
  • Mathlib.Algebra.Polynomial.Eval.Coeff
  • Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
  • Mathlib.FieldTheory.IsAlgClosed.Basic
  • Mathlib.RingTheory.Algebraic.Defs
  • Mathlib.RingTheory.Algebraic.Integral
  • Mathlib.RingTheory.DiscreteValuationRing.Basic
  • Mathlib.RingTheory.Ideal.Quotient.Defs
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Mathlib.RingTheory.Ideal.Span
  • Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  • Mathlib.RingTheory.LocalRing.ResidueField.Basic
  • Mathlib.RingTheory.LocalRing.RingHom.Basic
  • Mathlib.RingTheory.Polynomial.Content
  • Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
  • Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
  • Mathlib.RingTheory.Valuation.LocalSubring
  • Mathlib.RingTheory.Valuation.ValuationSubring
  • Mathlib.RingTheory.WittVector.Basic
  • Mathlib.RingTheory.WittVector.Complete
  • Mathlib.RingTheory.WittVector.DiscreteValuationRing
  • Mathlib.RingTheory.WittVector.Teichmuller
  • Mathlib.Tactic.Push
Imported by1

Declarations

theorem

mem_range_of_eval₂_eq_zero

L57 ↗
AlgebraicCurves.Valuations.Proofs.WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic.WittVector.WittBase.mem_range_of_eval₂_eq_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic
open IsLocalRing Polynomial
namespace WittVector
open _root_.WittVector
namespace WittBase
open _root_.WittVector
section General
Lean source · statement
theorem mem_range_of_eval₂_eq_zero {k K' : Type*} [Field k] [IsAlgClosed k] [Field K']
    (f : k →+* K') {q : k[X]} (hq : q ≠ 0) {z : K'} (hz : q.eval₂ f z = 0) : z ∈ Set.range f
theorem

exists_eq_C_mul_and_isUnit_coeff

L68 ↗
AlgebraicCurves.Valuations.Proofs.WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic.WittVector.WittBase.exists_eq_C_mul_and_isUnit_coeff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic
open IsLocalRing Polynomial
namespace WittVector
open _root_.WittVector
namespace WittBase
open _root_.WittVector
section General
Lean source · statement
theorem exists_eq_C_mul_and_isUnit_coeff {R : Type*} [CommRing R] [IsDomain R]
    [IsDiscreteValuationRing R] {g : R[X]} (hg : g ≠ 0) :
    ∃ (c : R) (g₁ : R[X]) (i : ℕ), c ≠ 0 ∧ g = C c * g₁ ∧ IsUnit (g₁.coeff i)
theorem

maximalIdeal_eq

L92 ↗
AlgebraicCurves.Valuations.Proofs.WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic.WittVector.WittBase.maximalIdeal_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic
open IsLocalRing Polynomial
namespace WittVector
open _root_.WittVector
namespace WittBase
open _root_.WittVector
variable (p : ℕ) [Fact p.Prime] (k : Type*) [Field k] [IsAlgClosed k] [CharP k p]
Lean source · statement
theorem maximalIdeal_eq : maximalIdeal (WittVector p k) = Ideal.span {(p : WittVector p k)}
theorem

maximalIdeal_eq_ker

L95 ↗
AlgebraicCurves.Valuations.Proofs.WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic.WittVector.WittBase.maximalIdeal_eq_ker
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic
open IsLocalRing Polynomial
namespace WittVector
open _root_.WittVector
namespace WittBase
open _root_.WittVector
variable (p : ℕ) [Fact p.Prime] (k : Type*) [Field k] [IsAlgClosed k] [CharP k p]
Lean source · statement
theorem maximalIdeal_eq_ker :
    maximalIdeal (WittVector p k) = RingHom.ker (WittVector.constantCoeff : WittVector p k →+* k)
def

resEquivInv

L102 ↗
AlgebraicCurves.Valuations.Proofs.WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic.WittVector.WittBase.resEquivInv
Documentation

Identify the residue field of the Witt-vector ring with its coefficient field via the constant coefficient.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic
open IsLocalRing Polynomial
namespace WittVector
open _root_.WittVector
namespace WittBase
open _root_.WittVector
variable (p : ℕ) [Fact p.Prime] (k : Type*) [Field k] [IsAlgClosed k] [CharP k p]
Lean source · statement
def resEquivInv : ResidueField (WittVector p k) ≃+* k
theorem

resEquivInv_residue

L108 ↗
AlgebraicCurves.Valuations.Proofs.WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic.WittVector.WittBase.resEquivInv_residue
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic
open IsLocalRing Polynomial
namespace WittVector
open _root_.WittVector
namespace WittBase
open _root_.WittVector
variable (p : ℕ) [Fact p.Prime] (k : Type*) [Field k] [IsAlgClosed k] [CharP k p]
Lean source · statement
theorem resEquivInv_residue (a : WittVector p k) :
    resEquivInv p k (residue (WittVector p k) a) = a.coeff 0
def

residueEquiv

L119 ↗
AlgebraicCurves.Valuations.Proofs.WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic.WittVector.WittBase.residueEquiv
Documentation

The inverse ring equivalence from the coefficient field to the residue field of its Witt-vector ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic
open IsLocalRing Polynomial
namespace WittVector
open _root_.WittVector
namespace WittBase
open _root_.WittVector
variable (p : ℕ) [Fact p.Prime] (k : Type*) [Field k] [IsAlgClosed k] [CharP k p]
Lean source · statement
def residueEquiv : k ≃+* ResidueField (WittVector p k)
theorem

residueEquiv_coeff_zero

L121 ↗
AlgebraicCurves.Valuations.Proofs.WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic.WittVector.WittBase.residueEquiv_coeff_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic
open IsLocalRing Polynomial
namespace WittVector
open _root_.WittVector
namespace WittBase
open _root_.WittVector
variable (p : ℕ) [Fact p.Prime] (k : Type*) [Field k] [IsAlgClosed k] [CharP k p]
Lean source · statement
theorem residueEquiv_coeff_zero (a : WittVector p k) :
    residueEquiv p k (a.coeff 0) = residue (WittVector p k) a
theorem

main

L128 ↗
AlgebraicCurves.Valuations.Proofs.WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic.WittVector.WittBase.main
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic
open IsLocalRing Polynomial
namespace WittVector
open _root_.WittVector
namespace WittBase
open _root_.WittVector
variable (p : ℕ) [Fact p.Prime] (k : Type*) [Field k] [IsAlgClosed k] [CharP k p]
variable (Ω : Type*) [Field Ω] [Algebra (WittVector p k) Ω] [FaithfulSMul (WittVector p k) Ω]
  [Algebra.IsAlgebraic (WittVector p k) Ω]
Lean source · statement
theorem main :
    ∃ (V : ValuationSubring Ω) (hV : ∀ a : WittVector p k, algebraMap (WittVector p k) Ω a ∈ V)
      (φ : k ≃+* ResidueField V),
      (∀ a ∈ maximalIdeal (WittVector p k), algebraMap (WittVector p k) Ω a ∈ V.nonunits) ∧
      ∀ a : WittVector p k, φ (a.coeff 0) = residue V ⟨algebraMap (WittVector p k) Ω a, hV a⟩
theorem

exists_valuationSubring_residueField_equiv_of_isAlgebraic

L200 ↗
WittVector.exists_valuationSubring_residueField_equiv_of_isAlgebraic
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic
open IsLocalRing Polynomial
Lean source · statement
theorem _root_.WittVector.exists_valuationSubring_residueField_equiv_of_isAlgebraic (p : ℕ) [Fact
  p.Prime] (k : Type*) [Field k] [IsAlgClosed k] [CharP k p] (Ω : Type*) [Field Ω] [Algebra
  (WittVector p k) Ω] [FaithfulSMul (WittVector p k) Ω] [Algebra.IsAlgebraic (WittVector p k) Ω] :
  ∃ (V : ValuationSubring Ω) (hV : ∀ a : WittVector p k, algebraMap (WittVector p k) Ω a ∈ V) (φ :
  k ≃+* IsLocalRing.ResidueField V), (∀ a ∈ IsLocalRing.maximalIdeal (WittVector p k), algebraMap
  (WittVector p k) Ω a ∈ V.nonunits) ∧ ∀ a : WittVector p k, φ (a.coeff 0) = IsLocalRing.residue V
  ⟨algebraMap (WittVector p k) Ω a, hV a⟩

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