FinitePlaceInertiaTransport.lean

theorem fieldAlgebra_isTorsionFree_forInertiaTransport
    {K L : Type*} [Field K] [Field L] [Algebra K L] :
    Module.IsTorsionFree K L

def algebraicClosureAlgEquivSeparableClosure
    (K : Type) [Field K] [CharZero K] :
    AlgebraicClosure K ≃ₐ[K] SeparableClosure K

theorem autCongr_algebraicClosureAlgEquivSeparableClosure
    (K : Type) [Field K] [CharZero K] :
    AlgEquiv.autCongr (algebraicClosureAlgEquivSeparableClosure K) =
      RamificationTheory.Field.absoluteGaloisGroup.separableClosureMulEquiv K

theorem decompositionGroupEquivAlgebraicLocalizationAut_mem_inertia_iff
    {K L : Type*} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
    (sigma : HilbertRamification.absoluteValueDecompositionGroup K w.1) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    decompositionGroupEquivAlgebraicLocalizationAut vK hvK w sigma ∈
        RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut
          vK.Completion
          (HilbertRamification.algebraicLocalizationValuationSubring vK w hw) ↔
      HilbertRamification.localizationRamificationGroups_absoluteValueDecompositionGroupEquiv
          vK hvK w hw sigma ∈
        RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K
          (HilbertRamification.absoluteValueExtensionValuationSubring vK w hw) := by
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let _ : SMul K w.1.Completion := hK.toSMul
  let _ := AbsoluteValue.completionAlgebra vK w.1 w.2
  let sigmaGlobal :=
    HilbertRamification.localizationRamificationGroups_absoluteValueDecompositionGroupEquiv
      vK hvK w hw sigma
  let sigmaLocal :=
    HilbertRamification.localizationRamificationGroups_valuationDecompositionGroupEquiv
      vK hvK w hw sigmaGlobal
  have hsigmaLocal :
      ((sigmaLocal :
          RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup
            vK.Completion
            (HilbertRamification.algebraicLocalizationValuationSubring vK w hw)) :
          AbsoluteValue.algebraicLocalization vK w.1 w.2 ≃ₐ[vK.Completion]
            AbsoluteValue.algebraicLocalization vK w.1 w.2) =
        decompositionGroupEquivAlgebraicLocalizationAut vK hvK w sigma := by
    rfl
  rw [← (open _root_.RamificationTheory.HilbertRamification in
    localizationRamificationGroups_valuationDecompositionGroupEquiv_mem_inertia_iff
      vK hvK w hw sigmaGlobal)]
  constructor
  · rintro ⟨tau, htau, htau_eq⟩
    have hlocal : sigmaLocal ∈
        RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup
          vK.Completion
          (HilbertRamification.algebraicLocalizationValuationSubring vK w hw) := by
      have htau_eq' : tau = sigmaLocal := by
        apply Subtype.ext
        rw [hsigmaLocal]
        exact htau_eq
      rw [← htau_eq']
      exact htau
    exact hlocal
  · intro hlocal
    refine ⟨sigmaLocal, hlocal, ?_⟩
    exact hsigmaLocal

theorem localSeparableValuationSubring_eq_comap_algEquiv
    (K : Type) (L : Type*) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [ValuativeRel L] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [(ValuativeRel.valuation K).HasExtension (ValuativeRel.valuation L)]
    (e : L ≃ₐ[K] SeparableClosure K) :
    localSeparableValuationSubring K =
      (ValuativeRel.valuation L).valuationSubring.comap e.symm.toRingHom

theorem algebraicLocalizationValuationSubring_eq_normValuationSubring
    {K L : Type} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (w : AbsoluteValueExtension vK L)
    (hvKna : IsNonarchimedean (vK : K → ℝ))
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : Valued (AbsoluteValue.algebraicLocalization vK w.1 w.2) NNReal :=
      localizedCompletionFinitePlaceValued vK w hvKna
    letI : ValuativeRel (AbsoluteValue.algebraicLocalization vK w.1 w.2) :=
      localizedCompletionFinitePlaceValuativeRel vK w hvKna
    HilbertRamification.algebraicLocalizationValuationSubring vK w hw =
      (ValuativeRel.valuation
        (AbsoluteValue.algebraicLocalization vK w.1 w.2)).valuationSubring := by
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let _ : SMul K w.1.Completion := hK.toSMul
  let _ := AbsoluteValue.completionAlgebra vK w.1 w.2
  let E := AbsoluteValue.algebraicLocalization vK w.1 w.2
  let _ : Valued E NNReal :=
    localizedCompletionFinitePlaceValued vK w hvKna
  let _ : ValuativeRel E :=
    localizedCompletionFinitePlaceValuativeRel vK w hvKna
  ext x
  rw [mem_absoluteValueValuationSubring_iff]
  change ‖x‖ ≤ 1 ↔
    x ∈ (ValuativeRel.valuation E).valuationSubring
  rw [← localizedCompletion_mem_integers_iff_norm_le_one vK w hvKna]
  rw [Valuation.mem_integer_iff, Valuation.mem_valuationSubring_iff]

theorem finitePlaceNormCompletionIsNonarchimedeanLocalField
    (F : Type) [Field F] [NumberField F]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    let vF := NumberField.HeightOneSpectrum.adicAbv F v
    @IsNonarchimedeanLocalField vF.Completion inferInstance
      (finitePlaceCompletionValuativeRel vF
        (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v))
      inferInstance := by
  let vF := NumberField.HeightOneSpectrum.adicAbv F v
  let hvFna :=
    NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
  let _ : IsUltrametricDist vF.Completion :=
    completionIsUltrametricDist vF hvFna
  let _ : NontriviallyNormedField vF.Completion :=
    absoluteValueExtension_completionNontriviallyNormedField vF
      (RayClass.adicAbv_isNontrivial v)
  let _ : LocallyCompactSpace vF.Completion :=
    AbsoluteValue.Completion.locallyCompactSpace
      (finitePlaceCompletionBaseMap_isometry v)
  let _ : Valued vF.Completion NNReal :=
    finitePlaceCompletionValued vF hvFna
  let nu : Valuation vF.Completion NNReal := Valued.v
  let _ : nu.IsNontrivial :=
    (inferInstance :
      (NormedField.valuation (K := vF.Completion)).IsNontrivial)
  let _ : ValuativeRel vF.Completion :=
    finitePlaceCompletionValuativeRel vF hvFna
  let _ : nu.Compatible := Valuation.Compatible.ofValuation nu
  let _ : ValuativeRel.IsNontrivial vF.Completion :=
    (ValuativeRel.isNontrivial_iff_isNontrivial nu).2 inferInstance
  let _ : IsValuativeTopology vF.Completion :=
    isValuativeTopology_of_valued_ofValuation vF.Completion NNReal
  exact
    { toIsValuativeTopology := inferInstance
      toLocallyCompactSpace := inferInstance
      toIsNontrivial := inferInstance }

def finitePlaceAlgebraicLocalizationAlgEquivSeparableClosure
    (F : Type) [Field F] [NumberField F]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    let vF := NumberField.HeightOneSpectrum.adicAbv F v
    let w := finitePlaceAbsoluteValueExtension F v
    letI hF := AbsoluteValue.extensionCompletionAlgebra (K := F) w.1
    letI : SMul F w.1.Completion := hF.toSMul
    letI := AbsoluteValue.completionAlgebra vF w.1 w.2
    AbsoluteValue.algebraicLocalization vF w.1 w.2 ≃ₐ[vF.Completion]
      SeparableClosure vF.Completion := by
  let vF := NumberField.HeightOneSpectrum.adicAbv F v
  let w := finitePlaceAbsoluteValueExtension F v
  letI hF := AbsoluteValue.extensionCompletionAlgebra (K := F) w.1
  letI : SMul F w.1.Completion := hF.toSMul
  letI := AbsoluteValue.completionAlgebra vF w.1 w.2
  let E := AbsoluteValue.algebraicLocalization vF w.1 w.2
  letI : CharZero vF.Completion :=
    charZero_of_injective_algebraMap
      (algebraMap F vF.Completion).injective
  exact
    (absoluteValueAlgebraicLocalizationAlgEquivAlgebraicClosure
      vF (RayClass.adicAbv_isNontrivial v)
        (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v) w).trans
      (algebraicClosureAlgEquivSeparableClosure vF.Completion)

def
    finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup
    (F : Type) [Field F] [NumberField F]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteDecompositionGroup F v ≃ₜ*
      Gal(SeparableClosure
        (NumberField.HeightOneSpectrum.adicAbv F v).Completion /
        (NumberField.HeightOneSpectrum.adicAbv F v).Completion)

theorem localResidueDegree_ker_eq_valuationInertiaGroupInAut
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    MonoidHom.ker (localResidueDegree K).toMonoidHom =
      RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut K
        (localSeparableValuationSubring K)

theorem finitePlaceDecompositionTransport_apply
    (F : Type) [Field F] [NumberField F]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    let vF := NumberField.HeightOneSpectrum.adicAbv F v
    let w := finitePlaceAbsoluteValueExtension F v
    letI hF := AbsoluteValue.extensionCompletionAlgebra (K := F) w.1
    letI : SMul F w.1.Completion := hF.toSMul
    letI := AbsoluteValue.completionAlgebra vF w.1 w.2
    finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup
        F v sigma =
      AlgEquiv.autCongr
        (finitePlaceAlgebraicLocalizationAlgEquivSeparableClosure F v)
        (decompositionGroupEquivAlgebraicLocalizationAut
          vF (RayClass.adicAbv_isNontrivial v) w sigma) := by
  let vF := NumberField.HeightOneSpectrum.adicAbv F v
  let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
  let w := finitePlaceAbsoluteValueExtension F v
  let hF := AbsoluteValue.extensionCompletionAlgebra (K := F) w.1
  let _ : SMul F w.1.Completion := hF.toSMul
  let _ := AbsoluteValue.completionAlgebra vF w.1 w.2
  let E := AbsoluteValue.algebraicLocalization vF w.1 w.2
  let _ : Module.IsTorsionFree vF.Completion E :=
    fieldAlgebra_isTorsionFree_forInertiaTransport
  let _ : IsAlgClosure vF.Completion E :=
    finitePlaceAlgebraicLocalization_isAlgClosure F v
  let _ : CharZero vF.Completion :=
    charZero_of_injective_algebraMap
      (algebraMap F vF.Completion).injective
  let eEA : E ≃ₐ[vF.Completion] AlgebraicClosure vF.Completion :=
    absoluteValueAlgebraicLocalizationAlgEquivAlgebraicClosure
      vF (RayClass.adicAbv_isNontrivial v) hvFna w
  let eAS : AlgebraicClosure vF.Completion ≃ₐ[vF.Completion]
      SeparableClosure vF.Completion :=
    algebraicClosureAlgEquivSeparableClosure vF.Completion
  change
    RamificationTheory.Field.absoluteGaloisGroup.separableClosureMulEquiv
        vF.Completion
        (AlgEquiv.autCongr eEA
          (decompositionGroupEquivAlgebraicLocalizationAut
            vF (RayClass.adicAbv_isNontrivial v) w sigma)) =
      AlgEquiv.autCongr (eEA.trans eAS)
        (decompositionGroupEquivAlgebraicLocalizationAut
          vF (RayClass.adicAbv_isNontrivial v) w sigma)
  rw [← autCongr_algebraicClosureAlgEquivSeparableClosure]
  exact DFunLike.congr_fun (AlgEquiv.autCongr_trans eEA eAS)
    (decompositionGroupEquivAlgebraicLocalizationAut
      vF (RayClass.adicAbv_isNontrivial v) w sigma)

theorem finitePlaceDecompositionTransport_mem_inertia_iff
    (F : Type) [Field F] [NumberField F]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    let vF := NumberField.HeightOneSpectrum.adicAbv F v
    let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
    letI : Valued vF.Completion NNReal :=
      finitePlaceCompletionValued vF hvFna
    letI : ValuativeRel vF.Completion :=
      finitePlaceCompletionValuativeRel vF hvFna
    letI : IsNonarchimedeanLocalField vF.Completion :=
      finitePlaceNormCompletionIsNonarchimedeanLocalField F v
    finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup
          F v sigma ∈
        RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut
          vF.Completion (localSeparableValuationSubring vF.Completion) ↔
      finitePlaceAbsoluteDecompositionValuationEquiv F v sigma ∈
        RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup F
          (finitePlaceAbsoluteValuationSubring F v) := by
  let vF := NumberField.HeightOneSpectrum.adicAbv F v
  let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
  let w := finitePlaceAbsoluteValueExtension F v
  let hw := finitePlaceAbsoluteValueExtension_nonarchimedean F v
  let _ : Valued vF.Completion NNReal :=
    finitePlaceCompletionValued vF hvFna
  let _ : ValuativeRel vF.Completion :=
    finitePlaceCompletionValuativeRel vF hvFna
  let _ : IsNonarchimedeanLocalField vF.Completion :=
    finitePlaceNormCompletionIsNonarchimedeanLocalField F v
  let hF := AbsoluteValue.extensionCompletionAlgebra (K := F) w.1
  let _ : SMul F w.1.Completion := hF.toSMul
  let _ := AbsoluteValue.completionAlgebra vF w.1 w.2
  let E := AbsoluteValue.algebraicLocalization vF w.1 w.2
  let _ : Module.IsTorsionFree vF.Completion E :=
    fieldAlgebra_isTorsionFree_forInertiaTransport
  let _ : IsAlgClosure vF.Completion E :=
    finitePlaceAlgebraicLocalization_isAlgClosure F v
  let _ : Normal vF.Completion E := IsAlgClosure.normal _ _
  let _ : CharZero vF.Completion :=
    charZero_of_injective_algebraMap
      (algebraMap F vF.Completion).injective
  let _ : Normal vF.Completion (SeparableClosure vF.Completion) :=
    inferInstance
  let _ : Valued E NNReal :=
    localizedCompletionFinitePlaceValued vF w hvFna
  let _ : ValuativeRel E :=
    localizedCompletionFinitePlaceValuativeRel vF w hvFna
  let _ : (ValuativeRel.valuation vF.Completion).HasExtension
      (ValuativeRel.valuation E) :=
    localizedCompletionValuationHasExtension vF w hvFna
  let e : E ≃ₐ[vF.Completion] SeparableClosure vF.Completion :=
    finitePlaceAlgebraicLocalizationAlgEquivSeparableClosure F v
  let A : ValuationSubring E :=
    HilbertRamification.algebraicLocalizationValuationSubring vF w hw
  let B : ValuationSubring (SeparableClosure vF.Completion) :=
    localSeparableValuationSubring vF.Completion
  have hA : A = (ValuativeRel.valuation E).valuationSubring :=
    algebraicLocalizationValuationSubring_eq_normValuationSubring
      vF w hvFna hw
  have hBA : B.comap e.toRingHom = A := by
    change (localSeparableValuationSubring vF.Completion).comap e.toRingHom = A
    rw [localSeparableValuationSubring_eq_comap_algEquiv
      vF.Completion E e, hA]
    ext x
    change e.symm (e x) ∈ (ValuativeRel.valuation E).valuationSubring ↔
      x ∈ (ValuativeRel.valuation E).valuationSubring
    rw [e.symm_apply_apply]
  let d := decompositionGroupEquivAlgebraicLocalizationAut
    vF (RayClass.adicAbv_isNontrivial v) w
  let localEquiv :=
    finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup F v
  let eMul := localEquiv.toMulEquiv
  let J : Subgroup Gal(SeparableClosure vF.Completion / vF.Completion) :=
    RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut
      vF.Completion (localSeparableValuationSubring vF.Completion)
  have htransport (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
      eMul sigma = AlgEquiv.autCongr e (d sigma) :=
    finitePlaceDecompositionTransport_apply F v sigma
  have hmem (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
      eMul sigma ∈ J ↔
        finitePlaceAbsoluteDecompositionValuationEquiv F v sigma ∈
          RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup F
            (finitePlaceAbsoluteValuationSubring F v) := by
    rw [htransport sigma]
    have hcongr :=
      autCongr_mem_valuationInertiaGroupInAut_iff e B (d sigma)
    rw [hBA] at hcongr
    rw [hcongr]
    exact decompositionGroupEquivAlgebraicLocalizationAut_mem_inertia_iff
      vF (RayClass.adicAbv_isNontrivial v) w hw sigma
  exact hmem sigma

theorem finitePlaceLocalInertia_comap_eq_absoluteInertia
    (F : Type) [Field F] [NumberField F]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    let vF := NumberField.HeightOneSpectrum.adicAbv F v
    let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
    letI : Valued vF.Completion NNReal :=
      finitePlaceCompletionValued vF hvFna
    letI : ValuativeRel vF.Completion :=
      finitePlaceCompletionValuativeRel vF hvFna
    letI : IsNonarchimedeanLocalField vF.Completion :=
      finitePlaceNormCompletionIsNonarchimedeanLocalField F v
    Subgroup.comap
        (finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup
          F v).toMonoidHom
        (RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut
          vF.Completion (localSeparableValuationSubring vF.Completion)) =
      finitePlaceAbsoluteInertiaSubgroup F v := by
  let vF := NumberField.HeightOneSpectrum.adicAbv F v
  let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
  let _ : Valued vF.Completion NNReal :=
    finitePlaceCompletionValued vF hvFna
  let _ : ValuativeRel vF.Completion :=
    finitePlaceCompletionValuativeRel vF hvFna
  let _ : IsNonarchimedeanLocalField vF.Completion :=
    finitePlaceNormCompletionIsNonarchimedeanLocalField F v
  ext sigma
  exact finitePlaceDecompositionTransport_mem_inertia_iff F v sigma

theorem finitePlaceAbsoluteInertia_map_eq_localResidueDegree_ker
    (F : Type) [Field F] [NumberField F]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    let vF := NumberField.HeightOneSpectrum.adicAbv F v
    let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
    letI : Valued vF.Completion NNReal :=
      finitePlaceCompletionValued vF hvFna
    letI : ValuativeRel vF.Completion :=
      finitePlaceCompletionValuativeRel vF hvFna
    letI : IsNonarchimedeanLocalField vF.Completion :=
      finitePlaceNormCompletionIsNonarchimedeanLocalField F v
    Subgroup.map
        (finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup
          F v).toMonoidHom
        (finitePlaceAbsoluteInertiaSubgroup F v) =
      MonoidHom.ker (localResidueDegree vF.Completion).toMonoidHom := by
  let vF := NumberField.HeightOneSpectrum.adicAbv F v
  let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
  let _ : Valued vF.Completion NNReal :=
    finitePlaceCompletionValued vF hvFna
  let _ : ValuativeRel vF.Completion :=
    finitePlaceCompletionValuativeRel vF hvFna
  let _ : IsNonarchimedeanLocalField vF.Completion :=
    finitePlaceNormCompletionIsNonarchimedeanLocalField F v
  let localEquiv :=
    finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup F v
  let eMul := localEquiv.toMulEquiv
  let J : Subgroup Gal(SeparableClosure vF.Completion / vF.Completion) :=
    RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut
      vF.Completion (localSeparableValuationSubring vF.Completion)
  have hcomap :
      Subgroup.comap eMul.toMonoidHom J =
        finitePlaceAbsoluteInertiaSubgroup F v :=
    finitePlaceLocalInertia_comap_eq_absoluteInertia F v
  have hmap :
      Subgroup.map eMul.toMonoidHom
          (finitePlaceAbsoluteInertiaSubgroup F v) = J := by
    rw [← hcomap]
    exact Subgroup.map_comap_eq_self_of_surjective eMul.surjective J
  change Subgroup.map eMul.toMonoidHom
      (finitePlaceAbsoluteInertiaSubgroup F v) =
    MonoidHom.ker (localResidueDegree vF.Completion).toMonoidHom
  calc
    Subgroup.map eMul.toMonoidHom
        (finitePlaceAbsoluteInertiaSubgroup F v) = J := hmap
    _ = MonoidHom.ker (localResidueDegree vF.Completion).toMonoidHom := by
      change
        RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut
            vF.Completion (localSeparableValuationSubring vF.Completion) =
          MonoidHom.ker (localResidueDegree vF.Completion).toMonoidHom
      exact
        (localResidueDegree_ker_eq_valuationInertiaGroupInAut
          vF.Completion).symm

def finitePlaceUnramifiedQuotientContinuousMulEquiv
    (F : Type) [Field F] [NumberField F]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    let vF := NumberField.HeightOneSpectrum.adicAbv F v
    let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
    letI : Valued vF.Completion NNReal :=
      finitePlaceCompletionValued vF hvFna
    letI : ValuativeRel vF.Completion :=
      finitePlaceCompletionValuativeRel vF hvFna
    letI : IsNonarchimedeanLocalField vF.Completion :=
      finitePlaceNormCompletionIsNonarchimedeanLocalField F v
    finitePlaceAbsoluteDecompositionGroup F v ⧸
        finitePlaceAbsoluteInertiaSubgroup F v ≃ₜ*
      LocalUnramifiedGaloisQuotient vF.Completion := by
  let vF := NumberField.HeightOneSpectrum.adicAbv F v
  let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
  letI : Valued vF.Completion NNReal :=
    finitePlaceCompletionValued vF hvFna
  letI : ValuativeRel vF.Completion :=
    finitePlaceCompletionValuativeRel vF hvFna
  letI : IsNonarchimedeanLocalField vF.Completion :=
    finitePlaceNormCompletionIsNonarchimedeanLocalField F v
  exact
    LocalFieldTheory.QuotientGroup.continuousCongr
      (finitePlaceAbsoluteInertiaSubgroup F v)
      (MonoidHom.ker (localResidueDegree vF.Completion).toMonoidHom)
      (finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup
        F v)
      (finitePlaceAbsoluteInertia_map_eq_localResidueDegree_ker F v)

theorem finitePlaceUnramifiedQuotientContinuousMulEquiv_mk
    (F : Type) [Field F] [NumberField F]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    let vF := NumberField.HeightOneSpectrum.adicAbv F v
    let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
    letI : Valued vF.Completion NNReal :=
      finitePlaceCompletionValued vF hvFna
    letI : ValuativeRel vF.Completion :=
      finitePlaceCompletionValuativeRel vF hvFna
    letI : IsNonarchimedeanLocalField vF.Completion :=
      finitePlaceNormCompletionIsNonarchimedeanLocalField F v
    finitePlaceUnramifiedQuotientContinuousMulEquiv F v
        (QuotientGroup.mk' (finitePlaceAbsoluteInertiaSubgroup F v) sigma) =
      QuotientGroup.mk'
        (MonoidHom.ker (localResidueDegree vF.Completion).toMonoidHom)
        (finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup
          F v sigma) := by
  let vF := NumberField.HeightOneSpectrum.adicAbv F v
  let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
  let _ : Valued vF.Completion NNReal :=
    finitePlaceCompletionValued vF hvFna
  let _ : ValuativeRel vF.Completion :=
    finitePlaceCompletionValuativeRel vF hvFna
  let _ : IsNonarchimedeanLocalField vF.Completion :=
    finitePlaceNormCompletionIsNonarchimedeanLocalField F v
  exact LocalFieldTheory.QuotientGroup.continuousCongr_mk
    (finitePlaceAbsoluteInertiaSubgroup F v)
    (MonoidHom.ker (localResidueDegree vF.Completion).toMonoidHom)
    (finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup
      F v)
    (finitePlaceAbsoluteInertia_map_eq_localResidueDegree_ker F v) sigma