CompactDegreeSeparation.lean

1 import PaperXI.CentralExtensionInducing
2 import Mathlib.Topology.Instances.Int
3 import Mathlib.GroupTheory.OrderOfElement
4 
5 /-!
6 # Compact subgroups have zero integer degree
7 
8 A continuous integer degree has finite image on a compact subgroup, because
9 the target has its usual discrete topology.  The image is a finite subgroup of
10 the torsion-free group `Multiplicative ℤ`, so it is trivial.  This supplies the
11 separation hypothesis for adjoining any element of nonzero degree.
12 -/
13 set_option autoImplicit false
14 noncomputable section
15 namespace PaperXI.CompactDegreeSeparation
16 
17 variable {G : Type*} [Group G] [TopologicalSpace G]
18 
19 /-- Compactness and continuity force a compact subgroup into the integer-degree kernel. -/
20 theorem compact_le_degree_ker (J : Subgroup G) (δ : G →* Multiplicative ℤ)
21     (hδ : Continuous δ) (hJ : IsCompact (J : Set G)) : J ≤ δ.ker := by
22   have hfinite : (J.map δ : Set (Multiplicative ℤ)).Finite := by
23     rw [Subgroup.coe_map]
24     exact (hJ.image hδ).finite_of_discrete
25   let : Finite (J.map δ) := hfinite.to_subtype
26   intro j hj
27   let x : J.map δ := ⟨δ j, ⟨j, hj, rfl⟩⟩
28   have hx : x = 1 := (isOfFinOrder_of_finite x).eq_one'
29   exact congrArg Subtype.val hx
30 
31 /-- A nonzero integer degree prevents a nonzero power from meeting a compact subgroup. -/
32 theorem hfree_from_compact_degree (J : Subgroup G) (δ : G →* Multiplicative ℤ)
33     (hδ : Continuous δ) (hJ : IsCompact (J : Set G))
34     (z : G) (hz : δ z ≠ 1) : ∀ n : ℤ, z ^ n ∈ J → n = 0 :=
35   CentralExtensionInducing.hfree_from_degree J δ (compact_le_degree_ker J δ hδ hJ) z hz
36 
37 end PaperXI.CompactDegreeSeparation

Back to source controls