InfiniteGlobalArtinSurjectivity.lean

def numberFieldPositiveArchimedeanIdele
    (K : Type) [Field K] [NumberField K] :
    ℝ≥0ˣ →* IdeleGroup K

theorem numberFieldPositiveArchimedeanIdele_finiteComponent
    (r : ℝ≥0ˣ)
    (v : HeightOneSpectrum (𝓞 K)) :
    IdeleGroup.finiteComponent v
        (numberFieldPositiveArchimedeanIdele K r) =
      1

theorem numberFieldPositiveArchimedeanIdele_infiniteComponent_mem_positive
    (r : ℝ≥0ˣ) (v : InfinitePlace K) :
    IdeleGroup.infiniteComponent v
        (numberFieldPositiveArchimedeanIdele K r) ∈
      RayClass.infinitePositiveSubgroup v

theorem numberFieldPositiveArchimedeanIdele_absoluteNorm
    (r : ℝ≥0ˣ) :
    IdeleGroup.absoluteNorm
        (numberFieldPositiveArchimedeanIdele K r) =
      r⁻¹

theorem globalArtinMonoidHom_positiveArchimedeanSection
    {L : Type}
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
    (r : ℝ≥0ˣ) :
    globalArtinMonoidHom
        (K := K) (L := L)
        (IdeleGroup.positiveArchimedeanSection K r) =
      1

theorem continuousMulEquivToLimit_infiniteGlobalArtinMonoidHom_apply'
    {K Ω : Type}
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K) :
    InfiniteGalois.continuousMulEquivToLimit K Ω
        (infiniteGlobalArtinMonoidHom K Ω a) =
      infiniteGlobalArtinToLimit K Ω a

theorem infiniteGlobalArtinMonoidHom_positiveArchimedeanSection
    (K Ω : Type)
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (r : ℝ≥0ˣ) :
    infiniteGlobalArtinMonoidHom K Ω
        (IdeleGroup.positiveArchimedeanSection K r) =
      1

theorem infiniteGlobalArtinMonoidHom_numberFieldPositiveArchimedeanIdele
    (K Ω : Type)
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (r : ℝ≥0ˣ) :
    infiniteGlobalArtinMonoidHom K Ω
        (numberFieldPositiveArchimedeanIdele K r) =
      1

theorem exists_normOneIdele_same_infiniteGlobalArtin
    (K Ω : Type)
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
    (a : IdeleGroup K) :
    ∃ b : IdeleGroup.normOneSubgroup (K := K),
      infiniteGlobalArtinMonoidHom K Ω b =
        infiniteGlobalArtinMonoidHom K Ω a

theorem
    infiniteGlobalIdeleClassArtinContinuousMonoidHom_normOne_denseRange
    (K Ω : Type)
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω] :
    DenseRange
      (fun c : IdeleClassGroup.normOneSubgroup (K := K) =>
        infiniteGlobalIdeleClassArtinContinuousMonoidHom
          (K := K) (Ω := Ω) (c : IdeleClassGroup K)) := by
  apply
    (infiniteGlobalIdeleClassArtinContinuousMonoidHom_denseRange
      (K := K) (Ω := Ω)).mono
  rintro σ ⟨c, rfl⟩
  obtain ⟨a, rfl⟩ :=
    QuotientGroup.mk'_surjective
      (IdeleGroup.principalSubgroup K) c
  obtain ⟨b, hb⟩ :=
    exists_normOneIdele_same_infiniteGlobalArtin K Ω a
  let d : IdeleClassGroup.normOneSubgroup (K := K) :=
    ⟨QuotientGroup.mk'
        (IdeleGroup.principalSubgroup K)
        (b : IdeleGroup K),
      (IdeleClassGroup.mk_mem_normOneSubgroup_iff
        (b : IdeleGroup K)).2 b.2⟩
  refine ⟨d, ?_⟩
  change
    infiniteGlobalIdeleClassArtinMonoidHom
        (K := K) (Ω := Ω)
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K)
          (b : IdeleGroup K)) =
      infiniteGlobalIdeleClassArtinMonoidHom
        (K := K) (Ω := Ω)
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K) a)
  rw [infiniteGlobalIdeleClassArtinMonoidHom_mk,
    infiniteGlobalIdeleClassArtinMonoidHom_mk]
  exact hb

theorem
    infiniteGlobalIdeleClassArtinContinuousMonoidHom_normOne_surjective
    (K Ω : Type)
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω] :
    Function.Surjective
      (fun c : IdeleClassGroup.normOneSubgroup (K := K) =>
        infiniteGlobalIdeleClassArtinContinuousMonoidHom
          (K := K) (Ω := Ω) (c : IdeleClassGroup K)) := by
  let f :=
    fun c : IdeleClassGroup.normOneSubgroup (K := K) =>
      infiniteGlobalIdeleClassArtinContinuousMonoidHom
        (K := K) (Ω := Ω) (c : IdeleClassGroup K)
  have hf : Continuous f := by
    exact
      (infiniteGlobalIdeleClassArtinContinuousMonoidHom
        (K := K) (Ω := Ω)).continuous_toFun.comp
          continuous_subtype_val
  have hclosed : IsClosed (Set.range f) :=
    (isCompact_range hf).isClosed
  have hdense : DenseRange f := by
    simpa only [f] using
      (infiniteGlobalIdeleClassArtinContinuousMonoidHom_normOne_denseRange
        K Ω)
  intro σ
  have hσ : σ ∈ closure (Set.range f) := by
    rw [hdense.closure_range]
    trivial
  rwa [hclosed.closure_eq] at hσ

theorem infiniteGlobalIdeleClassArtinContinuousMonoidHom_surjective
    (K Ω : Type)
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω] :
    Function.Surjective
      (infiniteGlobalIdeleClassArtinContinuousMonoidHom
        (K := K) (Ω := Ω))

theorem infiniteGlobalArtinMonoidHom_surjective
    (K Ω : Type)
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω] :
    Function.Surjective
      (infiniteGlobalArtinMonoidHom K Ω)