noncomputable def ArtinSymbol (K L : Type v) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (𝔔 : Ideal (NumberField.RingOfIntegers L)) [𝔔.IsPrime] [Finite (NumberField.RingOfIntegers L ⧸ 𝔔)] : Gal(L/K)

theorem ArtinSymbol.isArithFrob (K L : Type v) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (𝔔 : Ideal (NumberField.RingOfIntegers L)) [𝔔.IsPrime] [Finite (NumberField.RingOfIntegers L ⧸ 𝔔)] : IsArithFrobAt (NumberField.RingOfIntegers K) (ArtinSymbol K L 𝔔) 𝔔

structure GlobalCFT.IsCongruenceSubgroup (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) : Prop

• contains_ray : RayClassField.RayGroup K 𝔪 ≤ 𝒞

theorem GlobalCFT.FracIdealsCoprime_subgroup_le (K : Type u) [Field K] [NumberField K] (𝔪 𝔫 : RayClassField.Modulus K) (h : 𝔪.dvd 𝔫) : RayClassField.FracIdealsCoprime_subgroup K 𝔫 ≤ RayClassField.FracIdealsCoprime_subgroup K 𝔪

noncomputable def GlobalCFT.FracIdealsCoprime.inclusion (K : Type u) [Field K] [NumberField K] (𝔪 𝔫 : RayClassField.Modulus K) (h : 𝔪.dvd 𝔫) : RayClassField.FracIdealsCoprime K 𝔫 →* RayClassField.FracIdealsCoprime K 𝔪

theorem GlobalCFT.IsRayGenerator_inclusion (K : Type u) [Field K] [NumberField K] (𝔪 𝔫 : RayClassField.Modulus K) (h : 𝔪.dvd 𝔫) (I : RayClassField.FracIdealsCoprime K 𝔫) (hI : RayClassField.IsRayGenerator 𝔫 I) : RayClassField.IsRayGenerator 𝔪 ((Subgroup.inclusion ⋯) I)

theorem GlobalCFT.RayGroup.inclusion_le (K : Type u) [Field K] [NumberField K] (𝔪 𝔫 : RayClassField.Modulus K) (h : 𝔪.dvd 𝔫) (x : RayClassField.FracIdealsCoprime K 𝔫) : x ∈ RayClassField.RayGroup K 𝔫 → (FracIdealsCoprime.inclusion K 𝔪 𝔫 h) x ∈ RayClassField.RayGroup K 𝔪

def GlobalCFT.CongruenceSubgroupEquiv (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : RayClassField.Modulus K) (𝒞₁ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₁)) (𝒞₂ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₂)) : Prop

theorem GlobalCFT.congruenceSubgroupEquiv_refl (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) : CongruenceSubgroupEquiv K 𝔪 𝔪 𝒞 𝒞

theorem GlobalCFT.congruenceSubgroupEquiv_symm (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : RayClassField.Modulus K) (𝒞₁ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₁)) (𝒞₂ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₂)) (h : CongruenceSubgroupEquiv K 𝔪₁ 𝔪₂ 𝒞₁ 𝒞₂) : CongruenceSubgroupEquiv K 𝔪₂ 𝔪₁ 𝒞₂ 𝒞₁

theorem GlobalCFT.FracIdealsCoprime.inclusion_comp (K : Type u) [Field K] [NumberField K] (𝔪 𝔫 𝔭 : RayClassField.Modulus K) (h₁ : 𝔪.dvd 𝔫) (h₂ : 𝔫.dvd 𝔭) (h₃ : 𝔪.dvd 𝔭) (x : RayClassField.FracIdealsCoprime K 𝔭) : (inclusion K 𝔪 𝔫 h₁) ((inclusion K 𝔫 𝔭 h₂) x) = (inclusion K 𝔪 𝔭 h₃) x

theorem GlobalCFT.FracIdealsCoprime.exists_ray_mul_coprime (K : Type u) [Field K] [NumberField K] (𝔪 𝔫 : RayClassField.Modulus K) (h : 𝔪.dvd 𝔫) (x : RayClassField.FracIdealsCoprime K 𝔪) : ∃ r ∈ RayClassField.RayGroup K 𝔪, ↑(x * r⁻¹) ∈ RayClassField.FracIdealsCoprime_subgroup K 𝔫

theorem GlobalCFT.FracIdealsCoprime.approx_theorem (K : Type u) [Field K] [NumberField K] (𝔪 𝔫 : RayClassField.Modulus K) (h : 𝔪.dvd 𝔫) (x : RayClassField.FracIdealsCoprime K 𝔪) : ∃ (y : RayClassField.FracIdealsCoprime K 𝔫), ∃ r ∈ RayClassField.RayGroup K 𝔪, x = (inclusion K 𝔪 𝔫 h) y * r

theorem GlobalCFT.FracIdealsCoprime.inclusion_mk_surjective (K : Type u) [Field K] [NumberField K] (𝔪 𝔫 : RayClassField.Modulus K) (h : 𝔪.dvd 𝔫) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) [𝒞.Normal] (hCong : IsCongruenceSubgroup K 𝔪 𝒞) : Function.Surjective ⇑((QuotientGroup.mk' 𝒞).comp (inclusion K 𝔪 𝔫 h))

theorem GlobalCFT.congruenceSubgroupEquiv_trans (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ 𝔪₃ : RayClassField.Modulus K) (𝒞₁ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₁)) (𝒞₂ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₂)) (𝒞₃ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₃)) (h₁₂ : CongruenceSubgroupEquiv K 𝔪₁ 𝔪₂ 𝒞₁ 𝒞₂) (h₂₃ : CongruenceSubgroupEquiv K 𝔪₂ 𝔪₃ 𝒞₂ 𝒞₃) : CongruenceSubgroupEquiv K 𝔪₁ 𝔪₃ 𝒞₁ 𝒞₃

noncomputable def GlobalCFT.proposition_22_4_iso_aux (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : RayClassField.Modulus K) (𝒞₁ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₁)) (𝒞₂ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₂)) (hCong₁ : IsCongruenceSubgroup K 𝔪₁ 𝒞₁) (hCong₂ : IsCongruenceSubgroup K 𝔪₂ 𝒞₂) (𝔫 : RayClassField.Modulus K) (h𝔪₁ : 𝔪₁.dvd 𝔫) (h𝔪₂ : 𝔪₂.dvd 𝔫) (heq : Subgroup.comap (FracIdealsCoprime.inclusion K 𝔪₁ 𝔫 h𝔪₁) 𝒞₁ = Subgroup.comap (FracIdealsCoprime.inclusion K 𝔪₂ 𝔫 h𝔪₂) 𝒞₂) : RayClassField.FracIdealsCoprime K 𝔪₁ ⧸ 𝒞₁ ≃* RayClassField.FracIdealsCoprime K 𝔪₂ ⧸ 𝒞₂

noncomputable def GlobalCFT.proposition_22_4_iso (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : RayClassField.Modulus K) (𝒞₁ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₁)) (𝒞₂ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₂)) (hCong₁ : IsCongruenceSubgroup K 𝔪₁ 𝒞₁) (hCong₂ : IsCongruenceSubgroup K 𝔪₂ 𝒞₂) (h : CongruenceSubgroupEquiv K 𝔪₁ 𝔪₂ 𝒞₁ 𝒞₂) : RayClassField.FracIdealsCoprime K 𝔪₁ ⧸ 𝒞₁ ≃* RayClassField.FracIdealsCoprime K 𝔪₂ ⧸ 𝒞₂

theorem GlobalCFT.lemma_22_5 (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : RayClassField.Modulus K) (h_dvd : 𝔪₂.dvd 𝔪₁) (𝒞₁ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₁)) (h_cong : IsCongruenceSubgroup K 𝔪₁ 𝒞₁) : (∃ (𝒞₂ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₂)), IsCongruenceSubgroup K 𝔪₂ 𝒞₂ ∧ CongruenceSubgroupEquiv K 𝔪₁ 𝔪₂ 𝒞₁ 𝒞₂) ↔ ∀ (x : RayClassField.FracIdealsCoprime K 𝔪₁), (FracIdealsCoprime.inclusion K 𝔪₂ 𝔪₁ h_dvd) x ∈ RayClassField.RayGroup K 𝔪₂ → x ∈ 𝒞₁

theorem GlobalCFT.FracIdealsCoprime.subtype_inclusion (K : Type u) [Field K] [NumberField K] (𝔪 𝔫 : RayClassField.Modulus K) (h : 𝔪.dvd 𝔫) (x : RayClassField.FracIdealsCoprime K 𝔫) : (RayClassField.FracIdealsCoprime_subgroup K 𝔪).subtype ((inclusion K 𝔪 𝔫 h) x) = (RayClassField.FracIdealsCoprime_subgroup K 𝔫).subtype x

theorem GlobalCFT.mem_comap_inclusion_iff_mem_toAmbientSubgroup (K : Type u) [Field K] [NumberField K] (𝔪 𝔫 : RayClassField.Modulus K) (h : 𝔪.dvd 𝔫) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (x : RayClassField.FracIdealsCoprime K 𝔫) : x ∈ Subgroup.comap (FracIdealsCoprime.inclusion K 𝔪 𝔫 h) 𝒞 ↔ (RayClassField.FracIdealsCoprime_subgroup K 𝔫).subtype x ∈ Subgroup.map (RayClassField.FracIdealsCoprime_subgroup K 𝔪).subtype 𝒞

theorem GlobalCFT.isEquiv_to_congruenceSubgroupEquiv (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : RayClassField.Modulus K) (𝒞₁ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₁)) (𝒞₂ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₂)) (h₁ : IsCongruenceSubgroup K 𝔪₁ 𝒞₁) (h₂ : IsCongruenceSubgroup K 𝔪₂ 𝒞₂) (h_isEquiv : { modulus := 𝔪₁, subgroup := 𝒞₁, ray_le := ⋯ }.IsEquiv { modulus := 𝔪₂, subgroup := 𝒞₂, ray_le := ⋯ }) : CongruenceSubgroupEquiv K 𝔪₁ 𝔪₂ 𝒞₁ 𝒞₂

theorem GlobalCFT.isEquiv_of_dvd_comap (K : Type u) [Field K] [NumberField K] (𝔪 𝔫 : RayClassField.Modulus K) (hdvd : 𝔪.dvd 𝔫) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (𝒞_𝔫 : Subgroup (RayClassField.FracIdealsCoprime K 𝔫)) (h_cong_𝔫 : IsCongruenceSubgroup K 𝔫 𝒞_𝔫) (h_eq : 𝒞_𝔫 = Subgroup.comap (FracIdealsCoprime.inclusion K 𝔪 𝔫 hdvd) 𝒞) : { modulus := 𝔪, subgroup := 𝒞, ray_le := ⋯ }.IsEquiv { modulus := 𝔫, subgroup := 𝒞_𝔫, ray_le := ⋯ }

theorem GlobalCFT.congruenceSubgroupEquiv_to_isEquiv (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : RayClassField.Modulus K) (𝒞₁ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₁)) (𝒞₂ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₂)) (h₁ : IsCongruenceSubgroup K 𝔪₁ 𝒞₁) (h₂ : IsCongruenceSubgroup K 𝔪₂ 𝒞₂) (h_equiv : CongruenceSubgroupEquiv K 𝔪₁ 𝔪₂ 𝒞₁ 𝒞₂) : { modulus := 𝔪₁, subgroup := 𝒞₁, ray_le := ⋯ }.IsEquiv { modulus := 𝔪₂, subgroup := 𝒞₂, ray_le := ⋯ }

theorem GlobalCFT.proposition_22_6 (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : RayClassField.Modulus K) (𝒞₁ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₁)) (𝒞₂ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₂)) (h₁ : IsCongruenceSubgroup K 𝔪₁ 𝒞₁) (h₂ : IsCongruenceSubgroup K 𝔪₂ 𝒞₂) (h_equiv : CongruenceSubgroupEquiv K 𝔪₁ 𝔪₂ 𝒞₁ 𝒞₂) : ∃ (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K (𝔪₁.gcd 𝔪₂))), IsCongruenceSubgroup K (𝔪₁.gcd 𝔪₂) 𝒞 ∧ CongruenceSubgroupEquiv K 𝔪₁ (𝔪₁.gcd 𝔪₂) 𝒞₁ 𝒞 ∧ CongruenceSubgroupEquiv K 𝔪₂ (𝔪₁.gcd 𝔪₂) 𝒞₂ 𝒞

theorem GlobalCFT.equiv_moduli_closed_under_gcd (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (𝔪₁ 𝔪₂ : RayClassField.Modulus K) (h₁ : ∃ (𝒞₁ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₁)), IsCongruenceSubgroup K 𝔪₁ 𝒞₁ ∧ CongruenceSubgroupEquiv K 𝔪 𝔪₁ 𝒞 𝒞₁) (h₂ : ∃ (𝒞₂ : Subgroup (RayClassField.FracIdealsCoprime K 𝔪₂)), IsCongruenceSubgroup K 𝔪₂ 𝒞₂ ∧ CongruenceSubgroupEquiv K 𝔪 𝔪₂ 𝒞 𝒞₂) : ∃ (𝒞g : Subgroup (RayClassField.FracIdealsCoprime K (𝔪₁.gcd 𝔪₂))), IsCongruenceSubgroup K (𝔪₁.gcd 𝔪₂) 𝒞g ∧ CongruenceSubgroupEquiv K 𝔪 (𝔪₁.gcd 𝔪₂) 𝒞 𝒞g

theorem GlobalCFT.gcd_weight_lt_of_not_dvd {K : Type u} [Field K] [NumberField K] {𝔪₁ 𝔪₂ : RayClassField.Modulus K} (h : ¬𝔪₁.dvd 𝔪₂) : (𝔪₁.gcd 𝔪₂).weight < 𝔪₁.weight

theorem GlobalCFT.exists_minimal_equiv_modulus (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) : ∃ (𝔠 : RayClassField.Modulus K), (∃ (𝒞₀ : Subgroup (RayClassField.FracIdealsCoprime K 𝔠)), IsCongruenceSubgroup K 𝔠 𝒞₀ ∧ CongruenceSubgroupEquiv K 𝔪 𝔠 𝒞 𝒞₀) ∧ ∀ (𝔫 : RayClassField.Modulus K), (∃ (𝒟 : Subgroup (RayClassField.FracIdealsCoprime K 𝔫)), IsCongruenceSubgroup K 𝔫 𝒟 ∧ CongruenceSubgroupEquiv K 𝔪 𝔫 𝒞 𝒟) → 𝔠.dvd 𝔫

theorem GlobalCFT.corollary_22_7 (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) : ∃! 𝔠 : RayClassField.Modulus K, (∃ (𝒞₀ : Subgroup (RayClassField.FracIdealsCoprime K 𝔠)), IsCongruenceSubgroup K 𝔠 𝒞₀ ∧ CongruenceSubgroupEquiv K 𝔪 𝔠 𝒞 𝒞₀) ∧ ∀ (𝔫 : RayClassField.Modulus K), (∃ (𝒟 : Subgroup (RayClassField.FracIdealsCoprime K 𝔫)), IsCongruenceSubgroup K 𝔫 𝒟 ∧ CongruenceSubgroupEquiv K 𝔪 𝔫 𝒞 𝒟) → 𝔠.dvd 𝔫

noncomputable def GlobalCFT.conductorOfCongruenceSubgroup (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) : RayClassField.Modulus K

def GlobalCFT.IsPrimitive (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) : Prop

@[reducible, inline]

abbrev GlobalCFT.RayClassCharacter (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) : Type u

noncomputable def GlobalCFT.RayClassGroup.mapOfDvd {K : Type u} [Field K] [NumberField K] {𝔪₁ 𝔪₂ : RayClassField.Modulus K} (h : 𝔪₁.dvd 𝔪₂) : RayClassField.RayClassGroup K 𝔪₂ →* RayClassField.RayClassGroup K 𝔪₁

def GlobalCFT.IsInducedBy (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : RayClassField.Modulus K) (h : 𝔪₁.dvd 𝔪₂) (χ₁ : RayClassCharacter K 𝔪₁) (χ₂ : RayClassCharacter K 𝔪₂) : Prop

def GlobalCFT.kernelCongruenceSubgroup (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (χ : RayClassCharacter K 𝔪) : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)

theorem GlobalCFT.kernelCongruenceSubgroup_isCong (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (χ : RayClassCharacter K 𝔪) : IsCongruenceSubgroup K 𝔪 (kernelCongruenceSubgroup K 𝔪 χ)

noncomputable def GlobalCFT.conductorOfRayClassCharacter (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (χ : RayClassCharacter K 𝔪) : RayClassField.Modulus K

theorem GlobalCFT.conductorOfRayClassCharacter_dvd (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (χ : RayClassCharacter K 𝔪) : (conductorOfRayClassCharacter K 𝔪 χ).dvd 𝔪

def GlobalCFT.IsRayClassCharacterPrincipal (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (χ : RayClassCharacter K 𝔪) : Prop

noncomputable def GlobalCFT.WeberLFunction (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (χ : RayClassCharacter K 𝔪) : ℂ → ℂ

noncomputable def GlobalCFT.rayClassHolomorphicPart (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (γ : RayClassField.RayClassGroup K 𝔪) : ℂ → ℂ

noncomputable def GlobalCFT.PrimeToFracIdealsCoprime (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝔭 : RayClassField.Prime' K) (h_coprime : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0) : RayClassField.FracIdealsCoprime K 𝔪

def GlobalCFT.primesInCongruenceSubgroup (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) : Set (RayClassField.Prime' K)

noncomputable def GlobalCFT.PrimitiveCharsContaining (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) : Type u

theorem GlobalCFT.IsCongruenceSubgroup.finiteIndex {K : Type u} [Field K] [NumberField K] {𝔪 : RayClassField.Modulus K} {𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)} (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) : 𝒞.FiniteIndex

@[implicit_reducible]

noncomputable instance GlobalCFT.instFintypePrimitiveCharsContaining (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) [𝒞.FiniteIndex] : Fintype (PrimitiveCharsContaining K 𝔪 𝒞)

noncomputable def GlobalCFT.toRayClassCharOfPrimitive (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (χ : PrimitiveCharsContaining K 𝔪 𝒞) : RayClassCharacter K 𝔪

opaque GlobalCFT.orderOfVanishingPrimitive (_K : Type u) [Field _K] [NumberField _K] (_𝔪 : RayClassField.Modulus _K) (_𝒞 : Subgroup (RayClassField.FracIdealsCoprime _K _𝔪)) (_χ : PrimitiveCharsContaining _K _𝔪 _𝒞) : ℕ

def GlobalCFT.isPrincipalPrimitive (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (χ : PrimitiveCharsContaining K 𝔪 𝒞) : Prop

@[implicit_reducible]

noncomputable instance GlobalCFT.instDecidableIsPrincipalPrimitive (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (χ : PrimitiveCharsContaining K 𝔪 𝒞) : Decidable (isPrincipalPrimitive K 𝔪 𝒞 χ)

def GlobalCFT.AllLValuesNonzero (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) : Prop

noncomputable def GlobalCFT.dirichletDensityCongruence (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (_h_cong : IsCongruenceSubgroup K 𝔪 𝒞) : ℚ

noncomputable def GlobalCFT.dirichletDensityCoset (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (I : RayClassField.FracIdealsCoprime K 𝔪) : ℚ

theorem GlobalCFT.congruenceSubgroup_index_pos (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) : 0 < 𝒞.index

theorem GlobalCFT.coset_nthPower_meromorphicOrder_eq (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (I : RayClassField.FracIdealsCoprime K 𝔪) [𝒞.FiniteIndex] : have S := {𝔭 : RayClassField.Prime' K | ∃ (h : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), ↑(PrimeToFracIdealsCoprime K 𝔪 𝔭 h) = ↑I}; have E := ∑ χ : PrimitiveCharsContaining K 𝔪 𝒞, if isPrincipalPrimitive K 𝔪 𝒞 χ then 0 else orderOfVanishingPrimitive K 𝔪 𝒞 χ; meromorphicOrderAt (RayClassField.partialDedekindZeta K S ^ 𝒞.index) 1 = ↑(-(1 - ↑E))

theorem GlobalCFT.coset_nthPower_poleOrder (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (I : RayClassField.FracIdealsCoprime K 𝔪) [𝒞.FiniteIndex] : have S := {𝔭 : RayClassField.Prime' K | ∃ (h : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), ↑(PrimeToFracIdealsCoprime K 𝔪 𝔭 h) = ↑I}; have E := ∑ χ : PrimitiveCharsContaining K 𝔪 𝒞, if isPrincipalPrimitive K 𝔪 𝒞 χ then 0 else orderOfVanishingPrimitive K 𝔪 𝒞 χ; RayClassField.HasMeromorphicContinuationWithPoleOrder (RayClassField.partialDedekindZeta K S ^ 𝒞.index) (1 - ↑E)

theorem GlobalCFT.hasPolarDensity_coset (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (I : RayClassField.FracIdealsCoprime K 𝔪) : RayClassField.HasPolarDensity K {𝔭 : RayClassField.Prime' K | ∃ (h : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), ↑(PrimeToFracIdealsCoprime K 𝔪 𝔭 h) = ↑I} (dirichletDensityCongruence K 𝔪 𝒞 h_cong)

theorem GlobalCFT.dirichletDensityCongruence_nonneg (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) : 0 ≤ dirichletDensityCongruence K 𝔪 𝒞 h_cong

theorem GlobalCFT.theorem_22_20 (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (n : ℕ) (hn : 𝒞.index = n) (hn_pos : 0 < n) : (AllLValuesNonzero K 𝔪 𝒞 → dirichletDensityCongruence K 𝔪 𝒞 h_cong = 1 / ↑n) ∧ (¬AllLValuesNonzero K 𝔪 𝒞 → dirichletDensityCongruence K 𝔪 𝒞 h_cong = 0)

theorem GlobalCFT.hasDirichletDensity_coset (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (I : RayClassField.FracIdealsCoprime K 𝔪) : RayClassField.HasDirichletDensity K {𝔭 : RayClassField.Prime' K | ∃ (h : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), ↑(PrimeToFracIdealsCoprime K 𝔪 𝔭 h) = ↑I} (dirichletDensityCongruence K 𝔪 𝒞 h_cong)

theorem GlobalCFT.dirichletDensity_coset_eq_some (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (I : RayClassField.FracIdealsCoprime K 𝔪) : RayClassField.DirichletDensity K {𝔭 : RayClassField.Prime' K | ∃ (h : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), ↑(PrimeToFracIdealsCoprime K 𝔪 𝔭 h) = ↑I} = some (dirichletDensityCongruence K 𝔪 𝒞 h_cong)

theorem GlobalCFT.characterOrthogonality_coset_density (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (I : RayClassField.FracIdealsCoprime K 𝔪) : dirichletDensityCoset K 𝔪 𝒞 h_cong I = dirichletDensityCongruence K 𝔪 𝒞 h_cong

theorem GlobalCFT.dirichletDensityCoset_eq_congruence (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (I : RayClassField.FracIdealsCoprime K 𝔪) : dirichletDensityCoset K 𝔪 𝒞 h_cong I = dirichletDensityCongruence K 𝔪 𝒞 h_cong

theorem GlobalCFT.proposition_22_21 (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (n : ℕ) (hn : 𝒞.index = n) (hn_pos : 0 < n) (I : RayClassField.FracIdealsCoprime K 𝔪) : (AllLValuesNonzero K 𝔪 𝒞 → dirichletDensityCoset K 𝔪 𝒞 h_cong I = 1 / ↑n) ∧ (¬AllLValuesNonzero K 𝔪 𝒞 → dirichletDensityCoset K 𝔪 𝒞 h_cong I = 0)

theorem GlobalCFT.dirichletDensity_coprime_primes_eq_one (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (_h_cong : IsCongruenceSubgroup K 𝔪 𝒞) : RayClassField.DirichletDensity K {𝔭 : RayClassField.Prime' K | ∃ (_ : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), True} = some 1

theorem GlobalCFT.summable_rpow_inv_absNorm_prime {K : Type u_1} [Field K] [NumberField K] (S : Set (RayClassField.Prime' K)) (s : ℝ) (hs : 1 < s) : Summable fun (𝔭 : ↑S) => ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)

theorem GlobalCFT.dirichletDensity_nfold_coset_additivity (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (n : ℕ) (hn : 𝒞.index = n) (hn_pos : 0 < n) (reps : Fin n → RayClassField.FracIdealsCoprime K 𝔪) (h_reps : Function.Injective fun (i : Fin n) => ↑(reps i)) (ρ : ℚ) (h_density : RayClassField.DirichletDensity K {𝔭 : RayClassField.Prime' K | ∃ (_ : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), True} = some ρ) : ρ = ∑ i : Fin n, dirichletDensityCoset K 𝔪 𝒞 h_cong (reps i)

theorem GlobalCFT.dirichletDensity_coset_partition_sum (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (n : ℕ) (hn : 𝒞.index = n) (hn_pos : 0 < n) (reps : Fin n → RayClassField.FracIdealsCoprime K 𝔪) (h_reps : Function.Injective fun (i : Fin n) => ↑(reps i)) : (RayClassField.DirichletDensity K {𝔭 : RayClassField.Prime' K | ∃ (_ : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), True}).getD 0 = ∑ i : Fin n, dirichletDensityCoset K 𝔪 𝒞 h_cong (reps i)

theorem GlobalCFT.density_cosets_sum_one (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (n : ℕ) (hn : 𝒞.index = n) (hn_pos : 0 < n) (reps : Fin n → RayClassField.FracIdealsCoprime K 𝔪) (h_reps : Function.Injective fun (i : Fin n) => ↑(reps i)) : ∑ i : Fin n, dirichletDensityCoset K 𝔪 𝒞 h_cong (reps i) = 1

theorem GlobalCFT.corollary_22_22 (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (n : ℕ) (hn : 𝒞.index = n) (hn_pos : 0 < n) (reps : Fin n → RayClassField.FracIdealsCoprime K 𝔪) (h_reps : Function.Injective fun (i : Fin n) => ↑(reps i)) : AllLValuesNonzero K 𝔪 𝒞 ∧ ∀ (I : RayClassField.FracIdealsCoprime K 𝔪), dirichletDensityCoset K 𝔪 𝒞 h_cong I = 1 / ↑n

theorem GlobalCFT.ps9_dirichletDensity_mono {K : Type u_1} [Field K] [NumberField K] {S T : Set (RayClassField.Prime' K)} {ρS ρT : ℚ} (hST : S ⊆ T) (hS : RayClassField.HasDirichletDensity K S ρS) (hT : RayClassField.HasDirichletDensity K T ρT) : ρS ≤ ρT

theorem GlobalCFT.dirichletDensity_le_of_PrimeSetLe {K : Type u} [Field K] [NumberField K] {S T : Set (RayClassField.Prime' K)} {ρS ρT : ℚ} (hle : RayClassField.PrimeSetLe S T) (hS_polar : RayClassField.PolarDensity K S = some ρS) (hT_dir : RayClassField.HasDirichletDensity K T ρT) : ρS ≤ ρT

theorem GlobalCFT.corollary_22_23 (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : IsCongruenceSubgroup K 𝔪 𝒞) (h_spl : RayClassField.PrimeSetLe (RayClassField.Spl K L) (primesInCongruenceSubgroup K 𝔪 𝒞)) : 𝒞.index ≤ Module.finrank K L

noncomputable def GlobalCFT.extensionAdmissibleModulus (K L : Type u) [Field K] [NumberField K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : RayClassField.Modulus K

noncomputable def GlobalCFT.extensionNormSubgroup (K L : Type u) [Field K] [NumberField K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : Subgroup (RayClassField.FracIdealsCoprime K (extensionAdmissibleModulus K L))

theorem GlobalCFT.extensionNormSubgroup_isCong (K L : Type u) [Field K] [NumberField K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : IsCongruenceSubgroup K (extensionAdmissibleModulus K L) (extensionNormSubgroup K L)

noncomputable def GlobalCFT.extensionConductor (K L : Type u) [Field K] [NumberField K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : RayClassField.Modulus K

def GlobalCFT.IsUnramifiedIn (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (𝔭 : RayClassField.Prime' K) : Prop

def GlobalCFT.IsTamelyRamifiedIn (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (𝔭 : RayClassField.Prime' K) : Prop

def GlobalCFT.IsWildlyRamifiedIn (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (𝔭 : RayClassField.Prime' K) : Prop

def GlobalCFT.IsTotallyRamifiedIn (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (𝔭 : RayClassField.Prime' K) : Prop

def GlobalCFT.IsTotallyTamelyRamified (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (𝔭 : RayClassField.Prime' K) : Prop

def GlobalCFT.IsTotallyWildlyRamified (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (𝔭 : RayClassField.Prime' K) : Prop

theorem GlobalCFT.extensionConductor_eq_zero_of_unramified (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔭 : RayClassField.Prime' K) (_h : IsUnramifiedIn K L 𝔭) : (extensionConductor K L).toFun (RayClassField.Place.finite 𝔭) = 0

theorem GlobalCFT.IsUnramifiedIn_of_extensionConductor_eq_zero (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔭 : RayClassField.Prime' K) (h : (extensionConductor K L).toFun (RayClassField.Place.finite 𝔭) = 0) : IsUnramifiedIn K L 𝔭

theorem GlobalCFT.proposition_22_25_unramified (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔭 : RayClassField.Prime' K) : (extensionConductor K L).toFun (RayClassField.Place.finite 𝔭) = 0 ↔ IsUnramifiedIn K L 𝔭

theorem GlobalCFT.proposition_22_25_tame (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔭 : RayClassField.Prime' K) : (extensionConductor K L).toFun (RayClassField.Place.finite 𝔭) = 1 ↔ IsTamelyRamifiedIn K L 𝔭 ∧ ¬IsUnramifiedIn K L 𝔭

theorem GlobalCFT.proposition_22_25_wild (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔭 : RayClassField.Prime' K) : 2 ≤ (extensionConductor K L).toFun (RayClassField.Place.finite 𝔭) ↔ IsWildlyRamifiedIn K L 𝔭

theorem GlobalCFT.extensionNormSubgroup_equiv_at_modulus (K L : Type u) [Field K] [NumberField K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔫 : RayClassField.Modulus K) : ∃ (𝒟 : Subgroup (RayClassField.FracIdealsCoprime K 𝔫)), IsCongruenceSubgroup K 𝔫 𝒟 ∧ CongruenceSubgroupEquiv K (extensionAdmissibleModulus K L) 𝔫 (extensionNormSubgroup K L) 𝒟

theorem GlobalCFT.extensionConductor_infinite_zero (K L : Type u) [Field K] [NumberField K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (w : NumberField.InfinitePlace K) : NumberField.InfinitePlace.IsUnramifiedIn L w → (extensionConductor K L).toFun (RayClassField.Place.infinite w) = 0

theorem GlobalCFT.extensionConductor_infinite_one (K L : Type u) [Field K] [NumberField K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (w : NumberField.InfinitePlace K) : ¬NumberField.InfinitePlace.IsUnramifiedIn L w → (extensionConductor K L).toFun (RayClassField.Place.infinite w) = 1

noncomputable def GlobalCFT.NormGroup (K L : Type u) [Field K] [NumberField K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔪 : RayClassField.Modulus K) : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)

theorem GlobalCFT.normGroup_isCongruenceSubgroup (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔪 : RayClassField.Modulus K) (h_cond : (extensionConductor K L).dvd 𝔪) : IsCongruenceSubgroup K 𝔪 (NormGroup K L 𝔪)

noncomputable def GlobalCFT.choosePrimeOverHOS (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔭 : RayClassField.Prime' K) : RayClassField.Prime' L

theorem GlobalCFT.choosePrimeOverHOS_lyingUnder (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔭 : RayClassField.Prime' K) : RayClassField.lyingUnder K L (choosePrimeOverHOS K L 𝔭) = 𝔭

theorem GlobalCFT.theorem_6_10_norm_prime (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (𝔮 : RayClassField.Prime' L) : (RayClassField.fracIdealNorm K L) (RayClassField.primeAsUnitFracIdeal L 𝔮) = RayClassField.primeAsUnitFracIdeal K (RayClassField.lyingUnder K L 𝔮) ^ RayClassField.inertiaDegree' K L 𝔮

theorem GlobalCFT.primeAbove_coprime_extendModulus (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (𝔪 : RayClassField.Modulus K) (𝔭 : RayClassField.Prime' K) (𝔮 : RayClassField.Prime' L) (h_over : RayClassField.lyingUnder K L 𝔮 = 𝔭) (h_coprime : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0) : (RayClassField.extendModulus K L 𝔪).toFun (RayClassField.Place.finite 𝔮) = 0

theorem GlobalCFT.splitsCompletely_inertiaDeg_eq_one (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (𝔭 : RayClassField.Prime' K) (𝔮 : RayClassField.Prime' L) (h_split : RayClassField.SplitsCompletely K L 𝔭) (h_over : RayClassField.lyingUnder K L 𝔮 = 𝔭) : RayClassField.inertiaDegree' K L 𝔮 = 1

theorem GlobalCFT.splitsCompletely_coprime_mem_normGroup (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔪 : RayClassField.Modulus K) (h_cond : (extensionConductor K L).dvd 𝔪) (𝔭 : RayClassField.Prime' K) (h_split : RayClassField.SplitsCompletely K L 𝔭) (h_coprime : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0) : PrimeToFracIdealsCoprime K 𝔪 𝔭 h_coprime ∈ NormGroup K L 𝔪

theorem GlobalCFT.proposition_22_28 (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔪 : RayClassField.Modulus K) (h_cond : (extensionConductor K L).dvd 𝔪) : RayClassField.PrimeSetLe (RayClassField.Spl K L) (primesInCongruenceSubgroup K 𝔪 (NormGroup K L 𝔪))

theorem GlobalCFT.theorem_22_29_norm_index_inequality (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔪 : RayClassField.Modulus K) (h_cond : (extensionConductor K L).dvd 𝔪) : (NormGroup K L 𝔪).index ≤ Module.finrank K L

theorem GlobalCFT.completeness_theorem (K L : Type u) [Field K] [NumberField K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔪 : RayClassField.Modulus K) : (extensionConductor K L).dvd 𝔪 ↔ ∃ (M : Type u) (x : Field M) (x_1 : NumberField M) (x_2 : Algebra K M) (_ : FiniteDimensional K M) (x_4 : KroneckerWeber.IsAbelianExtension K M), RayClassField.IsRayClassField K M 𝔪 ∧ Nonempty (L →ₐ[K] M)

structure GlobalCFT.IsHilbertClassField (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] : Prop

• finiteDimensional : FiniteDimensional K L
• everywhere_unramified (𝔭 : RayClassField.Prime' K) : IsUnramifiedIn K L 𝔭
• maximal (M : Type u) [Field M] [NumberField M] [Algebra K M] [KroneckerWeber.IsAbelianExtension K M] [FiniteDimensional K M] : (∀ (𝔭 : RayClassField.Prime' K), IsUnramifiedIn K M 𝔭) → Nonempty (M →ₐ[K] L)

theorem GlobalCFT.hilbertClassField_ker_eq_rayGroup (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] (hunram : ∀ (𝔭 : RayClassField.Prime' K), IsUnramifiedIn K L 𝔭) (hmax : ∀ (M : Type u) [inst : Field M] [inst_1 : NumberField M] [inst_2 : Algebra K M] [KroneckerWeber.IsAbelianExtension K M] [FiniteDimensional K M], (∀ (𝔭 : RayClassField.Prime' K), IsUnramifiedIn K M 𝔭) → Nonempty (M →ₐ[K] L)) : (RayClassField.ArtinMap K L RayClassField.Modulus.trivial).ker = RayClassField.RayGroup K RayClassField.Modulus.trivial

theorem GlobalCFT.hilbertClassField_maximal (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [KroneckerWeber.IsAbelianExtension K L] [KroneckerWeber.IsAbelianExtension K M] (hL : RayClassField.IsRayClassField K L RayClassField.Modulus.trivial) (hunramM : ∀ (𝔭 : RayClassField.Prime' K), IsUnramifiedIn K M 𝔭) : Nonempty (M →ₐ[K] L)

structure GlobalArtinMap (K : Type u_1) [Field K] [NumberField K] : Type (max (max (max u_1 (u_2 + 1)) (u_3 + 1)) (u_4 + 1))

• I : Type u_2
• instPreorder : Preorder self.I
• GalLK : self.I → Type u_3
• instFintype (i : self.I) : Fintype (self.GalLK i)
• instCommGroup (i : self.I) : CommGroup (self.GalLK i)
• restrictMap {i j : self.I} : i ≤ j → self.GalLK j →* self.GalLK i
• artinMap (i : self.I) : Ideles.IdeleGroup K →* self.GalLK i
• artinMap_compat {i j : self.I} (h : i ≤ j) (a : Ideles.IdeleGroup K) : (self.restrictMap h) ((self.artinMap j) a) = (self.artinMap i) a
• GalAb : Type u_4
• galAb_group : CommGroup self.GalAb
• galAb_topologicalSpace : TopologicalSpace self.GalAb
• galAb_topologicalGroup : IsTopologicalGroup self.GalAb
• galAb_compactSpace : CompactSpace self.GalAb
• artinHom : Ideles.IdeleGroup K →* self.GalAb
• artinHom_continuous : Continuous ⇑self.artinHom
• proj (i : self.I) : self.GalAb →* self.GalLK i
• artinMap_eq_proj (i : self.I) (a : Ideles.IdeleGroup K) : (self.artinMap i) a = (self.proj i) (self.artinHom a)
• artinMap_surjective (i : self.I) : Function.Surjective ⇑(self.artinMap i)
• proj_jointly_injective (g : self.GalAb) : (∀ (i : self.I), (self.proj i) g = 1) → g = 1
• proj_compat {i j : self.I} (h : i ≤ j) (g : self.GalAb) : (self.restrictMap h) ((self.proj j) g) = (self.proj i) g
• principalInKer : Ideles.principalIdeles K ≤ self.artinHom.ker
• normSubgroup (i : self.I) : Subgroup (Ideles.IdeleClassGroup K)
• normSubgroup_normal (i : self.I) : (self.normSubgroup i).Normal
• artinMapCK_surjective (i : self.I) : Function.Surjective ⇑((self.proj i).comp (QuotientGroup.lift (Ideles.principalIdeles K) self.artinHom ⋯))
• ker_eq_normSubgroup (i : self.I) : ((self.proj i).comp (QuotientGroup.lift (Ideles.principalIdeles K) self.artinHom ⋯)).ker = self.normSubgroup i

theorem GlobalArtinMap.normSubgroup_existence {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (H : Subgroup (Ideles.IdeleClassGroup K)) (hopen : IsOpen ↑H) (hfin : H.FiniteIndex) : ∃! i : θ.I, θ.normSubgroup i = H

theorem proposition_28_3 {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (θ' : Ideles.IdeleGroup K →* θ.GalAb) (hcompat : ∀ (i : θ.I) (a : Ideles.IdeleGroup K), (θ.proj i) (θ' a) = (θ.artinMap i) a) (a : Ideles.IdeleGroup K) : θ' a = θ.artinHom a

theorem theorem_28_4_principal_in_ker {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) : Ideles.principalIdeles K ≤ θ.artinHom.ker

noncomputable def GlobalArtinMap.artinHomCK {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) : Ideles.IdeleClassGroup K →* θ.GalAb

theorem GlobalArtinMap.artinHomCK_comp {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (a : Ideles.IdeleGroup K) : θ.artinHomCK ↑a = θ.artinHom a

noncomputable def GlobalArtinMap.normSubgroupCK {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (i : θ.I) : Subgroup (Ideles.IdeleClassGroup K)

instance GlobalArtinMap.normSubgroupCK_normal {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (i : θ.I) : (θ.normSubgroupCK i).Normal

noncomputable def GlobalArtinMap.artinMapCK {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (i : θ.I) : Ideles.IdeleClassGroup K →* θ.GalLK i

theorem theorem_28_4_ker_eq_norm {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (i : θ.I) : (θ.artinMapCK i).ker = θ.normSubgroupCK i

theorem theorem_28_4_iso {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (i : θ.I) : Nonempty (Ideles.IdeleClassGroup K ⧸ θ.normSubgroupCK i ≃* θ.GalLK i)

theorem theorem_28_6_global_existence {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (H : Subgroup (Ideles.IdeleClassGroup K)) (hopen : IsOpen ↑H) (hfin : H.FiniteIndex) : ∃! i : θ.I, θ.normSubgroupCK i = H

def IsConjugationStable {G : Type u_1} [Group G] (C : Set G) : Prop

noncomputable def FrobeniusConjClass (K L : Type w) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (𝔭 : RayClassField.Prime' K) : Set Gal(L/K)

theorem FrobeniusConjClass.nonempty (K L : Type w) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (𝔭 : RayClassField.Prime' K) (_h_unram : GlobalCFT.IsUnramifiedIn K L 𝔭) : (FrobeniusConjClass K L 𝔭).Nonempty

def primesWithFrobInSet (K L : Type w) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (C : Set Gal(L/K)) : Set (RayClassField.Prime' K)

theorem rayGroup_isCongruenceSubgroup (K : Type w) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) : GlobalCFT.IsCongruenceSubgroup K 𝔪 (RayClassField.RayGroup K 𝔪)

theorem rayGroup_index_eq_natCard (K : Type w) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) : (RayClassField.RayGroup K 𝔪).index = Nat.card (RayClassField.RayClassGroup K 𝔪)

theorem corollary_22_22_hasDirichletDensity {K : Type u_1} [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : GlobalCFT.IsCongruenceSubgroup K 𝔪 𝒞) (n : ℕ) (hn : 𝒞.index = n) (hn_pos : 0 < n) (I : RayClassField.FracIdealsCoprime K 𝔪) : RayClassField.HasDirichletDensity K {𝔭 : RayClassField.Prime' K | ∃ (h : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), ↑(GlobalCFT.PrimeToFracIdealsCoprime K 𝔪 𝔭 h) = ↑I} (1 / ↑n)

theorem proposition_28_10 (K : Type w) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (c : RayClassField.RayClassGroup K 𝔪) : RayClassField.DirichletDensity K {𝔭 : RayClassField.Prime' K | ∃ (h : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), ↑(GlobalCFT.PrimeToFracIdealsCoprime K 𝔪 𝔭 h) = c} = some (1 / ↑(Nat.card (RayClassField.RayClassGroup K 𝔪)))

noncomputable def liftToGalLE {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (σ : Gal(L/K)) : Gal(L/↥(IntermediateField.fixedField (Subgroup.zpowers σ)))

theorem abelianFrobenius_rayClass_density_bridge (E L : Type w) [Field E] [Field L] [NumberField E] [NumberField L] [Algebra E L] [IsGalois E L] [FiniteDimensional E L] (σ : Gal(L/E)) : RayClassField.HasDirichletDensity E (primesWithFrobInSet E L {σ}) (1 / ↑(Fintype.card Gal(L/E)))

theorem abelianDensity_fixedField (K L : Type w) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (σ : Gal(L/K)) : let E := IntermediateField.fixedField (Subgroup.zpowers σ); RayClassField.HasDirichletDensity (↥E) (primesWithFrobInSet (↥E) L {liftToGalLE σ}) (1 / ↑(orderOf σ))

theorem dirichletSeries_conjClass_comparison (K L : Type w) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (σ : Gal(L/K)) : let E := IntermediateField.fixedField (Subgroup.zpowers σ); RayClassField.HasDirichletDensity (↥E) (primesWithFrobInSet (↥E) L {liftToGalLE σ}) (1 / ↑(orderOf σ)) → RayClassField.HasDirichletDensity K (primesWithFrobInSet K L (ConjClasses.mk σ).carrier) (↑⋯.toFinset.card / (↑(Subgroup.zpowers σ).index * ↑(orderOf σ)))

theorem conjClass_density_intermediate (K L : Type w) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (σ : Gal(L/K)) : RayClassField.HasDirichletDensity K (primesWithFrobInSet K L (ConjClasses.mk σ).carrier) (↑⋯.toFinset.card / (↑(Subgroup.zpowers σ).index * ↑(orderOf σ)))

theorem conjClass_hasDirichletDensity (K L : Type w) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (σ : Gal(L/K)) : RayClassField.HasDirichletDensity K (primesWithFrobInSet K L (ConjClasses.mk σ).carrier) (↑⋯.toFinset.card / ↑(Fintype.card Gal(L/K)))

theorem dirichletDensity_disjoint_union (K L : Type w) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (A B : Set Gal(L/K)) (hA : IsConjugationStable A) (hB : IsConjugationStable B) (h_disj : Disjoint A B) (dA dB : ℚ) (hdA : RayClassField.HasDirichletDensity K (primesWithFrobInSet K L A) dA) (hdB : RayClassField.HasDirichletDensity K (primesWithFrobInSet K L B) dB) : RayClassField.HasDirichletDensity K (primesWithFrobInSet K L (A ∪ B)) (dA + dB)

theorem primesWithFrobInSet_empty_hasDensity_zero (K L : Type w) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : RayClassField.HasDirichletDensity K (primesWithFrobInSet K L ∅) 0

theorem conjClass_subset_of_mem_conjStable {G : Type u_1} [Group G] (C : Set G) (hC : IsConjugationStable C) (σ : G) (hσ : σ ∈ C) : (ConjClasses.mk σ).carrier ⊆ C

theorem conjStable_sdiff {G : Type u_1} [Group G] (C : Set G) (hC : IsConjugationStable C) (σ : G) : IsConjugationStable (C \ (ConjClasses.mk σ).carrier)

theorem theorem_28_9_chebotarev (K L : Type w) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (C : Set Gal(L/K)) (hC : IsConjugationStable C) (hC_finite : C.Finite) : RayClassField.DirichletDensity K (primesWithFrobInSet K L C) = some (↑hC_finite.toFinset.card / ↑(Fintype.card Gal(L/K)))

theorem corollary_28_11 (K L : Type w) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] (hcomm : ∀ (a b : Gal(L/K)), a * b = b * a) (σ : Gal(L/K)) : RayClassField.DirichletDensity K (primesWithFrobInSet K L {σ}) = some (1 / ↑(Fintype.card Gal(L/K)))

structure GlobalArtinFunctoriality {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (θK : GlobalArtinMap K) (θL : GlobalArtinMap L) : Type (max u_5 u_8)

• transfer : θL.GalAb →* θK.GalAb
• transfer_continuous : Continuous ⇑self.transfer
• artinMap_comm (a : Ideles.IdeleGroup L) : θK.artinHom ((ideleNorm K L) a) = self.transfer (θL.artinHom a)

def theorem_28_8_functoriality {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (θK : GlobalArtinMap K) (θL : GlobalArtinMap L) : GlobalArtinFunctoriality θK θL

def GlobalArtinMap.transferMap {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (θK : GlobalArtinMap K) (θL : GlobalArtinMap L) : θL.GalAb →* θK.GalAb

theorem theorem_28_8_comm {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (θK : GlobalArtinMap K) (θL : GlobalArtinMap L) (a : Ideles.IdeleGroup L) : θK.artinHom ((ideleNorm K L) a) = (θK.transferMap θL) (θL.artinHom a)

theorem theorem_28_8_comm_classGroup {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (θK : GlobalArtinMap K) (θL : GlobalArtinMap L) (a : Ideles.IdeleClassGroup L) : θK.artinHomCK ((ideleNormCK K L) a) = (θK.transferMap θL) (θL.artinHomCK a)

theorem normSubgroup_finiteIndex {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (i : θ.I) : (θ.normSubgroupCK i).FiniteIndex

theorem normSubgroup_surjective {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (H : Subgroup (Ideles.IdeleClassGroup K)) (hopen : IsOpen ↑H) (hfin : H.FiniteIndex) : ∃ (i : θ.I), θ.normSubgroupCK i = H

theorem artinMap_quotient_iso {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) (i : θ.I) : Nonempty (Ideles.IdeleClassGroup K ⧸ θ.normSubgroupCK i ≃* θ.GalLK i)

theorem globalCFT_main_theorem {K : Type u_1} [Field K] [NumberField K] (θ : GlobalArtinMap K) : (∀ (i : θ.I), (θ.normSubgroupCK i).FiniteIndex) ∧ (∀ (H : Subgroup (Ideles.IdeleClassGroup K)), IsOpen ↑H → H.FiniteIndex → ∃ (i : θ.I), θ.normSubgroupCK i = H) ∧ ∀ (i : θ.I), Nonempty (Ideles.IdeleClassGroup K ⧸ θ.normSubgroupCK i ≃* θ.GalLK i)