FiniteIdeleArtin.lean

theorem finprod_fibers_eq_sigma
    {α β G : Type*} [CommMonoid G]
    (g : α → β) (f : α → G)
    (hf : HasFiniteMulSupport f) :
    (∏ᶠ b : β,
        ∏ᶠ x : {x : α // g x = b}, f x.1) =
      ∏ᶠ x : α, f x

theorem normUnits_mem_finitePlaceIntegerUnits
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K v) M)
    (x :
      ((finitePlaceExtensionCentre
        (K := K) (L := M) v w).adicCompletion M)ˣ)
    (hx :
      x ∈
        ((finitePlaceExtensionCentre
          (K := K) (L := M) v w).adicCompletionIntegers M).units) :
    letI : Algebra (v.adicCompletion K)
        ((finitePlaceExtensionCentre
          (K := K) (L := M) v w).adicCompletion M) :=
      (finitePlaceAdicCompletionMap K M v
        ⟨finitePlaceExtensionCentre (K := K) (L := M) v w,
          finitePlaceBelow_finitePlaceExtensionCentre
            (K := K) (L := M) v w⟩).toAlgebra
    LocalFieldTheory.normUnits
        (v.adicCompletion K)
        ((finitePlaceExtensionCentre
          (K := K) (L := M) v w).adicCompletion M) x ∈
      (v.adicCompletionIntegers K).units := by
  let W : {W : HeightOneSpectrum (𝓞 M) //
      _root_.finitePlaceBelow (K := K) W = v} :=
    ⟨finitePlaceExtensionCentre (K := K) (L := M) v w,
      finitePlaceBelow_finitePlaceExtensionCentre
        (K := K) (L := M) v w⟩
  let : Algebra (v.adicCompletion K)
      ((finitePlaceExtensionCentre
        (K := K) (L := M) v w).adicCompletion M) :=
    (finitePlaceAdicCompletionMap K M v W).toAlgebra
  let z : (W.1.adicCompletionIntegers M).units := ⟨x, hx⟩
  simpa only [W, z, Subgroup.coe_subtype] using
    IdeleGroup.finitePlace_normUnits_mem_integerUnits
      (K := K) (L := M) v W z

theorem finitePlaceArtinFactors_hasFiniteMulSupport
    (a : IdeleGroup K) :
    HasFiniteMulSupport
      (fun v : HeightOneSpectrum (𝓞 K) =>
        chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v
          (IdeleGroup.finiteComponent v a)) := by
  let S : Set (HeightOneSpectrum (𝓞 K)) :=
    {v | a.2 v ∉ (v.adicCompletionIntegers K).units}
  let T : Set (HeightOneSpectrum (𝓞 K)) :=
    {v | ∃ W : HeightOneSpectrum (𝓞 L),
      W.asIdeal.LiesOver v.asIdeal ∧
        ¬ Algebra.IsUnramifiedAt (𝓞 K) W.asIdeal}
  have hS : S.Finite :=
    Filter.eventually_cofinite.mp
      (FiniteIdeleGroup.eventually_mem_localUnits a.2)
  have hT : T.Finite :=
    AlgebraicNumberTheory.Ramification.finite_ramified_base_heightOne_primes
      (𝓞 K) (𝓞 L)
  rw [HasFiniteMulSupport]
  apply (hS.union hT).subset
  rw [mulSupport_subset_iff']
  intro v hv
  have hvS : v ∉ S := by
    intro hvS
    exact hv (Set.mem_union_left T hvS)
  have hvT : v ∉ T := by
    intro hvT
    exact hv (Set.mem_union_right S hvT)
  have hNorm :
      IdeleGroup.finiteComponent v a ∈
        chosenFinitePlaceLocalNormSubgroup
          (K := K) (L := L) v := by
    apply
      adicCompletionIntegerUnits_le_chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v
        (chosenFinitePlaceIsUnramified_of_isUnramifiedAt
          (K := K) (L := L) v (by
            by_contra hram
            apply hvT
            change
              ∃ W : HeightOneSpectrum (𝓞 L),
                W.asIdeal.LiesOver v.asIdeal ∧
                  ¬ Algebra.IsUnramifiedAt
                    (𝓞 K) W.asIdeal
            exact
              ⟨finitePlaceExtensionCentre
                  (K := K) (L := L) v
                  (chosenFinitePlaceExtension
                    (L := L) v),
                finitePlaceExtensionCentre_liesOver
                  (K := K) (L := L) v
                  (chosenFinitePlaceExtension
                    (L := L) v),
                hram⟩))
    simpa only [S, Set.mem_ofPred_eq, not_not,
      IdeleGroup.finiteComponent_apply] using hvS
  rw [← chosenFinitePlaceArtinMonoidHom_ker
    (K := K) (L := L) v] at hNorm
  exact MonoidHom.mem_ker.mp hNorm

theorem chosenFinitePlaceArtinMonoidHom_eq_one_of_integral_of_unramifiedAt
    (v : HeightOneSpectrum (𝓞 K))
    (a : IdeleGroup K)
    (ha :
      IdeleGroup.finiteComponent v a ∈
        (v.adicCompletionIntegers K).units)
    (hunram :
      Algebra.IsUnramifiedAt (𝓞 K)
        (finitePlaceExtensionCentre
          (K := K) (L := L) v
          (chosenFinitePlaceExtension
            (L := L) v)).asIdeal) :
    chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v
        (IdeleGroup.finiteComponent v a) = 1

theorem chosenFinitePlaceArtinMonoidHom_eq_one_of_mem_localNorm
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ)
    (hx : x ∈ chosenFinitePlaceLocalNormSubgroup
      (K := K) (L := L) v) :
    chosenFinitePlaceArtinMonoidHom (K := K) (L := L) v x = 1

def finitePlaceGlobalArtinMonoidHom :
    IdeleGroup K →* (L ≃ₐ[K] L) where
  toFun a :=
    ∏ᶠ v : HeightOneSpectrum (𝓞 K),
      chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v
        (IdeleGroup.finiteComponent v a)
  map_one' := by
    simp only [map_one]
    exact finprod_one
  map_mul' a b := by
    simp only [map_mul]
    exact
      finprod_mul_distrib
        (finitePlaceArtinFactors_hasFiniteMulSupport
          (K := K) (L := L) a)
        (finitePlaceArtinFactors_hasFiniteMulSupport
          (K := K) (L := L) b)

theorem finitePlaceGlobalArtinMonoidHom_continuous :
    Continuous
      (finitePlaceGlobalArtinMonoidHom
        (K := K) (L := L))

theorem finitePlaceGlobalArtinMonoidHom_norm_eq_finprod_fibers
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    (a : IdeleGroup M) :
    letI : ∀ v : HeightOneSpectrum (𝓞 K),
        Fintype {W : HeightOneSpectrum (𝓞 M) //
          finitePlaceBelow (K := K) W = v} :=
      fun v => by
        let vK := HeightOneSpectrum.adicAbv K v
        let hvK : vK.IsNontrivial :=
          RayClass.adicAbv_isNontrivial v
        letI :=
          completionTensorDecomposition_extensionFintype
            (K := K) (L := M) vK hvK
        exact
          Fintype.ofEquiv (AbsoluteValueExtension vK M)
            (finitePlaceExtensionEquivAbove
              (K := K) (L := M) v)
    letI : ∀ v : HeightOneSpectrum (𝓞 K),
        ∀ W : {W : HeightOneSpectrum (𝓞 M) //
          finitePlaceBelow (K := K) W = v},
          Algebra (v.adicCompletion K)
            (W.1.adicCompletion M) :=
      fun v W =>
        (finitePlaceAdicCompletionMap
          K M v W).toAlgebra
    finitePlaceGlobalArtinMonoidHom
        (K := K) (L := L)
        (IdeleGroup.norm K M a) =
      ∏ᶠ v : HeightOneSpectrum (𝓞 K),
        ∏ W : {W : HeightOneSpectrum (𝓞 M) //
            finitePlaceBelow (K := K) W = v},
          chosenFinitePlaceArtinMonoidHom
            (K := K) (L := L) v
            (LocalFieldTheory.normUnits
              (v.adicCompletion K)
              (W.1.adicCompletion M)
              (IdeleGroup.finiteComponent W.1 a)) := by
  classical
  let : ∀ v : HeightOneSpectrum (𝓞 K),
      Fintype {W : HeightOneSpectrum (𝓞 M) //
        finitePlaceBelow (K := K) W = v} :=
    fun v => by
      let vK := HeightOneSpectrum.adicAbv K v
      let hvK : vK.IsNontrivial :=
        RayClass.adicAbv_isNontrivial v
      letI :=
        completionTensorDecomposition_extensionFintype
          (K := K) (L := M) vK hvK
      exact
        Fintype.ofEquiv (AbsoluteValueExtension vK M)
          (finitePlaceExtensionEquivAbove
            (K := K) (L := M) v)
  let : ∀ v : HeightOneSpectrum (𝓞 K),
      ∀ W : {W : HeightOneSpectrum (𝓞 M) //
        finitePlaceBelow (K := K) W = v},
        Algebra (v.adicCompletion K)
          (W.1.adicCompletion M) :=
    fun v W =>
      (finitePlaceAdicCompletionMap
        K M v W).toAlgebra
  rw [finitePlaceGlobalArtinMonoidHom]
  apply finprod_congr
  intro v
  rw [IdeleGroup.finiteComponent_norm_eq_prod]
  rw [map_prod]

theorem finitePlaceNormArtinFactor_eq_one_of_component_unit_of_unramified
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    (a : IdeleGroup M)
    (W : HeightOneSpectrum (𝓞 M))
    (hComponentUnit :
      IdeleGroup.finiteComponent W a ∈
        (W.adicCompletionIntegers M).units)
    (hunram : ChosenFinitePlaceIsUnramified
      (K := K) (L := L) (finitePlaceBelow (K := K) W)) :
    let v := finitePlaceBelow (K := K) W
    letI : Algebra (v.adicCompletion K) (W.adicCompletion M) :=
      (finitePlaceAdicCompletionMap K M v ⟨W, rfl⟩).toAlgebra
    chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v
        (LocalFieldTheory.normUnits
          (v.adicCompletion K)
          (W.adicCompletion M)
          (IdeleGroup.finiteComponent W a)) = 1 := by
  let v := finitePlaceBelow (K := K) W
  let Wv :
      {Q : HeightOneSpectrum (𝓞 M) //
        finitePlaceBelow (K := K) Q = v} :=
    ⟨W, rfl⟩
  let z : (W.adicCompletionIntegers M).units :=
    ⟨IdeleGroup.finiteComponent W a, hComponentUnit⟩
  let : Algebra (v.adicCompletion K) (W.adicCompletion M) :=
    (finitePlaceAdicCompletionMap K M v Wv).toAlgebra
  have hNormUnit :
      LocalFieldTheory.normUnits
          (v.adicCompletion K)
          (W.adicCompletion M)
          (IdeleGroup.finiteComponent W a) ∈
        (v.adicCompletionIntegers K).units := by
    simpa only [z, Subgroup.coe_subtype] using
      IdeleGroup.finitePlace_normUnits_mem_integerUnits
        (K := K) (L := M) v Wv z
  apply
    chosenFinitePlaceArtinMonoidHom_eq_one_of_mem_localNorm
      (K := K) (L := L) v
  apply
    adicCompletionIntegerUnits_le_chosenFinitePlaceLocalNormSubgroup
      (K := K) (L := L) v hunram
  exact hNormUnit

theorem finitePlaceNormArtinFactors_hasFiniteMulSupport
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    (a : IdeleGroup M) :
    HasFiniteMulSupport
      (fun W : HeightOneSpectrum (𝓞 M) =>
        let v :=
          finitePlaceBelow (K := K) W
        letI : Algebra (v.adicCompletion K)
            (W.adicCompletion M) :=
          (finitePlaceAdicCompletionMap
            K M v ⟨W, rfl⟩).toAlgebra
        chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v
          (LocalFieldTheory.normUnits
            (v.adicCompletion K)
            (W.adicCompletion M)
            (IdeleGroup.finiteComponent W a))) := by
  let S : Set (HeightOneSpectrum (𝓞 M)) :=
    {W | a.2 W ∉ (W.adicCompletionIntegers M).units}
  let T : Set (HeightOneSpectrum (𝓞 K)) :=
    {v | ∃ V : HeightOneSpectrum (𝓞 L),
      V.asIdeal.LiesOver v.asIdeal ∧
        ¬ Algebra.IsUnramifiedAt (𝓞 K) V.asIdeal}
  let U : Set (HeightOneSpectrum (𝓞 M)) :=
    {W | finitePlaceBelow (K := K) W ∈ T}
  have hS : S.Finite :=
    Filter.eventually_cofinite.mp
      (FiniteIdeleGroup.eventually_mem_localUnits a.2)
  have hT : T.Finite :=
    AlgebraicNumberTheory.Ramification.finite_ramified_base_heightOne_primes
      (𝓞 K) (𝓞 L)
  have hU : U.Finite := by
    exact
      Set.Finite.preimage_finitePlaceBelow
        (K := K) (L := M) hT
  rw [HasFiniteMulSupport]
  apply (hS.union hU).subset
  rw [mulSupport_subset_iff']
  intro W hW
  have hWS : W ∉ S := by
    intro hWS
    exact hW (Set.mem_union_left U hWS)
  have hWU : W ∉ U := by
    intro hWU
    exact hW (Set.mem_union_right S hWU)
  let v :=
    finitePlaceBelow (K := K) W
  have hComponentUnit :
      IdeleGroup.finiteComponent W a ∈
        (W.adicCompletionIntegers M).units := by
    simpa only [S, Set.mem_ofPred_eq, not_not,
      IdeleGroup.finiteComponent_apply] using hWS
  have hvT : v ∉ T := by
    intro hvT
    apply hWU
    exact hvT
  apply
    finitePlaceNormArtinFactor_eq_one_of_component_unit_of_unramified
      (K := K) (L := L) a W hComponentUnit
  apply chosenFinitePlaceIsUnramified_of_isUnramifiedAt
    (K := K) (L := L) v
  by_contra hram
  apply hvT
  exact
    ⟨finitePlaceExtensionCentre
        (K := K) (L := L) v
        (chosenFinitePlaceExtension (L := L) v),
      finitePlaceExtensionCentre_liesOver
        (K := K) (L := L) v
        (chosenFinitePlaceExtension (L := L) v),
      hram⟩

theorem finitePlaceGlobalArtinMonoidHom_norm_eq_finprod
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    (a : IdeleGroup M) :
    letI : ∀ W : HeightOneSpectrum (𝓞 M),
        Algebra
          ((finitePlaceBelow
            (K := K) W).adicCompletion K)
          (W.adicCompletion M) :=
      fun W =>
        (finitePlaceAdicCompletionMap
          K M
          (finitePlaceBelow (K := K) W)
          ⟨W, rfl⟩).toAlgebra
    finitePlaceGlobalArtinMonoidHom
        (K := K) (L := L)
        (IdeleGroup.norm K M a) =
      ∏ᶠ W : HeightOneSpectrum (𝓞 M),
        chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L)
          (finitePlaceBelow (K := K) W)
          (LocalFieldTheory.normUnits
            ((finitePlaceBelow
              (K := K) W).adicCompletion K)
            (W.adicCompletion M)
            (IdeleGroup.finiteComponent W a)) := by
  classical
  let : ∀ W : HeightOneSpectrum (𝓞 M),
      Algebra
        ((finitePlaceBelow
          (K := K) W).adicCompletion K)
        (W.adicCompletion M) :=
    fun W =>
      (finitePlaceAdicCompletionMap
        K M
        (finitePlaceBelow (K := K) W)
        ⟨W, rfl⟩).toAlgebra
  let : ∀ v : HeightOneSpectrum (𝓞 K),
      Fintype {W : HeightOneSpectrum (𝓞 M) //
        finitePlaceBelow (K := K) W = v} :=
    fun v => by
      let vK := HeightOneSpectrum.adicAbv K v
      let hvK : vK.IsNontrivial :=
        RayClass.adicAbv_isNontrivial v
      letI :=
        completionTensorDecomposition_extensionFintype
          (K := K) (L := M) vK hvK
      exact
        Fintype.ofEquiv (AbsoluteValueExtension vK M)
          (finitePlaceExtensionEquivAbove
            (K := K) (L := M) v)
  let : ∀ v : HeightOneSpectrum (𝓞 K),
      ∀ W : {W : HeightOneSpectrum (𝓞 M) //
        finitePlaceBelow (K := K) W = v},
        Algebra (v.adicCompletion K)
          (W.1.adicCompletion M) :=
    fun v W =>
      (finitePlaceAdicCompletionMap
        K M v W).toAlgebra
  let g :
      HeightOneSpectrum (𝓞 M) →
        HeightOneSpectrum (𝓞 K) :=
    finitePlaceBelow (K := K)
  let f :
      HeightOneSpectrum (𝓞 M) →
        (L ≃ₐ[K] L) :=
    fun W =>
      chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) (g W)
        (LocalFieldTheory.normUnits
          ((g W).adicCompletion K)
          (W.adicCompletion M)
          (IdeleGroup.finiteComponent W a))
  have hf : HasFiniteMulSupport f := by
    simpa only [f, g] using
      finitePlaceNormArtinFactors_hasFiniteMulSupport
        (K := K) (L := L) a
  calc
    finitePlaceGlobalArtinMonoidHom
        (K := K) (L := L)
        (IdeleGroup.norm K M a) =
        ∏ᶠ v : HeightOneSpectrum (𝓞 K),
          ∏ W : {W : HeightOneSpectrum (𝓞 M) //
              g W = v},
            chosenFinitePlaceArtinMonoidHom
              (K := K) (L := L) v
              (LocalFieldTheory.normUnits
                (v.adicCompletion K)
                (W.1.adicCompletion M)
                (IdeleGroup.finiteComponent W.1 a)) := by
      simpa only [g] using
        finitePlaceGlobalArtinMonoidHom_norm_eq_finprod_fibers
          (K := K) (L := L) a
    _ = ∏ᶠ v : HeightOneSpectrum (𝓞 K),
          ∏ᶠ W : {W : HeightOneSpectrum (𝓞 M) //
              g W = v},
            f W.1 := by
      apply finprod_congr
      intro v
      rw [finprod_eq_prod_of_fintype]
      apply Finset.prod_congr rfl
      intro W _
      rcases W with ⟨W, hW⟩
      subst v
      simp only [f, g]
    _ = ∏ᶠ W : HeightOneSpectrum (𝓞 M), f W :=
      finprod_fibers_eq_sigma g f hf
    _ = ∏ᶠ W : HeightOneSpectrum (𝓞 M),
          chosenFinitePlaceArtinMonoidHom
            (K := K) (L := L)
            (finitePlaceBelow (K := K) W)
            (LocalFieldTheory.normUnits
              ((finitePlaceBelow (K := K) W).adicCompletion K)
              (W.adicCompletion M)
              (IdeleGroup.finiteComponent W a)) := by
      apply finprod_congr
      intro W
      simp only [f, g]

theorem finitePlaceGlobalArtinMonoidHom_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
        (finitePlaceGlobalArtinMonoidHom
          (K := K') (L := L')) =
      (finitePlaceGlobalArtinMonoidHom
        (K := K) (L := L)).comp
        (IdeleGroup.norm K K')

theorem finitePlaceGlobalArtinMonoidHom_finitePlaceIdele
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    finitePlaceGlobalArtinMonoidHom
        (K := K) (L := L)
        (finitePlaceIdele v x) =
      chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v x