Module

ValuationSubring_natDegree_map_eq_card_roots_of_splits.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_natDegree_map_eq_card_roots_of_splits

6 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring nat Degree map eq card roots of splits

Imports4

Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.Algebra.Polynomial.Roots
Mathlib.Algebra.Polynomial.Lifts
Mathlib.Tactic.Ring.RingNF

Imported by2

theorem

algebraMap_injective

L34 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natDegree_map_eq_card_roots_of_splits.ValuationRingRootCount.algebraMap_injective

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_natDegree_map_eq_card_roots_of_splits
open scoped Polynomial
open Polynomial
namespace ValuationRingRootCount
variable {E k : Type*} [Field E] [Field k] (A : ValuationSubring E) (σ : A →+* k)
  (hσ : RingHom.ker σ = IsLocalRing.maximalIdeal A)

Lean source · statement

theorem algebraMap_injective : Function.Injective (algebraMap A E)

theorem

isUnit_iff_inv_mem

L36 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natDegree_map_eq_card_roots_of_splits.ValuationRingRootCount.isUnit_iff_inv_mem

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_natDegree_map_eq_card_roots_of_splits
open scoped Polynomial
open Polynomial
namespace ValuationRingRootCount
variable {E k : Type*} [Field E] [Field k] (A : ValuationSubring E) (σ : A →+* k)
  (hσ : RingHom.ker σ = IsLocalRing.maximalIdeal A)

Lean source · statement

theorem isUnit_iff_inv_mem (z : A) (hz : (z : E) ≠ 0) : IsUnit z ↔ (z : E)⁻¹ ∈ A

theorem

inv_mem_maximalIdeal

L48 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natDegree_map_eq_card_roots_of_splits.ValuationRingRootCount.inv_mem_maximalIdeal

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_natDegree_map_eq_card_roots_of_splits
open scoped Polynomial
open Polynomial
namespace ValuationRingRootCount
variable {E k : Type*} [Field E] [Field k] (A : ValuationSubring E) (σ : A →+* k)
  (hσ : RingHom.ker σ = IsLocalRing.maximalIdeal A)

Lean source · statement

theorem inv_mem_maximalIdeal {α : E} (hα : α ∉ A) :
    ∃ h : α⁻¹ ∈ A, (⟨α⁻¹, h⟩ : A) ∈ IsLocalRing.maximalIdeal A

theorem

coeff_mem_of_one_sub_mul

L56 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natDegree_map_eq_card_roots_of_splits.ValuationRingRootCount.coeff_mem_of_one_sub_mul

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_natDegree_map_eq_card_roots_of_splits
open scoped Polynomial
open Polynomial
namespace ValuationRingRootCount
variable {E k : Type*} [Field E] [Field k] (A : ValuationSubring E) (σ : A →+* k)
  (hσ : RingHom.ker σ = IsLocalRing.maximalIdeal A)

Lean source · statement

theorem coeff_mem_of_one_sub_mul (β : E) (hβ : β ∈ A) (q : E[X])
    (h : ∀ n, ((1 - C β * X) * q).coeff n ∈ A) (n : ℕ) : q.coeff n ∈ A

theorem

main

L70 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natDegree_map_eq_card_roots_of_splits.ValuationRingRootCount.main

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_natDegree_map_eq_card_roots_of_splits
open scoped Polynomial
open Polynomial
namespace ValuationRingRootCount
variable {E k : Type*} [Field E] [Field k] (A : ValuationSubring E) (σ : A →+* k)
  (hσ : RingHom.ker σ = IsLocalRing.maximalIdeal A)
include hσ in

Lean source · statement

theorem main (n : ℕ) : ∀ p : A[X], p.natDegree = n → p.map σ ≠ 0 →
    Multiset.card (p.map (algebraMap A E)).roots = p.natDegree →
    (p.map σ).natDegree = Multiset.card p.roots

theorem

natDegree_map_eq_card_roots_of_splits

L183 ↗

ValuationSubring.natDegree_map_eq_card_roots_of_splits

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_natDegree_map_eq_card_roots_of_splits
open scoped Polynomial
open Polynomial

Lean source · statement

theorem _root_.ValuationSubring.natDegree_map_eq_card_roots_of_splits
    {E k : Type*} [Field E] [Field k] (A : ValuationSubring E) (σ : A →+* k)
    (hσ : RingHom.ker σ = IsLocalRing.maximalIdeal A)
    (p : A[X]) (hp : p.map σ ≠ 0)
    (hsplit : Multiset.card (p.map (algebraMap A E)).roots = p.natDegree) :
    (p.map σ).natDegree = Multiset.card p.roots

Module documentation

Valuation Subring nat Degree map eq card roots of splits

Declarations

algebraMap_injective

isUnit_iff_inv_mem

inv_mem_maximalIdeal

coeff_mem_of_one_sub_mul

main

natDegree_map_eq_card_roots_of_splits