ProductTopology.lean

1 import RealizationBoundaries.FiniteQuotients
2 import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
3 import Mathlib.Topology.Algebra.Group.Subgroup
4 
5 /-! # Product topology and density in the genuine infinite ambient group -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace RealizationBoundaries
9 
10 instance coordinateTopology (p : Prime) : TopologicalSpace (Coordinate p) := ⊥
11 instance coordinateDiscrete (p : Prime) : DiscreteTopology (Coordinate p) := ⟨rfl⟩
12 
13 /-- The unrestricted product of all finite prime coordinates is a profinite additive group. -/
14 def ambientProfinite : ProfiniteAddGrp := ProfiniteAddGrp.of Ambient
15 
16 /-- Every finite-support vector is an actual point of the infinite product, and these
17 points meet every nonempty open set in the product topology. -/
18 theorem finiteSupport_dense : Dense (finiteSupport : Set Ambient) := by
19   apply dense_iff_inter_open.mpr
20   intro U hU hne
21   obtain ⟨x, hx⟩ := hne
22   obtain ⟨J, fJ, hJ1, hJ2⟩ := isOpen_pi_iff.mp hU x hx
23   refine ⟨cut J x, ?_, cut_mem_finiteSupport J x⟩
24   apply hJ2
25   intro p hp
26   rw [cut_apply_mem J x p hp]
27   exact (hJ1 p hp).2
28 
29 /-- Every subgroup containing D is dense, independently of a presentation or selector. -/
30 theorem intermediate_dense (H : AddSubgroup Ambient) (hD : finiteSupport ≤ H) :
31     Dense (H : Set Ambient) := finiteSupport_dense.mono hD
32 
33 theorem preimage_dense (W : Submodule ℚ TailSpace) : Dense (preimage W : Set Ambient) :=
34   intermediate_dense _ (finiteSupport_le_preimage W)
35 
36 theorem preimage_denseRange (W : Submodule ℚ TailSpace) :
37     DenseRange (fun x : preimage W => x.val) := by
38   have hr : Set.range (fun x : preimage W => x.val) = (preimage W : Set Ambient) := by
39     ext x
40     constructor
41     · rintro ⟨y, rfl⟩
42       exact y.property
43     · intro hx
44       exact ⟨⟨x, hx⟩, rfl⟩
45   change Dense (Set.range (fun x : preimage W => x.val))
46   rw [hr]
47   exact preimage_dense W
48 
49 /-- Coordinate restriction on the whole ambient product. -/
50 def ambientCoordinates (m : ℕ) : Ambient →+ DivisorCoordinates m where
51   toFun x p := x p.val
52   map_zero' := rfl
53   map_add' _ _ := rfl
54 
55 theorem ambientCoordinates_continuous (m : ℕ) : Continuous (ambientCoordinates m) :=
56   continuous_pi fun p => continuous_apply p.val
57 
58 @[simp] theorem ambientCoordinates_subtype (W : Submodule ℚ TailSpace)
59     (m : ℕ) (x : preimage W) : ambientCoordinates m x.val = coordinateMap W m x := rfl
60 
61 /-- Finite products of discrete divisor coordinates are discrete. -/
62 theorem divisorCoordinates_discrete {m : ℕ} (hm : 0 < m) :
63     DiscreteTopology (DivisorCoordinates m) := by
64   let : Finite (DivisorPrime m) := divisorPrime_finite hm
65   infer_instance
66 
67 /-- At positive multipliers, every canonical congruence kernel is open. -/
68 theorem coordinateMap_kernel_open (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m) :
69     IsOpen ((coordinateMap W m).ker : Set (preimage W)) := by
70   let := divisorCoordinates_discrete hm
71   have hc : Continuous (coordinateMap W m) :=
72     (ambientCoordinates_continuous m).comp continuous_subtype_val
73   exact hc.isOpen_preimage _ (isOpen_discrete {0})
74 
75 theorem multiples_open (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m) :
76     IsOpen (multiples W m : Set (preimage W)) := by
77   rw [← coordinateMap_ker W hm]
78   exact coordinateMap_kernel_open W hm
79 
80 end RealizationBoundaries

Back to source controls