CompactQuotientPeriod69.lean

1 import Mathlib.Topology.Algebra.Group.Quotient
2 import Mathlib.Topology.Instances.Int
3 import Mathlib.Tactic
4 
5 /-! Compact fundamental domains from a finite period modulo a compact subgroup. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CompactQuotientPeriod69
9 open scoped Pointwise
10 variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
11 variable (J Z : Subgroup G) [Z.Normal] (t : G)
12 
13 /-- An explicit finite union of translates of a compact subgroup covers the quotient.
14 No compactness of the ambient group is assumed. -/
15 theorem compact_quotient_of_period
16     (hJ : IsCompact (J : Set G))
17     (hcover : ∀ g : G, ∃ r : ℤ, ∃ j : J, g = t ^ r * (j : G))
18     (m : ℕ) (hm : 0 < m)
19     (hperiod : (QuotientGroup.mk' Z t) ^ m ∈ J.map (QuotientGroup.mk' Z)) :
20     CompactSpace (G ⧸ Z) := by
21   let q := QuotientGroup.mk' Z
22   let U := J.map q
23   let : CompactSpace J := isCompact_iff_compactSpace.mp hJ
24   let F : Fin m × J → G ⧸ Z := fun p => q (t ^ (p.1 : ℕ) * (p.2 : G))
25   have hF : Continuous F := by
26     have hc : Continuous (fun i : Fin m => t ^ (i : ℕ)) := continuous_of_discreteTopology
27     exact QuotientGroup.continuous_mk.comp
28       ((hc.comp continuous_fst).mul (continuous_subtype_val.comp continuous_snd))
29   have hsurj : Function.Surjective F := by
30     intro x
31     obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective Z x
32     obtain ⟨r, j, rfl⟩ := hcover g
33     have hmz : (0 : ℤ) < m := Int.natCast_pos.mpr hm
34     have hrem0 : 0 ≤ r % (m : ℤ) := Int.emod_nonneg r (ne_of_gt hmz)
35     have hremm : r % (m : ℤ) < m := Int.emod_lt_of_pos r hmz
36     let i : Fin m := ⟨(r % (m : ℤ)).toNat, by omega⟩
37     have hi : (i : ℕ) = (r % (m : ℤ)).toNat := rfl
38     have hice : ((i : ℕ) : ℤ) = r % (m : ℤ) := Int.toNat_of_nonneg hrem0
39     have hp : q t ^ ((m : ℤ) * (r / (m : ℤ))) ∈ U := by
40       have h := U.zpow_mem hperiod (r / (m : ℤ))
41       simpa only [zpow_mul, zpow_natCast] using h
42     have hprod : q t ^ ((m : ℤ) * (r / (m : ℤ))) * q (j : G) ∈ U :=
43       U.mul_mem hp (Subgroup.mem_map.mpr ⟨j, j.property, rfl⟩)
44     obtain ⟨j', hj', hj'e⟩ := Subgroup.mem_map.mp hprod
45     refine ⟨(i, ⟨j', hj'⟩), ?_⟩
46     change q (t ^ (i : ℕ) * j') = q (t ^ r * (j : G))
47     rw [map_mul, map_pow, hj'e, map_mul, map_zpow]
48     rw [← mul_assoc, ← zpow_natCast (q t) (i : ℕ), ← zpow_add]
49     rw [hice, Int.emod_add_mul_ediv]
50   exact hsurj.compactSpace hF
51 
52 end PaperXI.CompactQuotientPeriod69

Back to source controls