Module

Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.lean

Nyll.AlgebraicCurves.Places.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt

61 declarations indexed from sourceView source ↗

Module documentation

Place mem and eval At trace eq sum ramification Index Along smul eval At

Imports14

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

trace_of_subsingleton

L48 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.trace_of_subsingleton

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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

L52 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.trace_eq_smul_finrank_of_isNilpotent_sub_algebraMap

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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

L67 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.ord_pos_of_not_isUnit

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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

L80 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.ord_neg_of_not_mem

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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

L106 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.mem_of_ord_nonneg

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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

L111 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.ord_nonneg_of_mem

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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

L121 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.mem_iff_ord_nonneg

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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

L125 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.eq_ord_of_addHom_of_nonneg_iff

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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

L190 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.residue_algebraMap

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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

L195 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.algebraMap_evalAt_coe

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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

L217 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.neg_log_valuation_fiberCenter_eq_ord

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L256 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.le_ord_iff_mem_pow_fiberCenter

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L279 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.ramificationIndex_eq_ramificationIdx_fiberCenter

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L306 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.toValuationSubringOfRestrictEq

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L312 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.coe_toValuationSubringOfRestrictEq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L318 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.residueOfCenter

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L322 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.residueOfCenter_apply

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L326 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.ker_residueOfCenter

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L332 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.surjective_residueOfCenter

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L395 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.residueFieldEquivQuotientCenter

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L400 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.residueFieldEquivQuotientCenter_mk

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L410 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.placeCongrEquiv

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L419 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.coe_placeCongrEquiv

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L423 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.restrictResidueFieldEquiv

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L427 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.restrictResidueFieldEquiv_residue

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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

L434 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Dict.inertiaDeg_eq_inertiaDeg_fiberCenter

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 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)

L470 ↗

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff

Lean source · statement

instance : DecidableEq (Place K F')

instance

instFreeIntegralClosureAt

L474 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.instFreeIntegralClosureAt

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L479 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal

Documentation

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

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L484 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal_ne_bot

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L493 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.conductorQuotientAlgebra

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L499 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.residue_trace_eq_trace_mk

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L510 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.fiberCenterPow

Documentation

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L515 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal_le_fiberCenterPow

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L519 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.fiberCenterPowQuotientAlgebra

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L525 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.instFiniteFiberCenterPowQuot

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L535 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.instFreeFiberCenterPowQuot

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L540 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.isNilpotent_mk_sub_algebraMap

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L558 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.trace_mk_fiberCenterPow

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L570 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.finrank_fiberCenterPow

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L599 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.fiberIdeal

Documentation

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L602 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.fiberIdeal_of_mem

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.fiberIdeal_of_notMem

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L608 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal_le_fiberIdeal

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L616 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.isCoprime_fiberIdeal

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L633 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.count_normalizedFactors_conductorIdeal

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L641 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal_eq_prod_fiber

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L685 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.prod_fiberIdeal_le_of_subset

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L691 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.conductorIdeal_le_prod_fiberIdeal

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L703 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.fiberIdealQuotientAlgebra

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L709 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.prodFiberIdealQuotientAlgebra

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L716 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.finite_quotient_of_conductorLE

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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'] [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

L726 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.trace_mk_prod_fiberIdeal

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L814 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.trace_mk_conductor_eq_sum_fiber

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L842 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceValueProof.Blocks.trace_mk_fiberIdeal_eq_trace_mk_fiberCenterPow

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
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

L878 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.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
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open 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)

L923 ↗

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open Blocks
variable {v : Place K F} [HasPrincipalDivisors K F']

Lean source · statement

instance : DecidableEq (Place K F')

theorem

residue_trace_eq_sum_evalAt

L925 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.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
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
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 le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff
open 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

mem_and_evalAt_trace_eq_sum_fiber

L966 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceLocEval.mem_and_evalAt_trace_eq_sum_fiber

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceLocEval
open _root_.AlgebraicCurve
open AlgebraicCurve.TraceValueProof AlgebraicCurve.TraceValueProof.Assembly
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place hiding le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff

Lean source · statement

theorem mem_and_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', 0 ≤ w.ord f) :
    Algebra.trace F F' f ∈ v.toValuationSubring ∧
      v.evalAt (Algebra.trace F F' f) = ∑ w ∈ v.fiber F', w.ramificationIndex F • w.evalAt f

theorem

evalAt_zero'

L985 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt.AlgebraicCurve.TraceLocEval.evalAt_zero'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TraceLocEval
open _root_.AlgebraicCurve
open AlgebraicCurve.TraceValueProof AlgebraicCurve.TraceValueProof.Assembly
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place hiding le_ord_iff_mem_pow_fiberCenter
  neg_log_valuation_fiberCenter_eq_ord eq_ord_of_addHom_of_nonneg_iff

Lean source · statement

theorem evalAt_zero' {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F) : v.evalAt (0
  : F) = 0

theorem

mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt

L994 ↗

AlgebraicCurve.Place.mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
open _root_.AlgebraicCurve AlgebraicCurve AlgebraicCurve.TraceLocEval in

Lean source · full declaration

theorem _root_.AlgebraicCurve.Place.mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
    {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [IsAlgClosed k]
    [IsCurveOver k F] [IsCurveOver k F']
    (φ : F →ₐ[k] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong k φ) (hsep : SeparableAlong
      k φ)
    (x : Place k F) (S : Finset (Place k F')) (hS : ∀ y : Place k F', y ∈ S ↔ y.restrictAlong φ hφ
      = x)
    (g : F') (hg : ∀ y ∈ S, g ∈ y.toValuationSubring) :
    letI := AlgebraicCurve.algebraAlong φ
    Algebra.trace F F' g ∈ x.toValuationSubring ∧
      x.evalAt (Algebra.trace F F' g) = ∑ y ∈ S, ((Place.ramificationIndexAlong φ y : ℕ) : k) •
        y.evalAt g := by
  classical
  let := AlgebraicCurve.algebraAlong φ
  have := AlgebraicCurve.isScalarTower_along φ
  have := AlgebraicCurve.isIntegral_along φ hφ
  have : FiniteDimensional F F' := hfin
  have : Algebra.IsSeparable F F' := hsep
  have : HasPrincipalDivisors k F' := IsCurveOver.hasPrincipalDivisors
  have hratF' : ∀ w : Place k F', w.IsRational := fun w =>
    (Place.isRational_iff_deg_eq_one w).mpr (IsCurveOver.deg_eq_one_of_isAlgClosed w)
  have hx : x.IsRational := (Place.isRational_iff_deg_eq_one x).mpr
    (IsCurveOver.deg_eq_one_of_isAlgClosed x)
  have hSfib : S = x.fiber F' := by
    ext y
    rw [hS y, Place.mem_fiber]
    rfl
  by_cases hg0 : g = 0
  · subst hg0
    refine ⟨by rw [map_zero]; exact zero_mem _, ?_⟩
    rw [map_zero, evalAt_zero']
    exact (Finset.sum_eq_zero fun y _ => by rw [evalAt_zero', smul_zero]).symm
  obtain ⟨hmem, hval⟩ := mem_and_evalAt_trace_eq_sum_fiber (K := k) x hx (fun w _ => hratF' w) g hg0
    (fun w hw => TraceValueProof.ord_nonneg_of_mem w (hg w (hSfib ▸ hw)))
  refine ⟨hmem, ?_⟩
  rw [hval, hSfib]
  refine Finset.sum_congr rfl fun y _ => ?_
  rw [Nat.cast_smul_eq_nsmul]
  rfl

Module documentation

Place mem and eval At trace eq sum ramification Index Along smul eval At

Declarations