NYLL
Module

Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.lean

Nyll.AlgebraicCurves.Places.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
15 declarations indexed from sourceView source ↗

Module documentation

Place card fiber eq finrank adjoin of ord eq one

Imports11
Imported by1

Declarations

theorem

evalAt_sub_algebraMap

L47 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.evalAt_sub_algebraMap
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem evalAt_sub_algebraMap {F : Type*} [Field F] [Algebra ℂ F]
    (v : Place ℂ F) (hv : v.IsRational) {f : F} (hf : f ∈ v.toValuationSubring) (c : ℂ) :
    v.evalAt (f - algebraMap ℂ F c) = v.evalAt f - c
theorem

evalAt_eq_zero_of_ord_pos

L59 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.evalAt_eq_zero_of_ord_pos
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem evalAt_eq_zero_of_ord_pos {F : Type*} [Field F] [Algebra ℂ F]
    (v : Place ℂ F) {g : F} (hg : g ≠ 0) (h : 0 < v.ord g) : v.evalAt g = 0
theorem

ord_eq_zero_of_evalAt_ne_zero

L75 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.ord_eq_zero_of_evalAt_ne_zero
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_eq_zero_of_evalAt_ne_zero {F : Type*} [Field F] [Algebra ℂ F]
    (v : Place ℂ F) {g : F} (hg : g ≠ 0) (hmem : g ∈ v.toValuationSubring)
    (hne : v.evalAt g ≠ 0) : v.ord g = 0
theorem

ord_pos_of_evalAt_eq_zero

L83 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.ord_pos_of_evalAt_eq_zero
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_pos_of_evalAt_eq_zero {F : Type*} [Field F] [Algebra ℂ F]
    (v : Place ℂ F) (hv : v.IsRational) {g : F} (hg : g ≠ 0)
    (hmem : g ∈ v.toValuationSubring) (hz : v.evalAt g = 0) : 0 < v.ord g
theorem

ord_multiset_prod

L91 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.ord_multiset_prod
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_multiset_prod {F : Type*} [Field F] [Algebra ℂ F]
    (v : Place ℂ F) (s : Multiset F) (hs : ∀ x ∈ s, x ≠ 0) :
    v.ord s.prod = (s.map v.ord).sum
theorem

ord_algebraMap_eq_zero

L103 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.ord_algebraMap_eq_zero
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_algebraMap_eq_zero {F : Type*} [Field F] [Algebra ℂ F]
    (v : Place ℂ F) {c : ℂ} (hc : c ≠ 0) : v.ord (algebraMap ℂ F c) = 0
theorem

sum_map_ite_count

L118 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.sum_map_ite_count
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem sum_map_ite_count (t : ℂ) (e : ℤ) (s : Multiset ℂ) :
    (s.map (fun r => if r = t then e else 0)).sum = (s.count t : ℤ) * e := by
  classical
  induction s using Multiset.induction_on with
  | empty => simp
  | cons a s ih =>
    rw [Multiset.map_cons, Multiset.sum_cons, ih, Multiset.count_cons]
    by_cases h : a = t
    · rw [ite_eq_left h, ite_eq_left h.symm]
      push_cast
      ring
    · rw [ite_eq_right h, ite_eq_right (fun hh => h hh.symm)]
      push_cast
      ring
theorem

ord_aeval

L133 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.ord_aeval
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_aeval {F : Type*} [Field F] [Algebra ℂ F]
    (v : Place ℂ F) (hv : v.IsRational) {f : F} (htr : Transcendental ℂ f)
    (hmem : f ∈ v.toValuationSubring) {p : ℂ[X]} (hp : p ≠ 0) :
    v.ord (Polynomial.aeval f p)
      = v.ord (f - algebraMap ℂ F (v.evalAt f)) * p.rootMultiplicity (v.evalAt f)
theorem

restrict_eq_restrict

L179 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.restrict_eq_restrict
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem restrict_eq_restrict {F : Type*} [Field F] [Algebra ℂ F]
    (w w' : Place ℂ F) (hw : w.IsRational) (hw' : w'.IsRational) {f : F}
    (htr : Transcendental ℂ f) (hwm : f ∈ w.toValuationSubring)
    (hw'm : f ∈ w'.toValuationSubring) (hval : w.evalAt f = w'.evalAt f)
    [FiniteDimensional (↥(IntermediateField.adjoin ℂ ({f} : Set F))) F] :
    w.restrict (IntermediateField.adjoin ℂ ({f} : Set F))
      = w'.restrict (IntermediateField.adjoin ℂ ({f} : Set F))
theorem

card_fiber_eq_finrank

L245 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.card_fiber_eq_finrank
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem card_fiber_eq_finrank {F : Type*} [Field F] [Algebra ℂ F] [IsCurveOver ℂ F]
    {f : F} (htr : Transcendental ℂ f)
    [FiniteDimensional (↥(IntermediateField.adjoin ℂ ({f} : Set F))) F]
    (hrat : ∀ w : Place ℂ F, w.IsRational)
    (hratE : ∀ u : Place ℂ (↥(IntermediateField.adjoin ℂ ({f} : Set F))), u.IsRational)
    (t : ℂ) (w₀ : Place ℂ F) (h₀m : f ∈ w₀.toValuationSubring) (h₀v : w₀.evalAt f = t)
    (hunram : ∀ w : Place ℂ F, f ∈ w.toValuationSubring → w.evalAt f = t →
      w.ord (f - algebraMap ℂ F t) = 1) :
    Nat.card {P : Place ℂ F // f ∈ P.toValuationSubring ∧ P.evalAt f = t}
      = Module.finrank (↥(IntermediateField.adjoin ℂ ({f} : Set F))) F
theorem

transcendental_adjoin_self

L351 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.transcendental_adjoin_self
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem transcendental_adjoin_self {F : Type*} [Field F] [Algebra ℂ F] {f : F}
    (htr : Transcendental ℂ f) :
    Transcendental ℂ (⟨f, IntermediateField.mem_adjoin_simple_self ℂ f⟩ :
      ↥(IntermediateField.adjoin ℂ ({f} : Set F)))
theorem

ord_sub_evalAt_eq_one_of_generator

L365 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.ord_sub_evalAt_eq_one_of_generator
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_sub_evalAt_eq_one_of_generator {E : Type*} [Field E] [Algebra ℂ E]
    {x₀ : E} (htr : Transcendental ℂ x₀)
    (hgen : ∀ y : E, ∃ pn pd : ℂ[X],
      y = Polynomial.aeval x₀ pn / Polynomial.aeval x₀ pd)
    (v : Place ℂ E) (hvr : v.IsRational) (hvm : x₀ ∈ v.toValuationSubring) :
    v.ord (x₀ - algebraMap ℂ E (v.evalAt x₀)) = 1
theorem

generator_adjoin

L408 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.generator_adjoin
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem generator_adjoin {F : Type*} [Field F] [Algebra ℂ F] (f : F) :
    ∀ y : ↥(IntermediateField.adjoin ℂ ({f} : Set F)), ∃ pn pd : ℂ[X],
      y = Polynomial.aeval
          (⟨f, IntermediateField.mem_adjoin_simple_self ℂ f⟩ :
            ↥(IntermediateField.adjoin ℂ ({f} : Set F))) pn
        / Polynomial.aeval
          (⟨f, IntermediateField.mem_adjoin_simple_self ℂ f⟩ :
            ↥(IntermediateField.adjoin ℂ ({f} : Set F))) pd
theorem

ord_sub_eq_one_of_ramificationIndex_eq_one

L432 ↗
AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one.C0RegionD.ord_sub_eq_one_of_ramificationIndex_eq_one
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace C0RegionD
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_sub_eq_one_of_ramificationIndex_eq_one {F : Type*} [Field F] [Algebra ℂ F]
    {f : F} (htr : Transcendental ℂ f)
    [FiniteDimensional (↥(IntermediateField.adjoin ℂ ({f} : Set F))) F]
    (w : Place ℂ F)
    (hvr : (w.restrict (IntermediateField.adjoin ℂ ({f} : Set F))).IsRational)
    (hwm : f ∈ w.toValuationSubring) {t : ℂ} (hwt : w.evalAt f = t)
    (hre : w.ramificationIndex (↥(IntermediateField.adjoin ℂ ({f} : Set F))) = 1) :
    w.ord (f - algebraMap ℂ F t) = 1
theorem

card_fiber_eq_finrank_adjoin_of_ord_eq_one

L472 ↗
AlgebraicCurve.Place.card_fiber_eq_finrank_adjoin_of_ord_eq_one
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
open AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.card_fiber_eq_finrank_adjoin_of_ord_eq_one
    (F : Type*) [Field F] [Algebra ℂ F] [IsCurveOver ℂ F] [Algebra.EssFiniteType ℂ F]
    {f : F} (htr : Transcendental ℂ f)
    [FiniteDimensional (↥(IntermediateField.adjoin ℂ ({f} : Set F))) F]
    (hrat : ∀ w : Place ℂ F, w.IsRational)
    (hratE : ∀ u : Place ℂ (↥(IntermediateField.adjoin ℂ ({f} : Set F))), u.IsRational)
    (t : ℂ) (w₀ : Place ℂ F) (h₀m : f ∈ w₀.toValuationSubring) (h₀v : w₀.evalAt f = t)
    (hunram : ∀ w : Place ℂ F, f ∈ w.toValuationSubring → w.evalAt f = t →
      w.ord (f - algebraMap ℂ F t) = 1) :
    Nat.card {P : Place ℂ F // f ∈ P.toValuationSubring ∧ P.evalAt f = t}
      = Module.finrank (↥(IntermediateField.adjoin ℂ ({f} : Set F))) F

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