Module

ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff

21 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring sum finrank residue Field le finrank of forall mem iff

Imports1

Mathlib.RingTheory.Valuation.ValuationSubring

Imported by1

Nyll.AlgebraicCurves.Valuations.All

theorem

one_lt_valuation_of_not_mem

L32 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.one_lt_valuation_of_not_mem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem one_lt_valuation_of_not_mem (O : ValuationSubring F) {z : F} (hz : z ∉ O) :
    1 < O.valuation z

theorem

ne_zero_of_not_mem

L36 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.ne_zero_of_not_mem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem ne_zero_of_not_mem (O : ValuationSubring F) {z : F} (hz : z ∉ O) : z ≠ 0

theorem

residue_mk_eq_zero_iff

L39 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.residue_mk_eq_zero_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem residue_mk_eq_zero_iff (O : ValuationSubring F) {x : F} (hx : x ∈ O) :
    residue O ⟨x, hx⟩ = 0 ↔ O.valuation x < 1

theorem

residue_mk_eq_residue_mk_iff

L43 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.residue_mk_eq_residue_mk_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem residue_mk_eq_residue_mk_iff (O : ValuationSubring F) {x y : F} (hx : x ∈ O)
    (hy : y ∈ O) : residue O ⟨x, hx⟩ = residue O ⟨y, hy⟩ ↔ O.valuation (x - y) < 1

theorem

valuation_eq_one_of_residue_ne_zero

L48 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.valuation_eq_one_of_residue_ne_zero

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem valuation_eq_one_of_residue_ne_zero (O : ValuationSubring F) {x : F} (hx : x ∈ O)
    (h : residue O ⟨x, hx⟩ ≠ 0) : O.valuation x = 1

theorem

inv_mem_of_one_le

L54 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.inv_mem_of_one_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem inv_mem_of_one_le (O : ValuationSubring F) {u : F} (hu : 1 ≤ O.valuation u) :
    u⁻¹ ∈ O

theorem

inv_sub_one

L59 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.inv_sub_one

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem inv_sub_one (O : ValuationSubring F) {u : F} (h1 : O.valuation (u - 1) < 1) :
    O.valuation u = 1 ∧ u⁻¹ ∈ O ∧ O.valuation (u⁻¹ - 1) < 1

theorem

prod_sub_one

L75 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.prod_sub_one

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem prod_sub_one (O : ValuationSubring F) {ι : Type*} (s : Finset ι) (f : ι → F)
    (hf : ∀ l ∈ s, f l ∈ O ∧ O.valuation (f l - 1) < 1) :
    (∏ l ∈ s, f l) ∈ O ∧ O.valuation (∏ l ∈ s, f l - 1) < 1

theorem

geom_mem

L95 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.geom_mem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem geom_mem (O : ValuationSubring F) {z : F} (hz : z ∈ O) (m : ℕ) :
    (∑ k ∈ Finset.range m, z ^ k) ∈ O

theorem

residue_geom

L99 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.residue_geom

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem residue_geom (O : ValuationSubring F) {z : F} (hz : z ∈ O) (m : ℕ) :
    residue O ⟨∑ k ∈ Finset.range m, z ^ k, geom_mem O hz m⟩ =
      ∑ k ∈ Finset.range m, (residue O ⟨z, hz⟩) ^ k

theorem

valuation_geom_sub_one_lt

L110 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.valuation_geom_sub_one_lt

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem valuation_geom_sub_one_lt (O : ValuationSubring F) {z : F} (hz : z ∈ O)
    (hv : O.valuation z < 1) {m : ℕ} (hm : 1 ≤ m) :
    O.valuation ((∑ k ∈ Finset.range m, z ^ k) - 1) < 1

theorem

valuation_le_valuation_geom

L122 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.valuation_le_valuation_geom

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem valuation_le_valuation_geom (O : ValuationSubring F) {z : F} (hz : z ∉ O) {m : ℕ}
    (hm : 2 ≤ m) :
    (∑ k ∈ Finset.range m, z ^ k) ≠ 0 ∧
      O.valuation z ≤ O.valuation (∑ k ∈ Finset.range m, z ^ k)

theorem

geom_sum_ne_zero_of_not_dvd

L145 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.geom_sum_ne_zero_of_not_dvd

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · full declaration

theorem geom_sum_ne_zero_of_not_dvd {K : Type*} [Field K] (a : K) [Decidable (a = 1)] {m : ℕ}
    (h : ¬ ((if a = 1 then ringChar K else orderOf a) ∣ m)) :
    (∑ k ∈ Finset.range m, a ^ k) ≠ 0 := by
  intro hs
  apply h
  split_ifs with ha
  · subst ha
    simp only [one_pow, Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_one] at hs
    exact (ringChar.spec K m).mp hs
  · have hgeom := geom_sum_mul a m
    rw [hs, zero_mul, eq_comm, sub_eq_zero] at hgeom
    exact orderOf_dvd_of_pow_eq_one hgeom

theorem

badMod_ne_one

L158 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.badMod_ne_one

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · full declaration

theorem badMod_ne_one {K : Type*} [Field K] (a : K) [Decidable (a = 1)] :
    (if a = 1 then ringChar K else orderOf a) ≠ 1 := by
  split_ifs with ha
  · intro h1
    have h := ringChar.Nat.cast_ringChar (R := K)
    rw [h1, Nat.cast_one] at h
    exact one_ne_zero h
  · rwa [Ne, orderOf_eq_one_iff]

theorem

exists_geom_sum_ne_zero

L167 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.exists_geom_sum_ne_zero

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem exists_geom_sum_ne_zero {ι : Type*} [Finite ι] (κ : ι → Type*) [∀ i, Field (κ i)]
    (a : ∀ i, κ i) : ∃ m : ℕ, 2 ≤ m ∧ ∀ i, (∑ k ∈ Finset.range m, a i ^ k) ≠ 0

theorem

exists_mem_lt_one_not_mem

L188 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.exists_mem_lt_one_not_mem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem exists_mem_lt_one_not_mem (O₁ O₂ : ValuationSubring F) (h₁₂ : ¬ O₁ ≤ O₂)
    (h₂₁ : ¬ O₂ ≤ O₁) : ∃ t ∈ O₁, O₁.valuation t < 1 ∧ t ∉ O₂

theorem

exists_lift

L211 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.exists_lift

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section valuationSubring
variable {F : Type*} [Field F]

Lean source · statement

theorem exists_lift {ι : Type*} [Finite ι] (O' : ι → ValuationSubring F)
    (hinc : ∀ i l, i ≠ l → ¬ O' i ≤ O' l) (j : ι) {y : F} (hy : y ∈ O' j) :
    ∃ r : F, (∀ i, r ∈ O' i) ∧ (O' j).valuation (r - y) < 1 ∧
      ∀ i, i ≠ j → (O' i).valuation r < 1

theorem

eq_of_le_of_over

L311 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.eq_of_le_of_over

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section algebraic
variable {E F : Type*} [Field E] [Field F] [Algebra E F]

Lean source · statement

theorem eq_of_le_of_over [Algebra.IsAlgebraic E F] (O : ValuationSubring E)
    {O₁ O₂ : ValuationSubring F} (hle : O₁ ≤ O₂)
    (h₁ : ∀ x : E, algebraMap E F x ∈ O₁ ↔ x ∈ O)
    (h₂ : ∀ x : E, algebraMap E F x ∈ O₂ ↔ x ∈ O) : O₁ = O₂

theorem

finite_and_finrank_le

L408 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.finite_and_finrank_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing
section linearAlgebra
variable {E F : Type*} [Field E] [Field F] [Algebra E F]

Lean source · statement

theorem finite_and_finrank_le [FiniteDimensional E F] (O : ValuationSubring E)
    {V : Type*} [AddCommGroup V] [Module (ResidueField O) V] (S : Set F) (ψ : F → V)
    (hψ : ∀ (s : Finset V) (c : V → O) (y : V → F), (∀ v ∈ s, y v ∈ S) →
      ψ (∑ v ∈ s, algebraMap E F (c v) * y v) = ∑ v ∈ s, residue O (c v) • ψ (y v))
    (hsurj : ∀ w : V, ∃ x ∈ S, ψ x = w) :
    Module.Finite (ResidueField O) V ∧
      Module.finrank (ResidueField O) V ≤ Module.finrank E F

theorem

result

L475 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff.EsbLeGen.result

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
namespace EsbLeGen
open IsLocalRing

Lean source · statement

theorem result {E F : Type*} [Field E] [Field F] [Algebra E F] [FiniteDimensional E F]
    (O : ValuationSubring E) {ι : Type*} [Fintype ι] (O' : ι → ValuationSubring F)
    (hinj : Function.Injective O')
    (hO : ∀ (j : ι) (x : E), algebraMap E F x ∈ O' j ↔ x ∈ O)
    [∀ j, Algebra (ResidueField O) (ResidueField (O' j))]
    (hcompat : ∀ (j : ι) (a : O), algebraMap (ResidueField O) (ResidueField (O' j))
        (residue O a) = residue (O' j) ⟨algebraMap E F a, (hO j a).mpr a.2⟩) :
    (∀ j, FiniteDimensional (ResidueField O) (ResidueField (O' j))) ∧
      ∑ j, Module.finrank (ResidueField O) (ResidueField (O' j)) ≤ Module.finrank E F

theorem

sum_finrank_residueField_le_finrank_of_forall_mem_iff

L550 ↗

ValuationSubring.sum_finrank_residueField_le_finrank_of_forall_mem_iff

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff

Lean source · statement

theorem _root_.ValuationSubring.sum_finrank_residueField_le_finrank_of_forall_mem_iff
    {E F : Type*} [Field E] [Field F] [Algebra E F]
    [FiniteDimensional E F]
    (O : ValuationSubring E)
    {ι : Type*} [Fintype ι]
    (O' : ι → ValuationSubring F)
    (hinj : Function.Injective O')
    (hO : ∀ (j : ι) (x : E), algebraMap E F x ∈ O' j ↔ x ∈ O)
    [∀ j, Algebra (IsLocalRing.ResidueField O) (IsLocalRing.ResidueField (O' j))]
    (hcompat : ∀ (j : ι) (a : O), algebraMap (IsLocalRing.ResidueField O) (IsLocalRing.ResidueField
      (O' j))
        (IsLocalRing.residue O a) = IsLocalRing.residue (O' j) ⟨algebraMap E F a, (hO j a).mpr
          a.2⟩) :
    (∀ j, FiniteDimensional (IsLocalRing.ResidueField O) (IsLocalRing.ResidueField (O' j))) ∧
      ∑ j, Module.finrank (IsLocalRing.ResidueField O) (IsLocalRing.ResidueField (O' j)) ≤
        Module.finrank E F

Module documentation

Valuation Subring sum finrank residue Field le finrank of forall mem iff

Declarations