@[reducible, inline]

abbrev restrictedProduct {ι : Type u_1} (X : ι → Type u_2) (U : (i : ι) → Set (X i)) : Type (max u_2 u_1)

@[reducible, inline]

abbrev IsDirectSystem {I : Type u_1} [Preorder I] (F : I → Type u_2) (f : ⦃i j : I⦄ → i ≤ j → F i → F j) : Prop

def IsFiniteAbelianExtension (K : Type u_1) (Ksep : Type u_2) [Field K] [Field Ksep] [Algebra K Ksep] (L : IntermediateField K Ksep) : Prop

def IsFiniteUnramifiedExtension (K : Type u_1) (Ksep : Type u_2) [Field K] [Field Ksep] [Algebra K Ksep] (L : IntermediateField K Ksep) : Prop

def maximalAbelianExtension (K : Type u_1) (Ksep : Type u_2) [Field K] [Field Ksep] [Algebra K Ksep] : IntermediateField K Ksep

structure LocalArtinReciprocity : Type (max (max (max (u_1 + 1) (u_2 + 1)) (u_3 + 1)) (u_4 + 1))

• Kx : Type u_1
• kx_comm_group : CommGroup self.Kx
• kx_topological_space : TopologicalSpace self.Kx
• kx_topological_group : IsTopologicalGroup self.Kx
• I : Type u_2
• ext_preorder : PartialOrder self.I
• GalLK : self.I → Type u_3
• gal_comm_group (i : self.I) : CommGroup (self.GalLK i)
• gal_fintype (i : self.I) : Fintype (self.GalLK i)
• normGroup : self.I → Subgroup self.Kx
• artinMap (i : self.I) : self.Kx →* self.GalLK i
• artinMap_surjective (i : self.I) : Function.Surjective ⇑(self.artinMap i)
• artinMap_ker (i : self.I) : (self.artinMap i).ker = self.normGroup i
• restrictMap {i j : self.I} : i ≤ j → self.GalLK j →* self.GalLK i
• artinMap_compat {i j : self.I} (h : i ≤ j) (x : self.Kx) : (self.restrictMap h) ((self.artinMap j) x) = (self.artinMap i) x
• normGroup_antitone {i j : self.I} : i ≤ j → self.normGroup j ≤ self.normGroup i
• normGroup_reflects_le {i j : self.I} : self.normGroup j ≤ self.normGroup i → i ≤ j
• exists_sup (i j : self.I) : ∃ (k : self.I), i ≤ k ∧ j ≤ k ∧ self.normGroup k = self.normGroup i ⊓ self.normGroup j
• exists_inf (i j : self.I) : ∃ k ≤ i, k ≤ j ∧ self.normGroup k = self.normGroup i ⊔ self.normGroup j
• normGroup_isClosed (i : self.I) : IsClosed ↑(self.normGroup i)
• galois_subext (i : self.I) (S : Subgroup (self.GalLK i)) : ∃ j ≤ i, self.normGroup j = Subgroup.comap (self.artinMap i) S
• J : Type u_4
• unramifiedEmb : self.J → self.I
• frobElt (j : self.J) : self.GalLK (self.unramifiedEmb j)
• IsUniformizer : self.Kx → Prop
• artinMap_uniformizer_eq_frob (j : self.J) (π : self.Kx) : self.IsUniformizer π → (self.artinMap (self.unramifiedEmb j)) π = self.frobElt j

def LocalArtinReciprocity.IsNormGroup (D : LocalArtinReciprocity) (H : Subgroup D.Kx) : Prop

def LocalArtinReciprocity.normSubgroup (D : LocalArtinReciprocity) (i : D.I) : Subgroup D.Kx

noncomputable def LocalArtinReciprocity.artinMap_quotient_equiv (D : LocalArtinReciprocity) (i : D.I) : D.Kx ⧸ D.normGroup i ≃* D.GalLK i

theorem LocalArtinReciprocity.ext_eq_of_le_of_normGroup_eq (D : LocalArtinReciprocity) {i j : D.I} (hij : i ≤ j) (hn : D.normGroup i = D.normGroup j) : i = j

theorem LocalArtinReciprocity.normGroup_injective (D : LocalArtinReciprocity) {i j : D.I} (h : D.normGroup i = D.normGroup j) : i = j

theorem LocalArtinReciprocity.normGroup_map_injective (D : LocalArtinReciprocity) : Function.Injective D.normGroup

theorem LocalArtinReciprocity.normGroup_finiteIndex (D : LocalArtinReciprocity) (i : D.I) : (D.normGroup i).FiniteIndex

theorem LocalArtinReciprocity.closed_finiteIndex_isOpen {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (H : Subgroup G) [H.FiniteIndex] (hclosed : IsClosed ↑H) : IsOpen ↑H

theorem LocalArtinReciprocity.normGroup_isOpen (D : LocalArtinReciprocity) (i : D.I) : IsOpen ↑(D.normGroup i)

class LocalArtinReciprocity.LocalExistenceTheorem (D : LocalArtinReciprocity) : Prop

• open_finiteIndex_isNormGroup (H : Subgroup D.Kx) : H.FiniteIndex → IsOpen ↑H → D.IsNormGroup H

theorem LocalArtinReciprocity.restrictMap_jointly_injective (D : LocalArtinReciprocity) {j k m : D.I} (hj : j ≤ m) (hk : k ≤ m) (hnorm : D.normGroup m = D.normGroup j ⊓ D.normGroup k) (g₁ g₂ : D.GalLK m) (hgj : (D.restrictMap hj) g₁ = (D.restrictMap hj) g₂) (hgk : (D.restrictMap hk) g₁ = (D.restrictMap hk) g₂) : g₁ = g₂

theorem LocalArtinReciprocity.artinMap_unique (D : LocalArtinReciprocity) (θ₁ θ₂ : (i : D.I) → D.Kx →* D.GalLK i) (_h_surj₁ : ∀ (i : D.I), Function.Surjective ⇑(θ₁ i)) (_h_surj₂ : ∀ (i : D.I), Function.Surjective ⇑(θ₂ i)) (h_ker₁ : ∀ (i : D.I), (θ₁ i).ker = D.normGroup i) (h_ker₂ : ∀ (i : D.I), (θ₂ i).ker = D.normGroup i) (h_frob₁ : ∀ (j : D.J) (π : D.Kx), D.IsUniformizer π → (θ₁ (D.unramifiedEmb j)) π = D.frobElt j) (h_frob₂ : ∀ (j : D.J) (π : D.Kx), D.IsUniformizer π → (θ₂ (D.unramifiedEmb j)) π = D.frobElt j) (h_compat₁ : ∀ {i j : D.I} (h : i ≤ j) (x : D.Kx), (D.restrictMap h) ((θ₁ j) x) = (θ₁ i) x) (h_compat₂ : ∀ {i j : D.I} (h : i ≤ j) (x : D.Kx), (D.restrictMap h) ((θ₂ j) x) = (θ₂ i) x) (uniformizers_generate : Subgroup.closure {π : D.Kx | D.IsUniformizer π} = ⊤) (_h_LET : ∀ (U : Subgroup D.Kx), U.FiniteIndex → IsOpen ↑U → ∃ (i : D.I), D.normGroup i = U) (kab_eq_kpi_kunr : ∀ (π : D.Kx), D.IsUniformizer π → ∀ (i : D.I), ∃ (j : D.J) (k : D.I), π ∈ D.normGroup k ∧ ∃ (m : D.I), D.unramifiedEmb j ≤ m ∧ k ≤ m ∧ i ≤ m ∧ D.normGroup m = D.normGroup (D.unramifiedEmb j) ⊓ D.normGroup k) (i : D.I) (x : D.Kx) : (θ₁ i) x = (θ₂ i) x

structure LocalArtinMapextends LocalArtinReciprocity : Type (max (max (max (max (u_1 + 1) (u_2 + 1)) (u_3 + 1)) (u_4 + 1)) (u_5 + 1))

• Kx : Type u_5
• kx_comm_group : CommGroup self.Kx
• kx_topological_space : TopologicalSpace self.Kx
• kx_topological_group : IsTopologicalGroup self.Kx
• I : Type u_4
• ext_preorder : PartialOrder self.I
• GalLK : self.I → Type u_3
• gal_comm_group (i : self.I) : CommGroup (self.GalLK i)
• gal_fintype (i : self.I) : Fintype (self.GalLK i)
• normGroup : self.I → Subgroup self.Kx
• artinMap (i : self.I) : self.Kx →* self.GalLK i
• artinMap_surjective (i : self.I) : Function.Surjective ⇑(self.artinMap i)
• artinMap_ker (i : self.I) : (self.artinMap i).ker = self.normGroup i
• restrictMap {i j : self.I} : i ≤ j → self.GalLK j →* self.GalLK i
• artinMap_compat {i j : self.I} (h : i ≤ j) (x : self.Kx) : (self.restrictMap h) ((self.artinMap j) x) = (self.artinMap i) x
• normGroup_antitone {i j : self.I} : i ≤ j → self.normGroup j ≤ self.normGroup i
• normGroup_reflects_le {i j : self.I} : self.normGroup j ≤ self.normGroup i → i ≤ j
• exists_sup (i j : self.I) : ∃ (k : self.I), i ≤ k ∧ j ≤ k ∧ self.normGroup k = self.normGroup i ⊓ self.normGroup j
• exists_inf (i j : self.I) : ∃ k ≤ i, k ≤ j ∧ self.normGroup k = self.normGroup i ⊔ self.normGroup j
• normGroup_isClosed (i : self.I) : IsClosed ↑(self.normGroup i)
• galois_subext (i : self.I) (S : Subgroup (self.GalLK i)) : ∃ j ≤ i, self.normGroup j = Subgroup.comap (self.artinMap i) S
• J : Type u_2
• unramifiedEmb : self.J → self.I
• frobElt (j : self.J) : self.GalLK (self.unramifiedEmb j)
• IsUniformizer : self.Kx → Prop
• artinMap_uniformizer_eq_frob (j : self.J) (π : self.Kx) : self.IsUniformizer π → (self.artinMap (self.unramifiedEmb j)) π = self.frobElt j
• GalAb : Type u_1
• galAb_group : CommGroup self.GalAb
• galAb_topological_space : TopologicalSpace self.GalAb
• galAb_topological_group : IsTopologicalGroup self.GalAb
• galAb_compact : CompactSpace self.GalAb
• gal_topological_space (i : self.I) : TopologicalSpace (self.GalLK i)
• gal_discrete_topology (i : self.I) : DiscreteTopology (self.GalLK i)
• artinHom : self.Kx →* self.GalAb
• artinHom_continuous : Continuous ⇑self.artinHom
• proj (i : self.I) : self.GalAb →* self.GalLK i
• proj_continuous (i : self.I) : Continuous ⇑(self.proj i)
• artinMap_eq_proj (i : self.I) (x : self.Kx) : (self.artinMap i) x = (self.proj i) (self.artinHom x)
• 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
• proj_nhd_basis (g : self.GalAb) (U : Set self.GalAb) : U ∈ nhds g → ∃ (i : self.I), {h : self.GalAb | (self.proj i) h = (self.proj i) g} ⊆ U

def LocalArtinMap.ProfiniteCompletionKx (M : LocalArtinMap) : Subgroup ((i : M.I) → M.Kx ⧸ M.normGroup i)

def LocalArtinMap.InvLimGalLK (M : LocalArtinMap) : Subgroup ((i : M.I) → M.GalLK i)

noncomputable def LocalArtinMap.profiniteCompletionIso (M : LocalArtinMap) : ↥M.ProfiniteCompletionKx ≃* ↥M.InvLimGalLK

theorem LocalArtinMap.proj_fiber_mem_nhds (M : LocalArtinMap) (i : M.I) (g : M.GalAb) : {h : M.GalAb | (M.proj i) h = (M.proj i) g} ∈ nhds g

theorem LocalArtinMap.proj_fiber_isOpen (M : LocalArtinMap) (i : M.I) (c : M.GalLK i) : IsOpen {g : M.GalAb | (M.proj i) g = c}

theorem LocalArtinMap.proj_fiber_isClosed (M : LocalArtinMap) (i : M.I) (c : M.GalLK i) : IsClosed {g : M.GalAb | (M.proj i) g = c}

noncomputable def LocalArtinMap.galAbIso (M : LocalArtinMap) : M.GalAb ≃* ↥M.InvLimGalLK

noncomputable def LocalArtinMap.profiniteCompletionMulEquiv (M : LocalArtinMap) : ↥M.ProfiniteCompletionKx ≃* M.GalAb