CoordinateDeepIdeal111.lean

1 import PaperXI.OnePlusIntersection110
2 import Mathlib.NumberTheory.LocalField.Basic
3 import Mathlib.LinearAlgebra.Matrix.Ideal
4 import Mathlib.Topology.Algebra.LinearTopology
5 import Mathlib.Topology.Algebra.OpenSubgroup
6 import Mathlib.Topology.Algebra.Group.Matrix
7 import Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
8 
9 /-! A common open ideal in an actual coordinate integral matrix order.
10 The ideal lives in the integral order, not the full field matrix algebra. -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.CoordinateDeepIdeal111
14 open Matrix Topology Filter
15 open scoped Topology
16 
17 section MatrixNeighborhood
18 variable {R m : Type*} [Ring R] [TopologicalSpace R]
19   [IsTopologicalRing R] [IsLinearTopology R R] [Fintype m] [DecidableEq m]
20 
21 def uncurryHomeomorph : Matrix m m R ≃ₜ ((m × m) → R) where
22   toFun x p := x p.1 p.2
23   invFun x i j := x (i,j)
24   left_inv _ := rfl
25   right_inv _ := rfl
26   continuous_toFun := by fun_prop
27   continuous_invFun := by fun_prop
28 
29 /-- Every actual matrix zero-neighborhood contains matrices over one open
30 coefficient ideal. This constructs an ideal of the integral matrix ring. -/
31 theorem exists_open_matrix_ideal_subset (U : Set (Matrix m m R))
32     (hU : U ∈ 𝓝 0) : ∃ I : Ideal R, IsOpen (I : Set R) ∧
33       (I.matrix m : Set (Matrix m m R)) ⊆ U := by
34   have hpre : (uncurryHomeomorph (R := R) (m := m)).symm ⁻¹' U ∈
35       𝓝 (0 : (m × m) → R) :=
36     (uncurryHomeomorph (R := R) (m := m)).symm.continuous.continuousAt hU
37   rw [nhds_pi] at hpre
38   obtain ⟨⟨s, I⟩, ⟨_, hI⟩, hsub⟩ :=
39     (IsLinearTopology.hasBasis_open_ideal (R := R)).pi_self.mem_iff.mp hpre
40   refine ⟨I, hI, ?_⟩
41   intro x hx
42   exact hsub (fun p _ => hx p.1 p.2)
43 
44 omit [IsTopologicalRing R] [IsLinearTopology R R] in
45 theorem matrix_ideal_open (I : Ideal R) (hI : IsOpen (I : Set R)) :
46     IsOpen (I.matrix m : Set (Matrix m m R)) := by
47   have he : (I.matrix m : Set (Matrix m m R)) =
48       ⋂ i, ⋂ j, {x : Matrix m m R | x i j ∈ I} := by ext x; simp
49   rw [he]
50   apply isOpen_iInter_of_finite
51   intro i
52   apply isOpen_iInter_of_finite
53   intro j
54   exact hI.preimage ((continuous_apply j).comp (continuous_apply i))
55 
56 end MatrixNeighborhood
57 
58 section CompactOrder
59 variable {R m : Type*} [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
60   [IsLinearTopology R R] [CompactSpace R] [Fintype m] [DecidableEq m]
61 
62 /-- Containment and finiteness are constructed from openness inside the literal
63 compact integral matrix order, rather than supplied as hypotheses. -/
64 theorem exists_common_ideal_finite (L M : AddSubgroup (Matrix m m R))
65     (hL : IsOpen (L : Set (Matrix m m R)))
66     (hM : IsOpen (M : Set (Matrix m m R))) :
67     ∃ I : Ideal R, IsOpen (I : Set R) ∧
68       (I.matrix m).toAddSubgroup ≤ L ⊓ M ∧
69       Finite (L ⧸ (I.matrix m).toAddSubgroup.addSubgroupOf L) := by
70   let : CompactSpace (Matrix m m R) := inferInstanceAs (CompactSpace (m → m → R))
71   obtain ⟨I, hI, hsub⟩ := exists_open_matrix_ideal_subset (R := R) (m := m)
72     (↑(L ⊓ M) : Set (Matrix m m R))
73     ((hL.inter hM).mem_nhds (by exact ⟨L.zero_mem, M.zero_mem⟩))
74   refine ⟨I, hI, hsub, ?_⟩
75   exact AddSubgroup.quotient_finite_of_isOpen' L _ hL
76     ((matrix_ideal_open I hI).preimage continuous_subtype_val)
77 
78 end CompactOrder
79 end PaperXI.CoordinateDeepIdeal111

Back to source controls