Module

ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank

37 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring finsum ramification Idx mul inertia Deg eq finrank

Imports29

Mathlib.Algebra.BigOperators.Finprod
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Mathlib.Algebra.BigOperators.Group.Finset.Defs
Mathlib.Algebra.Module.Torsion.Free
Mathlib.LinearAlgebra.Dimension.Finrank
Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Mathlib.LinearAlgebra.Dimension.Localization
Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.RingTheory.Valuation.LocalSubring
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.Integral
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.DedekindDomain.Basic
Mathlib.RingTheory.DedekindDomain.AdicValuation
Mathlib.RingTheory.DedekindDomain.Dvr
Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.NumberTheory.RamificationInertia.Ramification
Mathlib.RingTheory.RamificationInertia.Ramification
Mathlib.RingTheory.RamificationInertia.Inertia
Mathlib.RingTheory.RamificationInertia.Basic
Mathlib.Tactic.Ext

Imported by2

theorem

isUnit_iff_inv_mem

L61 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.isUnit_iff_inv_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)

Lean source · statement

theorem isUnit_iff_inv_mem {L : Type*} [Field L] (C : ValuationSubring L) (x : C)
    (hx0 : (x : L) ≠ 0) : IsUnit x ↔ (x : L)⁻¹ ∈ C

theorem

mem_maximalIdeal_iff_inv_not_mem

L72 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.mem_maximalIdeal_iff_inv_not_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)

Lean source · statement

theorem mem_maximalIdeal_iff_inv_not_mem {L : Type*} [Field L] (C : ValuationSubring L) (x : C)
    (hx0 : (x : L) ≠ 0) : x ∈ maximalIdeal C ↔ (x : L)⁻¹ ∉ C

theorem

inertiaDeg_maximalIdeal_eq_one_of_isLocalization

L76 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.inertiaDeg_maximalIdeal_eq_one_of_isLocalization

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)

Lean source · statement

theorem inertiaDeg_maximalIdeal_eq_one_of_isLocalization {R : Type*} [CommRing R]
    (p : Ideal R) [p.IsMaximal] (Rₚ : Type*) [CommRing Rₚ] [Algebra R Rₚ]
    [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] :
    (maximalIdeal Rₚ).inertiaDeg R = 1

def

Over

L96 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.Over

Documentation

The condition that the valuation ring restricts to the given base valuation ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)

Lean source · statement

def Over (B : ValuationSubring F) : Prop

abbrev

overAlgebra

L101 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.overAlgebra

Documentation

The algebra structure on the valuation subring induced by the base-ring map landing in it.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}

Lean source · statement

abbrev overAlgebra (B : ValuationSubring F) (h : Over A B) : Algebra A B

theorem

coe_algebraMap_overAlgebra

L104 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.coe_algebraMap_overAlgebra

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}

Lean source · full declaration

theorem coe_algebraMap_overAlgebra (B : ValuationSubring F) (h : Over A B) (a : A) :
    letI := overAlgebra B h
    ((algebraMap A B a : B) : F) = algebraMap K F a := rfl

theorem

isScalarTower_overAlgebra

L108 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.isScalarTower_overAlgebra

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}

Lean source · full declaration

theorem isScalarTower_overAlgebra (B : ValuationSubring F) (h : Over A B) :
    letI := overAlgebra B h
    IsScalarTower A B F := by
  let := overAlgebra B h
  refine IsScalarTower.of_algebraMap_eq fun a => ?_
  change algebraMap K F a = ((algebraMap A B a : B) : F)
  rfl

theorem

algebraMap_overAlgebra_injective

L116 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.algebraMap_overAlgebra_injective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}

Lean source · full declaration

theorem algebraMap_overAlgebra_injective (B : ValuationSubring F) (h : Over A B) :
    letI := overAlgebra B h
    Function.Injective (algebraMap A B) := by
  let := overAlgebra B h
  intro a b hab
  have := congrArg (fun z : B => (z : F)) hab
  simp only [coe_algebraMap_overAlgebra] at this
  exact Subtype.ext ((algebraMap K F).injective this)

theorem

comap_maximalIdeal_overAlgebra

L125 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.comap_maximalIdeal_overAlgebra

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}

Lean source · full declaration

theorem comap_maximalIdeal_overAlgebra (B : ValuationSubring F) (h : Over A B) :
    letI := overAlgebra B h
    (maximalIdeal B).comap (algebraMap A B) = maximalIdeal A := by
  let := overAlgebra B h
  ext a
  rw [Ideal.mem_comap]
  by_cases ha0 : (a : K) = 0
  · have : a = 0 := Subtype.ext ha0
    subst this
    simp
  have hb0 : ((algebraMap A B a : B) : F) ≠ 0 := by
    rw [coe_algebraMap_overAlgebra]
    exact (map_ne_zero _).mpr ha0
  rw [mem_maximalIdeal_iff_inv_not_mem B _ hb0, mem_maximalIdeal_iff_inv_not_mem A _ ha0,
    coe_algebraMap_overAlgebra, ← map_inv₀, h]

theorem

mem_of_mem_integralClosure

L141 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.mem_of_mem_integralClosure

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}

Lean source · statement

theorem mem_of_mem_integralClosure (B : ValuationSubring F) (h : Over A B)
    {y : F} (hy : y ∈ integralClosure A F) : y ∈ B

theorem

ne_top_of_over

L150 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.ne_top_of_over

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}

Lean source · statement

theorem ne_top_of_over [IsDiscreteValuationRing A] (B : ValuationSubring F) (h : Over A B) :
    B ≠ ⊤

theorem

maximalIdeal_ne_bot

L164 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.maximalIdeal_ne_bot

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)

Lean source · statement

theorem maximalIdeal_ne_bot [IsDiscreteValuationRing A] : maximalIdeal A ≠ ⊥

theorem

coe_algebraMap_integralClosure

L167 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.coe_algebraMap_integralClosure

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)

Lean source · statement

theorem coe_algebraMap_integralClosure (a : A) :
    ((algebraMap A (integralClosure A F) a : integralClosure A F) : F) = algebraMap K F a

theorem

algebraMap_integralClosure_injective

L170 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.algebraMap_integralClosure_injective

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)

Lean source · statement

theorem algebraMap_integralClosure_injective :
    Function.Injective (algebraMap A (integralClosure A F))

theorem

isTorsionFree_integralClosure

L177 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.isTorsionFree_integralClosure

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)

Lean source · statement

theorem isTorsionFree_integralClosure : Module.IsTorsionFree A (integralClosure A F)

theorem

liesOver_maximalIdeal

L187 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.liesOver_maximalIdeal

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure

Lean source · statement

theorem liesOver_maximalIdeal [IsDiscreteValuationRing A]
    (v : HeightOneSpectrum (integralClosure A F)) :
    v.asIdeal.LiesOver (maximalIdeal A)

def

toOver

L200 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.toOver

Documentation

The inclusion of the integral closure into a valuation ring lying over the base ring.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}

Lean source · statement

def toOver (B : ValuationSubring F) (h : Over A B) : integralClosure A F →+* B

theorem

coe_toOver

L203 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.coe_toOver

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}

Lean source · statement

theorem coe_toOver (B : ValuationSubring F) (h : Over A B) (s : integralClosure A F)
  :
    ((toOver B h s : B) : F) = (s : F)

def

center

L208 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.center

Documentation

The center of an extending valuation on the integral closure.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}

Lean source · statement

def center (B : ValuationSubring F) (h : Over A B) : Ideal (integralClosure A F)

theorem

mem_center_iff

L211 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.mem_center_iff

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}

Lean source · statement

theorem mem_center_iff (B : ValuationSubring F) (h : Over A B) (s : integralClosure A F) :
    s ∈ center B h ↔ (s : F) ∈ B.nonunits

instance

center_isPrime

L216 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.center_isPrime

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}

Lean source · statement

instance center_isPrime (B : ValuationSubring F) (h : Over A B) : (center B h).IsPrime

theorem

center_ne_bot

L219 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.center_ne_bot

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}

Lean source · statement

theorem center_ne_bot [IsDiscreteValuationRing A] (B : ValuationSubring F) (h : Over A B) :
    center B h ≠ ⊥

def

vOf

L231 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.vOf

Documentation

The height-one prime corresponding to the center of the extending valuation.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}

Lean source · statement

def vOf [IsDiscreteValuationRing A] (B : ValuationSubring F) (h : Over A B) :
    HeightOneSpectrum (integralClosure A F)

theorem

isFractionRing_integralClosure

L240 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.isFractionRing_integralClosure

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]

Lean source · statement

theorem isFractionRing_integralClosure : IsFractionRing (integralClosure A F) F

theorem

isDedekindDomain_integralClosure

L247 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.isDedekindDomain_integralClosure

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]

Lean source · statement

theorem isDedekindDomain_integralClosure : IsDedekindDomain (integralClosure A F)

abbrev

W

L259 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.W

Documentation

The valuation ring attached to a height-one prime of the integral closure.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]
attribute [local instance] isDedekindDomain_integralClosure

Lean source · statement

abbrev W (v : HeightOneSpectrum (integralClosure A F)) : ValuationSubring F

theorem

isDiscreteValuationRing_W

L262 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.isDiscreteValuationRing_W

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]
attribute [local instance] isDedekindDomain_integralClosure

Lean source · statement

theorem isDiscreteValuationRing_W (v : HeightOneSpectrum (integralClosure A F)) :
    IsDiscreteValuationRing (W A v)

theorem

coe_algebraMap_W

L267 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.coe_algebraMap_W

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]
attribute [local instance] isDedekindDomain_integralClosure

Lean source · statement

theorem coe_algebraMap_W (v : HeightOneSpectrum (integralClosure A F)) (s : integralClosure A F) :
    ((algebraMap (integralClosure A F) (W A v) s : W A v) : F) = (s : F)

theorem

over_W

L270 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.over_W

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]
attribute [local instance] isDedekindDomain_integralClosure

Lean source · statement

theorem over_W (v : HeightOneSpectrum (integralClosure A F)) : Over A (W A v)

theorem

W_vOf_le

L303 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.W_vOf_le

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]
attribute [local instance] isDedekindDomain_integralClosure
variable {A}

Lean source · statement

theorem W_vOf_le (B : ValuationSubring F) (h : Over A B) : W A (vOf B h) ≤ B

theorem

W_vOf_eq

L316 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.W_vOf_eq

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]
attribute [local instance] isDedekindDomain_integralClosure
variable {A}

Lean source · statement

theorem W_vOf_eq (B : ValuationSubring F) (h : Over A B) : W A (vOf B h) = B

theorem

vOf_W

L319 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.vOf_W

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]
attribute [local instance] isDedekindDomain_integralClosure
variable {A}

Lean source · statement

theorem vOf_W (v : HeightOneSpectrum (integralClosure A F)) : vOf (W A v) (over_W A v) = v

def

overEquiv

L330 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.overEquiv

Documentation

The equivalence between extending valuation rings and height-one primes of the integral closure.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]
attribute [local instance] isDedekindDomain_integralClosure
variable {A}
variable (A)

Lean source · full declaration

def overEquiv :
    {B : ValuationSubring F // Over A B} ≃ HeightOneSpectrum (integralClosure A F) where
  toFun B := vOf B.1 B.2
  invFun v := ⟨W A v, over_W A v⟩
  left_inv B := Subtype.ext (W_vOf_eq B.1 B.2)
  right_inv v := vOf_W v

def

hosEquiv

L339 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.hosEquiv

Documentation

The equivalence between height-one primes and the finite set of primes over the maximal ideal.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]
attribute [local instance] isDedekindDomain_integralClosure
variable {A}
variable (A)

Lean source · full declaration

def hosEquiv : HeightOneSpectrum (integralClosure A F) ≃
    ↥(IsDedekindDomain.primesOverFinset (maximalIdeal A) (integralClosure A F)) where
  toFun v := ⟨v.asIdeal, (IsDedekindDomain.mem_primesOverFinset_iff (maximalIdeal_ne_bot A)
    (integralClosure A F)).mpr ⟨v.isPrime, liesOver_maximalIdeal A v⟩⟩
  invFun P :=
    haveI := ((IsDedekindDomain.mem_primesOverFinset_iff (maximalIdeal_ne_bot A)
      (integralClosure A F)).mp P.2).1
    haveI := ((IsDedekindDomain.mem_primesOverFinset_iff (maximalIdeal_ne_bot A)
      (integralClosure A F)).mp P.2).2
    ⟨P.1, inferInstance, Ideal.ne_bot_of_liesOver_of_ne_bot (maximalIdeal_ne_bot A) P.1⟩
  left_inv _ := rfl
  right_inv _ := rfl

theorem

ramificationIdx_mul_inertiaDeg_W

L352 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.ramificationIdx_mul_inertiaDeg_W

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]
attribute [local instance] isDedekindDomain_integralClosure
variable {A}
variable (A)

Lean source · full declaration

theorem ramificationIdx_mul_inertiaDeg_W (v : HeightOneSpectrum (integralClosure A F)) :
    letI := overAlgebra (W A v) (over_W A v)
    (maximalIdeal A).ramificationIdx' (maximalIdeal (W A v)) *
      (maximalIdeal (W A v)).inertiaDeg A =
    (maximalIdeal A).ramificationIdx' v.asIdeal * v.asIdeal.inertiaDeg A := by
  let : Algebra A (W A v) := overAlgebra (W A v) (over_W A v)
  have : IsScalarTower A (integralClosure A F) (W A v) :=
    IsScalarTower.of_algebraMap_eq fun a => Subtype.ext rfl
  have : IsDiscreteValuationRing (W A v) := isDiscreteValuationRing_W A v
  have hmapS : Ideal.map (algebraMap (integralClosure A F) (W A v)) v.asIdeal =
      maximalIdeal (W A v) :=
    IsLocalization.AtPrime.map_eq_maximalIdeal v.asIdeal (W A v)
  have hmW0 : maximalIdeal (W A v) ≠ ⊥ := IsDiscreteValuationRing.not_a_field _
  have : (maximalIdeal (W A v)).LiesOver v.asIdeal :=
    ⟨(IsLocalization.AtPrime.under_maximalIdeal (W A v) v.asIdeal).symm⟩
  have he : (maximalIdeal A).ramificationIdx' (maximalIdeal (W A v)) =
      (maximalIdeal A).ramificationIdx' v.asIdeal *
        v.asIdeal.ramificationIdx' (maximalIdeal (W A v)) :=
    Ideal.ramificationIdx'_algebra_tower (by rw [hmapS]; exact hmW0)
      (by
        rw [Ne, Ideal.map_eq_bot_iff_of_injective (algebraMap_overAlgebra_injective _ _)]
        exact maximalIdeal_ne_bot A)
      hmapS.le
  have he1 : v.asIdeal.ramificationIdx' (maximalIdeal (W A v)) = 1 := by
    rw [← hmapS]
    exact Ideal.ramificationIdx'_map_self_eq_one
      (by rw [hmapS]; exact (maximalIdeal.isMaximal _).ne_top) (by rw [hmapS]; exact hmW0)
  have hf : (maximalIdeal (W A v)).inertiaDeg A =
      v.asIdeal.inertiaDeg A * (maximalIdeal (W A v)).inertiaDeg (integralClosure A F) :=
    Ideal.inertiaDeg_tower (R := A) v.asIdeal (maximalIdeal (W A v))
  have hf1 : (maximalIdeal (W A v)).inertiaDeg (integralClosure A F) = 1 :=
    inertiaDeg_maximalIdeal_eq_one_of_isLocalization v.asIdeal (W A v)
  rw [he, he1, hf, hf1, mul_one, mul_one]

theorem

main

L386 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank.ValuationSubring.FundamentalEquality.main

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
namespace FundamentalEquality
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
variable {A}
variable (A)
attribute [local instance] isTorsionFree_integralClosure
attribute [local instance] liesOver_maximalIdeal
variable {A}
section finite
variable (A)
variable [FiniteDimensional K F]
attribute [local instance] isFractionRing_integralClosure
variable [IsDiscreteValuationRing A] [Module.Finite A (integralClosure A F)]
attribute [local instance] isDedekindDomain_integralClosure
variable {A}
variable (A)

Lean source · full declaration

theorem main :
    {B : ValuationSubring F | ∀ x : K, algebraMap K F x ∈ B ↔ x ∈ A}.Finite ∧
    (∀ B : ValuationSubring F, (∀ x : K, algebraMap K F x ∈ B ↔ x ∈ A) →
      IsDiscreteValuationRing B) ∧
    ∑ᶠ B : {B : ValuationSubring F // ∀ x : K, algebraMap K F x ∈ B ↔ x ∈ A},
      (letI : Algebra A B.1 := (((algebraMap K F).comp A.subtype).codRestrict B.1
          fun a => (B.2 a).mpr a.2).toAlgebra
       (maximalIdeal A).ramificationIdx' (maximalIdeal B.1) *
         (maximalIdeal B.1).inertiaDeg A) =
      Module.finrank K F := by
  let ε := (overEquiv A (F := F)).trans (hosEquiv A)
  have : Fintype {B : ValuationSubring F // Over A B} := Fintype.ofEquiv _ ε.symm
  refine ⟨?_, ?_, ?_⟩
  · exact Set.finite_coe_iff.mp (Finite.of_fintype {B : ValuationSubring F // Over A B})
  · intro B h
    rw [← W_vOf_eq B h]
    exact isDiscreteValuationRing_W A _
  · change ∑ᶠ B : {B : ValuationSubring F // Over A B},
      (letI := overAlgebra B.1 B.2
       (maximalIdeal A).ramificationIdx' (maximalIdeal B.1) *
         (maximalIdeal B.1).inertiaDeg A) = Module.finrank K F
    rw [finsum_eq_sum_of_fintype]
    have hsum :
        ∑ P ∈ IsDedekindDomain.primesOverFinset (maximalIdeal A) (integralClosure A F),
          (maximalIdeal A).ramificationIdx' P * P.inertiaDeg A =
            Module.finrank K F := by
      calc
        _ = ∑ P ∈ IsDedekindDomain.primesOverFinset (maximalIdeal A) (integralClosure A F),
              P.ramificationIdx A * P.inertiaDeg A := by
            refine Finset.sum_congr rfl ?_
            intro P hP
            obtain ⟨hPprime, hPover⟩ :=
              (IsDedekindDomain.mem_primesOverFinset_iff (maximalIdeal_ne_bot A)
                (integralClosure A F)).mp hP
            let : P.IsPrime := hPprime
            let : P.LiesOver (maximalIdeal A) := hPover
            rw [Ideal.ramificationIdx'_eq_ramificationIdx _ _ (maximalIdeal_ne_bot A)]
        _ = ∑ P : (IsDedekindDomain.primesOverFinset (maximalIdeal A) (integralClosure A F)),
              P.1.ramificationIdx A * P.1.inertiaDeg A := by
            exact (Finset.sum_coe_sort
              (IsDedekindDomain.primesOverFinset (maximalIdeal A) (integralClosure A F))
              (fun P : Ideal (integralClosure A F) => P.ramificationIdx A * P.inertiaDeg A)).symm
        _ = ∑ P : (maximalIdeal A).primesOver (integralClosure A F),
              P.1.ramificationIdx A * P.1.inertiaDeg A := by
            exact Fintype.sum_equiv
              (Set.equivOfEq (IsDedekindDomain.coe_primesOverFinset
                (maximalIdeal_ne_bot A) (integralClosure A F))) _ _ (by intro P; rfl)
        _ = Module.finrank A (integralClosure A F) :=
          Ideal.sum_ramification_inertia_eq_finrank (maximalIdeal A) (integralClosure A F)
        _ = Module.finrank K F :=
          (IsFractionRing.finrank_eq A K (integralClosure A F) F).symm
    rw [← hsum, ← Finset.sum_coe_sort
      (IsDedekindDomain.primesOverFinset (maximalIdeal A) (integralClosure A F))]
    symm
    refine Fintype.sum_equiv ε.symm _ _ ?_
    intro P
    exact (ramificationIdx_mul_inertiaDeg_W A ((hosEquiv (F := F) A).symm P)).symm

theorem

finsum_ramificationIdx_mul_inertiaDeg_eq_finrank

L449 ↗

ValuationSubring.finsum_ramificationIdx_mul_inertiaDeg_eq_finrank

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
open IsLocalRing IsDedekindDomain

Lean source · full declaration

theorem _root_.ValuationSubring.finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
    {K F : Type*} [Field K] [Field F] [Algebra K F] [FiniteDimensional K F]
    (A : ValuationSubring K) [IsDiscreteValuationRing A]
    [Module.Finite A (integralClosure A F)] :
    {B : ValuationSubring F | ∀ x : K, algebraMap K F x ∈ B ↔ x ∈ A}.Finite ∧
    (∀ B : ValuationSubring F, (∀ x : K, algebraMap K F x ∈ B ↔ x ∈ A) →
      IsDiscreteValuationRing B) ∧
    ∑ᶠ B : {B : ValuationSubring F // ∀ x : K, algebraMap K F x ∈ B ↔ x ∈ A},
      (letI : Algebra A B.1 := (((algebraMap K F).comp A.subtype).codRestrict B.1
          fun a => (B.2 a).mpr a.2).toAlgebra
       (IsLocalRing.maximalIdeal A).ramificationIdx' (IsLocalRing.maximalIdeal B.1) *
         (IsLocalRing.maximalIdeal B.1).inertiaDeg A) =
      Module.finrank K F :=
  ValuationSubring.FundamentalEquality.main A

Module documentation

Valuation Subring finsum ramification Idx mul inertia Deg eq finrank

Declarations