PacketBoundaryTests.lean

1 import PaperIRelease.ExactSequences
2 import PaperIRelease.PacketExactSequence
3 import PaperIRelease.PacketTopology
4 
5 /-! Boundary assertions for the new exact-sequence and packet-descent block. -/
6 
7 set_option autoImplicit false
8 
9 namespace Komorebi.PaperIRelease.PacketBoundaryTests
10 
11 open Komorebi.Foundation Komorebi.Foundation.LinearProjectorFamily
12 open Komorebi.SeedRankBasics
13 
14 universe u v w
15 
16 section General
17 
18 variable {R : Type u} {M : Type v} {ι : Type w}
19 variable [Ring R] [AddCommGroup M] [Module R M] [Fintype ι]
20 
21 theorem all_preserve_bot (P : LinearProjectorFamily R M ι) : P.Preserves ⊥ := by
22   intro i x hx
23   have hx0 : x = 0 := hx
24   simp [hx0]
25 
26 theorem all_preserve_top (P : LinearProjectorFamily R M ι) : P.Preserves ⊤ := by
27   intro i x _
28   trivial
29 
30 theorem restriction_to_zero_is_zero (P : LinearProjectorFamily R M ι) (i : ι) :
31     (P.restrictTo ⊥ (all_preserve_bot P)).proj i = 0 := by
32   apply Subsingleton.elim
33 
34 theorem quotient_by_whole_is_zero (P : LinearProjectorFamily R M ι) (i : ι) :
35     (P.descendTo ⊤ (all_preserve_top P)).proj i = 0 := by
36   apply Subsingleton.elim
37 
38 theorem whole_quotient_has_no_nonzero_packets
39     (P : LinearProjectorFamily R M ι) :
40     IsEmpty (P.descendTo ⊤ (all_preserve_top P)).NonzeroIndex :=
41   ⟨fun i ↦ i.property (quotient_by_whole_is_zero P i.val)⟩
42 
43 theorem zero_restriction_has_no_nonzero_packets
44     (P : LinearProjectorFamily R M ι) :
45     IsEmpty (P.restrictTo ⊥ (all_preserve_bot P)).NonzeroIndex :=
46   ⟨fun i ↦ i.property (restriction_to_zero_is_zero P i.val)⟩
47 
48 theorem whole_submodule_packet_exact
49     (P : LinearProjectorFamily R M ι) (i : ι) :
50     LinearMap.range (P.packetInclusion ⊤ (all_preserve_top P) i) =
51       LinearMap.ker (P.packetQuotientMap ⊤ (all_preserve_top P) i) :=
52   P.packet_sequence_exact ⊤ (all_preserve_top P) i
53 
54 theorem zero_submodule_packet_exact
55     (P : LinearProjectorFamily R M ι) (i : ι) :
56     LinearMap.range (P.packetInclusion ⊥ (all_preserve_bot P) i) =
57       LinearMap.ker (P.packetQuotientMap ⊥ (all_preserve_bot P) i) :=
58   P.packet_sequence_exact ⊥ (all_preserve_bot P) i
59 
60 end General
61 
62 /-- The exact-sequence rank theorem applies to a countably generated free
63 integer module, so no hidden finite-dimensional instance is being used. -/
64 theorem infinite_free_quotient_bounds (K : Submodule ℤ (ℕ →₀ ℤ)) :
65     seedRank ℤ ((ℕ →₀ ℤ) ⧸ K) ≤ seedRank ℤ (ℕ →₀ ℤ) ∧
66       seedRank ℤ (ℕ →₀ ℤ) ≤ seedRank ℤ K + seedRank ℤ ((ℕ →₀ ℤ) ⧸ K) :=
67   submodule_quotient_seedRank_bounds K
68 
69 /-- A nontrivial family exists on a zero module even with no indices. -/
70 def emptyFamily : LinearProjectorFamily ℤ (Fin 0 → ℤ) (Fin 0) where
71   proj i := Fin.elim0 i
72   idempotent i := Fin.elim0 i
73   orthogonal := by intro i; exact Fin.elim0 i
74   complete x := Subsingleton.elim _ _
75 
76 theorem empty_family_packet_exact :
77     Function.Injective (emptyFamily.packetCoordinateInclusion ⊥
78       (all_preserve_bot emptyFamily)) ∧
79       LinearMap.range (emptyFamily.packetCoordinateInclusion ⊥
80         (all_preserve_bot emptyFamily)) =
81         LinearMap.ker (emptyFamily.packetCoordinateQuotient ⊥
82           (all_preserve_bot emptyFamily)) ∧
83       Function.Surjective (emptyFamily.packetCoordinateQuotient ⊥
84         (all_preserve_bot emptyFamily)) :=
85   emptyFamily.packetCoordinate_shortExact ⊥ (all_preserve_bot emptyFamily)
86 
87 /-- The first coordinate line is preserved by the packet projections, but
88 not by the coordinate swap. -/
89 def horizontal : Submodule ℤ (ℤ × ℤ) := LinearMap.ker (LinearMap.snd ℤ ℤ ℤ)
90 
91 def swapEnd : Module.End ℤ (ℤ × ℤ) := (LinearEquiv.prodComm ℤ ℤ ℤ).toLinearMap
92 
93 /-- A concrete obstruction: without invariance an ambient operator need not
94 admit any quotient operator intertwining with the quotient map. -/
95 theorem coordinate_swap_cannot_descend :
96     ¬ ∃ U : Module.End ℤ ((ℤ × ℤ) ⧸ horizontal),
97       U.comp horizontal.mkQ = horizontal.mkQ.comp swapEnd := by
98   rintro ⟨U, hU⟩
99   have hz : horizontal.mkQ (1, 0) = 0 :=
100     (Submodule.Quotient.mk_eq_zero horizontal).mpr (by rfl)
101   have h : horizontal.mkQ (0, 1) = 0 := by
102     have hpoint := congrArg (fun f : (ℤ × ℤ) →ₗ[ℤ] (ℤ × ℤ) ⧸ horizontal ↦
103       f (1, 0)) hU
104     change U (horizontal.mkQ (1, 0)) = horizontal.mkQ (0, 1) at hpoint
105     simpa [hz] using hpoint.symm
106   have hmem := (Submodule.Quotient.mk_eq_zero horizontal).mp h
107   change (1 : ℤ) = 0 at hmem
108   exact one_ne_zero hmem
109 
110 /-- The quotient norm estimate includes the degenerate zero quotient. -/
111 theorem whole_quotient_projector_norm_zero
112     {𝕜 : Type u} {X : Type v} {ι : Type w}
113     [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
114     [Fintype ι] (P : LinearProjectorFamily 𝕜 X ι)
115     (hP : ∀ i, Continuous (P.proj i)) (i : ι) :
116     ‖P.quotientProjectorCLM hP ⊤ (all_preserve_top P) i‖ = 0 := by
117   have hzero : P.quotientProjectorCLM hP ⊤ (all_preserve_top P) i = 0 :=
118     Subsingleton.elim _ _
119   rw [hzero, norm_zero]
120 
121 /-- In the zero-submodule case the constructed bounded equivalence is still
122 the literal quotient map on every source-packet representative. -/
123 theorem zero_submodule_bounded_equiv_mk
124     {𝕜 : Type u} {X : Type v} {ι : Type w}
125     [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
126     [Fintype ι] (P : LinearProjectorFamily 𝕜 X ι)
127     (hP : ∀ i, Continuous (P.proj i)) (i : ι)
128     (x : LinearMap.range (P.proj i)) :
129     (P.packetQuotientEquivL hP ⊥ (all_preserve_bot P) i (Submodule.Quotient.mk x) :
130       X ⧸ (⊥ : Submodule 𝕜 X)) = (⊥ : Submodule 𝕜 X).mkQ (x : X) := rfl
131 
132 end Komorebi.PaperIRelease.PacketBoundaryTests
133 
134 #print axioms Komorebi.PaperIRelease.PacketBoundaryTests.infinite_free_quotient_bounds
135 #print axioms Komorebi.PaperIRelease.PacketBoundaryTests.empty_family_packet_exact
136 #print axioms Komorebi.PaperIRelease.PacketBoundaryTests.coordinate_swap_cannot_descend
137 #print axioms Komorebi.PaperIRelease.PacketBoundaryTests.whole_quotient_projector_norm_zero

Back to source controls