RayClassSubgroupEmbedding.lean

theorem subgroupArtin_prime_eq_arithmeticPrimeArtin
    {K : Type} [Field K] [NumberField K]
    {m : RayClassModulus K} {H : Subgroup (RayClassGroup m)}
    (R : RayClassSubgroupRealization K m H)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    R.artin (rayClassOfFinitePrime m v hv) =
      GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := R.extension) v

theorem subgroupRealization_mem_norm_range_iff
    {K : Type} [Field K] [NumberField K]
    {m : RayClassModulus K} {H : Subgroup (RayClassGroup m)}
    (R : RayClassSubgroupRealization K m H)
    (x : IdeleClassGroup K) :
    x ∈ (_root_.ideleClassNorm K R.extension).range ↔
      (GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele K m).symm
        (QuotientGroup.mk'
          (GlobalClassFieldComparison.rayClassModulusToOriginal K m).congruenceSubgroup
          x) ∈ H

theorem arithmeticPrimeArtin_restrict_tower
    {K E L : Type}
    [Field K] [NumberField K]
    [Field E] [NumberField E]
    [Field L] [NumberField L]
    [Algebra K E] [Algebra E L] [Algebra K L] [IsScalarTower K E L]
    [IsAbelianGalois K E] [IsAbelianGalois K L]
    (v : HeightOneSpectrum (𝓞 K)) :
    AlgEquiv.restrictNormalHom E
        (GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
          (K := K) (L := L) v) =
      GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := E) v

theorem exists_rayClassSubgroupEmbedding_artinNaturality
    (K : Type) [Field K] [NumberField K]
    (m : RayClassModulus K)
    {H J : Subgroup (RayClassGroup m)} (hHJ : H ≤ J)
    (RH : RayClassSubgroupRealization K m H)
    (RJ : RayClassSubgroupRealization K m J) :
    ∃ f : RJ.extension →ₐ[K] RH.extension,
      ∀ (x : RayClassGroup m) (y : RJ.extension),
        RH.artin x (f y) = f (RJ.artin x y)