RepresentationTopology.lean

1 import PaperX.RepresentationLimits
2 import Mathlib.Topology.Instances.Matrix
3 import Mathlib.Topology.LocallyConstant.Basic
4 
5 /-! Actual continuity, using the specified ideal-adic coefficient topology.
6 Continuity of finite-precision entries means local constancy into a discrete
7 quotient. It is not inferred from the algebraic homomorphism laws. -/
8 set_option autoImplicit false
9 namespace PaperX.RepresentationTopology
10 open scoped Topology
11 open Filter
12 open PaperX.RepresentationLimits
13 variable {R : Type*} [CommRing R] (I : Ideal R)
14 variable {X : Type*} [TopologicalSpace X]
15 
16 /-- Local constancy expressed by neighborhoods; equivalent to continuity to the
17 explicit discrete topology, irrespective of any other topology on B. -/
18 def FiniteContinuous {B : Type*} (f : X → B) : Prop :=
19   ∀ x, ∀ᶠ y in 𝓝 x, f y = f x
20 
21 theorem finiteContinuous_iff {B : Type*} (f : X → B) :
22     FiniteContinuous f ↔ @Continuous X B inferInstance ⊥ f := by
23   let : TopologicalSpace B := ⊥
24   let : DiscreteTopology B := ⟨rfl⟩
25   simp only [FiniteContinuous, continuous_iff_continuousAt, ContinuousAt,
26     nhds_discrete, tendsto_pure]
27 
28 /-- The same finite-precision test proves genuine convergence of nets. -/
29 theorem adic_tendsto_of_reductions {A : Type*} (F : Filter A) (f : A → R) (b : R)
30     (h : ∀ k, ∀ᶠ x in F, Ideal.Quotient.mk (I^k) (f x) = Ideal.Quotient.mk (I^k) b) :
31     @Filter.Tendsto A R f F (@nhds R I.adicTopology b) := by
32   apply (I.hasBasis_nhds_adic b).tendsto_right_iff.mpr
33   intro k _
34   filter_upwards [h k] with x hx
35   exact ⟨f x - b, Ideal.Quotient.eq.mp hx, by simp⟩
36 
37 /-- All finite reductions locally constant implies actual adic continuity. -/
38 theorem continuous_of_reductions (f : X → R)
39     (h : ∀ k, FiniteContinuous (fun x => Ideal.Quotient.mk (I^k) (f x))) :
40     @Continuous X R inferInstance I.adicTopology f := by
41   let : TopologicalSpace R := I.adicTopology
42   rw [continuous_iff_continuousAt]
43   intro x
44   apply (I.hasBasis_nhds_adic (f x)).tendsto_right_iff.mpr
45   intro k _
46   filter_upwards [h k x] with y hy
47   refine ⟨f y - f x, ?_, ?_⟩
48   · exact Ideal.Quotient.eq.mp hy
49   · simp
50 
51 /-- Adic continuity is detected at finite precision, with no completeness assumption. -/
52 theorem reductions_of_continuous (f : X → R)
53     (h : @Continuous X R inferInstance I.adicTopology f) (k : ℕ) :
54     FiniteContinuous (fun x => Ideal.Quotient.mk (I^k) (f x)) := by
55   let : TopologicalSpace R := I.adicTopology
56   intro x
57   have H := (I.hasBasis_nhds_adic (f x)).tendsto_right_iff.mp
58     (h.continuousAt (x := x)) k trivial
59   filter_upwards [H] with y hy
60   obtain ⟨z, hz, he⟩ := hy
61   apply Ideal.Quotient.eq.mpr
62   rw [← he]
63   simpa using hz
64 
65 theorem adic_continuous_iff (f : X → R) :
66     @Continuous X R inferInstance I.adicTopology f ↔
67       ∀ k, FiniteContinuous (fun x => Ideal.Quotient.mk (I^k) (f x)) :=
68   ⟨reductions_of_continuous I f, continuous_of_reductions I f⟩
69 
70 variable {G : Type*} [Group G] [TopologicalSpace G]
71 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
72 
73 /-- A finite representation is continuous precisely when each matrix entry is
74 locally constant. The finite matrix has its ordinary product topology. -/
75 def FiniteRepContinuous {B : Type*} [CommRing B] (ρ : MatrixRep B G ι) : Prop :=
76   ∀ i j, FiniteContinuous (fun g => ρ g i j)
77 
78 /-- The coefficient topology is ideal-adic and the matrix topology is its usual
79 finite product. The definition is independent of an ambient default topology. -/
80 def AdicRepContinuous (ρ : MatrixRep R G ι) : Prop :=
81   let : TopologicalSpace R := I.adicTopology
82   Continuous ρ
83 
84 theorem reconstructed_continuous [IsAdicComplete I R] (f : Family R I G ι)
85     (hf : ∀ k, FiniteRepContinuous (f.maps k)) :
86     AdicRepContinuous I (reconstruct I f) := by
87   let : TopologicalSpace R := I.adicTopology
88   apply continuous_pi
89   intro i
90   apply continuous_pi
91   intro j
92   apply continuous_of_reductions I
93   intro k
94   have H : (fun g => Ideal.Quotient.mk (I^k) (reconstruct I f g i j)) =
95       (fun g => f.maps k g i j) := by
96     funext g
97     exact congrArg (fun ρ => ρ g i j) (reconstruct_reduces I f k)
98   rw [H]
99   exact hf k i j
100 
101 omit [TopologicalSpace G] in
102 /-- A condition specified by vanishing on a subgroup is preserved; this includes
103 unramifiedness once an inertia subgroup is actually supplied. -/
104 theorem unramified_of_all_reductions [IsAdicComplete I R] (f : Family R I G ι)
105     (H : Subgroup G) (hf : ∀ k g, g ∈ H → f.maps k g = 1) :
106     ∀ g, g ∈ H → reconstruct I f g = 1 := by
107   intro g hg
108   apply matrix_ext I
109   intro k
110   change (liftMatrix I f g).map _ = _
111   rw [liftMatrix_reduces, hf k g hg]
112   symm
113   exact (Ideal.Quotient.mk (I^k)).mapMatrix.map_one
114 
115 /-- Continuous coefficient inclusion transports the representation to a local
116 field with its declared topology. No topology on that field is silently inferred. -/
117 theorem coefficient_change_continuous {K : Type*} [CommRing K] [TopologicalSpace K]
118     (inc : R →+* K) (hinc : @Continuous R K I.adicTopology inferInstance inc)
119     (ρ : MatrixRep R G ι) (hρ : AdicRepContinuous I ρ) :
120     Continuous (changeCoefficients inc ρ) := by
121   let : TopologicalSpace R := I.adicTopology
122   exact Continuous.matrix_map hρ hinc
123 
124 end PaperX.RepresentationTopology

Back to source controls