feat(field_theory/krull_topology): added krull_topology_totally_disco…

…nnected (#12398)






Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Sebastian-Monnet <54352341+Sebastian-Monnet@users.noreply.github.com>

src/field_theory/krull_topology.lean

@@ -6,7 +6,9 @@ Authors: Sebastian Monnet
 
 import field_theory.galois
 import topology.algebra.filter_basis
-import algebra.algebra.subalgebra
+import topology.algebra.open_subgroup
+import tactic.by_contra
+
 
 /-!
 # Krull topology
@@ -34,10 +36,12 @@ all intermediate fields `E` with `E/K` finite dimensional.
 
 ## Main Results
 
-- `krull_topology_t2 K L h_int`. For an integral field extension `L/K` (one that satisfies
-  `h_int : algebra.is_integral K L`), the Krull topology on `L ≃ₐ[K] L`, `krull_topology K L`,
+- `krull_topology_t2 K L`. For an integral field extension `L/K`, the topology `krull_topology K L`
   is Hausdorff.
 
+- `krull_topology_totally_disconnected K L`. For an integral field extension `L/K`, the topology
+  `krull_topology K L` is totally disconnected.
+
 ## Notations
 
 - In docstrings, we will write `Gal(L/E)` to denote the fixing subgroup of an intermediate field
@@ -198,23 +202,6 @@ section krull_t2
 
 open_locale topological_space filter
 
-/-- If a subgroup of a topological group has `1` in its interior, then it is open. -/
-lemma subgroup.is_open_of_one_mem_interior {G : Type*} [group G] [topological_space G]
-  [topological_group G] {H : subgroup G} (h_1_int : (1 : G) ∈ interior (H : set G)) :
-  is_open (H : set G) :=
-begin
-  have h : 𝓝 1 ≤ 𝓟 (H : set G) :=
-    nhds_le_of_le h_1_int (is_open_interior) (filter.principal_mono.2 interior_subset),
-  rw is_open_iff_nhds,
-  intros g hg,
-  rw (show 𝓝 g = filter.map ⇑(homeomorph.mul_left g) (𝓝 1), by simp),
-  convert filter.map_mono h,
-  simp only [homeomorph.coe_mul_left, filter.map_principal, set.image_mul_left,
-  filter.principal_eq_iff_eq],
-  ext,
-  simp [H.mul_mem_cancel_left (H.inv_mem hg)],
-end
-
 /-- Let `L/E/K` be a tower of fields with `E/K` finite. Then `Gal(L/E)` is an open subgroup of
   `L ≃ₐ[K] L`. -/
 lemma intermediate_field.fixing_subgroup_is_open {K L : Type*} [field K] [field L] [algebra K L]
@@ -229,8 +216,15 @@ begin
   exact subgroup.is_open_of_one_mem_interior ⟨U, ⟨hU_open, hU_le⟩, h1U⟩,
 end
 
+/-- Given a tower of fields `L/E/K`, with `E/K` finite, the subgroup `Gal(L/E) ≤ L ≃ₐ[K] L` is
+  closed. -/
+lemma intermediate_field.fixing_subgroup_is_closed {K L : Type*} [field K] [field L] [algebra K L]
+  (E : intermediate_field K L) [finite_dimensional K E] :
+  is_closed (E.fixing_subgroup : set (L ≃ₐ[K] L)) :=
+open_subgroup.is_closed ⟨E.fixing_subgroup, E.fixing_subgroup_is_open⟩
+
 /-- If `L/K` is an algebraic extension, then the Krull topology on `L ≃ₐ[K] L` is Hausdorff. -/
-lemma krull_topology_t2 (K L : Type*) [field K] [field L] [algebra K L]
+lemma krull_topology_t2 {K L : Type*} [field K] [field L] [algebra K L]
   (h_int : algebra.is_integral K L) : t2_space (L ≃ₐ[K] L) :=
 { t2 := λ f g hfg,
   begin
@@ -270,3 +264,26 @@ lemma krull_topology_t2 (K L : Type*) [field K] [field L] [algebra K L]
   end }
 
 end krull_t2
+
+section totally_disconnected
+
+/-- If `L/K` is an algebraic field extension, then the Krull topology on `L ≃ₐ[K] L` is
+  totally disconnected. -/
+lemma krull_topology_totally_disconnected {K L : Type*} [field K] [field L] [algebra K L]
+  (h_int : algebra.is_integral K L) : is_totally_disconnected (set.univ : set (L ≃ₐ[K] L)) :=
+begin
+  apply is_totally_disconnected_of_clopen_set,
+  intros σ τ h_diff,
+  have hστ : σ⁻¹ * τ ≠ 1,
+  { rwa [ne.def, inv_mul_eq_one] },
+  rcases (fun_like.exists_ne hστ) with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩,
+  let E := intermediate_field.adjoin K ({x} : set L),
+  haveI := intermediate_field.adjoin.finite_dimensional (h_int x),
+  refine ⟨left_coset σ E.fixing_subgroup,
+    ⟨E.fixing_subgroup_is_open.left_coset σ, E.fixing_subgroup_is_closed.left_coset σ⟩,
+    ⟨1, E.fixing_subgroup.one_mem', by simp⟩, _⟩,
+  simp only [mem_left_coset_iff, set_like.mem_coe, mem_fixing_subgroup_iff, not_forall],
+  exact ⟨x, intermediate_field.mem_adjoin_simple_self K x, hx⟩,
+end
+
+end totally_disconnected

src/topology/algebra/open_subgroup.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin
 -/
 import topology.opens
 import topology.algebra.ring
+import topology.algebra.filter_basis
 /-!
 # Open subgroups of a topological groups
 
@@ -205,8 +206,27 @@ lemma is_open_of_open_subgroup {U : open_subgroup G} (h : U.1 ≤ H) :
   is_open (H : set G) :=
 H.is_open_of_mem_nhds (filter.mem_of_superset U.mem_nhds_one h)
 
+/-- If a subgroup of a topological group has `1` in its interior, then it is open. -/
+@[to_additive "If a subgroup of an additive topological group has `0` in its interior, then it is
+open."]
+lemma is_open_of_one_mem_interior {G : Type*} [group G] [topological_space G]
+  [topological_group G] {H : subgroup G} (h_1_int : (1 : G) ∈ interior (H : set G)) :
+  is_open (H : set G) :=
+begin
+  have h : 𝓝 1 ≤ filter.principal (H : set G) :=
+    nhds_le_of_le h_1_int (is_open_interior) (filter.principal_mono.2 interior_subset),
+  rw is_open_iff_nhds,
+  intros g hg,
+  rw (show 𝓝 g = filter.map ⇑(homeomorph.mul_left g) (𝓝 1), by simp),
+  convert filter.map_mono h,
+  simp only [homeomorph.coe_mul_left, filter.map_principal, set.image_mul_left,
+  filter.principal_eq_iff_eq],
+  ext,
+  simp [H.mul_mem_cancel_left (H.inv_mem hg)],
+end
+
 @[to_additive]
-lemma is_open_mono {H₁ H₂ : subgroup G} (h : H₁ ≤ H₂) (h₁ : is_open (H₁  :set G)) :
+lemma is_open_mono {H₁ H₂ : subgroup G} (h : H₁ ≤ H₂) (h₁ : is_open (H₁ : set G)) :
   is_open (H₂ : set G) :=
 @is_open_of_open_subgroup _ _ _ _ H₂ { is_open' := h₁, .. H₁ } h
 

src/topology/connected.lean

@@ -1101,6 +1101,22 @@ begin
     exact ht.is_preconnected.subsingleton.image _ }
 end
 
+/-- Let `X` be a topological space, and suppose that for all distinct `x,y ∈ X`, there
+  is some clopen set `U` such that `x ∈ U` and `y ∉ U`. Then `X` is totally disconnected. -/
+lemma is_totally_disconnected_of_clopen_set {X : Type*} [topological_space X]
+  (hX : ∀ {x y : X} (h_diff : x ≠ y), ∃ (U : set X) (h_clopen : is_clopen U), x ∈ U ∧ y ∉ U) :
+  is_totally_disconnected (set.univ : set X) :=
+begin
+  rintro S - hS,
+  unfold set.subsingleton,
+  by_contra' h_contra,
+  rcases h_contra with ⟨x, hx, y, hy, hxy⟩,
+  obtain ⟨U, h_clopen, hxU, hyU⟩ := hX hxy,
+  specialize hS U Uᶜ h_clopen.1 h_clopen.compl.1 (λ a ha, em (a ∈ U)) ⟨x, hx, hxU⟩ ⟨y, hy, hyU⟩,
+  rw [inter_compl_self, set.inter_empty] at hS,
+  exact set.not_nonempty_empty hS,
+end
+
 /-- A space is totally disconnected iff its connected components are subsingletons. -/
 lemma totally_disconnected_space_iff_connected_component_subsingleton :
   totally_disconnected_space α ↔ ∀ x : α, (connected_component x).subsingleton :=