NYLL
Module

ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
17 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring exists forall mem and sub mem nonunits

Imports12
  • Mathlib.RingTheory.Valuation.ValuationSubring
  • Mathlib.RingTheory.LocalRing.ResidueField.Basic
  • Mathlib.GroupTheory.OrderOfElement
  • Mathlib.Data.Fintype.Pigeonhole
  • Mathlib.RingTheory.Ideal.Operations
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Mathlib.Tactic.GCongr.Core
  • Mathlib.Tactic.Choose
  • Mathlib.Tactic.Ring.RingNF
  • Mathlib.Tactic.LinearCombination
  • Mathlib.Tactic.FieldSimp
  • Mathlib.Tactic.Linarith.Frontend
Imported by4

Declarations

theorem

pow_eq_self_of_orderOf_dvd

L41 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.pow_eq_self_of_orderOf_dvd
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
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

L46 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.eq_of_pow_eq_pow_of_not_isOfFinOrder
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
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

L59 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.exists_exponent
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
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

L108 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.exists_mul_mem_forall
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
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

inter

L192 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.inter
Documentation

The intersection of the given family of valuation rings.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
def inter (R : ι → ValuationSubring K) : Subring K
theorem

mem_inter

L194 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.mem_inter
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
theorem mem_inter {R : ι → ValuationSubring K} {z : K} : z ∈ inter R ↔ ∀ j, z ∈ R j
def

centre

L198 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.centre
Documentation

The ideal cut out on the intersection ring by one valuation's maximal ideal.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · full declaration
def centre (R : ι → ValuationSubring K) (j : ι) : Ideal (inter R) where
  carrier := {b | (R j).valuation (b : K) < 1}
  add_mem' {a b} ha hb := by
    change (R j).valuation ((a : K) + b) < 1
    exact Valuation.map_add_lt _ ha hb
  zero_mem' := by change (R j).valuation ((0 : inter R) : K) < 1; simp
  smul_mem' c b hb := by
    change (R j).valuation ((c : K) * b) < 1
    rw [map_mul]
    calc (R j).valuation (c : K) * (R j).valuation (b : K)
        ≤ 1 * (R j).valuation (b : K) := by
          gcongr
          exact ((R j).valuation_le_one_iff _).mpr (mem_inter.mp c.2 j)
      _ < 1 := by rwa [one_mul]
theorem

mem_centre

L213 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.mem_centre
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
theorem mem_centre {R : ι → ValuationSubring K} {j : ι} {b : inter R} :
    b ∈ centre R j ↔ (R j).valuation (b : K) < 1
theorem

valuation_eq_one_of_not_mem_centre

L216 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.valuation_eq_one_of_not_mem_centre
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
theorem valuation_eq_one_of_not_mem_centre {R : ι → ValuationSubring K} {j : ι} {b : inter R}
    (hb : b ∉ centre R j) : (R j).valuation (b : K) = 1
theorem

centre_isPrime

L220 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.centre_isPrime
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
theorem centre_isPrime (R : ι → ValuationSubring K) (j : ι) : (centre R j).IsPrime
theorem

isUnit_of_forall_not_mem_centre

L237 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.isUnit_of_forall_not_mem_centre
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
theorem isUnit_of_forall_not_mem_centre {R : ι → ValuationSubring K} (i : ι) {b : inter R}
    (hb : ∀ j, b ∉ centre R j) : IsUnit b
theorem

exists_le_centre

L250 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.exists_le_centre
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
theorem exists_le_centre [Finite ι] {R : ι → ValuationSubring K} (i : ι) {J : Ideal (inter R)}
    (hJ : J ≠ ⊤) : ∃ j, J ≤ centre R j
theorem

le_of_centre_le_centre

L265 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.le_of_centre_le_centre
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
theorem le_of_centre_le_centre [Finite ι] {R : ι → ValuationSubring K} {i j : ι}
    (h : centre R i ≤ centre R j) : R j ≤ R i
theorem

isCoprime_centre

L283 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.isCoprime_centre
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
theorem isCoprime_centre [Finite ι] {R : ι → ValuationSubring K}
    (hR : ∀ i j, R i ≤ R j → i = j) {i j : ι} (hij : i ≠ j) :
    IsCoprime (centre R i) (centre R j)
theorem

exists_mem_inter_sub_lt

L293 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.exists_mem_inter_sub_lt
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
theorem exists_mem_inter_sub_lt [Finite ι] {R : ι → ValuationSubring K}
    (hR : ∀ i j, R i ≤ R j → i = j) (i : ι) {a : K} (ha : a ∈ R i) :
    ∃ c ∈ inter R, (R i).valuation (c - a) < 1
theorem

exists_forall_mem_and_sub_mem_nonunits'

L327 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits.ValuationSubring.W7XK3A.exists_forall_mem_and_sub_mem_nonunits'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
namespace ValuationSubring
open _root_.ValuationSubring
namespace W7XK3A
open _root_.ValuationSubring
open IsLocalRing
variable {K : Type*} [Field K] {ι : Type*}
Lean source · statement
theorem exists_forall_mem_and_sub_mem_nonunits' [Finite ι] (R : ι → ValuationSubring K)
    (hR : ∀ i j, R i ≤ R j → i = j) (a : ι → K) (ha : ∀ i, a i ∈ R i) :
    ∃ z : K, ∀ i, z ∈ R i ∧ z - a i ∈ (R i).nonunits
theorem

exists_forall_mem_and_sub_mem_nonunits

L346 ↗
ValuationSubring.exists_forall_mem_and_sub_mem_nonunits
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
open ValuationSubring.W7XK3A in
Lean source · statement
theorem _root_.ValuationSubring.exists_forall_mem_and_sub_mem_nonunits
    {K : Type*} [Field K] {ι : Type*} [Finite ι] (R : ι → ValuationSubring K)
    (hR : ∀ i j, R i ≤ R j → i = j) (a : ι → K) (ha : ∀ i, a i ∈ R i) :
    ∃ z : K, ∀ i, z ∈ R i ∧ z - a i ∈ (R i).nonunits

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