ActualOnePlusTopology111.lean

1 import PaperXI.ActualCoordinateDeepIdeal111
2 import PaperXI.ActualIntegralGeneralLinear
3 import Mathlib.Topology.Algebra.IsOpenUnits
4 import Mathlib.Topology.Instances.Matrix
5 
6 /-! Openness of an actual one-plus group supplies additive lattice openness. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.ActualOnePlusTopology111
10 open Matrix Topology
11 open PaperXI.ActualCoordinateDeepIdeal111 PaperXI.OnePlusIntersection110
12 
13 section MatrixUnits
14 variable (F d : Type*) [Field F] [TopologicalSpace F] [IsTopologicalRing F]
15   [ContinuousInv₀ F] [T1Space F] [Fintype d] [DecidableEq d]
16 
17 /-- The actual matrix unit topology agrees with the open nonzero-determinant
18 subspace, using continuity of the nonsingular matrix inverse there. -/
19 def matrixUnitsHomeomorph : (Matrix d d F)ˣ ≃ₜ {A : Matrix d d F | A.det ≠ 0} where
20   toFun u := ⟨u, (Matrix.isUnits_det_units u).ne_zero⟩
21   invFun A := ⟨A.1, A.1⁻¹,
22     Matrix.mul_nonsing_inv A.1 (isUnit_iff_ne_zero.mpr A.2),
23     Matrix.nonsing_inv_mul A.1 (isUnit_iff_ne_zero.mpr A.2)⟩
24   left_inv u := by apply Units.ext; rfl
25   right_inv A := rfl
26   continuous_toFun := Units.continuous_val.subtype_mk _
27   continuous_invFun := by
28     apply Units.continuous_iff.mpr
29     refine ⟨continuous_subtype_val, ?_⟩
30     change Continuous (fun A : {A : Matrix d d F | A.det ≠ 0} => A.1⁻¹)
31     apply continuous_iff_continuousAt.mpr
32     intro A
33     apply (continuousAt_matrix_inv A.1 ?_).comp continuous_subtype_val.continuousAt
34     simpa only [Ring.inverse_eq_inv'] using (continuousAt_inv₀ A.2)
35 
36 /-- This is derived for actual matrices; no matrix open-units instance is
37 assumed as an input. -/
38 theorem matrix_isOpenUnits : IsOpenUnits (Matrix d d F) := by
39   have hoF : IsOpen {x : F | x ≠ 0} := isOpen_ne
40   have ho : IsOpen {A : Matrix d d F | A.det ≠ 0} :=
41     hoF.preimage continuous_id.matrix_det
42   exact ⟨ho.isOpenEmbedding_subtypeVal.comp (matrixUnitsHomeomorph F d).isOpenEmbedding⟩
43 
44 end MatrixUnits
45 
46 section ActualLocalField
47 open ValuativeRel
48 variable (F : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
49   [IsNonarchimedeanLocalField F]
50 variable (d : Type*) [Fintype d] [DecidableEq d]
51 
52 /-- Actual local-field matrices have an open unit embedding. -/
53 theorem actual_matrix_isOpenUnits : IsOpenUnits (Matrix d d F) := by
54   let : T2Space F := PaperXI.ActualIntegralGeneralLinear.field_t2Space F
55   exact matrix_isOpenUnits F d
56 
57 /-- Exact one-plus carrier identities turn openness of the actual ambient
58 image group into openness of its additive integral-order lattice. -/
59 theorem additive_open_of_image_group_open
60     (L : AddSubgroup (Matrix d d 𝒪[F])) (K : Subgroup (Matrix d d 𝒪[F])ˣ)
61     (hK : ∀ g : K, ((g : (Matrix d d 𝒪[F])ˣ) : Matrix d d 𝒪[F]) - 1 ∈ L)
62     (hL : ∀ x : L, ∃ g : K, ((g : (Matrix d d 𝒪[F])ˣ) : Matrix d d 𝒪[F]) = 1 + (x : _))
63     (hopen : IsOpen (K.map (Units.map (integralEmbedding F d).toMonoidHom) :
64       Set (GL d F))) : IsOpen (L : Set (Matrix d d 𝒪[F])) := by
65   let : IsOpenUnits (Matrix d d F) := actual_matrix_isOpenUnits F d
66   let f := integralEmbedding F d
67   let H := K.map (Units.map f.toMonoidHom)
68   have hu : IsOpen ((Units.val : (Matrix d d F)ˣ → Matrix d d F) '' (H : Set _)) :=
69     IsOpenUnits.isOpenEmbedding_unitsVal.isOpenMap _ hopen
70   have hoff : IsOpen ((fun x : Matrix d d F => x - 1) ''
71       ((Units.val : (Matrix d d F)ˣ → Matrix d d F) '' (H : Set _))) :=
72     (Homeomorph.subRight (1 : Matrix d d F)).isOpenMap _ hu
73   have he : ((fun x : Matrix d d F => x - 1) ''
74       ((Units.val : (Matrix d d F)ˣ → Matrix d d F) '' (H : Set _))) =
75         (L.map f.toAddMonoidHom : Set (Matrix d d F)) := by
76     ext x
77     constructor
78     · rintro ⟨_, ⟨g, hg, rfl⟩, rfl⟩
79       exact mapped_offsets f L K hK ⟨g, hg⟩
80     · intro hx
81       obtain ⟨g, hg⟩ := mapped_onePlus f L K hL ⟨x, hx⟩
82       refine ⟨(g : (Matrix d d F)ˣ), ⟨g, g.property, rfl⟩, ?_⟩
83       rw [hg]
84       simp
85   rw [he] at hoff
86   have hinj : Function.Injective f := Matrix.map_injective Subtype.val_injective
87   have hpre : f ⁻¹' (L.map f.toAddMonoidHom : Set (Matrix d d F)) =
88       (L : Set (Matrix d d 𝒪[F])) := by
89     ext x
90     constructor
91     · rintro ⟨z, hz, he⟩
92       exact hinj he ▸ hz
93     · intro hx
94       exact ⟨x, hx, rfl⟩
95   rw [← hpre]
96   exact hoff.preimage (integralEmbedding_open F d).continuous
97 
98 /-- Both lattice openness and the common ideal/finite quotient now follow from
99 actual group openness and exact one-plus carriers. -/
100 theorem onePlus_conjugate_relIndex_of_group_open
101     (L : AddSubgroup (Matrix d d 𝒪[F])) (K : Subgroup (Matrix d d 𝒪[F])ˣ)
102     (hK : ∀ g : K, ((g : (Matrix d d 𝒪[F])ˣ) : Matrix d d 𝒪[F]) - 1 ∈ L)
103     (hL : ∀ x : L, ∃ g : K, ((g : (Matrix d d 𝒪[F])ˣ) : Matrix d d 𝒪[F]) = 1 + (x : _))
104     (hopen : IsOpen (K.map (Units.map (integralEmbedding F d).toMonoidHom) : Set (GL d F)))
105     (y : GL d F) :
106     (K.map (Units.map ((innerRing y).toRingHom.comp (integralEmbedding F d)).toMonoidHom)).relIndex
107         (K.map (Units.map (integralEmbedding F d).toMonoidHom)) =
108       (L.map ((innerRing y).toRingHom.comp (integralEmbedding F d)).toAddMonoidHom).relIndex
109         (L.map (integralEmbedding F d).toAddMonoidHom) :=
110   onePlus_conjugate_relIndex F d L
111     (additive_open_of_image_group_open F d L K hK hL hopen) K hK hL y
112 
113 end ActualLocalField
114 end PaperXI.ActualOnePlusTopology111

Back to source controls