NYLL
Module

ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card.lean

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

Module documentation

Valuation Subring exists sub mem nonunits of finrank le card

Imports1
Imported by1

Declarations

theorem

mul_lt_one_aux

L33 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card.ValuationSubring.CompleteSplitting.mul_lt_one_aux
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace CompleteSplitting
open _root_.ValuationSubring
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
Lean source · statement
theorem mul_lt_one_aux {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] {a b : Γ₀}
    (ha : a ≤ 1) (hb : b < 1) : a * b < 1
theorem

mem_iff

L45 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card.ValuationSubring.CompleteSplitting.mem_iff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace CompleteSplitting
open _root_.ValuationSubring
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Over
variable {O : ValuationSubring F} {V : ValuationSubring F'}
  (hV : V.comap (algebraMap F F') = O)
include hV
Lean source · statement
theorem mem_iff (x : F) : algebraMap F F' x ∈ V ↔ x ∈ O
theorem

algebraMap_mem

L48 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card.ValuationSubring.CompleteSplitting.algebraMap_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace CompleteSplitting
open _root_.ValuationSubring
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Over
variable {O : ValuationSubring F} {V : ValuationSubring F'}
  (hV : V.comap (algebraMap F F') = O)
include hV
Lean source · statement
theorem algebraMap_mem (x : O) : algebraMap F F' (x : F) ∈ V
theorem

lt_one_iff

L50 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card.ValuationSubring.CompleteSplitting.lt_one_iff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace CompleteSplitting
open _root_.ValuationSubring
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Over
variable {O : ValuationSubring F} {V : ValuationSubring F'}
  (hV : V.comap (algebraMap F F') = O)
include hV
Lean source · statement
theorem lt_one_iff (x : F) : V.valuation (algebraMap F F' x) < 1 ↔ O.valuation x < 1
theorem

le_one

L55 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card.ValuationSubring.CompleteSplitting.le_one
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace CompleteSplitting
open _root_.ValuationSubring
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Over
variable {O : ValuationSubring F} {V : ValuationSubring F'}
  (hV : V.comap (algebraMap F F') = O)
include hV
Lean source · statement
theorem le_one (x : O) : V.valuation (algebraMap F F' (x : F)) ≤ 1
theorem

eq_one_iff

L58 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card.ValuationSubring.CompleteSplitting.eq_one_iff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace CompleteSplitting
open _root_.ValuationSubring
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Over
variable {O : ValuationSubring F} {V : ValuationSubring F'}
  (hV : V.comap (algebraMap F F') = O)
include hV
Lean source · statement
theorem eq_one_iff (x : F) : V.valuation (algebraMap F F' x) = 1 ↔ O.valuation x = 1
theorem

valuation_eq_one_of_le

L78 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card.ValuationSubring.CompleteSplitting.valuation_eq_one_of_le
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace CompleteSplitting
open _root_.ValuationSubring
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Incomparable
variable {O : ValuationSubring F} {V W : ValuationSubring F'}
Lean source · statement
theorem valuation_eq_one_of_le (hVW : V ≤ W) {u : F'} (hu : V.valuation u = 1) :
    W.valuation u = 1
theorem

sum_ne_zero

L93 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card.ValuationSubring.CompleteSplitting.sum_ne_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace CompleteSplitting
open _root_.ValuationSubring
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Incomparable
variable {O : ValuationSubring F} {V W : ValuationSubring F'}
Lean source · statement
theorem sum_ne_zero (hV : V.comap (algebraMap F F') = O) (hW : W.comap (algebraMap F F') = O)
    (hVW : V ≤ W) {y : F'} (hyV : V.valuation y < 1) (hyW : W.valuation y = 1)
    (c : ℕ → F) (hc : ∀ k, c k ∈ O) {j N : ℕ} (hjN : j < N) (hj : O.valuation (c j) = 1)
    (hlow : ∀ k < j, O.valuation (c k) < 1) :
    ∑ k ∈ Finset.range N, algebraMap F F' (c k) * y ^ k ≠ 0
theorem

eq_of_le

L138 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card.ValuationSubring.CompleteSplitting.eq_of_le
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace CompleteSplitting
open _root_.ValuationSubring
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Incomparable
variable {O : ValuationSubring F} {V W : ValuationSubring F'}
Lean source · statement
theorem eq_of_le [Algebra.IsAlgebraic F F'] (hV : V.comap (algebraMap F F') = O)
    (hW : W.comap (algebraMap F F') = O) (hVW : V ≤ W) : V = W
theorem

exists_sub_mem_nonunits_of_finrank_le_card

L211 ↗
ValuationSubring.exists_sub_mem_nonunits_of_finrank_le_card
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card
open Polynomial
open ValuationSubring.CompleteSplitting in
Lean source · statement
theorem _root_.ValuationSubring.exists_sub_mem_nonunits_of_finrank_le_card
    {F F' : Type*} [Field F] [Field F'] [Algebra F F'] [FiniteDimensional F F']
    (O : ValuationSubring F) {ι : Type*} [Fintype ι] (O' : ι → ValuationSubring F')
    (hinj : Function.Injective O') (hO' : ∀ i, (O' i).comap (algebraMap F F') = O)
    (hcard : Module.finrank F F' ≤ Fintype.card ι) (i : ι) (x : F') (hx : x ∈ O' i) :
    ∃ y ∈ O, x - algebraMap F F' y ∈ (O' i).nonunits

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