PublicRayClassComparison.lean

def rayClassModulusToOriginal
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) : RayClass.Modulus K where
  finitePart := m.finitePart
  infinitePart := m.infinitePart

theorem principalIdele_mem_infinitePositiveSubgroup_iff
    (K : Type u) [Field K] [NumberField K] (x : Kˣ)
    (v : {v : InfinitePlace K // v.IsReal}) :
    IdeleGroup.infiniteComponent v.1 (IdeleGroup.principalIdele K x) ∈
        RayClass.infinitePositiveSubgroup v.1 ↔
      0 < v.1.embedding_of_isReal v.2 (x : K)

theorem principalIdele_mem_primeTo_iff_isRayCongruent
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) (x : Kˣ) :
    IdeleGroup.principalIdele K x ∈
        RayClass.idelePrimeToModulusSubgroup
          (rayClassModulusToOriginal K m) ↔
      IsRayCongruent m x

theorem principalIdele_mem_narrowPrimeTo_iff_isRayCongruent
    (K : Type u) [Field K] [NumberField K] (x : Kˣ) :
    IdeleGroup.principalIdele K x ∈
        RayClass.idelePrimeToModulusSubgroup
          (RayClass.Modulus.narrowOfFinite (0 : RayClass.FiniteModulus K)) ↔
      IsRayCongruent (narrowRayClassModulus K) x

theorem rayPrincipalIdealSubgroup_eq
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) :
    rayPrincipalIdealSubgroupInPrimeTo m =
      RayClass.principalRayIdealSubgroup
        (rayClassModulusToOriginal K m)

theorem narrowRayPrincipalIdealSubgroup_eq
    (K : Type u) [Field K] [NumberField K] :
    rayPrincipalIdealSubgroupInPrimeTo (narrowRayClassModulus K) =
      RayClass.principalRayIdealSubgroup
        (RayClass.Modulus.narrowOfFinite (0 : RayClass.FiniteModulus K))

def rayClassGroupEquivOriginal
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) :
    RayClassGroup m ≃*
      RayClass.IdealRayClassGroup (rayClassModulusToOriginal K m)

theorem rayClassGroupEquivOriginal_prime
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    rayClassGroupEquivOriginal K m (rayClassOfFinitePrime m v hv) =
      QuotientGroup.mk'
        (RayClass.principalRayIdealSubgroup (rayClassModulusToOriginal K m))
        (RayClass.primeToModulusIdeal
          (rayClassModulusToOriginal K m) v hv)

def rayClassGroupEquivOriginalIdele
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) :
    RayClassGroup m ≃*
      RayClass.RayClassGroup (rayClassModulusToOriginal K m)

theorem rayClassGroupEquivOriginalIdele_prime
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    rayClassGroupEquivOriginalIdele K m (rayClassOfFinitePrime m v hv) =
      QuotientGroup.mk'
        (RayClass.Modulus.congruenceSubgroup (rayClassModulusToOriginal K m))
        (QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
          (IdeleGroup.finitePrimeIdele v))

def narrowRayClassGroupEquivNarrowClassGroup
    (K : Type) [Field K] [NumberField K] :
    RayClassGroup (narrowRayClassModulus K) ≃*
      RayClass.NarrowClassGroup K

theorem rayClassField_normSubgroup
    (K : Type) [Field K] [NumberField K]
    (m : RayClass.Modulus K) :
    (_root_.ideleClassNorm K
      (GlobalClassFieldTheory.GlobalClassFields.rayClassField K m)).range =
      RayClass.Modulus.congruenceSubgroup m

theorem unramifiedOutsideModulus_of_definingModulus
    (K E : Type) [Field K] [NumberField K]
    [Field E] [NumberField E] [Algebra K E]
    [FiniteDimensional K E] [IsAbelianGalois K E]
    (m : RayClassModulus K)
    (hm : RayClass.Modulus.congruenceSubgroup
        (rayClassModulusToOriginal K m) ≤
          (_root_.ideleClassNorm K E).range) :
    IsUnramifiedOutsideModulus K E m

theorem rayClassField_unramifiedOutsideModulus
    (K : Type) [Field K] [NumberField K]
    (m : RayClassModulus K) :
    IsUnramifiedOutsideModulus K
      (GlobalClassFieldTheory.GlobalClassFields.rayClassField K
        (rayClassModulusToOriginal K m)) m

theorem rayClassField_reciprocity
    (K : Type) [Field K] [NumberField K]
    (m : RayClass.Modulus K) :
    Nonempty
      ((GlobalClassFieldTheory.GlobalClassFields.rayClassField K m ≃ₐ[K]
          GlobalClassFieldTheory.GlobalClassFields.rayClassField K m) ≃*
        RayClass.RayClassGroup m)

theorem rayClassField_degree
    (K : Type) [Field K] [NumberField K]
    (m : RayClass.Modulus K) :
    Module.finrank K
        (GlobalClassFieldTheory.GlobalClassFields.rayClassField K m) =
      Nat.card (RayClass.RayClassGroup m)

theorem embedsInRayClassField_iff_conductor_le
    {K : Type} [Field K] [NumberField K]
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
    [IsAbelianGalois K L]
    (m : RayClass.Modulus K) :
    Nonempty
        (L →ₐ[K]
          GlobalClassFieldTheory.GlobalClassFields.rayClassField K m) ↔
      (GlobalClassFieldTheory.GlobalClassFields.ideleClassNormConductorialSubgroup
          (K := K) (L := L)).fullConductor ≤ m

theorem rayClassSubgroup_existence
    (K : Type) [Field K] [NumberField K]
    (m : RayClassModulus K) (H : Subgroup (RayClassGroup m)) :
    Nonempty (RayClassSubgroupRealization K m H)

theorem normFullConductor_isAbelianConductor
    (K : Type) [Field K] [NumberField K]
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [IsAbelianGalois K L] :
    IsAbelianConductor K L
      { finitePart :=
          (GlobalClassFieldTheory.GlobalClassFields.ideleClassNormConductorialSubgroup
            (K := K) (L := L)).fullConductor.finitePart
        infinitePart :=
          (GlobalClassFieldTheory.GlobalClassFields.ideleClassNormConductorialSubgroup
            (K := K) (L := L)).fullConductor.infinitePart }