NYLL
Module

Place_evalAt_trace_eq_sum_fiber.lean

Nyll.AlgebraicCurves.Places.Place_evalAt_trace_eq_sum_fiber
59 declarations indexed from sourceView source ↗

Module documentation

Place eval At trace eq sum fiber

Imports8
Imported by1

Declarations

theorem

trace_of_subsingleton

L41 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.trace_of_subsingleton
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
section AbstractTrace
Lean source · statement
theorem trace_of_subsingleton {R A : Type*} [CommRing R] [CommRing A]
    [Algebra R A] [Subsingleton A] (a : A) : Algebra.trace R A a = 0
theorem

trace_eq_smul_finrank_of_isNilpotent_sub_algebraMap

L45 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.trace_eq_smul_finrank_of_isNilpotent_sub_algebraMap
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
section AbstractTrace
Lean source · statement
theorem trace_eq_smul_finrank_of_isNilpotent_sub_algebraMap {R A : Type*}
    [CommRing R] [IsReduced R] [StrongRankCondition R] [CommRing A] [Algebra R A]
    [Module.Free R A] {a : A} {μ : R} (h : IsNilpotent (a - algebraMap R A μ)) :
    Algebra.trace R A a = Module.finrank R A • μ
theorem

ord_pos_of_not_isUnit

L60 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.ord_pos_of_not_isUnit
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_pos_of_not_isUnit (v : Place K F) {a : v.toValuationSubring} (ha : a ≠ 0)
    (hu : ¬IsUnit a) : 0 < v.ord (a : F)
theorem

ord_neg_of_not_mem

L73 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.ord_neg_of_not_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_neg_of_not_mem (v : Place K F) {f : F} (hf : f ∉ v.toValuationSubring) :
    v.ord f < 0
theorem

mem_of_ord_nonneg

L99 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.mem_of_ord_nonneg
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
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_nonneg_of_mem

L104 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.ord_nonneg_of_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
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_iff_ord_nonneg

L114 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.mem_iff_ord_nonneg
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mem_iff_ord_nonneg (v : Place K F) {f : F} (_hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f
theorem

eq_ord_of_addHom_of_nonneg_iff

L118 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.eq_ord_of_addHom_of_nonneg_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem eq_ord_of_addHom_of_nonneg_iff (w : Place K F) (φ : F → ℤ)
    (hmul : ∀ x y, x ≠ 0 → y ≠ 0 → φ (x * y) = φ x + φ y)
    (hone : ∃ t, t ≠ 0 ∧ φ t = 1)
    (hiff : ∀ x, x ≠ 0 → (0 ≤ φ x ↔ x ∈ w.toValuationSubring))
    {x : F} (hx : x ≠ 0) : φ x = w.ord x
theorem

residue_algebraMap

L183 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.residue_algebraMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem residue_algebraMap (v : Place K F) (lam : K) :
    IsLocalRing.residue v.toValuationSubring (algebraMap K v.toValuationSubring lam)
      = algebraMap K v.ResidueField lam
theorem

algebraMap_evalAt_coe

L188 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.algebraMap_evalAt_coe
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem algebraMap_evalAt_coe (v : Place K F) (hv : v.IsRational) (r : v.toValuationSubring) :
    algebraMap K v.ResidueField
        (v.evalAt (algebraMap v.toValuationSubring F r))
      = IsLocalRing.residue v.toValuationSubring r
theorem

neg_log_valuation_fiberCenter_eq_ord

L210 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.neg_log_valuation_fiberCenter_eq_ord
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem neg_log_valuation_fiberCenter_eq_ord (hw : w.restrict F = v) {x : F'} (hx : x ≠ 0) :
    -log ((fiberCenter F' v hw).valuation F' x) = w.ord x
theorem

le_ord_iff_mem_pow_fiberCenter

L249 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.le_ord_iff_mem_pow_fiberCenter
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem le_ord_iff_mem_pow_fiberCenter (hw : w.restrict F = v)
    {c : integralClosureAt F' v} (hc : c ≠ 0) (n : ℕ) :
    (n : ℤ) ≤ w.ord (algebraMap (integralClosureAt F' v) F' c) ↔
      c ∈ (fiberCenter F' v hw).asIdeal ^ n
theorem

ramificationIndex_eq_ramificationIdx_fiberCenter

L272 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.ramificationIndex_eq_ramificationIdx_fiberCenter
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem ramificationIndex_eq_ramificationIdx_fiberCenter (hw : w.restrict F = v) :
    w.ramificationIndex F =
      (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
        (fiberCenter F' v hw).asIdeal
def

toValuationSubringOfRestrictEq

L299 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.toValuationSubringOfRestrictEq
Documentation

The map from the integral closure to the valuation subring of the extending place.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def toValuationSubringOfRestrictEq (hw : w.restrict F = v) :
    integralClosureAt F' v →+* w.toValuationSubring
theorem

coe_toValuationSubringOfRestrictEq

L306 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.coe_toValuationSubringOfRestrictEq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in
Lean source · statement
theorem coe_toValuationSubringOfRestrictEq (hw : w.restrict F = v)
    (c : integralClosureAt F' v) :
    (toValuationSubringOfRestrictEq hw c : F')
      = algebraMap (integralClosureAt F' v) F' c
def

residueOfCenter

L312 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.residueOfCenter
Documentation

The residue homomorphism on the integral closure, induced by the place above v.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def residueOfCenter (hw : w.restrict F = v) :
    integralClosureAt F' v →+* w.ResidueField
theorem

residueOfCenter_apply

L317 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.residueOfCenter_apply
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in
Lean source · statement
theorem residueOfCenter_apply (hw : w.restrict F = v) (c : integralClosureAt F' v) :
    residueOfCenter hw c = IsLocalRing.residue w.toValuationSubring
      (toValuationSubringOfRestrictEq hw c)
theorem

ker_residueOfCenter

L321 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.ker_residueOfCenter
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem ker_residueOfCenter (hw : w.restrict F = v) :
    RingHom.ker (residueOfCenter hw) = (fiberCenter F' v hw).asIdeal
theorem

surjective_residueOfCenter

L327 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.surjective_residueOfCenter
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem surjective_residueOfCenter (hw : w.restrict F = v) :
    Function.Surjective (residueOfCenter hw)
def

residueFieldEquivQuotientCenter

L390 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.residueFieldEquivQuotientCenter
Documentation

The quotient by the fibre centre identified with the residue field of the place.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def residueFieldEquivQuotientCenter (hw : w.restrict F = v) :
    integralClosureAt F' v ⧸ (fiberCenter F' v hw).asIdeal ≃+* w.ResidueField
theorem

residueFieldEquivQuotientCenter_mk

L395 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.residueFieldEquivQuotientCenter_mk
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem residueFieldEquivQuotientCenter_mk (hw : w.restrict F = v)
    (c : integralClosureAt F' v) :
    residueFieldEquivQuotientCenter hw (Ideal.Quotient.mk _ c) = residueOfCenter hw c
def

placeCongrEquiv

L405 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.placeCongrEquiv
Documentation

The valuation-subring equivalence induced by equality of two places.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · full declaration
def placeCongrEquiv {u u' : Place K F} (h : u = u') :
    u.toValuationSubring ≃+* u'.toValuationSubring where
  toFun x := ⟨x.1, h ▸ x.2⟩
  invFun x := ⟨x.1, h.symm ▸ x.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl
  map_add' _ _ := rfl
theorem

coe_placeCongrEquiv

L414 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.coe_placeCongrEquiv
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem coe_placeCongrEquiv {u u' : Place K F} (h : u = u') (x : u.toValuationSubring) :
    (placeCongrEquiv h x : F) = (x : F)
def

restrictResidueFieldEquiv

L418 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.restrictResidueFieldEquiv
Documentation

The residue-field equivalence induced by equality of the restricted and base places.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def restrictResidueFieldEquiv (hw : w.restrict F = v) :
    (w.restrict F).ResidueField ≃+* IsLocalRing.ResidueField v.toValuationSubring
theorem

restrictResidueFieldEquiv_residue

L423 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.restrictResidueFieldEquiv_residue
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in
Lean source · statement
theorem restrictResidueFieldEquiv_residue (hw : w.restrict F = v)
    (a : (w.restrict F).toValuationSubring) :
    restrictResidueFieldEquiv hw (IsLocalRing.residue _ a)
      = IsLocalRing.residue _ (placeCongrEquiv hw a)
theorem

inertiaDeg_eq_inertiaDeg_fiberCenter

L430 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict.inertiaDeg_eq_inertiaDeg_fiberCenter
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Dict
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem inertiaDeg_eq_inertiaDeg_fiberCenter (hw : w.restrict F = v) :
    w.inertiaDeg F =
      (fiberCenter F' v hw).asIdeal.inertiaDeg v.toValuationSubring
instance

(anonymous instance)

L468 ↗
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
Lean source · statement
instance : DecidableEq (Place K F')
instance

instFreeIntegralClosureAt

L472 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.instFreeIntegralClosureAt
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
Lean source · statement
instance instFreeIntegralClosureAt : Module.Free v.toValuationSubring (integralClosureAt F'
  v)
abbrev

conductorIdeal

L477 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal
Documentation

The extension of the maximal ideal of the base valuation ring to the integral closure.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
Lean source · statement
abbrev conductorIdeal : Ideal (integralClosureAt F' v)
theorem

conductorIdeal_ne_bot

L482 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal_ne_bot
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
omit [Algebra K F'] [IsScalarTower K F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] in
Lean source · statement
theorem conductorIdeal_ne_bot : conductorIdeal (F' := F') v ≠ ⊥
instance

conductorQuotientAlgebra

L491 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.conductorQuotientAlgebra
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
Lean source · statement
instance conductorQuotientAlgebra :
    Algebra (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ conductorIdeal (F' := F') v)
theorem

residue_trace_eq_trace_mk

L497 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.residue_trace_eq_trace_mk
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
omit [Algebra K F'] [IsScalarTower K F F'] in
Lean source · statement
theorem residue_trace_eq_trace_mk (c : integralClosureAt F' v) :
    IsLocalRing.residue v.toValuationSubring
        (Algebra.trace v.toValuationSubring (integralClosureAt F' v) c)
      = Algebra.trace (IsLocalRing.ResidueField v.toValuationSubring)
          (integralClosureAt F' v ⧸ conductorIdeal (F' := F') v)
          (Ideal.Quotient.mk (conductorIdeal (F' := F') v) c)
abbrev

fiberCenterPow

L508 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.fiberCenterPow
Documentation

The ideal of the fibre centre raised to its ramification index.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
Lean source · statement
abbrev fiberCenterPow (hw : w.restrict F = v) : Ideal (integralClosureAt F' v)
theorem

conductorIdeal_le_fiberCenterPow

L513 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal_le_fiberCenterPow
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
Lean source · statement
theorem conductorIdeal_le_fiberCenterPow (hw : w.restrict F = v) :
    conductorIdeal (F' := F') v ≤ fiberCenterPow hw
instance

fiberCenterPowQuotientAlgebra

L517 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.fiberCenterPowQuotientAlgebra
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
Lean source · statement
instance fiberCenterPowQuotientAlgebra (hw : w.restrict F = v) :
    Algebra (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ fiberCenterPow hw)
instance

instFiniteFiberCenterPowQuot

L523 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.instFiniteFiberCenterPowQuot
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
Lean source · statement
instance instFiniteFiberCenterPowQuot (hw : w.restrict F = v) :
    Module.Finite (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ fiberCenterPow hw)
instance

instFreeFiberCenterPowQuot

L533 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.instFreeFiberCenterPowQuot
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
Lean source · statement
instance instFreeFiberCenterPowQuot (hw : w.restrict F = v) :
    Module.Free (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ fiberCenterPow hw)
theorem

isNilpotent_mk_sub_algebraMap

L538 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.isNilpotent_mk_sub_algebraMap
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
Lean source · statement
theorem isNilpotent_mk_sub_algebraMap (hw : w.restrict F = v) {c : integralClosureAt F' v}
    {r : v.toValuationSubring}
    (hr : c - algebraMap v.toValuationSubring (integralClosureAt F' v) r
      ∈ (fiberCenter F' v hw).asIdeal) :
    IsNilpotent (Ideal.Quotient.mk (fiberCenterPow hw) c
      - algebraMap (IsLocalRing.ResidueField v.toValuationSubring)
          (integralClosureAt F' v ⧸ fiberCenterPow hw)
          (IsLocalRing.residue v.toValuationSubring r))
theorem

trace_mk_fiberCenterPow

L556 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.trace_mk_fiberCenterPow
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
Lean source · statement
theorem trace_mk_fiberCenterPow (hw : w.restrict F = v) {c : integralClosureAt F' v}
    {r : v.toValuationSubring}
    (hr : c - algebraMap v.toValuationSubring (integralClosureAt F' v) r
      ∈ (fiberCenter F' v hw).asIdeal) :
    Algebra.trace (IsLocalRing.ResidueField v.toValuationSubring)
        (integralClosureAt F' v ⧸ fiberCenterPow hw)
        (Ideal.Quotient.mk (fiberCenterPow hw) c)
      = Module.finrank (IsLocalRing.ResidueField v.toValuationSubring)
            (integralClosureAt F' v ⧸ fiberCenterPow hw)
          • IsLocalRing.residue v.toValuationSubring r
theorem

finrank_fiberCenterPow

L568 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.finrank_fiberCenterPow
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
Lean source · statement
theorem finrank_fiberCenterPow (hw : w.restrict F = v) (hwrat : w.IsRational)
    (hvrat : v.IsRational) :
    Module.finrank (IsLocalRing.ResidueField v.toValuationSubring)
        (integralClosureAt F' v ⧸ fiberCenterPow hw)
      = w.ramificationIndex F
def

fiberIdeal

L597 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.fiberIdeal
Documentation

The ramification power for a place above v, and the unit ideal for other places.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
Lean source · statement
def fiberIdeal (w : Place K F') : Ideal (integralClosureAt F' v)
theorem

fiberIdeal_of_mem

L601 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.fiberIdeal_of_mem
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
omit [HasPrincipalDivisors K F'] in
Lean source · statement
theorem fiberIdeal_of_mem {w : Place K F'} (hw : w.restrict F = v) :
    fiberIdeal v w = fiberCenterPow hw
theorem

fiberIdeal_of_notMem

L605 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.fiberIdeal_of_notMem
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
omit [HasPrincipalDivisors K F'] in
Lean source · statement
theorem fiberIdeal_of_notMem {w : Place K F'} (hw : ¬w.restrict F = v) :
    fiberIdeal v w = ⊤
theorem

conductorIdeal_le_fiberIdeal

L609 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal_le_fiberIdeal
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
omit [HasPrincipalDivisors K F'] in
Lean source · statement
theorem conductorIdeal_le_fiberIdeal (w : Place K F') :
    conductorIdeal (F' := F') v ≤ fiberIdeal v w
theorem

isCoprime_fiberIdeal

L618 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.isCoprime_fiberIdeal
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
omit [HasPrincipalDivisors K F'] in
Lean source · statement
theorem isCoprime_fiberIdeal {w w' : Place K F'} (hne : w ≠ w') :
    IsCoprime (fiberIdeal v w) (fiberIdeal v w')
theorem

count_normalizedFactors_conductorIdeal

L636 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.count_normalizedFactors_conductorIdeal
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
omit [HasPrincipalDivisors K F'] in
Lean source · statement
theorem count_normalizedFactors_conductorIdeal {w : Place K F'} (hw : w.restrict F = v) :
    (normalizedFactors (conductorIdeal (F' := F') v)).count (fiberCenter F' v hw).asIdeal
      = (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
          (fiberCenter F' v hw).asIdeal
theorem

conductorIdeal_eq_prod_fiber

L644 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal_eq_prod_fiber
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
Lean source · statement
theorem conductorIdeal_eq_prod_fiber :
    conductorIdeal (F' := F') v = ∏ w ∈ v.fiber F', fiberIdeal v w
theorem

prod_fiberIdeal_le_of_subset

L689 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.prod_fiberIdeal_le_of_subset
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
omit [HasPrincipalDivisors K F'] in
Lean source · statement
theorem prod_fiberIdeal_le_of_subset {s t : Finset (Place K F')} (hst : s ⊆ t) :
    ∏ w ∈ t, fiberIdeal v w ≤ ∏ w ∈ s, fiberIdeal v w
theorem

conductorIdeal_le_prod_fiberIdeal

L695 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal_le_prod_fiberIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
Lean source · statement
theorem conductorIdeal_le_prod_fiberIdeal (s : Finset (Place K F')) :
    conductorIdeal (F' := F') v ≤ ∏ w ∈ s, fiberIdeal v w
instance

fiberIdealQuotientAlgebra

L707 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.fiberIdealQuotientAlgebra
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
Lean source · statement
instance fiberIdealQuotientAlgebra (w : Place K F') :
    Algebra (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ fiberIdeal v w)
instance

prodFiberIdealQuotientAlgebra

L713 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.prodFiberIdealQuotientAlgebra
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
Lean source · statement
instance prodFiberIdealQuotientAlgebra (s : Finset (Place K F')) :
    Algebra (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ ∏ w ∈ s, fiberIdeal v w)
theorem

finite_quotient_of_conductorLE

L721 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.finite_quotient_of_conductorLE
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
omit [HasPrincipalDivisors K F'] in
omit [Algebra K F'] [IsScalarTower K F F'] in
Lean source · statement
theorem finite_quotient_of_conductorLE (Q : Ideal (integralClosureAt F' v))
    [Algebra (IsLocalRing.ResidueField v.toValuationSubring) (integralClosureAt F' v ⧸ Q)]
    [IsScalarTower v.toValuationSubring (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ Q)] :
    Module.Finite (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ Q)
theorem

trace_mk_prod_fiberIdeal

L731 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.trace_mk_prod_fiberIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
Lean source · statement
theorem trace_mk_prod_fiberIdeal (c : integralClosureAt F' v) (s : Finset (Place K F')) :
    Algebra.trace (IsLocalRing.ResidueField v.toValuationSubring)
        (integralClosureAt F' v ⧸ ∏ w ∈ s, fiberIdeal v w)
        (Ideal.Quotient.mk (∏ w ∈ s, fiberIdeal v w) c)
      = ∑ w ∈ s,
          Algebra.trace (IsLocalRing.ResidueField v.toValuationSubring)
            (integralClosureAt F' v ⧸ fiberIdeal v w)
            (Ideal.Quotient.mk (fiberIdeal v w) c)
theorem

trace_mk_conductor_eq_sum_fiber

L819 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.trace_mk_conductor_eq_sum_fiber
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
Lean source · statement
theorem trace_mk_conductor_eq_sum_fiber (c : integralClosureAt F' v) :
    Algebra.trace (IsLocalRing.ResidueField v.toValuationSubring)
        (integralClosureAt F' v ⧸ conductorIdeal (F' := F') v)
        (Ideal.Quotient.mk (conductorIdeal (F' := F') v) c)
      = ∑ w ∈ v.fiber F',
          Algebra.trace (IsLocalRing.ResidueField v.toValuationSubring)
            (integralClosureAt F' v ⧸ fiberIdeal v w)
            (Ideal.Quotient.mk (fiberIdeal v w) c)
theorem

trace_mk_fiberIdeal_eq_trace_mk_fiberCenterPow

L848 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks.trace_mk_fiberIdeal_eq_trace_mk_fiberCenterPow
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Blocks
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Dict
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
variable {v} {w : Place K F'}
variable (v) [HasPrincipalDivisors K F']
omit [HasPrincipalDivisors K F'] in
Lean source · statement
theorem trace_mk_fiberIdeal_eq_trace_mk_fiberCenterPow [HasPrincipalDivisors K F']
    {w : Place K F'} (hw : w.restrict F = v) (c : integralClosureAt F' v) :
    Algebra.trace (IsLocalRing.ResidueField v.toValuationSubring)
        (integralClosureAt F' v ⧸ fiberIdeal v w)
        (Ideal.Quotient.mk (fiberIdeal v w) c)
      = Algebra.trace (IsLocalRing.ResidueField v.toValuationSubring)
          (integralClosureAt F' v ⧸ fiberCenterPow hw)
          (Ideal.Quotient.mk (fiberCenterPow hw) c)
theorem

sub_algebraMap_evalAt_mem_fiberCenter

L885 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Assembly.sub_algebraMap_evalAt_mem_fiberCenter
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Assembly
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks
variable {v : Place K F} [HasPrincipalDivisors K F']
omit [HasPrincipalDivisors K F'] in
Lean source · statement
theorem sub_algebraMap_evalAt_mem_fiberCenter {w : Place K F'} (hw : w.restrict F = v)
    (hwrat : w.IsRational) (c : integralClosureAt F' v) :
    c - algebraMap v.toValuationSubring (integralClosureAt F' v)
        (algebraMap K v.toValuationSubring
          (w.evalAt (algebraMap (integralClosureAt F' v) F' c)))
      ∈ (fiberCenter F' v hw).asIdeal
instance

(anonymous instance)

L930 ↗
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Assembly
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks
variable {v : Place K F} [HasPrincipalDivisors K F']
Lean source · statement
instance : DecidableEq (Place K F')
theorem

residue_trace_eq_sum_evalAt

L932 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Assembly.residue_trace_eq_sum_evalAt
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceValueProof
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
namespace Assembly
open _root_.AlgebraicCurve.Place hiding mem_iff_ord_nonneg ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open _root_.AlgebraicCurves.Places.Proofs
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve.TraceValueProof.Blocks
variable {v : Place K F} [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
Lean source · statement
theorem residue_trace_eq_sum_evalAt (hv : v.IsRational)
    (hrat : ∀ w ∈ v.fiber F', Place.IsRational w) (c : integralClosureAt F' v) :
    IsLocalRing.residue v.toValuationSubring
        (Algebra.trace v.toValuationSubring (integralClosureAt F' v) c)
      = ∑ w ∈ v.fiber F',
          w.ramificationIndex F
            • algebraMap K v.ResidueField
                (w.evalAt (algebraMap (integralClosureAt F' v) F' c))
theorem

evalAt_trace_eq_sum_fiber

L963 ↗
AlgebraicCurve.Place.evalAt_trace_eq_sum_fiber
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_trace_eq_sum_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
open _root_.AlgebraicCurves.Places.Proofs in
open _root_.AlgebraicCurve.Place hiding
  mem_iff_ord_nonneg
  ord_nonneg_of_mem
  le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord
  eq_ord_of_addHom_of_nonneg_iff in
open _root_.AlgebraicCurve in
open Place_evalAt_trace_eq_sum_fiber.AlgebraicCurve in
open TraceValueProof in
open TraceValueProof.Assembly in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.evalAt_trace_eq_sum_fiber {K F F' : Type*} [Field K] [Field F]
    [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F'] [HasPrincipalDivisors K F']
    (v : Place K F) (hv : v.IsRational) (hrat : ∀ w ∈ v.fiber F', Place.IsRational w)
    (f : F') (hf : f ≠ 0) (hord : ∀ w ∈ v.fiber F', w.ord f = 0) :
    v.evalAt (Algebra.trace F F' f) = ∑ w ∈ v.fiber F', w.ramificationIndex F • w.evalAt f

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