InfinitePlaceArtin.lean

def ramifiedInfinitePlaceConjugation
    (w : InfinitePlace L) (hRamified : w.IsRamified K) :
    L ≃ₐ[K] L

theorem ramifiedInfinitePlaceConjugation_isConj
    (w : InfinitePlace L) (hRamified : w.IsRamified K) :
    NumberField.ComplexEmbedding.IsConj
      (InfinitePlace.embedding w)
      (ramifiedInfinitePlaceConjugation
        (K := K) w hRamified)

theorem ramifiedInfinitePlaceConjugation_sq
    (w : InfinitePlace L) (hRamified : w.IsRamified K) :
    ramifiedInfinitePlaceConjugation
          (K := K) w hRamified *
        ramifiedInfinitePlaceConjugation
          (K := K) w hRamified =
      1

def infinitePlaceArtinMonoidHomOfPlace
    (v : InfinitePlace K) (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v) :
    v.Completionˣ →* (L ≃ₐ[K] L)

def chosenInfinitePlaceArtinMonoidHom
    (v : InfinitePlace K) :
    v.Completionˣ →* (L ≃ₐ[K] L)

theorem chosenInfinitePlaceArtinMonoidHom_neg_one_isConj_of_ramified
    (v : InfinitePlace K)
    (hRamified :
      (chosenInfinitePlaceAbove (L := L) v).IsRamified K) :
    NumberField.ComplexEmbedding.IsConj
      (InfinitePlace.embedding
        (chosenInfinitePlaceAbove (L := L) v))
      (chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v (-1 : v.Completionˣ))

theorem infinitePlaceArtinMonoidHomOfPlace_eq
    (v : InfinitePlace K)
    (w w' : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v)
    (hw' : w'.comap (algebraMap K L) = v) :
    infinitePlaceArtinMonoidHomOfPlace
        (K := K) (L := L) v w hw =
      infinitePlaceArtinMonoidHomOfPlace
        (K := K) (L := L) v w' hw'

theorem infinitePlaceArtinMonoidHomOfPlace_restrict_tower
    {E : Type}
    [Field E] [NumberField E]
    [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [IsGalois K E]
    (v : InfinitePlace K)
    (wL : InfinitePlace L)
    (hwL : wL.comap (algebraMap K L) = v)
    (hwE :
      (wL.comap (algebraMap E L)).comap
          (algebraMap K E) = v) :
    (AlgEquiv.restrictNormalHom E).comp
        (infinitePlaceArtinMonoidHomOfPlace
          (K := K) (L := L) v wL hwL) =
      infinitePlaceArtinMonoidHomOfPlace
        (K := K) (L := E) v
        (wL.comap (algebraMap E L)) hwE

theorem infinitePlace_normUnits_real_complex_pos
    {K' : Type}
    [Field K'] [NumberField K'] [Algebra K K']
    (v : InfinitePlace K) (W : InfinitePlace K')
    (hW : W.comap (algebraMap K K') = v)
    (hvReal : v.IsReal) (hWComplex : W.IsComplex)
    (x : W.Completionˣ) :
    letI : W.1.LiesOver v.1 :=
      ⟨congrArg (fun q : InfinitePlace K => q.1) hW⟩
    0 <
      InfinitePlace.Completion.ringEquivRealOfIsReal
        hvReal
        (LocalFieldTheory.normUnits
          v.Completion W.Completion x :
            v.Completion) := by
  let : W.1.LiesOver v.1 :=
    ⟨congrArg (fun q : InfinitePlace K => q.1) hW⟩
  let eReal :
      v.Completion ≃+* ℝ :=
    InfinitePlace.Completion.ringEquivRealOfIsReal
      hvReal
  let eComplex :
      W.Completion ≃+* ℂ :=
    InfinitePlace.Completion.ringEquivComplexOfIsComplex
      hWComplex
  let :
      NumberField.ComplexEmbedding.LiesOver
        (InfinitePlace.Completion.extensionEmbedding W)
        (InfinitePlace.Completion.extensionEmbedding v) :=
    InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal
      W hvReal
  have hCompatible :
      RingHom.comp (algebraMap ℝ ℂ) eReal =
        RingHom.comp eComplex
          (algebraMap v.Completion W.Completion) := by
    ext z
    simp [eReal, eComplex]
  have hNorm :=
    LocalClassFieldTheory.normUnits_map_ringEquiv
      eReal eComplex hCompatible x
  have hNormVal := congrArg Units.val hNorm
  change
    0 <
      ((Units.mapEquiv eReal.toMulEquiv
        (LocalFieldTheory.normUnits
          v.Completion W.Completion x) : ℝˣ) : ℝ)
  rw [hNormVal]
  change
    0 <
      Algebra.norm ℝ
        (eComplex (x : W.Completion))
  rw [Algebra.norm_complex_apply, Complex.normSq_pos]
  exact (map_ne_zero eComplex).2 (Units.ne_zero x)

theorem infinitePlace_normUnits_real_real
    {K' : Type}
    [Field K'] [NumberField K'] [Algebra K K']
    (v : InfinitePlace K) (W : InfinitePlace K')
    (hW : W.comap (algebraMap K K') = v)
    (hvReal : v.IsReal) (hWReal : W.IsReal)
    (x : W.Completionˣ) :
    letI : W.1.LiesOver v.1 :=
      ⟨congrArg (fun q : InfinitePlace K => q.1) hW⟩
    Units.mapEquiv
        (InfinitePlace.Completion.ringEquivRealOfIsReal
          hvReal).toMulEquiv
        (LocalFieldTheory.normUnits
          v.Completion W.Completion x) =
      Units.mapEquiv
        (InfinitePlace.Completion.ringEquivRealOfIsReal
          hWReal).toMulEquiv x := by
  let : W.1.LiesOver v.1 :=
    ⟨congrArg (fun q : InfinitePlace K => q.1) hW⟩
  let eBase :
      v.Completion ≃+* ℝ :=
    InfinitePlace.Completion.ringEquivRealOfIsReal
      hvReal
  let eExtension :
      W.Completion ≃+* ℝ :=
    InfinitePlace.Completion.ringEquivRealOfIsReal
      hWReal
  let :
      NumberField.ComplexEmbedding.LiesOver
        (InfinitePlace.Completion.extensionEmbedding W)
        (InfinitePlace.Completion.extensionEmbedding v) :=
    InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal
      W hvReal
  have hCompatible :
      RingHom.comp (algebraMap ℝ ℝ) eBase =
        RingHom.comp eExtension
          (algebraMap v.Completion W.Completion) := by
    ext z
    change
      InfinitePlace.Completion.extensionEmbeddingOfIsReal
          hvReal z =
        InfinitePlace.Completion.extensionEmbeddingOfIsReal
          hWReal ((algebraMap v.Completion W.Completion) z)
    apply Complex.ofReal_injective
    simpa only [
      InfinitePlace.Completion.extensionEmbeddingOfIsReal_apply] using
      (InfinitePlace.Completion.liesOver_extensionEmbedding_apply
        W (v := v)).symm
  simpa only [
    LocalFieldTheory.normUnits,
    Algebra.norm_self,
    Units.map_id,
    MonoidHom.id_apply
  ] using
    LocalClassFieldTheory.normUnits_map_ringEquiv
      eBase eExtension hCompatible x

theorem infinitePlaceArtinMonoidHomOfPlace_norm_restriction
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : InfinitePlace K) (W : InfinitePlace K')
    (w' : InfinitePlace L')
    (hW : W.comap (algebraMap K K') = v)
    (hw' : w'.comap (algebraMap K' L') = W) :
    let w := w'.comap (algebraMap L L')
    let hw : w.comap (algebraMap K L) = v := by
      dsimp only [w]
      rw [← InfinitePlace.comap_comp,
        ← IsScalarTower.algebraMap_eq K L L',
        IsScalarTower.algebraMap_eq K K' L',
        InfinitePlace.comap_comp, hw', hW]
    letI : W.1.LiesOver v.1 :=
      ⟨congrArg (fun q : InfinitePlace K => q.1) hW⟩
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)).comp
        (infinitePlaceArtinMonoidHomOfPlace
          (K := K') (L := L') W w' hw') =
      (infinitePlaceArtinMonoidHomOfPlace
        (K := K) (L := L) v w hw).comp
        (LocalFieldTheory.normUnits
          v.Completion W.Completion) := by
  classical
  let w := w'.comap (algebraMap L L')
  have hw :
      w.comap (algebraMap K L) = v := by
    dsimp only [w]
    rw [← InfinitePlace.comap_comp,
      ← IsScalarTower.algebraMap_eq K L L',
      IsScalarTower.algebraMap_eq K K' L',
      InfinitePlace.comap_comp, hw', hW]
  let : W.1.LiesOver v.1 :=
    ⟨congrArg (fun q : InfinitePlace K => q.1) hW⟩
  dsimp only
  by_cases hUpperUnramified : w'.IsUnramified K'
  · by_cases hLowerUnramified : w.IsUnramified K
    · have hLowerUnramified' :
          (w'.comap (algebraMap L L')).IsUnramified K := by
        simpa only [w] using hLowerUnramified
      unfold infinitePlaceArtinMonoidHomOfPlace
      rw [dite_eq_left hUpperUnramified, dite_eq_left hLowerUnramified']
      simp
    · have hLowerUnramified' :
          ¬ (w'.comap (algebraMap L L')).IsUnramified K := by
        simpa only [w] using hLowerUnramified
      have hLowerRamified : w.IsRamified K :=
        hLowerUnramified
      have hvReal : v.IsReal := by
        rw [← hw]
        exact hLowerRamified.isReal
      have hw'Complex : w'.IsComplex := by
        rw [← InfinitePlace.not_isReal_iff_isComplex]
        intro hw'Real
        have hwReal : w.IsReal := by
          exact hw'Real.comap (algebraMap L L')
        exact
          (InfinitePlace.not_isComplex_iff_isReal.mpr
            hwReal) hLowerRamified.isComplex
      have hWComplex : W.IsComplex := by
        rcases
            InfinitePlace.isUnramified_iff.mp
              hUpperUnramified with
          hw'Real | hWComplex
        · exact
            (InfinitePlace.not_isReal_iff_isComplex.mpr
              hw'Complex hw'Real).elim
        · simpa only [hw'] using hWComplex
      apply MonoidHom.ext
      intro x
      have hPositive :=
        infinitePlace_normUnits_real_complex_pos
          (K := K) v W hW hvReal hWComplex x
      have hSign :
          LocalClassFieldTheory.realUnitsSign
              (Units.mapEquiv
                (InfinitePlace.Completion.ringEquivRealOfIsReal
                  hvReal).toMulEquiv
                (LocalFieldTheory.normUnits
                  v.Completion W.Completion x)) =
            1 :=
        MonoidHom.mem_ker.mp
          ((LocalClassFieldTheory.mem_realUnitsSign_ker_iff _).2
            hPositive)
      unfold infinitePlaceArtinMonoidHomOfPlace
      rw [dite_eq_left hUpperUnramified, dite_eq_right hLowerUnramified']
      simp only [MonoidHom.comp_apply]
      dsimp
      split_ifs with hsign
      · exact map_one _
      · exact (hsign hSign).elim
  · have hUpperRamified : w'.IsRamified K' :=
      hUpperUnramified
    have hWReal : W.IsReal := by
      rw [← hw']
      exact hUpperRamified.isReal
    have hvReal : v.IsReal := by
      rw [← hW]
      exact hWReal.comap (algebraMap K K')
    let sigmaUpper :=
      ramifiedInfinitePlaceConjugation
        (K := K') w' hUpperRamified
    let sigmaRestricted : L ≃ₐ[K] L :=
      ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)) sigmaUpper
    have hSigmaUpper :=
      ramifiedInfinitePlaceConjugation_isConj
        (K := K') w' hUpperRamified
    let phi : L →+* ℂ :=
      (InfinitePlace.embedding w').comp
        (algebraMap L L')
    have hphi :
        NumberField.ComplexEmbedding.IsConj
          phi sigmaRestricted := by
      apply RingHom.ext
      intro x
      change
        star
            (InfinitePlace.embedding w'
              (algebraMap L L' x)) =
          InfinitePlace.embedding w'
            (algebraMap L L' (sigmaRestricted x))
      rw [show
        algebraMap L L' (sigmaRestricted x) =
          sigmaUpper (algebraMap L L' x) by
          dsimp [sigmaRestricted]
          change
            algebraMap L L'
                ((AlgEquiv.restrictNormal
                  (AlgEquiv.restrictScalars K sigmaUpper) L) x) =
              sigmaUpper (algebraMap L L' x)
          rw [AlgEquiv.restrictNormal_commutes]
          rfl]
      exact (hSigmaUpper.eq (algebraMap L L' x)).symm
    have hmk : InfinitePlace.mk phi = w := by
      change
        InfinitePlace.mk
            ((InfinitePlace.embedding w').comp
              (algebraMap L L')) =
          w'.comap (algebraMap L L')
      conv_rhs => rw [← InfinitePlace.mk_embedding w']
      rw [InfinitePlace.comap_mk]
    have hSign (x : W.Completionˣ) :
        LocalClassFieldTheory.realUnitsSign
            (Units.mapEquiv
              (InfinitePlace.Completion.ringEquivRealOfIsReal
                hWReal).toMulEquiv x) =
          LocalClassFieldTheory.realUnitsSign
            (Units.mapEquiv
              (InfinitePlace.Completion.ringEquivRealOfIsReal
                hvReal).toMulEquiv
              (LocalFieldTheory.normUnits
                v.Completion W.Completion x)) := by
      rw [infinitePlace_normUnits_real_real
        (K := K) v W hW hvReal hWReal x]
    by_cases hLowerUnramified : w.IsUnramified K
    · have hLowerUnramified' :
          (w'.comap (algebraMap L L')).IsUnramified K := by
        simpa only [w] using hLowerUnramified
      have hSigmaRestricted : sigmaRestricted = 1 :=
        hphi.isUnramified_mk_iff.mp
          (hmk.symm ▸ hLowerUnramified)
      apply MonoidHom.ext
      intro x
      unfold infinitePlaceArtinMonoidHomOfPlace
      rw [dite_eq_right hUpperUnramified, dite_eq_left hLowerUnramified']
      simp only [MonoidHom.comp_apply]
      dsimp
      split_ifs with hsign
      · change
          ((AlgEquiv.restrictNormalHom L).comp
            (AlgEquiv.restrictScalarsHom K)) 1 =
            1
        exact map_one _
      · simpa [sigmaRestricted, sigmaUpper] using hSigmaRestricted
    · have hLowerUnramified' :
          ¬ (w'.comap (algebraMap L L')).IsUnramified K := by
        simpa only [w] using hLowerUnramified
      have hLowerRamified : w.IsRamified K :=
        hLowerUnramified
      let sigmaLower :=
        ramifiedInfinitePlaceConjugation
          (K := K) w hLowerRamified
      have hSigmaLower :=
        ramifiedInfinitePlaceConjugation_isConj
          (K := K) w hLowerRamified
      have hSigmaRestrictedNe :
          sigmaRestricted ≠ 1 := by
        intro hSigmaRestricted
        have :
            (InfinitePlace.mk phi).IsUnramified K :=
          hphi.isUnramified_mk_iff.mpr
            hSigmaRestricted
        exact hLowerUnramified (hmk ▸ this)
      have hSigmaRestrictedMem :
          sigmaRestricted ∈
            MulAction.stabilizer
              (L ≃ₐ[K] L) w := by
        rw [← hmk,
          InfinitePlace.mem_stabilizer_mk_iff]
        exact Or.inr hphi
      have hSigmaRestrictedAtW :
          NumberField.ComplexEmbedding.IsConj
            (InfinitePlace.embedding w)
            sigmaRestricted := by
        rw [← InfinitePlace.mk_embedding w,
          InfinitePlace.mem_stabilizer_mk_iff] at hSigmaRestrictedMem
        exact
          hSigmaRestrictedMem.resolve_left
            hSigmaRestrictedNe
      have hSigmaEq :
          sigmaRestricted = sigmaLower :=
        hSigmaRestrictedAtW.ext hSigmaLower
      apply MonoidHom.ext
      intro x
      unfold infinitePlaceArtinMonoidHomOfPlace
      rw [dite_eq_right hUpperUnramified, dite_eq_right hLowerUnramified']
      simp only [MonoidHom.comp_apply]
      dsimp
      split_ifs with hsignUpper hsignLower hsignLower
      · exact map_one _
      · exact (hsignLower ((hSign x).symm.trans hsignUpper)).elim
      · exact (hsignUpper ((hSign x).trans hsignLower)).elim
      · simpa [sigmaRestricted, sigmaUpper, sigmaLower] using hSigmaEq

theorem chosenInfinitePlaceArtinMonoidHom_restrict_tower
    {E : Type}
    [Field E] [NumberField E]
    [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [IsAbelianGalois K E]
    (v : InfinitePlace K) :
    (AlgEquiv.restrictNormalHom E).comp
        (chosenInfinitePlaceArtinMonoidHom
          (K := K) (L := L) v) =
      chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := E) v

theorem chosenInfinitePlaceArtinMonoidHom_norm_restriction
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (W : InfinitePlace K') :
    let v := infinitePlaceBelow (K := K) W
    letI : W.1.LiesOver v.1 := ⟨rfl⟩
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)).comp
        (chosenInfinitePlaceArtinMonoidHom
          (K := K') (L := L') W) =
      (chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v).comp
        (LocalFieldTheory.normUnits
          v.Completion W.Completion) := by
  let v := infinitePlaceBelow (K := K) W
  let w' :=
    chosenInfinitePlaceAbove
      (L := L') W
  let w := w'.comap (algebraMap L L')
  have hW :
      W.comap (algebraMap K K') = v := rfl
  have hw' :
      w'.comap (algebraMap K' L') = W :=
    chosenInfinitePlaceAbove_comap
      (L := L') W
  have hw :
      w.comap (algebraMap K L) = v := by
    dsimp only [w]
    rw [← InfinitePlace.comap_comp,
      ← IsScalarTower.algebraMap_eq K L L',
      IsScalarTower.algebraMap_eq K K' L',
      InfinitePlace.comap_comp, hw', hW]
  let : W.1.LiesOver v.1 := ⟨rfl⟩
  calc
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)).comp
        (chosenInfinitePlaceArtinMonoidHom
          (K := K') (L := L') W) =
      (infinitePlaceArtinMonoidHomOfPlace
        (K := K) (L := L) v w hw).comp
          (LocalFieldTheory.normUnits
            v.Completion W.Completion) :=
      infinitePlaceArtinMonoidHomOfPlace_norm_restriction
        (K := K) (L := L) v W w' hW hw'
    _ =
      (chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v).comp
          (LocalFieldTheory.normUnits
            v.Completion W.Completion) := by
      rw [chosenInfinitePlaceArtinMonoidHom]
      rw [infinitePlaceArtinMonoidHomOfPlace_eq
        (K := K) (L := L) v w
        (chosenInfinitePlaceAbove
          (L := L) v)
        hw
        (chosenInfinitePlaceAbove_comap
          (L := L) v)]

theorem chosenInfinitePlaceArtinMonoidHom_continuous
    (v : InfinitePlace K) :
    Continuous
      (chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v)

theorem chosenInfinitePlaceArtinMonoidHom_eq_one_of_real_pos
    (v : InfinitePlace K) (hvReal : v.IsReal)
    (x : v.Completionˣ)
    (hx :
      0 <
        InfinitePlace.Completion.ringEquivRealOfIsReal
          hvReal (x : v.Completion)) :
    chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v x = 1

theorem chosenInfinitePlaceArtinMonoidHom_ker
    (v : InfinitePlace K) :
    MonoidHom.ker
        (chosenInfinitePlaceArtinMonoidHom
          (K := K) (L := L) v) =
      infiniteTensorNormSubgroup
        (K := K) (L := L) v

def infinitePlaceGlobalArtinMonoidHom :
    IdeleGroup K →* (L ≃ₐ[K] L)

theorem infinitePlaceGlobalArtinMonoidHom_continuous :
    Continuous
      (infinitePlaceGlobalArtinMonoidHom
        (K := K) (L := L))

theorem infinitePlaceGlobalArtinMonoidHom_norm_eq_prod
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    (a : IdeleGroup M) :
    letI : ∀ W : InfinitePlace M,
        W.1.LiesOver
          (infinitePlaceBelow (K := K) W).1 :=
      fun _ => ⟨rfl⟩
    infinitePlaceGlobalArtinMonoidHom
        (K := K) (L := L)
        (IdeleGroup.norm K M a) =
      ∏ W : InfinitePlace M,
        chosenInfinitePlaceArtinMonoidHom
          (K := K) (L := L)
          (infinitePlaceBelow (K := K) W)
          (LocalFieldTheory.normUnits
            (infinitePlaceBelow
              (K := K) W).Completion
            W.Completion
            (IdeleGroup.infiniteComponent W a)) := by
  classical
  let : ∀ W : InfinitePlace M,
      W.1.LiesOver
        (infinitePlaceBelow (K := K) W).1 :=
    fun _ => ⟨rfl⟩
  let factor : InfinitePlace M → (L ≃ₐ[K] L) :=
    fun W =>
      chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L)
        (infinitePlaceBelow (K := K) W)
        (LocalFieldTheory.normUnits
          (infinitePlaceBelow
            (K := K) W).Completion
          W.Completion
          (IdeleGroup.infiniteComponent W a))
  unfold infinitePlaceGlobalArtinMonoidHom
  rw [MonoidHom.finsetProd_apply]
  change
    (∏ v : InfinitePlace K,
      chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v
        (IdeleGroup.infiniteComponent v
          (IdeleGroup.norm K M a))) =
      ∏ W : InfinitePlace M, factor W
  calc
    (∏ v : InfinitePlace K,
        chosenInfinitePlaceArtinMonoidHom
          (K := K) (L := L) v
          (IdeleGroup.infiniteComponent v
            (IdeleGroup.norm K M a))) =
        ∏ v : InfinitePlace K,
          ∏ W ∈ Finset.univ with
              infinitePlaceBelow (K := K) W = v,
            factor W := by
      apply Finset.prod_congr rfl
      intro v _
      let vK := v.1
      let hvK : vK.IsNontrivial := v.isNontrivial
      let eAbove :=
        infinitePlaceAboveEquivExtension
          (K := K) (L := M) v
      let :=
        AlgebraicNumberTheory.Valuations.completionTensorDecomposition_extensionFintype
          (K := K) (L := M) vK hvK
      let : Fintype {W : InfinitePlace M //
          infinitePlaceBelow (K := K) W = v} :=
        Fintype.ofEquiv
          (AlgebraicNumberTheory.Valuations.AbsoluteValueExtension vK M)
          eAbove.symm
      let : ∀ W : {W : InfinitePlace M //
          infinitePlaceBelow (K := K) W = v},
          W.1.1.LiesOver v.1 :=
        fun W =>
          ⟨congrArg (fun q : InfinitePlace K => q.1) W.2⟩
      rw [IdeleGroup.infiniteComponent_norm_eq_prod]
      rw [map_prod]
      symm
      rw [Finset.prod_subtype
        (p := fun W : InfinitePlace M =>
          infinitePlaceBelow (K := K) W = v)
        (s := Finset.univ.filter fun W : InfinitePlace M =>
          infinitePlaceBelow (K := K) W = v)
        (by intro W; simp)]
      apply Finset.prod_congr rfl
      intro W _
      rcases W with ⟨W, rfl⟩
      rfl
    _ = ∏ W : InfinitePlace M, factor W :=
      Finset.prod_fiberwise
        Finset.univ
        (infinitePlaceBelow (K := K))
        factor

theorem infinitePlaceGlobalArtinMonoidHom_norm_restriction
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L'] :
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)).comp
        (infinitePlaceGlobalArtinMonoidHom
          (K := K') (L := L')) =
      (infinitePlaceGlobalArtinMonoidHom
        (K := K) (L := L)).comp
        (IdeleGroup.norm K K')

theorem infinitePlaceGlobalArtinMonoidHom_finitePlaceIdele
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    infinitePlaceGlobalArtinMonoidHom
        (K := K) (L := L)
        (finitePlaceIdele v x) =
  1