InfiniteGlobalArtin.lean

theorem rationalInfinitePlace_isReal
    (v : InfinitePlace ℚ) :
    v.IsReal

def rationalPositiveArchimedeanLocalComponent
    (v : InfinitePlace ℚ) :
    ℝ≥0ˣ →* v.Completionˣ

def rationalPositiveArchimedeanInfinitePart :
    ℝ≥0ˣ →* InfiniteIdeleGroup ℚ

theorem rationalPositiveArchimedeanInfinitePart_component
    (r : ℝ≥0ˣ) (v : InfinitePlace ℚ) :
    ContinuousMulEquiv.piUnits
        (rationalPositiveArchimedeanInfinitePart r) v =
      rationalPositiveArchimedeanLocalComponent v r

def rationalPositiveArchimedeanIdele :
    ℝ≥0ˣ →* IdeleGroup ℚ

theorem rationalPositiveArchimedeanIdele_finiteComponent
    (r : ℝ≥0ˣ)
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    IdeleGroup.finiteComponent v
        (rationalPositiveArchimedeanIdele r) =
      1

theorem rationalPositiveArchimedeanIdele_infiniteComponent
    (r : ℝ≥0ˣ) :
    Units.mapEquiv
        (InfinitePlace.Completion.ringEquivRealOfIsReal
          Rat.isReal_infinitePlace).toMulEquiv
        (IdeleGroup.infiniteComponent Rat.infinitePlace
          (rationalPositiveArchimedeanIdele r)) =
      Units.map NNReal.toRealHom.toMonoidHom r

theorem rationalPositiveArchimedeanIdele_absoluteNorm
    (r : ℝ≥0ˣ) :
    IdeleGroup.absoluteNorm
        (rationalPositiveArchimedeanIdele r) =
      r⁻¹

theorem globalArtinMonoidHom_rationalPositiveArchimedeanIdele
    {L : Type}
    [Field L] [NumberField L] [Algebra ℚ L]
    [IsAbelianGalois ℚ L]
    (r : ℝ≥0ˣ) :
    globalArtinMonoidHom
        (K := ℚ) (L := L)
        (rationalPositiveArchimedeanIdele r) =
      1

def infiniteGlobalArtinLimitPoint
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K) :
    limit
      (InfiniteGalois.asProfiniteGaloisGroupFunctor
        K Ω)

def infiniteGlobalArtinToLimit
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω] :
    IdeleGroup K →ₜ*
      limit
        (InfiniteGalois.asProfiniteGaloisGroupFunctor
          K Ω)

def infiniteGlobalArtinMonoidHom
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω] :
    IdeleGroup K →ₜ* (Ω ≃ₐ[K] Ω)

theorem restrictNormalHom_infiniteGlobalArtinMonoidHom_of_numberField
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K)
    (E : FiniteGaloisIntermediateField K Ω)
    (hE : NumberField E) :
    letI : NumberField E := hE
    AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a) =
      globalArtinMonoidHom
        (K := K) (L := E) a := by
  let : NumberField E := hE
  have hcomponent :=
    congrArg
      (InfiniteGalois.proj
        (k := K) (K := Ω) E)
      ((InfiniteGalois.continuousMulEquivToLimit
        K Ω).apply_symm_apply
          (infiniteGlobalArtinToLimit K Ω a))
  exact hcomponent

theorem restrictNormalHom_infiniteGlobalArtinMonoidHom_of_structures
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K)
    (E : FiniteGaloisIntermediateField K Ω)
    (hE : NumberField E)
    (hAbelian : IsAbelianGalois K E) :
    letI : NumberField E := hE
    letI : IsAbelianGalois K E := hAbelian
    AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a) =
      globalArtinMonoidHom
        (K := K) (L := E) a := by
  let : NumberField E := hE
  let : IsAbelianGalois K E := hAbelian
  exact
    restrictNormalHom_infiniteGlobalArtinMonoidHom_of_numberField
      K Ω a E hE

theorem restrictNormalHom_infiniteGlobalArtinMonoidHom_of_intermediateField
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K) (E : IntermediateField K Ω)
    [FiniteDimensional K E] [IsGalois K E]
    (hE : NumberField E)
    (hAbelian : IsAbelianGalois K E) :
    letI : NumberField E := hE
    letI : IsAbelianGalois K E := hAbelian
    AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a) =
      globalArtinMonoidHom (K := K) (L := E) a := by
  let G : FiniteGaloisIntermediateField K Ω :=
    { toIntermediateField := E
      finiteDimensional := inferInstance
      isGalois := inferInstance }
  let : NumberField E := hE
  let : IsAbelianGalois K E := hAbelian
  exact
    restrictNormalHom_infiniteGlobalArtinMonoidHom_of_structures
      K Ω a G hE hAbelian

theorem restrictNormalHom_infiniteGlobalArtinMonoidHom_intermediateField
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K) (E : IntermediateField K Ω)
    [FiniteDimensional K E] [NumberField E] [IsAbelianGalois K E] :
    AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a) =
      globalArtinMonoidHom (K := K) (L := E) a

theorem restrictNormalHom_infiniteGlobalArtinMonoidHom_of_numberField_apply
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K)
    (E : FiniteGaloisIntermediateField K Ω)
    (hE : NumberField E)
    (x : E) :
    letI : NumberField E := hE
    AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a) x =
      globalArtinMonoidHom
        (K := K) (L := E) a x := by
  let : NumberField E := hE
  exact DFunLike.congr_fun
    (restrictNormalHom_infiniteGlobalArtinMonoidHom_of_numberField
      K Ω a E hE) x

theorem map_restrictNormalHom_infiniteGlobalArtinMonoidHom_of_numberField
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K)
    (E : FiniteGaloisIntermediateField K Ω)
    (hE : NumberField E)
    {M : Type} (f : (E ≃ₐ[K] E) → M) :
    letI : NumberField E := hE
    f (AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a)) =
      f (globalArtinMonoidHom
        (K := K) (L := E) a) := by
  let : NumberField E := hE
  exact congrArg f
    (restrictNormalHom_infiniteGlobalArtinMonoidHom_of_numberField
      K Ω a E hE)

theorem map_restrictNormalHom_infiniteGlobalArtinMonoidHom_of_structures
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K)
    (E : FiniteGaloisIntermediateField K Ω)
    (hE : NumberField E)
    (hAbelian : IsAbelianGalois K E)
    {M : Type} (f : (E ≃ₐ[K] E) → M) :
    letI : NumberField E := hE
    letI : IsAbelianGalois K E := hAbelian
    f (AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a)) =
      f (globalArtinMonoidHom
        (K := K) (L := E) a) := by
  let : NumberField E := hE
  let : IsAbelianGalois K E := hAbelian
  exact congrArg f
    (restrictNormalHom_infiniteGlobalArtinMonoidHom_of_structures
      K Ω a E hE hAbelian)

theorem
    map_restrictNormalHom_infiniteGlobalArtinMonoidHom_of_intermediateField
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K) (E : IntermediateField K Ω)
    [FiniteDimensional K E] [IsGalois K E]
    (hE : NumberField E)
    (hAbelian : IsAbelianGalois K E)
    {M : Type} (f : (E ≃ₐ[K] E) → M) :
    letI : NumberField E := hE
    letI : IsAbelianGalois K E := hAbelian
    f (AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a)) =
      f (globalArtinMonoidHom (K := K) (L := E) a) := by
  let : NumberField E := hE
  let : IsAbelianGalois K E := hAbelian
  exact congrArg f
    (restrictNormalHom_infiniteGlobalArtinMonoidHom_of_intermediateField
      K Ω a E hE hAbelian)

def globalArtinMonoidHomOfNumberField
    (K L : Type) [Field K] [NumberField K]
    [Field L] [Algebra K L] [IsAbelianGalois K L]
    (hL : NumberField L) :
    IdeleGroup K →* (L ≃ₐ[K] L)

theorem globalArtinMonoidHomOfNumberField_norm_restriction
    (K L K' L' : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
    [Field K'] [NumberField K']
    [Field L'] [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (hL' : NumberField L') :
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)).comp
        (globalArtinMonoidHomOfNumberField K' L' hL') =
      (globalArtinMonoidHom (K := K) (L := L)).comp
        (IdeleGroup.norm K K')

theorem comp_restrictNormalHom_infiniteGlobalArtinMonoidHom_of_numberField
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K)
    (E : FiniteGaloisIntermediateField K Ω)
    (hE : NumberField E)
    {M : Type} [Monoid M]
    (f : (E ≃ₐ[K] E) →* M) :
    letI : NumberField E := hE
    f (AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a)) =
      (f.comp (globalArtinMonoidHomOfNumberField K E hE)) a := by
  let : NumberField E := hE
  exact
    (map_restrictNormalHom_infiniteGlobalArtinMonoidHom_of_numberField
      K Ω a E hE f).trans rfl

def
    compRestrictNormalHomInfiniteGlobalArtinDataOfNumberField
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K)
    (E : FiniteGaloisIntermediateField K Ω)
    (hE : NumberField E)
    {M : Type} [Monoid M]
    (f : (E ≃ₐ[K] E) →* M) :
    letI : NumberField E := hE
    {x : M //
      x = (f.comp
        (globalArtinMonoidHomOfNumberField K E hE)) a} := by
  letI : NumberField E := hE
  exact
    ⟨f (AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a)),
      comp_restrictNormalHom_infiniteGlobalArtinMonoidHom_of_numberField
        K Ω a E hE f⟩

def
    compRestrictNormalHomInfiniteGlobalArtinNaturalityDataOfNumberField
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K)
    (E : FiniteGaloisIntermediateField K Ω)
    (hE : NumberField E)
    {M : Type} [Monoid M]
    (f : (E ≃ₐ[K] E) →* M)
    (g : IdeleGroup K →* M)
    (hnat :
      f.comp (globalArtinMonoidHomOfNumberField K E hE) = g) :
    letI : NumberField E := hE
    {x : M // x = g a} := by
  letI : NumberField E := hE
  have hprojection :=
    comp_restrictNormalHom_infiniteGlobalArtinMonoidHom_of_numberField
      K Ω a E hE f
  exact
    ⟨f (AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a)),
      hprojection.trans (DFunLike.congr_fun hnat a)⟩

theorem map_restrictNormalHom_infiniteGlobalArtinMonoidHom
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K)
    (E : FiniteGaloisIntermediateField K Ω)
    [NumberField E]
    {M : Type} (f : (E ≃ₐ[K] E) → M) :
    f (AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a)) =
      f (globalArtinMonoidHom
        (K := K) (L := E) a)

theorem restrictNormalHom_infiniteGlobalArtinMonoidHom
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K)
    (E : FiniteGaloisIntermediateField K Ω) :
    letI : NumberField E :=
      NumberField.of_module_finite K E
    AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a) =
      globalArtinMonoidHom
        (K := K) (L := E) a := by
  exact
    restrictNormalHom_infiniteGlobalArtinMonoidHom_of_numberField
      K Ω a E (NumberField.of_module_finite K E)

theorem restrictNormalHom_infiniteGlobalArtinMonoidHom_of_scalarTower
    (K E Ω : Type) [Field K] [NumberField K]
    [Field E] [NumberField E] [Algebra K E]
    [IsAbelianGalois K E]
    [Field Ω] [Algebra K Ω] [Algebra E Ω]
    [IsScalarTower K E Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K) :
    AlgEquiv.restrictNormalHom E
        (infiniteGlobalArtinMonoidHom K Ω a) =
      globalArtinMonoidHom (K := K) (L := E) a

theorem infiniteGlobalArtinMonoidHom_denseRange
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω] :
    DenseRange (infiniteGlobalArtinMonoidHom K Ω)

def rationalCyclotomicZHatGlobalArtin :
    IdeleGroup ℚ →ₜ*
      (rationalCyclotomicZHatField ≃ₐ[ℚ]
        rationalCyclotomicZHatField)

theorem
    continuousMulEquivToLimit_rationalCyclotomicZHatGlobalArtin_apply
    (a : IdeleGroup ℚ) :
    InfiniteGalois.continuousMulEquivToLimit
        ℚ rationalCyclotomicZHatField
        (rationalCyclotomicZHatGlobalArtin a) =
      infiniteGlobalArtinToLimit
        ℚ rationalCyclotomicZHatField a

theorem restrictNormalHom_rationalCyclotomicZHatGlobalArtin
    (a : IdeleGroup ℚ)
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField) :
    letI : NumberField E :=
      NumberField.of_module_finite ℚ E
    letI : IsAbelianGalois ℚ E :=
      IsAbelianGalois.of_algHom E.toIntermediateField.val
    AlgEquiv.restrictNormalHom E
        (rationalCyclotomicZHatGlobalArtin a) =
      globalArtinMonoidHom
        (K := ℚ) (L := E) a :=
  restrictNormalHom_infiniteGlobalArtinMonoidHom
    ℚ rationalCyclotomicZHatField a E

theorem restrictNormalHom_rationalCyclotomicZHatGlobalArtin_of_structures
    (a : IdeleGroup ℚ)
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField)
    (hE : NumberField E)
    (hAbelian : IsAbelianGalois ℚ E) :
    letI : NumberField E := hE
    letI : IsAbelianGalois ℚ E := hAbelian
    AlgEquiv.restrictNormalHom E
        (rationalCyclotomicZHatGlobalArtin a) =
      globalArtinMonoidHom
        (K := ℚ) (L := E) a := by
  let : NumberField E := hE
  let : IsAbelianGalois ℚ E := hAbelian
  exact
    restrictNormalHom_infiniteGlobalArtinMonoidHom_of_structures
      ℚ rationalCyclotomicZHatField a E hE hAbelian

def
    compRestrictNormalHomInfiniteGlobalArtinRationalCyclotomicDataOfNumberField
    (K Ω : Type) [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K)
    (E' : FiniteGaloisIntermediateField K Ω)
    (hE' : NumberField E')
    (E :
      FiniteGaloisIntermediateField
        ℚ rationalCyclotomicZHatField)
    (hE : NumberField E)
    (hAbelian : IsAbelianGalois ℚ E)
    (f : (E' ≃ₐ[K] E') →* Gal(E/ℚ))
    (hnat :
      letI : NumberField E' := hE'
      letI : NumberField E := hE
      letI : IsAbelianGalois ℚ E := hAbelian
      f.comp (globalArtinMonoidHomOfNumberField K E' hE') =
        (globalArtinMonoidHom (K := ℚ) (L := E)).comp
          (IdeleGroup.norm ℚ K)) :
    letI : NumberField E' := hE'
    letI : NumberField E := hE
    letI : IsAbelianGalois ℚ E := hAbelian
    {x : Gal(E / ℚ) × Gal(E / ℚ) × Gal(E / ℚ) //
      x.1 = x.2.1 ∧ x.2.1 = x.2.2} := by
  letI : NumberField E' := hE'
  letI : NumberField E := hE
  letI : IsAbelianGalois ℚ E := hAbelian
  let relativeData :=
    compRestrictNormalHomInfiniteGlobalArtinNaturalityDataOfNumberField
      K Ω a E' hE' f
      ((globalArtinMonoidHom (K := ℚ) (L := E)).comp
        (IdeleGroup.norm ℚ K))
      hnat
  have hcomp :
      ((globalArtinMonoidHom (K := ℚ) (L := E)).comp
        (IdeleGroup.norm ℚ K)) a =
        globalArtinMonoidHom (K := ℚ) (L := E)
          (IdeleGroup.norm ℚ K a) :=
    rfl
  exact
    ⟨(relativeData.1,
        ((globalArtinMonoidHom (K := ℚ) (L := E)).comp
          (IdeleGroup.norm ℚ K)) a,
        AlgEquiv.restrictNormalHom E
          (rationalCyclotomicZHatGlobalArtin
            (IdeleGroup.norm ℚ K a))),
      relativeData.2,
      hcomp.trans
        (restrictNormalHom_rationalCyclotomicZHatGlobalArtin_of_structures
          (IdeleGroup.norm ℚ K a) E hE hAbelian).symm⟩

theorem rationalCyclotomicZHatGlobalArtin_denseRange :
    DenseRange rationalCyclotomicZHatGlobalArtin

theorem
    rationalCyclotomicZHatGlobalArtin_rationalPositiveArchimedeanIdele
    (r : ℝ≥0ˣ) :
    rationalCyclotomicZHatGlobalArtin
        (rationalPositiveArchimedeanIdele r) =
      1

theorem
    exists_normOneIdele_same_rationalCyclotomicZHatGlobalArtin
    (a : IdeleGroup ℚ) :
    ∃ b : IdeleGroup.normOneSubgroup (K := ℚ),
      rationalCyclotomicZHatGlobalArtin b =
        rationalCyclotomicZHatGlobalArtin a

theorem rationalCyclotomicZHatGlobalArtin_normOne_denseRange :
    DenseRange
      (fun b : IdeleGroup.normOneSubgroup (K := ℚ) =>
        rationalCyclotomicZHatGlobalArtin b) := by
  apply rationalCyclotomicZHatGlobalArtin_denseRange.mono
  rintro σ ⟨a, rfl⟩
  obtain ⟨b, hb⟩ :=
    exists_normOneIdele_same_rationalCyclotomicZHatGlobalArtin a
  exact ⟨b, hb⟩