Nyll.ClassFieldTheory.AlgebraicNumberTheory.Completion.UnramifiedComparison.RamificationIndex

theorem

chosenFinitePlace_completed_ramificationIdx'_eq_centre

Documentation

The ramification index of the maximal ideals in the explicit localized completions is the ramification index of the corresponding global ideals.

Source context 8 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem chosenFinitePlace_completed_ramificationIdx'_eq_centre
    (v : HeightOneSpectrum (𝓞 K)) :
    (𝓂[ChosenFinitePlaceBaseCompletion (K := K) v] :
        Ideal 𝒪[ChosenFinitePlaceBaseCompletion (K := K) v]).ramificationIdx'
      (𝓂[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v] :
        Ideal 𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v]) =
      v.asIdeal.ramificationIdx'
        (finitePlaceExtensionCentre
          (K := K) (L := L) v
          (chosenFinitePlaceExtension (L := L) v)).asIdeal

theorem

chosenFinitePlace_chosenLocal_ramificationIndex_eq_centre

L201 ↗

Documentation

The ramification index computed using the integral-closure valuation chosen for the finite local extension equals the ideal-theoretic index at the corresponding global centre.

Source context 8 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · full declaration

theorem chosenFinitePlace_chosenLocal_ramificationIndex_eq_centre
    (v : HeightOneSpectrum (𝓞 K)) :
    let C := ChosenFinitePlaceBaseCompletion (K := K) v;
    let E := ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v;
    letI : FiniteDimensional C E :=
      chosenFinitePlaceLocalizedFiniteDimensional (K := K) (L := L) v;
    letI : Algebra.IsSeparable C E :=
      (chosenFinitePlaceLocalizedIsGalois
        (K := K) (L := L) v).to_isSeparable;
    ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
      (localCompleteDVF C).toDVF
      (chosenLocalExtensionCompleteDVF C E).toDVF =
      v.asIdeal.ramificationIdx'
        (finitePlaceExtensionCentre
          (K := K) (L := L) v
          (chosenFinitePlaceExtension (L := L) v)).asIdeal := by
  dsimp only
  let C := ChosenFinitePlaceBaseCompletion (K := K) v
  let E := ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v
  let : FiniteDimensional C E :=
    chosenFinitePlaceLocalizedFiniteDimensional (K := K) (L := L) v
  let : Algebra.IsSeparable C E :=
    (chosenFinitePlaceLocalizedIsGalois
      (K := K) (L := L) v).to_isSeparable
  let base := localCompleteDVF C
  let target := chosenLocalExtensionCompleteDVF C E
  let V := base.valuation.valuationSubring
  let : HenselianRing V (IsLocalRing.maximalIdeal V) :=
    ValuationTheory.DiscreteValuationField.Valuation.henselianRing
      base.valuation
  let : base.valuation.HasExtension target.valuation :=
    chosenLocalExtensionCompleteDVF_hasExtension C E
  let : base.valuation.HasExtension (ValuativeRel.valuation E) :=
    chosenFinitePlaceLocalizedValuationHasExtension
      (K := K) (L := L) v
  let : V.valuation.HasExtension target.valuation :=
    ⟨(Valuation.isEquiv_valuation_valuationSubring
      base.valuation).symm.trans
        (Valuation.HasExtension.val_isEquiv_comap
          (vR := base.valuation) (vA := target.valuation))⟩
  let : V.valuation.HasExtension (ValuativeRel.valuation E) :=
    ⟨(Valuation.isEquiv_valuation_valuationSubring
      base.valuation).symm.trans
        (Valuation.HasExtension.val_isEquiv_comap
          (vR := base.valuation) (vA := ValuativeRel.valuation E))⟩
  have hRing :
      target.valuation.valuationSubring =
        (ValuativeRel.valuation E).valuationSubring :=
    ValuationTheory.Henselian.valuationSubring_eq_of_henselianRing
      V target.valuation (ValuativeRel.valuation E)
  let intrinsic := (ValuativeRel.valuation E).valuationSubring
  let : Algebra base.valuationSubring intrinsic :=
    Valuation.HasExtension.instAlgebra_valuationSubring
      base.valuation (ValuativeRel.valuation E)
  let eTarget : target.valuationSubring ≃+* intrinsic :=
    RingEquiv.subringCongr
      (congrArg ValuationSubring.toSubring hRing)
  let eAlg : target.valuationSubring ≃ₐ[base.valuationSubring] intrinsic :=
    AlgEquiv.ofRingEquiv (f := eTarget) (by
      intro a
      apply Subtype.ext
      rfl)
  have htransport :=
    Ideal.ramificationIdx'_map_eq
      (base.maximalIdeal) (target.maximalIdeal) eAlg
  have hMax :
      Ideal.map eTarget target.maximalIdeal =
        IsLocalRing.maximalIdeal intrinsic :=
    ValuationTheory.ringEquiv_map_maximalIdeal eTarget
  change
    ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
      base.toDVF target.toDVF = _
  calc
    ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
        base.toDVF target.toDVF =
        Ideal.ramificationIdx' base.maximalIdeal target.maximalIdeal := rfl
    _ = Ideal.ramificationIdx' base.maximalIdeal
          (Ideal.map eTarget target.maximalIdeal) := htransport.symm
    _ = Ideal.ramificationIdx' base.maximalIdeal
          (IsLocalRing.maximalIdeal intrinsic) := by rw [hMax]
    _ = v.asIdeal.ramificationIdx'
          (finitePlaceExtensionCentre
            (K := K) (L := L) v
            (chosenFinitePlaceExtension (L := L) v)).asIdeal := by
      change
        (𝓂[C] : Ideal 𝒪[C]).ramificationIdx'
          (𝓂[E] : Ideal 𝒪[E]) = _
      exact chosenFinitePlace_completed_ramificationIdx'_eq_centre
        (K := K) (L := L) v

RamificationIndex.lean

Module documentation

Ramification index and finite-place completion

chosenFinitePlace_completed_ramificationIdx'_eq_centre

chosenFinitePlace_chosenLocal_ramificationIndex_eq_centre

Module documentation

Ramification index and finite-place completion

Declarations

chosenFinitePlace_completed_ramificationIdx'_eq_centre

chosenFinitePlace_chosenLocal_ramificationIndex_eq_centre