@[reducible, inline]

abbrev Ideles.IdeleGroup (K : Type u_1) [Field K] [NumberField K] : Type u_1

noncomputable def Ideles.principalIdeleEmb (K : Type u_1) [Field K] [NumberField K] : Kˣ →* IdeleGroup K

noncomputable def Ideles.principalIdeles (K : Type u_1) [Field K] [NumberField K] : Subgroup (IdeleGroup K)

@[reducible, inline]

abbrev Ideles.IdeleClassGroup (K : Type u_1) [Field K] [NumberField K] : Type u_1

instance Ideles.ideleGroup_locallyCompact (K : Type u_1) [Field K] [NumberField K] : LocallyCompactSpace (IdeleGroup K)

theorem Ideles.principalIdeles_discrete (K : Type u_1) [Field K] [NumberField K] : DiscreteTopology ↥(principalIdeles K)

theorem Ideles.adeleRing_unit_fin_norm_finMulSupport (K : Type u_1) [Field K] [NumberField K] (a : IdeleGroup K) : (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => ‖(↑a).2 v‖).Finite

noncomputable def Ideles.adelicNorm (K : Type u_1) [Field K] [NumberField K] : IdeleGroup K →* ℝ

theorem Ideles.adelicNorm_eq (K : Type u_1) [Field K] [NumberField K] (a : IdeleGroup K) : (adelicNorm K) a = NumberField.Adeles.adelicAbsVal ↑a

noncomputable def Ideles.OneIdeleGroup (K : Type u_1) [Field K] [NumberField K] : Subgroup (IdeleGroup K)

theorem Ideles.mem_OneIdeleGroup (K : Type u_1) [Field K] [NumberField K] (a : IdeleGroup K) : a ∈ OneIdeleGroup K ↔ (adelicNorm K) a = 1

theorem Ideles.mem_OneIdeleGroup_iff (K : Type u_1) [Field K] [NumberField K] (a : IdeleGroup K) : a ∈ OneIdeleGroup K ↔ NumberField.Adeles.adelicAbsVal ↑a = 1

theorem Ideles.adelicAbsVal_algebraMap (K : Type u_1) [Field K] [NumberField K] (x : K) : NumberField.Adeles.adelicAbsVal ((algebraMap K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) x) = (∏ w : NumberField.InfinitePlace K, w x ^ w.mult) * ∏ᶠ (w : NumberField.FinitePlace K), w x

theorem Ideles.principalIdeles_le_oneIdeleGroup (K : Type u_1) [Field K] [NumberField K] : principalIdeles K ≤ OneIdeleGroup K

theorem Ideles.finAdeleRing_openSet (K : Type u_1) [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : S.Finite) : IsOpen {x : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K | ∀ v ∉ S, x v ∈ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}

theorem Ideles.locallyFinite_finNorm (K : Type u_1) [Field K] [NumberField K] : LocallyFinite fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => Function.mulSupport fun (a : IdeleGroup K) => ‖(↑a).2 v‖

theorem Ideles.continuous_adelicNorm (K : Type u_1) [Field K] [NumberField K] : Continuous ⇑(adelicNorm K)

theorem Ideles.oneIdeles_isClosed_in_ideles (K : Type u_1) [Field K] [NumberField K] : IsClosed ↑(OneIdeleGroup K)

theorem Ideles.infiniteAdeleRing_units_isOpen (K : Type u_1) [Field K] [NumberField K] : IsOpen {x : NumberField.InfiniteAdeleRing K | IsUnit x}

theorem Ideles.finiteAdeleRing_units_isOpen (K : Type u_2) [Field K] [NumberField K] : IsOpen {x : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K | IsUnit x}

theorem Ideles.adeleRing_units_isOpen (K : Type u_1) [Field K] [NumberField K] : IsOpen {x : NumberField.AdeleRing (NumberField.RingOfIntegers K) K | IsUnit x}

theorem Ideles.oneIdeles_isClosed_in_adeles (K : Type u_1) [Field K] [NumberField K] : IsClosed (Units.val '' ↑(OneIdeleGroup K))

theorem Ideles.ring_inverse_prod_eq_of_isUnit {A : Type u_2} {B : Type u_3} [Ring A] [Ring B] (x : A × B) (hx : IsUnit x) : Ring.inverse x = (Ring.inverse x.1, Ring.inverse x.2)

theorem Ideles.infiniteAdeleRing_inverse_apply (K : Type u_1) [Field K] (x : NumberField.InfiniteAdeleRing K) (hx : IsUnit x) (w : NumberField.InfinitePlace K) : Ring.inverse x w = Ring.inverse (x w)

theorem Ideles.infiniteAdeleRing_continuousOn_ringInverse (K : Type u_1) [Field K] : ContinuousOn Ring.inverse {x : NumberField.InfiniteAdeleRing K | IsUnit x}

theorem Ideles.finiteAdeleRing_inverse_apply (K : Type u_1) [Field K] [NumberField K] (x : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (hx : IsUnit x) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (Ring.inverse x) v = Ring.inverse (x v)

theorem Ideles.finiteAdeleRing_continuousOn_ringInverse' (K : Type u_2) [Field K] [NumberField K] : ContinuousOn Ring.inverse {x : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K | IsUnit x}

theorem Ideles.finiteAdeleRing_continuousOn_ringInverse (K : Type u_1) [Field K] [NumberField K] : ContinuousOn Ring.inverse {x : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K | IsUnit x}

theorem Ideles.adeleRing_continuousOn_ringInverse (K : Type u_1) [Field K] [NumberField K] : ContinuousOn Ring.inverse {x : NumberField.AdeleRing (NumberField.RingOfIntegers K) K | IsUnit x}

theorem Ideles.adeleRing_isEmbedding_units_val (K : Type u_1) [Field K] [NumberField K] : Topology.IsEmbedding Units.val

theorem Ideles.closure_oneIdeles_image_subset_units (K : Type u_1) [Field K] [NumberField K] : closure (Units.val '' ↑(OneIdeleGroup K)) ⊆ {x : NumberField.AdeleRing (NumberField.RingOfIntegers K) K | IsUnit x}

theorem Ideles.oneIdeles_topology_eq (K : Type u_1) [Field K] [NumberField K] : instTopologicalSpaceSubtype = TopologicalSpace.induced (fun (x : ↥(OneIdeleGroup K)) => ↑↑x) inferInstance

theorem Ideles.lemma_26_8 (K : Type u_1) [Field K] [NumberField K] : IsClosed ↑(OneIdeleGroup K) ∧ IsClosed (Units.val '' ↑(OneIdeleGroup K)) ∧ instTopologicalSpaceSubtype = TopologicalSpace.induced (fun (x : ↥(OneIdeleGroup K)) => ↑↑x) inferInstance

theorem Ideles.oneIdeles_isClosed (K : Type u_1) [Field K] [NumberField K] : IsClosed ↑(OneIdeleGroup K)

theorem Ideles.adelic_box_isCompact (K : Type u_1) [Field K] [NumberField K] (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) : IsCompact {x : NumberField.AdeleRing (NumberField.RingOfIntegers K) K | ∀ (v : NumberField.Adeles.Place K), NumberField.Adeles.placeNormAdele v x ≤ NumberField.Adeles.placeNormAdele v a}

theorem Ideles.adelic_box_inter_oneIdeles_isCompact (K : Type u_1) [Field K] [NumberField K] (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) : IsCompact (Subtype.val ⁻¹' (Units.val ⁻¹' {x : NumberField.AdeleRing (NumberField.RingOfIntegers K) K | ∀ (v : NumberField.Adeles.Place K), NumberField.Adeles.placeNormAdele v x ≤ NumberField.Adeles.placeNormAdele v a}))

theorem Ideles.adelicAbsVal_mul (K : Type u_1) [Field K] [NumberField K] (a b : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (ha : (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => ‖a.2 v‖).Finite) (hb : (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => ‖b.2 v‖).Finite) : NumberField.Adeles.adelicAbsVal (a * b) = NumberField.Adeles.adelicAbsVal a * NumberField.Adeles.adelicAbsVal b

theorem Ideles.placeNormAdele_mul (K : Type u_1) [Field K] [NumberField K] (v : NumberField.Adeles.Place K) (a b : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) : NumberField.Adeles.placeNormAdele v (a * b) = NumberField.Adeles.placeNormAdele v a * NumberField.Adeles.placeNormAdele v b

theorem Ideles.adelic_box_surjects_onto_quotient (K : Type u_1) [Field K] [NumberField K] (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (ha : NumberField.Adeles.adelicAbsVal a > Classical.choose ⋯) (ha_fin : (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => ‖a.2 v‖).Finite) (q : ↥(OneIdeleGroup K) ⧸ (principalIdeles K).subgroupOf (OneIdeleGroup K)) : ∃ c ∈ Subtype.val ⁻¹' (Units.val ⁻¹' {x : NumberField.AdeleRing (NumberField.RingOfIntegers K) K | ∀ (v : NumberField.Adeles.Place K), NumberField.Adeles.placeNormAdele v x ≤ NumberField.Adeles.placeNormAdele v a}), (QuotientGroup.mk' ((principalIdeles K).subgroupOf (OneIdeleGroup K))) c = q

theorem Ideles.fujisaki_compact_fundamental_region (K : Type u_1) [Field K] [NumberField K] : ∃ (C : Set ↥(OneIdeleGroup K)), IsCompact C ∧ ∀ (q : ↥(OneIdeleGroup K) ⧸ (principalIdeles K).subgroupOf (OneIdeleGroup K)), ∃ c ∈ C, (QuotientGroup.mk' ((principalIdeles K).subgroupOf (OneIdeleGroup K))) c = q

theorem Ideles.fujisaki_lemma (K : Type u_1) [Field K] [NumberField K] : CompactSpace (↥(OneIdeleGroup K) ⧸ (principalIdeles K).subgroupOf (OneIdeleGroup K))

theorem Ideles.fujisaki_lemma_discrete (K : Type u_1) [Field K] [NumberField K] : DiscreteTopology ↥((principalIdeles K).subgroupOf (OneIdeleGroup K))

theorem Ideles.fujisaki_lemma_full (K : Type u_1) [Field K] [NumberField K] : DiscreteTopology ↥((principalIdeles K).subgroupOf (OneIdeleGroup K)) ∧ CompactSpace (↥(OneIdeleGroup K) ⧸ (principalIdeles K).subgroupOf (OneIdeleGroup K))

@[reducible, inline]

abbrev Ideles.NormOneIdeleClassGroup (K : Type u_1) [Field K] [NumberField K] : Type u_1

class Ideles.IsProfiniteGroup (G : Type u_1) [Group G] [TopologicalSpace G] : Prop

• isInverseLimitOfFiniteGroups : ∃ (J : Type) (x : CategoryTheory.SmallCategory J) (F : CategoryTheory.Functor J FiniteGrp.{0}), Nonempty (G ≃ₜ* ↑(ProfiniteGrp.limit (F.comp (CategoryTheory.forget₂ FiniteGrp.{0} ProfiniteGrp.{0}))).toProfinite.toTop)

theorem Ideles.compact_totally_disconnected_is_profinite (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] [CompactSpace G] [TotallyDisconnectedSpace G] : IsProfiniteGroup G

theorem Ideles.profinite_iff_totallyDisconnected_compact (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] : IsProfiniteGroup G ↔ CompactSpace G ∧ TotallyDisconnectedSpace G

def Ideles.profiniteTransitionMap {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N₁ N₂ : OpenNormalSubgroup G) (h : N₁ ≤ N₂) : G ⧸ ↑N₁.toOpenSubgroup →* G ⧸ ↑N₂.toOpenSubgroup

def Ideles.profiniteCompletionSubgroup (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Subgroup ((N : OpenNormalSubgroup G) → G ⧸ ↑N.toOpenSubgroup)

def Ideles.toProfiniteCompletion (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : G →* ↥(profiniteCompletionSubgroup G)

theorem Ideles.profiniteCompletion_denseRange (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : DenseRange ⇑(toProfiniteCompletion G)

def Ideles.IsStronglyComplete (G : Type u_1) [Group G] [TopologicalSpace G] : Prop

noncomputable def Ideles.abstractTransitionMap {G : Type u_1} [Group G] (N₁ N₂ : FiniteIndexNormalSubgroup G) (h : N₁ ≤ N₂) : G ⧸ N₁.toSubgroup →* G ⧸ N₂.toSubgroup

noncomputable def Ideles.abstractProfiniteCompletionSubgroup (G : Type u_1) [Group G] : Subgroup ((N : FiniteIndexNormalSubgroup G) → G ⧸ N.toSubgroup)

noncomputable def Ideles.toAbstractProfiniteCompletion (G : Type u_1) [Group G] : G →* ↥(abstractProfiniteCompletionSubgroup G)

noncomputable def Ideles.OpenNormalSubgroup.comapContinuousMulEquiv {G : Type u_1} {H : Type u_2} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalGroup G] [IsTopologicalGroup H] (e : G ≃ₜ* H) (N : OpenNormalSubgroup H) : OpenNormalSubgroup G

noncomputable def Ideles.quotientMulEquivOfContinuousMulEquiv {G : Type u_1} {H : Type u_2} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalGroup G] [IsTopologicalGroup H] (e : G ≃ₜ* H) (N : OpenNormalSubgroup H) : H ⧸ ↑N.toOpenSubgroup ≃* G ⧸ ↑(OpenNormalSubgroup.comapContinuousMulEquiv e N).toOpenSubgroup

theorem Ideles.profiniteGroup_iso_invLim_quotients (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] [IsProfiniteGroup G] : ∃ (J : Type) (x : CategoryTheory.SmallCategory J) (F : CategoryTheory.Functor J FiniteGrp.{0}), Nonempty (G ≃ₜ* ↑(ProfiniteGrp.limit (F.comp (CategoryTheory.forget₂ FiniteGrp.{0} ProfiniteGrp.{0}))).toProfinite.toTop) ∧ ∀ (j : J), ∃ (U : OpenNormalSubgroup G), Nonempty (↑(F.obj j).toGrp ≃* G ⧸ ↑U.toOpenSubgroup)

theorem Ideles.isClosed_finiteIndexNormal_of_bijective_abstractCompletion (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] [CompactSpace G] [TotallyDisconnectedSpace G] (hbij : Function.Bijective ⇑(toAbstractProfiniteCompletion G)) (N : FiniteIndexNormalSubgroup G) : IsClosed ↑N.toSubgroup

theorem Ideles.profiniteGroup_stronglyComplete_iff (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] [IsProfiniteGroup G] : IsStronglyComplete G ↔ Function.Bijective ⇑(toAbstractProfiniteCompletion G)

theorem Ideles.profiniteGroup_closed_finiteIndex_isOpen (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [IsProfiniteGroup G] (H : Subgroup G) [H.FiniteIndex] (hcl : IsClosed ↑H) : IsOpen ↑H

theorem Ideles.profiniteGroup_isCompletion_of_denseSubgroup (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] [IsProfiniteGroup G] (Γ : Subgroup G) (hΓ : Dense ↑Γ) : ∃ (Ĝ : Type) (x : Group Ĝ) (x_1 : TopologicalSpace Ĝ) (_ : IsProfiniteGroup Ĝ) (φ : ↥Γ →* Ĝ) (_ : Dense (Set.range ⇑φ)), Nonempty (G ≃* Ĝ)

theorem Ideles.restrictNormalHom_surjective {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (F : IntermediateField k K) [Normal k ↥F] : Function.Surjective ⇑(AlgEquiv.restrictNormalHom ↥F)

theorem Ideles.fixedField_of_fixingSubgroup {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (F : IntermediateField k K) : IntermediateField.fixedField F.fixingSubgroup = F

theorem Ideles.fixingSubgroup_normal_of_normal {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (F : IntermediateField k K) [Normal k ↥F] : F.fixingSubgroup.Normal

theorem Ideles.krullTopology_nhds_one_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (A : Set Gal(K/k)) : A ∈ nhds 1 ↔ ∃ (E : IntermediateField k K), FiniteDimensional k ↥E ∧ ↑E.fixingSubgroup ⊆ A

noncomputable def Ideles.galoisGroup_continuousMulEquiv_limit {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] : Gal(K/k) ≃ₜ* ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop

theorem Ideles.galoisGroup_openNormalSubgroups {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (N : Subgroup Gal(K/k)) : IsOpen ↑N ∧ N.Normal ↔ ∃ (F : IntermediateField k K), FiniteDimensional k ↥F ∧ Normal k ↥F ∧ N = F.fixingSubgroup

theorem Ideles.fundamentalTheoremInfiniteGalois {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] : Nonempty ((IntermediateField k K)ᵒᵈ ≃o ClosedSubgroup Gal(K/k))

theorem Ideles.fixedField_finrank_eq_index {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (H : ClosedSubgroup Gal(K/k)) : Module.finrank k ↥(IntermediateField.fixedField ↑H) = (↑H).index

@[deprecated Ideles.fixedField_finrank_eq_index (since := "2025-05-04")]

theorem Ideles.theorem_26_24_degree_eq_index {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (H : ClosedSubgroup Gal(K/k)) : Module.finrank k ↥(IntermediateField.fixedField ↑H) = (↑H).index

Alias of Ideles.fixedField_finrank_eq_index.

theorem Ideles.quotient_continuousMulEquiv_fixedField {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (H : ClosedSubgroup Gal(K/k)) [(↑H).Normal] : Nonempty (Gal(K/k) ⧸ ↑H ≃ₜ* Gal(↥(IntermediateField.fixedField ↑H)/k))

@[deprecated Ideles.quotient_continuousMulEquiv_fixedField (since := "2025-05-04")]

theorem Ideles.theorem_26_24_normal_quotient_iso {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (H : ClosedSubgroup Gal(K/k)) [(↑H).Normal] : Nonempty (Gal(K/k) ⧸ ↑H ≃ₜ* Gal(↥(IntermediateField.fixedField ↑H)/k))

Alias of Ideles.quotient_continuousMulEquiv_fixedField.

theorem Ideles.isOpen_iff_finiteDimensional {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (L : IntermediateField k K) : IsOpen ↑L.fixingSubgroup ↔ FiniteDimensional k ↥L

theorem Ideles.normal_iff_isGalois {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (L : IntermediateField k K) : L.fixingSubgroup.Normal ↔ IsGalois k ↥L

theorem Ideles.closure_eq_fixingSubgroup {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] (H : Subgroup Gal(K/k)) : H.topologicalClosure = (IntermediateField.fixedField H).fixingSubgroup

noncomputable def Ideles.absoluteGaloisGroup_profinite_iso (K₀ : Type u_3) [Field K₀] [CharZero K₀] : Gal(AlgebraicClosure K₀/K₀) ≃ₜ* ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor K₀ (AlgebraicClosure K₀))).toProfinite.toTop

theorem Ideles.absoluteGaloisGroup_isProfiniteGroup (K₀ : Type) [Field K₀] [CharZero K₀] : IsProfiniteGroup Gal(AlgebraicClosure K₀/K₀)

theorem Ideles.waterhouse_theorem (G : Type u_3) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [IsProfiniteGroup G] : ∃ (k' : Type) (K' : Type) (x : Field k') (x_1 : Field K') (x_2 : Algebra k' K') (_ : IsGalois k' K'), Nonempty (G ≃* Gal(K'/k'))