ActualCoordinateDeepIdeal111.lean

1 import PaperXI.CoordinateDeepIdeal111
2 
3 /-! The actual integral coordinate-order instance and its one-plus index
4 application. Ideal containment and quotient finiteness are conclusions. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.ActualCoordinateDeepIdeal111
8 open Matrix Topology ValuativeRel
9 open PaperXI.OnePlusIntersection110 PaperXI.CoordinateDeepIdeal111
10 
11 section InnerTopology
12 variable {S : Type*} [Ring S] [TopologicalSpace S] [IsTopologicalRing S]
13 
14 def innerHomeomorph (y : Sˣ) : S ≃ₜ S where
15   toEquiv := (innerRing y).toEquiv
16   continuous_toFun := by change Continuous (fun x : S => (y : S) * x * ((y⁻¹ : Sˣ) : S)); fun_prop
17   continuous_invFun := by change Continuous (fun x : S => ((y⁻¹ : Sˣ) : S) * x * (y : S)); fun_prop
18 
19 end InnerTopology
20 
21 variable (F : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
22   [IsNonarchimedeanLocalField F]
23 variable (d : Type*) [Fintype d] [DecidableEq d]
24 
25 /-- Entrywise inclusion of the actual coordinate integral order. -/
26 def integralEmbedding : Matrix d d 𝒪[F] →+* Matrix d d F :=
27   RingHom.mapMatrix (valuation F).integer.subtype
28 
29 theorem integralEmbedding_open : IsOpenEmbedding (integralEmbedding F d) := by
30   have h : IsOpenEmbedding ((valuation F).integer.subtype : 𝒪[F] → F) :=
31     (Valuation.isOpen_integer (v := valuation F)).isOpenEmbedding_subtypeVal
32   exact Topology.IsOpenEmbedding.piMap
33     (fun _ : d => Topology.IsOpenEmbedding.piMap (fun _ : d => h))
34 
35 /-- Conjugation of an open additive lattice in the actual integral order has
36 open image in the external field matrix algebra. -/
37 theorem conjugate_lattice_open
38     (L : AddSubgroup (Matrix d d 𝒪[F])) (hL : IsOpen (L : Set (Matrix d d 𝒪[F])))
39     (y : GL d F) :
40     IsOpen (L.map ((innerRing y).toRingHom.comp (integralEmbedding F d)).toAddMonoidHom :
41       Set (Matrix d d F)) := by
42   change IsOpen ((fun x => innerHomeomorph y (integralEmbedding F d x)) '' (L : Set _))
43   simpa only [Set.image_image] using (innerHomeomorph y).isOpenMap _
44     ((integralEmbedding_open F d).isOpenMap _ hL)
45 
46 /-- An actual open additive lattice and its arbitrary conjugate contain a
47 common open ideal of the original compact integral order. The relevant
48 quotient is finite by compactness and openness. -/
49 theorem exists_conjugate_common_ideal
50     (L : AddSubgroup (Matrix d d 𝒪[F])) (hL : IsOpen (L : Set (Matrix d d 𝒪[F])))
51     (y : GL d F) :
52     ∃ I : Ideal 𝒪[F], IsOpen (I : Set 𝒪[F]) ∧
53       (I.matrix d).toAddSubgroup ≤ pullbackLattice (integralEmbedding F d) L
54         (L.map ((innerRing y).toRingHom.comp (integralEmbedding F d)).toAddMonoidHom) ∧
55       Finite (L ⧸ (I.matrix d).toAddSubgroup.addSubgroupOf L) := by
56   let M := pullbackLattice (integralEmbedding F d) L
57     (L.map ((innerRing y).toRingHom.comp (integralEmbedding F d)).toAddMonoidHom)
58   have hM : IsOpen (M : Set (Matrix d d 𝒪[F])) :=
59     hL.inter ((conjugate_lattice_open F d L hL y).preimage
60       (integralEmbedding_open F d).continuous)
61   obtain ⟨I, hI, hsub, hfin⟩ := exists_common_ideal_finite L M hL hM
62   exact ⟨I, hI, le_trans hsub inf_le_right, hfin⟩
63 
64 /-- The common-ideal and finite-quotient premises of the continuation110
65 one-plus theorem are discharged in the literal actual coordinate order. -/
66 theorem onePlus_conjugate_relIndex
67     (L : AddSubgroup (Matrix d d 𝒪[F])) (hopen : IsOpen (L : Set (Matrix d d 𝒪[F])))
68     (K : Subgroup (Matrix d d 𝒪[F])ˣ)
69     (hK : ∀ g : K, ((g : (Matrix d d 𝒪[F])ˣ) : Matrix d d 𝒪[F]) - 1 ∈ L)
70     (hL : ∀ x : L, ∃ g : K, ((g : (Matrix d d 𝒪[F])ˣ) : Matrix d d 𝒪[F]) = 1 + (x : _))
71     (y : GL d F) :
72     (K.map (Units.map ((innerRing y).toRingHom.comp (integralEmbedding F d)).toMonoidHom)).relIndex
73         (K.map (Units.map (integralEmbedding F d).toMonoidHom)) =
74       (L.map ((innerRing y).toRingHom.comp (integralEmbedding F d)).toAddMonoidHom).relIndex
75         (L.map (integralEmbedding F d).toAddMonoidHom) := by
76   obtain ⟨I, _, hI, hfin⟩ := exists_conjugate_common_ideal F d L hopen y
77   let : Finite (L ⧸ (I.matrix d).toAddSubgroup.addSubgroupOf L) := hfin
78   exact conjugate_intersection_relIndex_eq (integralEmbedding F d) y (I.matrix d) L K hK hL hI
79 
80 end PaperXI.ActualCoordinateDeepIdeal111

Back to source controls