ArchimedeanNormQuotient.lean

def infinitePlaceAbsoluteValueExtension
    (v : InfinitePlace K) (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v) :
    AbsoluteValueExtension v.1 L

def absoluteCompletionRingEquivReal
    (v : InfinitePlace K) (hv : v.IsReal) :
    v.1.Completion ≃+* ℝ

def absoluteCompletionRingEquivComplex
    (v : InfinitePlace K) (hv : v.IsComplex) :
    v.1.Completion ≃+* ℂ

theorem absoluteValueDecompositionGroup_eq_infinitePlaceStabilizer
    (w : InfinitePlace L) :
    absoluteValueDecompositionGroup K w.1 =
      MulAction.stabilizer (L ≃ₐ[K] L) w

theorem normUnits_map_ringEquiv
    {K : Type u} {L : Type v} {K' : Type w} {L' : Type z}
    [Field K] [Field L] [Field K'] [Field L']
    [Algebra K L] [Algebra K' L']
    (eK : K ≃+* K') (eL : L ≃+* L')
    (he :
      RingHom.comp (algebraMap K' L') eK =
        RingHom.comp eL (algebraMap K L))
    (x : Lˣ) :
    Units.mapEquiv eK.toMulEquiv (normUnits K L x) =
      normUnits K' L'
        (Units.mapEquiv eL.toMulEquiv x)

theorem ringEquiv_compat_symm
    {K : Type u} {L : Type v} {K' : Type w} {L' : Type z}
    [Field K] [Field L] [Field K'] [Field L']
    [Algebra K L] [Algebra K' L']
    (eK : K ≃+* K') (eL : L ≃+* L')
    (he :
      RingHom.comp (algebraMap K' L') eK =
        RingHom.comp eL (algebraMap K L)) :
    RingHom.comp (algebraMap K L) eK.symm =
      RingHom.comp eL.symm (algebraMap K' L')

def normQuotientMapOfRingEquiv
    {K L K' L' : Type}
    [Field K] [Field L] [Field K'] [Field L']
    [Algebra K L] [Algebra K' L']
    (eK : K ≃+* K') (eL : L ≃+* L')
    (he :
      RingHom.comp (algebraMap K' L') eK =
        RingHom.comp eL (algebraMap K L)) :
    NormQuotient K L →* NormQuotient K' L'

theorem normQuotientMapOfRingEquiv_normClass
    {K L K' L' : Type}
    [Field K] [Field L] [Field K'] [Field L']
    [Algebra K L] [Algebra K' L']
    (eK : K ≃+* K') (eL : L ≃+* L')
    (he :
      RingHom.comp (algebraMap K' L') eK =
        RingHom.comp eL (algebraMap K L))
    (x : Kˣ) :
    normQuotientMapOfRingEquiv eK eL he
        (normClass K L x) =
      normClass K' L'
        (Units.mapEquiv eK.toMulEquiv x)

def normQuotientEquivOfRingEquiv
    {K L K' L' : Type}
    [Field K] [Field L] [Field K'] [Field L']
    [Algebra K L] [Algebra K' L']
    (eK : K ≃+* K') (eL : L ≃+* L')
    (he :
      RingHom.comp (algebraMap K' L') eK =
        RingHom.comp eL (algebraMap K L)) :
    NormQuotient K L ≃* NormQuotient K' L' where
  toFun := normQuotientMapOfRingEquiv eK eL he
  invFun :=
    normQuotientMapOfRingEquiv eK.symm eL.symm
      (ringEquiv_compat_symm eK eL he)
  left_inv q := by
    refine NormQuotient.inductionOn
      (motive := fun q =>
        normQuotientMapOfRingEquiv eK.symm eL.symm
            (ringEquiv_compat_symm eK eL he)
            (normQuotientMapOfRingEquiv eK eL he q) =
          q)
      q ?_
    intro x
    rw [normQuotientMapOfRingEquiv_normClass,
      normQuotientMapOfRingEquiv_normClass]
    congr 1
    exact (Units.mapEquiv eK.toMulEquiv).symm_apply_apply x
  right_inv q := by
    refine NormQuotient.inductionOn
      (motive := fun q =>
        normQuotientMapOfRingEquiv eK eL he
            (normQuotientMapOfRingEquiv eK.symm eL.symm
              (ringEquiv_compat_symm eK eL he) q) =
          q)
      q ?_
    intro x
    rw [normQuotientMapOfRingEquiv_normClass,
      normQuotientMapOfRingEquiv_normClass]
    congr 1
    exact (Units.mapEquiv eK.toMulEquiv).apply_symm_apply x
  map_mul' := fun x y =>
    map_mul (normQuotientMapOfRingEquiv eK eL he) x y

theorem herbrandH0_card_eq_one_of_group_card_eq_one
    {G A : Type*}
    [Group G] [Fintype G]
    [CommGroup A] [MulDistribMulAction G A]
    (hG : Nat.card G = 1) :
    Nat.card (HerbrandH0 G A) = 1

def infiniteCompletionNormQuotientEquivRealComplex
    (v : InfinitePlace K) (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v)
    (hv : v.IsReal) (hwc : w.IsComplex) :
    letI : w.1.LiesOver v.1 :=
      ⟨congrArg (fun q : InfinitePlace K => q.1) hw⟩
    NormQuotient v.Completion w.Completion ≃*
      NormQuotient ℝ ℂ := by
  letI : w.1.LiesOver v.1 :=
    ⟨congrArg (fun q : InfinitePlace K => q.1) hw⟩
  letI :
      NumberField.ComplexEmbedding.LiesOver
        (InfinitePlace.Completion.extensionEmbedding w)
        (InfinitePlace.Completion.extensionEmbedding v) :=
    InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal
      w hv
  exact
    normQuotientEquivOfRingEquiv
      (InfinitePlace.Completion.ringEquivRealOfIsReal hv)
      (InfinitePlace.Completion.ringEquivComplexOfIsComplex hwc)
      (by ext; simp)

def localizedCompletionNormQuotientEquivAbsoluteCompletions
    (v : InfinitePlace K) (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v) :
    let u :=
      infinitePlaceAbsoluteValueExtension v w hw
    letI hL :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K) u.1
    letI : SMul K u.1.Completion := hL.toSMul
    letI : Algebra v.1.Completion u.1.Completion :=
      AbsoluteValue.completionAlgebra v.1 u.1 u.2
    letI : Algebra v.1.Completion w.1.Completion :=
      AbsoluteValue.completionAlgebra v.1 w.1
        (infinitePlaceAbsoluteValueExtension v w hw).2
    NormQuotient v.1.Completion
        (LocalizedCompletion v.1 u) ≃*
      NormQuotient v.1.Completion w.1.Completion := by
  let u :=
    infinitePlaceAbsoluteValueExtension v w hw
  letI hL :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) u.1
  letI : SMul K u.1.Completion := hL.toSMul
  letI : Algebra v.1.Completion u.1.Completion :=
    AbsoluteValue.completionAlgebra v.1 u.1 u.2
  letI : Algebra v.1.Completion w.1.Completion :=
    AbsoluteValue.completionAlgebra v.1 w.1
      (infinitePlaceAbsoluteValueExtension v w hw).2
  let eLAlg :
      LocalizedCompletion v.1 u ≃ₐ[v.1.Completion]
        w.1.Completion :=
    localizedCompletionEquivCompletion
      v.1 v.isNontrivial u
  let eL : LocalizedCompletion v.1 u ≃+* w.1.Completion :=
    eLAlg.toRingEquiv
  exact
    normQuotientEquivOfRingEquiv
      (RingEquiv.refl v.1.Completion) eL
      (by
        ext x
        exact eLAlg.commutes x)

def absoluteCompletionNormQuotientEquivRealComplex
    (v : InfinitePlace K) (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v)
    (hv : v.IsReal) (hwc : w.IsComplex) :
    let u :=
      infinitePlaceAbsoluteValueExtension v w hw
    letI hL :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K) u.1
    letI : SMul K u.1.Completion := hL.toSMul
    letI : Algebra v.1.Completion u.1.Completion :=
      AbsoluteValue.completionAlgebra v.1 u.1 u.2
    letI : Algebra v.1.Completion w.1.Completion :=
      AbsoluteValue.completionAlgebra v.1 w.1
        (infinitePlaceAbsoluteValueExtension v w hw).2
    NormQuotient v.1.Completion w.1.Completion ≃*
      NormQuotient ℝ ℂ := by
  let u :=
    infinitePlaceAbsoluteValueExtension v w hw
  letI hL :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) u.1
  letI : SMul K u.1.Completion := hL.toSMul
  letI : Algebra v.1.Completion u.1.Completion :=
    AbsoluteValue.completionAlgebra v.1 u.1 u.2
  letI : Algebra v.1.Completion w.1.Completion :=
    AbsoluteValue.completionAlgebra v.1 w.1
      (infinitePlaceAbsoluteValueExtension v w hw).2
  letI : w.1.LiesOver v.1 :=
    ⟨congrArg (fun q : InfinitePlace K => q.1) hw⟩
  have hEmbedding :
      w.embedding.comp (algebraMap K L) =
        v.embedding :=
    (InfinitePlace.LiesOver.embedding_liesOver_of_isReal
      w hv).over
  have hCompletionEmbedding :
      ∀ x : v.1.Completion,
        InfinitePlace.Completion.extensionEmbedding w
            ((InfinitePlace.Completion.equiv w).symm
              (AbsoluteValue.completionMap
                v.1 w.1
                (infinitePlaceAbsoluteValueExtension
                  v w hw).2 x)) =
          InfinitePlace.Completion.extensionEmbedding v
            ((InfinitePlace.Completion.equiv v).symm x) := by
    intro x
    refine
      UniformSpace.Completion.induction_on
        (α := WithAbs v.1) x ?_ ?_
    · exact
        isClosed_eq
          ((InfinitePlace.Completion.isometry_extensionEmbedding
              w).continuous.comp
            ((InfinitePlace.Completion.continuous_ofCompletion
              w).comp
              (AbsoluteValue.completionMap_isometry
                v.1 w.1
                (infinitePlaceAbsoluteValueExtension
                  v w hw).2).continuous))
          ((InfinitePlace.Completion.isometry_extensionEmbedding
              v).continuous.comp
            (InfinitePlace.Completion.continuous_ofCompletion v))
    · intro y
      have hy :
          (y : v.1.Completion) =
            algebraMap K v.1.Completion
              (WithAbs.equiv v.1 y) := by
        rw [← AbsoluteValue.toCompletion_eq_algebraMap]
        simp
      have hmap :
          AbsoluteValue.completionMap v.1 w.1
              (infinitePlaceAbsoluteValueExtension v w hw).2
              (y : v.1.Completion) =
            AbsoluteValue.toCompletion w.1
              (algebraMap K L (WithAbs.equiv v.1 y)) :=
        (congrArg
          (AbsoluteValue.completionMap v.1 w.1
            (infinitePlaceAbsoluteValueExtension v w hw).2) hy).trans
          (AbsoluteValue.completionMap_coe v.1 w.1
            (infinitePlaceAbsoluteValueExtension v w hw).2
            (WithAbs.equiv v.1 y))
      have hwEmbedding :
          InfinitePlace.Completion.extensionEmbedding w
              ((InfinitePlace.Completion.equiv w).symm
                (AbsoluteValue.toCompletion w.1
                  (algebraMap K L (WithAbs.equiv v.1 y)))) =
            w.embedding (algebraMap K L (WithAbs.equiv v.1 y)) :=
        (InfinitePlace.Completion.extensionEmbedding_coe w
          ((WithAbs.equiv w.1).symm
            (algebraMap K L (WithAbs.equiv v.1 y)))).trans
          (congrArg w.embedding
            ((WithAbs.equiv w.1).apply_symm_apply
              (algebraMap K L (WithAbs.equiv v.1 y))))
      exact
        (congrArg (fun z : w.1.Completion =>
          InfinitePlace.Completion.extensionEmbedding w
            ((InfinitePlace.Completion.equiv w).symm z)) hmap).trans
          (hwEmbedding.trans
            ((DFunLike.congr_fun hEmbedding (WithAbs.equiv v.1 y)).trans
              (InfinitePlace.Completion.extensionEmbedding_coe v y).symm))
  exact
    normQuotientEquivOfRingEquiv
      (absoluteCompletionRingEquivReal v hv)
      (absoluteCompletionRingEquivComplex w hwc)
      (by
        ext x
        exact
          (InfinitePlace.Completion.extensionEmbeddingOfIsReal_apply hv
            ((InfinitePlace.Completion.equiv v).symm x)).trans
            (hCompletionEmbedding x).symm)

def realUnitsSign : ℝˣ →* ℤˣ

theorem realUnitsSign_coe (x : ℝˣ) :
    ((realUnitsSign x : ℤˣ) : ℤ) =
      (SignType.sign (x : ℝ) : ℤ)

theorem realUnitsSign_surjective :
    Function.Surjective realUnitsSign

theorem mem_realUnitsSign_ker_iff (x : ℝˣ) :
    x ∈ realUnitsSign.ker ↔ 0 < (x : ℝ)

theorem realUnitsSign_continuous :
    Continuous realUnitsSign

theorem realUnitsSign_ker_eq_complexNormSubgroup :
    realUnitsSign.ker = localNormSubgroup ℝ ℂ

def realComplexNormQuotientEquivSign :
    NormQuotient ℝ ℂ ≃* ℤˣ

instance realComplexNormQuotientFinite :
    Finite (NormQuotient ℝ ℂ)

theorem realComplexNormQuotient_card_eq_two :
    Nat.card (NormQuotient ℝ ℂ) = 2

theorem infinitePlaceLocalHerbrandH0_card_eq_localDegree
    (v : InfinitePlace K) (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v) :
    let u :=
      infinitePlaceAbsoluteValueExtension v w hw
    letI hL :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K) u.1
    letI : SMul K u.1.Completion := hL.toSMul
    letI : Algebra v.1.Completion u.1.Completion :=
      AbsoluteValue.completionAlgebra v.1 u.1 u.2
    letI := localizedCompletionGlobalAlgebra v.1 u
    letI := localizedCompletionIsScalarTower v.1 u
    letI : FiniteDimensional v.1.Completion
        (LocalizedCompletion v.1 u) :=
      localizedCompletionModuleFinite v.1 v.isNontrivial u
    letI : IsGalois v.1.Completion
        (LocalizedCompletion v.1 u) :=
      HilbertRamification.algebraicLocalization_isGalois v.1 u
    letI : Fintype (absoluteValueDecompositionGroup K w.1) :=
      Fintype.ofFinite _
    letI : MulDistribMulAction
        (absoluteValueDecompositionGroup K w.1)
        (LocalizedCompletion v.1 u)ˣ :=
      decompositionGroupLocalUnitsAction
        v.1 v.isNontrivial u
    Nat.card
        (HerbrandH0
          (absoluteValueDecompositionGroup K w.1)
          (LocalizedCompletion v.1 u)ˣ) =
      if w.IsUnramified K then 1 else 2 := by
  let u :=
    infinitePlaceAbsoluteValueExtension v w hw
  let hL :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) u.1
  let : SMul K u.1.Completion := hL.toSMul
  let : Algebra v.1.Completion u.1.Completion :=
    AbsoluteValue.completionAlgebra v.1 u.1 u.2
  let := localizedCompletionGlobalAlgebra v.1 u
  let := localizedCompletionIsScalarTower v.1 u
  let : FiniteDimensional v.1.Completion
      (LocalizedCompletion v.1 u) :=
    localizedCompletionModuleFinite v.1 v.isNontrivial u
  let : IsGalois v.1.Completion
      (LocalizedCompletion v.1 u) :=
    HilbertRamification.algebraicLocalization_isGalois v.1 u
  let : Fintype (absoluteValueDecompositionGroup K w.1) :=
    Fintype.ofFinite _
  let : MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (LocalizedCompletion v.1 u)ˣ :=
    decompositionGroupLocalUnitsAction
      v.1 v.isNontrivial u
  by_cases hUnramified : w.IsUnramified K
  · rw [ite_eq_left hUnramified]
    apply herbrandH0_card_eq_one_of_group_card_eq_one
    rw [absoluteValueDecompositionGroup_eq_infinitePlaceStabilizer w,
      InfinitePlace.card_stabilizer, ite_eq_left hUnramified]
  · rw [ite_eq_right hUnramified]
    have hRamified : w.IsRamified K := hUnramified
    have hvReal : v.IsReal := by
      rw [← hw]
      exact hRamified.isReal
    have hwComplex : w.IsComplex :=
      hRamified.isComplex
    let eH0 :=
      localHerbrandH0EquivNormQuotient
        v.1 v.isNontrivial u
    let eCompletion :=
      localizedCompletionNormQuotientEquivAbsoluteCompletions
        v w hw
    let eRealComplex :=
      absoluteCompletionNormQuotientEquivRealComplex
        v w hw hvReal hwComplex
    calc
      Nat.card
          (HerbrandH0
            (absoluteValueDecompositionGroup K w.1)
            (LocalizedCompletion v.1 u)ˣ) =
          Nat.card (NormQuotient ℝ ℂ) :=
        Nat.card_congr
          (eH0.trans
            (eCompletion.trans eRealComplex)).toEquiv
      _ = 2 := realComplexNormQuotient_card_eq_two

theorem infinitePlaceLocalClassAxiom_cards
    (v : InfinitePlace K) (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v)
    (σ : L ≃ₐ[K] L)
    (hgen : ∀ τ : L ≃ₐ[K] L,
      τ ∈ Subgroup.zpowers σ) :
    let u :=
      infinitePlaceAbsoluteValueExtension v w hw
    letI hL :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K) u.1
    letI : SMul K u.1.Completion := hL.toSMul
    letI : Algebra v.1.Completion u.1.Completion :=
      AbsoluteValue.completionAlgebra v.1 u.1 u.2
    letI := localizedCompletionGlobalAlgebra v.1 u
    letI := localizedCompletionIsScalarTower v.1 u
    letI : FiniteDimensional v.1.Completion
        (LocalizedCompletion v.1 u) :=
      localizedCompletionModuleFinite v.1 v.isNontrivial u
    letI : IsGalois v.1.Completion
        (LocalizedCompletion v.1 u) :=
      HilbertRamification.algebraicLocalization_isGalois v.1 u
    letI : Fintype (absoluteValueDecompositionGroup K w.1) :=
      Fintype.ofFinite _
    letI : MulDistribMulAction
        (absoluteValueDecompositionGroup K w.1)
        (LocalizedCompletion v.1 u)ˣ :=
      decompositionGroupLocalUnitsAction
        v.1 v.isNontrivial u
    Nat.card
        (HerbrandHMinusOne
          (absoluteValueDecompositionGroup K w.1)
          (LocalizedCompletion v.1 u)ˣ
          (subgroupGeneratorOfGenerator
            (absoluteValueDecompositionGroup K w.1)
            σ hgen)) = 1 ∧
      Nat.card
          (HerbrandH0
            (absoluteValueDecompositionGroup K w.1)
            (LocalizedCompletion v.1 u)ˣ) =
        if w.IsUnramified K then 1 else 2 := by
  let u :=
    infinitePlaceAbsoluteValueExtension v w hw
  let hL :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) u.1
  let : SMul K u.1.Completion := hL.toSMul
  let : Algebra v.1.Completion u.1.Completion :=
    AbsoluteValue.completionAlgebra v.1 u.1 u.2
  let := localizedCompletionGlobalAlgebra v.1 u
  let := localizedCompletionIsScalarTower v.1 u
  let : FiniteDimensional v.1.Completion
      (LocalizedCompletion v.1 u) :=
    localizedCompletionModuleFinite v.1 v.isNontrivial u
  let : IsGalois v.1.Completion
      (LocalizedCompletion v.1 u) :=
    HilbertRamification.algebraicLocalization_isGalois v.1 u
  let : Fintype (absoluteValueDecompositionGroup K w.1) :=
    Fintype.ofFinite _
  let : MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (LocalizedCompletion v.1 u)ˣ :=
    decompositionGroupLocalUnitsAction
      v.1 v.isNontrivial u
  exact
    ⟨localHerbrandHMinusOne_card_eq_one_of_absoluteValue
        v.1 v.isNontrivial u σ hgen,
      infinitePlaceLocalHerbrandH0_card_eq_localDegree
        v w hw⟩

theorem infinitePlaceLocalHerbrandH0Finite
    (v : InfinitePlace K) (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v) :
    let u :=
      infinitePlaceAbsoluteValueExtension v w hw
    letI : Fintype (absoluteValueDecompositionGroup K w.1) :=
      Fintype.ofFinite _
    letI : MulDistribMulAction
        (absoluteValueDecompositionGroup K w.1)
        (LocalizedCompletion v.1 u)ˣ :=
      decompositionGroupLocalUnitsAction
        v.1 v.isNontrivial u
    Finite
      (HerbrandH0
        (absoluteValueDecompositionGroup K w.1)
        (LocalizedCompletion v.1 u)ˣ) := by
  let u :=
    infinitePlaceAbsoluteValueExtension v w hw
  let hL :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) u.1
  let : SMul K u.1.Completion := hL.toSMul
  let : Algebra v.1.Completion u.1.Completion :=
    AbsoluteValue.completionAlgebra v.1 u.1 u.2
  let := localizedCompletionGlobalAlgebra v.1 u
  let := localizedCompletionIsScalarTower v.1 u
  let : FiniteDimensional v.1.Completion
      (LocalizedCompletion v.1 u) :=
    localizedCompletionModuleFinite v.1 v.isNontrivial u
  let : IsGalois v.1.Completion
      (LocalizedCompletion v.1 u) :=
    HilbertRamification.algebraicLocalization_isGalois v.1 u
  let : Fintype (absoluteValueDecompositionGroup K w.1) :=
    Fintype.ofFinite _
  let : MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (LocalizedCompletion v.1 u)ˣ :=
    decompositionGroupLocalUnitsAction
      v.1 v.isNontrivial u
  change
    Finite
      (HerbrandH0
        (absoluteValueDecompositionGroup K w.1)
        (LocalizedCompletion v.1 u)ˣ)
  by_cases hUnramified : w.IsUnramified K
  · have hGroup :
        Nat.card (absoluteValueDecompositionGroup K w.1) = 1 := by
      rw [absoluteValueDecompositionGroup_eq_infinitePlaceStabilizer w,
        InfinitePlace.card_stabilizer, ite_eq_left hUnramified]
    let : Subsingleton (absoluteValueDecompositionGroup K w.1) :=
      (Nat.card_eq_one_iff_unique.mp hGroup).1
    let :
        Subsingleton
          (HerbrandH0
            (absoluteValueDecompositionGroup K w.1)
            (LocalizedCompletion v.1 u)ˣ) :=
      herbrandH0_subsingleton_of_fixed_le_tateNormSubgroup
        (G := absoluteValueDecompositionGroup K w.1)
        (A := (LocalizedCompletion v.1 u)ˣ) (by
          intro a ha
          refine ⟨a, ?_⟩
          rw [tateNormHom_apply]
          unfold tateNorm
          classical
          have huniv :
              (Finset.univ :
                Finset (absoluteValueDecompositionGroup K w.1)) =
                {1} := by
            ext g
            simp [Subsingleton.elim g 1]
          rw [huniv]
          simp)
    exact
      Finite.of_injective
        (fun _ :
          HerbrandH0
            (absoluteValueDecompositionGroup K w.1)
            (LocalizedCompletion v.1 u)ˣ => false)
        (fun x y _ => Subsingleton.elim x y)
  · have hRamified : w.IsRamified K := hUnramified
    have hvReal : v.IsReal := by
      rw [← hw]
      exact hRamified.isReal
    have hwComplex : w.IsComplex :=
      hRamified.isComplex
    let eH0 :=
      localHerbrandH0EquivNormQuotient
        v.1 v.isNontrivial u
    let eCompletion :=
      localizedCompletionNormQuotientEquivAbsoluteCompletions
        v w hw
    let eRealComplex :=
      absoluteCompletionNormQuotientEquivRealComplex
        v w hw hvReal hwComplex
    exact
      Finite.of_equiv
        (NormQuotient ℝ ℂ)
        (eH0.trans
          (eCompletion.trans eRealComplex)).symm.toEquiv

theorem infinitePlaceLocalHerbrandHMinusOneFinite
    (v : InfinitePlace K) (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v)
    (σ : L ≃ₐ[K] L)
    (hgen : ∀ τ : L ≃ₐ[K] L,
      τ ∈ Subgroup.zpowers σ) :
    let u :=
      infinitePlaceAbsoluteValueExtension v w hw
    letI : Fintype (absoluteValueDecompositionGroup K w.1) :=
      Fintype.ofFinite _
    letI : MulDistribMulAction
        (absoluteValueDecompositionGroup K w.1)
        (LocalizedCompletion v.1 u)ˣ :=
      decompositionGroupLocalUnitsAction
        v.1 v.isNontrivial u
    Finite
      (HerbrandHMinusOne
        (absoluteValueDecompositionGroup K w.1)
        (LocalizedCompletion v.1 u)ˣ
        (subgroupGeneratorOfGenerator
          (absoluteValueDecompositionGroup K w.1)
          σ hgen)) := by
  let u :=
    infinitePlaceAbsoluteValueExtension v w hw
  let hL :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) u.1
  let : SMul K u.1.Completion := hL.toSMul
  let : Algebra v.1.Completion u.1.Completion :=
    AbsoluteValue.completionAlgebra v.1 u.1 u.2
  let := localizedCompletionGlobalAlgebra v.1 u
  let := localizedCompletionIsScalarTower v.1 u
  let : FiniteDimensional v.1.Completion
      (LocalizedCompletion v.1 u) :=
    localizedCompletionModuleFinite v.1 v.isNontrivial u
  let : IsGalois v.1.Completion
      (LocalizedCompletion v.1 u) :=
    HilbertRamification.algebraicLocalization_isGalois v.1 u
  let : Fintype (absoluteValueDecompositionGroup K w.1) :=
    Fintype.ofFinite _
  let : MulDistribMulAction
      (absoluteValueDecompositionGroup K w.1)
      (LocalizedCompletion v.1 u)ˣ :=
    decompositionGroupLocalUnitsAction
      v.1 v.isNontrivial u
  change
    Finite
      (HerbrandHMinusOne
        (absoluteValueDecompositionGroup K w.1)
        (LocalizedCompletion v.1 u)ˣ
        (subgroupGeneratorOfGenerator
          (absoluteValueDecompositionGroup K w.1)
          σ hgen))
  let :
      Subsingleton
        (HerbrandHMinusOne
          (absoluteValueDecompositionGroup K w.1)
          (LocalizedCompletion v.1 u)ˣ
          (subgroupGeneratorOfGenerator
            (absoluteValueDecompositionGroup K w.1)
            σ hgen)) :=
    localHerbrandHMinusOne_subsingleton
      v.1 v.isNontrivial u σ hgen
  exact
    Finite.of_injective
      (fun _ => false)
      (fun x y _ => Subsingleton.elim x y)