NYLL
Module

Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.lean

Nyll.AlgebraicCurves.Places.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
14 declarations indexed from sourceView source ↗

Module documentation

Place exists is Integral adjoin eq top ord sub algebra Map eq one

Imports4
Imported by2

Declarations

theorem

ord_nonneg_of_mem

L41 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.ord_nonneg_of_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_nonneg_of_mem (v : Place K F) {f : F} (hf : f ∈ v.toValuationSubring) :
    0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L54 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.mem_of_ord_nonneg
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mem_of_ord_nonneg (v : Place K F) {f : F} (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring
theorem

ord_eq_zero_of_mem_of_inv_mem

L64 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.ord_eq_zero_of_mem_of_inv_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_eq_zero_of_mem_of_inv_mem (v : Place K F) {f : F} (hf : f ∈ v.toValuationSubring)
    (hfi : f⁻¹ ∈ v.toValuationSubring) : v.ord f = 0
theorem

ord_algebraMap

L71 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.ord_algebraMap
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_algebraMap (v : Place K F) (c : K) : v.ord (algebraMap K F c) = 0
theorem

ord_neg

L77 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.ord_neg
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_neg (v : Place K F) (a : F) : v.ord (-a) = v.ord a
theorem

ord_add_eq_of_lt

L83 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.ord_add_eq_of_lt
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_add_eq_of_lt (v : Place K F) {a b : F} (ha : a ≠ 0) (hb : b ≠ 0)
    (h : v.ord a < v.ord b) : a + b ≠ 0 ∧ v.ord (a + b) = v.ord a
theorem

ord_add_eq_of_lt'

L100 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.ord_add_eq_of_lt'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_add_eq_of_lt' (v : Place K F) {a b : F} (ha : a ≠ 0)
    (h : b = 0 ∨ v.ord a < v.ord b) : a + b ≠ 0 ∧ v.ord (a + b) = v.ord a
def

kC

L118 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.kC
Documentation

A base-field constant viewed in the integral closure at the chosen place.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section Fibre
variable {K E F : Type*} [Field K] [Field E] [Field F] [Algebra K E] [Algebra K F] [Algebra E F]
  [IsScalarTower K E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
variable (v : Place K E)
Lean source · statement
def kC (a : K) : Place.integralClosureAt F v
theorem

algebraMap_kC

L122 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.algebraMap_kC
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section Fibre
variable {K E F : Type*} [Field K] [Field E] [Field F] [Algebra K E] [Algebra K F] [Algebra E F]
  [IsScalarTower K E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
variable (v : Place K E)
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] in
Lean source · statement
theorem algebraMap_kC (a : K) :
    algebraMap (Place.integralClosureAt F v) F (kC (F := F) v a) = algebraMap K F a
theorem

exists_uniformizer_mem

L129 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.exists_uniformizer_mem
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section Fibre
variable {K E F : Type*} [Field K] [Field E] [Field F] [Algebra K E] [Algebra K F] [Algebra E F]
  [IsScalarTower K E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
variable (v : Place K E)
variable {v}
Lean source · statement
theorem exists_uniformizer_mem {w : Place K F} (hw : w.restrict E = v) :
    ∃ π : Place.integralClosureAt F v,
      π ∈ (Place.fiberCenter F v hw).asIdeal ∧
      w.ord (algebraMap (Place.integralClosureAt F v) F π) = 1
theorem

two_le_ord_of_mem_sq

L147 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.two_le_ord_of_mem_sq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section Fibre
variable {K E F : Type*} [Field K] [Field E] [Field F] [Algebra K E] [Algebra K F] [Algebra E F]
  [IsScalarTower K E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
variable (v : Place K E)
variable {v}
Lean source · statement
theorem two_le_ord_of_mem_sq {w : Place K F} (hw : w.restrict E = v)
    {r : Place.integralClosureAt F v} (hr : r ∈ (Place.fiberCenter F v hw).asIdeal ^ 2) :
    algebraMap (Place.integralClosureAt F v) F r = 0 ∨
      2 ≤ w.ord (algebraMap (Place.integralClosureAt F v) F r)
theorem

one_le_ord_of_mem

L156 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.one_le_ord_of_mem
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section Fibre
variable {K E F : Type*} [Field K] [Field E] [Field F] [Algebra K E] [Algebra K F] [Algebra E F]
  [IsScalarTower K E F] [FiniteDimensional E F] [Algebra.IsSeparable E F]
variable (v : Place K E)
variable {v}
Lean source · statement
theorem one_le_ord_of_mem {w : Place K F} (hw : w.restrict E = v)
    {r : Place.integralClosureAt F v} (hr : r ∈ (Place.fiberCenter F v hw).asIdeal) :
    algebraMap (Place.integralClosureAt F v) F r = 0 ∨
      1 ≤ w.ord (algebraMap (Place.integralClosureAt F v) F r)
theorem

main

L172 ↗
AlgebraicCurves.Places.Proofs.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one.AlgebraicCurve.AdaptedPrimitiveProof.main
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace AdaptedPrimitiveProof
open _root_.AlgebraicCurve
section Construction
variable {K E F : Type*} [Field K] [Field E] [Field F] [Algebra K E] [Algebra K F] [Algebra E F]
  [IsScalarTower K E F] [Infinite K] [FiniteDimensional E F] [Algebra.IsSeparable E F]
Lean source · statement
theorem main (w : Place K F) :
    ∃ θ : F, IsIntegral (w.restrict E).toValuationSubring θ ∧
      IntermediateField.adjoin E ({θ} : Set F) = ⊤ ∧
      ∃ c : K, w.ord (θ - algebraMap K F c) = 1 ∧
        ∀ w' : Place K F, w'.restrict E = w.restrict E → w' ≠ w →
          w'.ord (θ - algebraMap K F c) = 0
theorem

exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one

L331 ↗
AlgebraicCurve.Place.exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsLocalRing
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
    {K E F : Type*} [Field K] [Field E] [Field F] [Algebra K E] [Algebra K F] [Algebra E F]
    [IsScalarTower K E F] [Infinite K] [FiniteDimensional E F] [Algebra.IsSeparable E F]
    (w : AlgebraicCurve.Place K F) :
    ∃ θ : F, IsIntegral (w.restrict E).toValuationSubring θ ∧
      IntermediateField.adjoin E ({θ} : Set F) = ⊤ ∧
      ∃ c : K, w.ord (θ - algebraMap K F c) = 1 ∧
        ∀ w' : AlgebraicCurve.Place K F, w'.restrict E = w.restrict E → w' ≠ w →
          w'.ord (θ - algebraMap K F c) = 0

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