PacketTopologyGeneral.lean

1 import PaperIRelease.PacketExactSequence
2 import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
3 import Mathlib.Analysis.Normed.Group.Quotient
4 import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
5 
6 /-!
7 # Banach packet exact sequences over arbitrary normed fields
8 
9 This includes trivially valued fields. Boundedness is an explicit hypothesis;
10 continuity alone is not substituted for boundedness. Every map is the actual
11 map from the algebraic packet exact sequence.
12 -/
13 
14 noncomputable section
15 set_option autoImplicit false
16 set_option linter.style.haveILetI false
17 
18 namespace Komorebi.PaperIRelease.GeneralPacketTopology
19 
20 open Komorebi.Foundation Komorebi.Foundation.LinearProjectorFamily
21 
22 universe u v w
23 variable {𝕜 : Type u} {X : Type v} {ι : Type w}
24 variable [NormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [Fintype ι]
25 
26 variable (P : LinearProjectorFamily 𝕜 X ι)
27 variable (hP : ∀ i, IsBoundedLinearMap 𝕜 (P.proj i))
28 variable (K : Submodule 𝕜 X) (hK : P.Preserves K)
29 
30 def projectorCLM (i : ι) : X →L[𝕜] X :=
31   { toLinearMap := P.proj i
32     cont := ((hP i).toContinuousLinearMap (P.proj i)).continuous }
33 
34 def restrictionCLM (i : ι) : K →L[𝕜] K where
35   toLinearMap := (P.restrictTo K hK).proj i
36   cont := ((projectorCLM P hP i).continuous.comp continuous_subtype_val).subtype_mk _
37 
38 def quotientProjectorCLM (i : ι) : (X ⧸ K) →L[𝕜] (X ⧸ K) :=
39   K.liftQL (K.mkQL.comp (projectorCLM P hP i)) (by
40     intro x hx
41     change K.mkQ (P.proj i x) = 0
42     exact (Submodule.Quotient.mk_eq_zero K).mpr (hK i x hx))
43 
44 @[simp] theorem quotientProjectorCLM_toLinearMap (i : ι) :
45     (quotientProjectorCLM P hP K hK i).toLinearMap = (P.descendTo K hK).proj i := rfl
46 
47 /-- Every original norm bound passes to the actual quotient norm. -/
48 theorem quotient_bound (i : ι) (C : ℝ) (hC : 0 ≤ C)
49     (hbound : ∀ x : X, ‖P.proj i x‖ ≤ C * ‖x‖) (z : X ⧸ K) :
50     ‖quotientProjectorCLM P hP K hK i z‖ ≤ C * ‖z‖ := by
51   apply le_of_forall_pos_le_add
52   intro ε hε
53   obtain ⟨x, hx, hnorm⟩ := Submodule.Quotient.norm_mk_lt z
54     (show 0 < ε / (C + 1) by positivity)
55   have hbase : ‖quotientProjectorCLM P hP K hK i z‖ ≤ C * ‖x‖ := by
56     rw [← hx]
57     exact (Submodule.Quotient.norm_mk_le K (P.proj i x)).trans (hbound x)
58   have hmul : C * ‖x‖ ≤ C * (‖z‖ + ε / (C + 1)) :=
59     mul_le_mul_of_nonneg_left hnorm.le hC
60   have hsmall : C * (ε / (C + 1)) ≤ ε := by
61     rw [← mul_div_assoc]
62     apply (div_le_iff₀ (show 0 < C + 1 by positivity)).mpr
63     nlinarith
64   exact hbase.trans (hmul.trans (by nlinarith))
65 
66 include hP in
67 theorem quotientProjector_bounded (i : ι) :
68     IsBoundedLinearMap 𝕜 ((P.descendTo K hK).proj i) := by
69   obtain ⟨C, hC, hbound⟩ := (hP i).bound
70   exact ((P.descendTo K hK).proj i).isLinear.with_bound C
71     (quotient_bound P hP K hK i C hC.le hbound)
72 
73 include hP in
74 theorem restrictedProjector_bounded (i : ι) :
75     IsBoundedLinearMap 𝕜 ((P.restrictTo K hK).proj i) := by
76   obtain ⟨C, _, hbound⟩ := (hP i).bound
77   exact ((P.restrictTo K hK).proj i).isLinear.with_bound C
78     (fun x ↦ hbound (x : X))
79 
80 /-- The bounded additive operator norm is available even over a trivially
81 valued scalar field and equals the usual infimum of valid operator bounds. -/
82 def projectorNormedHom (i : ι) : NormedAddGroupHom X X :=
83   (P.proj i).toAddMonoidHom.mkNormedAddGroupHom
84     (Classical.choose (hP i).bound) (Classical.choose_spec (hP i).bound).2
85 
86 theorem quotient_bound_operatorNorm (i : ι) (z : X ⧸ K) :
87     ‖quotientProjectorCLM P hP K hK i z‖ ≤ ‖projectorNormedHom P hP i‖ * ‖z‖ :=
88   quotient_bound P hP K hK i _ (norm_nonneg _) (fun x ↦ (projectorNormedHom P hP i).le_opNorm x) z
89 
90 def packetInclusionCLM (i : ι) :
91     LinearMap.range ((P.restrictTo K hK).proj i) →L[𝕜] LinearMap.range (P.proj i) :=
92   (K.subtypeL.comp (LinearMap.range ((P.restrictTo K hK).proj i)).subtypeL).codRestrict
93     (LinearMap.range (P.proj i)) (fun x ↦ (P.packetInclusion K hK i x).property)
94 
95 def packetQuotientCLM (i : ι) :
96     LinearMap.range (P.proj i) →L[𝕜] LinearMap.range ((P.descendTo K hK).proj i) :=
97   (K.mkQL.comp (LinearMap.range (P.proj i)).subtypeL).codRestrict
98     (LinearMap.range ((P.descendTo K hK).proj i))
99     (fun x ↦ (P.packetQuotientMap K hK i x).property)
100 
101 theorem packetInclusion_bounded (i : ι) :
102     IsBoundedLinearMap 𝕜 (P.packetInclusion K hK i) :=
103   (P.packetInclusion K hK i).isLinear.with_bound 1 (fun x ↦ by
104     change ‖((x : LinearMap.range ((P.restrictTo K hK).proj i)) : K)‖ ≤ 1 * ‖x‖
105     simp)
106 
107 theorem packetQuotient_bounded (i : ι) :
108     IsBoundedLinearMap 𝕜 (P.packetQuotientMap K hK i) :=
109   (P.packetQuotientMap K hK i).isLinear.with_bound 1 (fun x ↦ by
110     change ‖(Submodule.Quotient.mk (x : X) : X ⧸ K)‖ ≤ 1 * ‖x‖
111     simpa using Submodule.Quotient.norm_mk_le K (x : X))
112 
113 include hP in
114 theorem isClosed_packet (i : ι) : IsClosed (LinearMap.range (P.proj i) : Set X) := by
115   apply ContinuousLinearMap.IsIdempotentElem.isClosed_range (p := projectorCLM P hP i)
116   apply ContinuousLinearMap.ext
117   intro x
118   exact P.idempotent i x
119 
120 variable [hclosed : IsClosed (K : Set X)] [CompleteSpace X]
121 
122 include hP in
123 theorem packet_spaces_complete (i : ι) :
124     CompleteSpace (LinearMap.range ((P.restrictTo K hK).proj i)) ∧
125       CompleteSpace (LinearMap.range (P.proj i)) ∧
126       CompleteSpace (LinearMap.range ((P.descendTo K hK).proj i)) := by
127   letI : IsClosed (LinearMap.range ((P.restrictTo K hK).proj i) : Set K) :=
128     isClosed_packet (P.restrictTo K hK) (restrictedProjector_bounded P hP K hK) i
129   letI : IsClosed (LinearMap.range (P.proj i) : Set X) := isClosed_packet P hP i
130   letI : IsClosed (LinearMap.range ((P.descendTo K hK).proj i) : Set (X ⧸ K)) :=
131     isClosed_packet (P.descendTo K hK) (quotientProjector_bounded P hP K hK) i
132   exact ⟨inferInstance, inferInstance, inferInstance⟩
133 
134 include hP in
135 /-- The complete printed Banach packet exact sequence over an arbitrary
136 normed field, including a trivially valued field. -/
137 theorem banach_packet_shortExact (i : ι) :
138     CompleteSpace (LinearMap.range ((P.restrictTo K hK).proj i)) ∧
139       CompleteSpace (LinearMap.range (P.proj i)) ∧
140       CompleteSpace (LinearMap.range ((P.descendTo K hK).proj i)) ∧
141       IsBoundedLinearMap 𝕜 (P.packetInclusion K hK i) ∧
142       IsBoundedLinearMap 𝕜 (P.packetQuotientMap K hK i) ∧
143       Function.Injective (P.packetInclusion K hK i) ∧
144       LinearMap.range (P.packetInclusion K hK i) = LinearMap.ker (P.packetQuotientMap K hK i) ∧
145       Function.Surjective (P.packetQuotientMap K hK i) ∧
146       IsBoundedLinearMap 𝕜 ((P.descendTo K hK).proj i) := by
147   obtain ⟨hc1, hc2, hc3⟩ := packet_spaces_complete P hP K hK i
148   obtain ⟨hinj, hexact, hsurj⟩ := P.packet_shortExact K hK i
149   exact ⟨hc1, hc2, hc3, packetInclusion_bounded P K hK i, packetQuotient_bounded P K hK i,
150     hinj, hexact, hsurj, quotientProjector_bounded P hP K hK i⟩
151 
152 end Komorebi.PaperIRelease.GeneralPacketTopology
153 
154 #print axioms Komorebi.PaperIRelease.GeneralPacketTopology.banach_packet_shortExact
155 #print axioms Komorebi.PaperIRelease.GeneralPacketTopology.quotient_bound_operatorNorm

Back to source controls