NYLL
Module

ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
21 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring exists valuation mul eq one of forall sup eq top

Imports1
Imported by2

Declarations

theorem

mul_lt_one_aux

L33 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.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_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
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_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.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_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
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

lt_one_iff

L48 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.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_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
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

L53 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.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_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
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 : F} (hx : x ∈ O) : V.valuation (algebraMap F F' x) ≤ 1
theorem

eq_one_iff

L56 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.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_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
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

L76 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.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_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
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

L91 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.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_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
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

L136 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.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_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
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

pow_eq_self_of_orderOf_dvd

L208 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.pow_eq_self_of_orderOf_dvd
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Nagata
Lean source · statement
theorem pow_eq_self_of_orderOf_dvd {M : Type*} [Monoid M] (u : M) {D : ℕ}
    (hD : orderOf u ∣ D) (N : ℕ) : u ^ (1 + N * D) = u
theorem

eq_of_pow_eq_pow_of_not_isOfFinOrder

L213 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.eq_of_pow_eq_pow_of_not_isOfFinOrder
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Nagata
Lean source · statement
theorem eq_of_pow_eq_pow_of_not_isOfFinOrder {κ : Type*} [Field κ] {u : κ} (hu : u ≠ 0)
    (hfin : ¬ IsOfFinOrder u) {a b : ℕ} (h : u ^ a = u ^ b) : a = b
theorem

exists_exponent

L226 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.exists_exponent
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Nagata
Lean source · statement
theorem exists_exponent {ι : Type*} [Finite ι] (κ : ι → Type*) [∀ j, Field (κ j)]
    (u : ∀ j, κ j) (hu : ∀ j, u j ≠ 0) :
    ∃ m : ℕ, 2 ≤ m ∧ ∀ j, 1 - u j + u j ^ m ≠ 0
theorem

exists_mul_mem_forall

L275 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.exists_mul_mem_forall
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Nagata
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
theorem exists_mul_mem_forall [Finite ι] (R : ι → ValuationSubring K) (x : K) :
    ∃ t : K, (∀ j, t ∈ R j) ∧ (∀ j, t * x ∈ R j) ∧
      (∀ j, x ∈ R j → (R j).valuation t = 1)
def

locAt

L365 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.locAt
Documentation

The valuation overring defined by bounds on all powers against the selected test elements.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Indep
variable {K : Type*} [Field K]
Lean source · full declaration
def locAt (A : ValuationSubring K) (D : Set K) : ValuationSubring K where
  carrier := {x | ∀ d ∈ D, A.valuation d < 1 → ∀ n : ℕ, A.valuation (d * x ^ n) < 1}
  mul_mem' := by
    intro x y hx hy d hdD hd n
    have key : ∀ x y : K, A.valuation x ≤ A.valuation y →
        (∀ n : ℕ, A.valuation (d * y ^ n) < 1) → A.valuation (d * (x * y) ^ n) < 1 := by
      intro x y h hy'
      calc A.valuation (d * (x * y) ^ n)
          = A.valuation d * (A.valuation x ^ n * A.valuation y ^ n) := by
            rw [map_mul, mul_pow, map_mul, map_pow, map_pow]
        _ ≤ A.valuation d * (A.valuation y ^ n * A.valuation y ^ n) := by
            gcongr
        _ = A.valuation (d * y ^ (2 * n)) := by
            rw [map_mul, map_pow, two_mul, pow_add]
        _ < 1 := hy' (2 * n)
    rcases le_total (A.valuation x) (A.valuation y) with h | h
    · exact key x y h (hy d hdD hd)
    · rw [mul_comm x y]; exact key y x h (hx d hdD hd)
  one_mem' := by
    intro d _ hd n
    simpa using hd
  add_mem' := by
    intro x y hx hy d hdD hd n
    have key : ∀ x y : K, A.valuation x ≤ A.valuation y →
        (∀ n : ℕ, A.valuation (d * y ^ n) < 1) → A.valuation (d * (x + y) ^ n) < 1 := by
      intro x y h hy'
      have hxy : A.valuation (x + y) ≤ A.valuation y :=
        (Valuation.map_add _ _ _).trans (max_le h le_rfl)
      calc A.valuation (d * (x + y) ^ n)
          = A.valuation d * A.valuation (x + y) ^ n := by rw [map_mul, map_pow]
        _ ≤ A.valuation d * A.valuation y ^ n := by gcongr
        _ = A.valuation (d * y ^ n) := by rw [map_mul, map_pow]
        _ < 1 := hy' n
    rcases le_total (A.valuation x) (A.valuation y) with h | h
    · exact key x y h (hy d hdD hd)
    · rw [add_comm x y]; exact key y x h (hx d hdD hd)
  zero_mem' := by
    intro d _ hd n
    cases n with
    | zero => simpa using hd
    | succ n => simp
  neg_mem' := by
    intro x hx d hdD hd n
    have h := hx d hdD hd n
    have e : A.valuation (d * (-x) ^ n) = A.valuation (d * x ^ n) := by
      rw [map_mul, map_mul, map_pow, map_pow, Valuation.map_neg]
    rwa [e]
  mem_or_inv_mem' := by
    intro x
    by_contra h
    rw [not_or] at h
    obtain ⟨h1, h2⟩ := h
    simp only [Set.mem_ofPred_eq, not_forall, not_lt, exists_prop] at h1 h2
    obtain ⟨d, -, hd, n, hn⟩ := h1
    obtain ⟨d', -, hd', n', hn'⟩ := h2
    have one_lt : ∀ (d z : K) (n : ℕ), A.valuation d < 1 → 1 ≤ A.valuation (d * z ^ n) →
        1 < A.valuation z := by
      intro d z n hd hn
      by_contra hz
      rw [not_lt] at hz
      have : A.valuation (d * z ^ n) < 1 := by
        rw [map_mul, map_pow]
        calc A.valuation d * A.valuation z ^ n ≤ A.valuation d * 1 := by
              gcongr; exact pow_le_one₀ zero_le hz
          _ < 1 := by rw [mul_one]; exact hd
      exact (lt_irrefl _) (lt_of_le_of_lt hn this)
    have hx1 := one_lt d x n hd hn
    have hx2 := one_lt d' x⁻¹ n' hd' hn'
    have hx0 : x ≠ 0 := by
      rintro rfl
      rw [map_zero] at hx1
      exact not_lt_zero hx1
    rw [map_inv₀] at hx2
    have : A.valuation x < 1 := by
      have h := one_lt_inv₀ (zero_lt_iff.mpr ((Valuation.ne_zero_iff _).mpr hx0)) |>.mp hx2
      exact h
    exact lt_irrefl _ (hx1.trans this)
theorem

mem_locAt_iff

L443 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.mem_locAt_iff
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Indep
variable {K : Type*} [Field K]
Lean source · statement
theorem mem_locAt_iff (A : ValuationSubring K) (D : Set K) (x : K) :
    x ∈ locAt A D ↔ ∀ d ∈ D, A.valuation d < 1 → ∀ n : ℕ, A.valuation (d * x ^ n) < 1
theorem

le_locAt

L447 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.le_locAt
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Indep
variable {K : Type*} [Field K]
Lean source · statement
theorem le_locAt (A : ValuationSubring K) (D : Set K) : A ≤ locAt A D
theorem

inv_not_mem_locAt

L455 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.inv_not_mem_locAt
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Indep
variable {K : Type*} [Field K]
Lean source · statement
theorem inv_not_mem_locAt (A : ValuationSubring K) {D : Set K} {d : K} (hdD : d ∈ D)
    (hd : A.valuation d < 1) (hd0 : d ≠ 0) : d⁻¹ ∉ locAt A D
theorem

exists_le_and_one_le

L462 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.exists_le_and_one_le
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Indep
variable {K : Type*} [Field K]
Lean source · statement
theorem exists_le_and_one_le (P₀ P : ValuationSubring K) (hsup : P₀ ⊔ P = ⊤) {d : K}
    (hd0 : d ≠ 0) (hd : P₀.valuation d < 1) :
    ∃ y : K, y ≠ 0 ∧ P₀.valuation y ≤ P₀.valuation d ∧ 1 ≤ P.valuation y
theorem

exists_deep

L489 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.exists_deep
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Indep
variable {K : Type*} [Field K]
Lean source · statement
theorem exists_deep {ι : Type*} [Finite ι] (R : ι → ValuationSubring K) (i₀ i : ι)
    (hsup : R i₀ ⊔ R i = ⊤) {d : K} (hd0 : d ≠ 0) (hd : (R i₀).valuation d < 1) :
    ∃ t : K, (∀ j, t ∈ R j) ∧ (R i).valuation t = 1 ∧
      (R i₀).valuation t ≤ (R i₀).valuation d
theorem

valuation_sum_eq_one_of_sub

L525 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.valuation_sum_eq_one_of_sub
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Counting
Lean source · statement
theorem valuation_sum_eq_one_of_sub {O : ValuationSubring F} {V : ValuationSubring F'}
    (hV : V.comap (algebraMap F F') = O) {σ : Type*} (s : Finset σ) (a : σ → F)
    (ha : ∀ i, a i ∈ O) (ω ω' : σ → F') (hωω' : ∀ i ∈ s, a i ≠ 0 → V.valuation (ω' i - ω i) < 1)
    (h : V.valuation (∑ i ∈ s, algebraMap F F' (a i) * ω i) = 1) :
    V.valuation (∑ i ∈ s, algebraMap F F' (a i) * ω' i) = 1
theorem

exists_valuation_mul_eq_one_of_forall_sup_eq_top

L544 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top.ValuationSubring.IndepMember.exists_valuation_mul_eq_one_of_forall_sup_eq_top
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
namespace ValuationSubring
open _root_.ValuationSubring
namespace IndepMember
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Counting
variable [FiniteDimensional F F']
Lean source · statement
theorem exists_valuation_mul_eq_one_of_forall_sup_eq_top
    (Q : ValuationSubring F) (S : Finset (ValuationSubring F'))
    (hS : ∀ P ∈ S, P.comap (algebraMap F F') = Q)
    {σ : Type*} [Fintype σ] (cls : σ → ValuationSubring F') (hcls : ∀ s, cls s ∈ S)
    (ω : σ → F') (hω : ∀ s, ω s ∈ cls s)
    (hind : ∀ P ∈ S, ∀ a : σ → F, (∀ s, a s ∈ Q) → (∀ s, cls s ≠ P → a s = 0) →
      (∃ s, Q.valuation (a s) = 1) → P.valuation (∑ s, algebraMap F F' (a s) * ω s) = 1)
    (hcard : Module.finrank F F' ≤ Fintype.card σ)
    (P₀ : ValuationSubring F') (hP₀ : P₀ ∈ S) (hindep : ∀ P ∈ S, P ≠ P₀ → P₀ ⊔ P = ⊤)
    (g : F') (hg : g ≠ 0) :
    ∃ h : F, P₀.valuation (algebraMap F F' h * g) = 1
theorem

exists_valuation_mul_eq_one_of_forall_sup_eq_top

L858 ↗
ValuationSubring.exists_valuation_mul_eq_one_of_forall_sup_eq_top
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
Lean source · statement
theorem _root_.ValuationSubring.exists_valuation_mul_eq_one_of_forall_sup_eq_top
    {F F' : Type*} [Field F] [Field F'] [Algebra F F'] [FiniteDimensional F F']
    (Q : ValuationSubring F) (S : Finset (ValuationSubring F'))
    (hS : ∀ P ∈ S, P.comap (algebraMap F F') = Q)
    {σ : Type*} [Fintype σ] (cls : σ → ValuationSubring F') (hcls : ∀ s, cls s ∈ S)
    (ω : σ → F') (hω : ∀ s, ω s ∈ cls s)
    (hind : ∀ P ∈ S, ∀ a : σ → F, (∀ s, a s ∈ Q) → (∀ s, cls s ≠ P → a s = 0) →
      (∃ s, Q.valuation (a s) = 1) → P.valuation (∑ s, algebraMap F F' (a s) * ω s) = 1)
    (hcard : Module.finrank F F' ≤ Fintype.card σ)
    (P₀ : ValuationSubring F') (hP₀ : P₀ ∈ S) (hindep : ∀ P ∈ S, P ≠ P₀ → P₀ ⊔ P = ⊤)
    (g : F') (hg : g ≠ 0) :
    ∃ h : F, P₀.valuation (algebraMap F F' h * g) = 1

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