PacketExactSequence.lean

1 import PaperIRelease.PacketDescent
2 
3 set_option autoImplicit false
4 
5 namespace Komorebi.Foundation.LinearProjectorFamily
6 
7 universe u v w
8 
9 variable {R : Type u} {M : Type v} {ι : Type w}
10 variable [Ring R] [AddCommGroup M] [Module R M] [Fintype ι]
11 
12 /-- Exact coordinates in the literal finite direct sum of the actual packet
13 ranges, using the standard finite-product/direct-sum equivalence. -/
14 noncomputable def exactPacketDirectSumCoordinates
15     (P : LinearProjectorFamily R M ι) :
16     M ≃ₗ[R] DirectSum ι (fun i ↦ LinearMap.range (P.proj i)) := by
17   classical
18   exact P.exactPacketCoordinates.trans
19     (DirectSum.linearEquivFunOnFintype R ι (fun i ↦ LinearMap.range (P.proj i))).symm
20 
21 /-- Inclusion of the actual restricted packet into its ambient packet. -/
22 def packetInclusion (P : LinearProjectorFamily R M ι) (K : Submodule R M)
23     (hK : P.Preserves K) (i : ι) :
24     LinearMap.range ((P.restrictTo K hK).proj i) →ₗ[R]
25       LinearMap.range (P.proj i) where
26   toFun x := ⟨(x : K), by
27     obtain ⟨y, hy⟩ := x.property
28     exact ⟨(y : M), congrArg (fun z : K ↦ (z : M)) hy⟩⟩
29   map_add' _ _ := rfl
30   map_smul' _ _ := rfl
31 
32 theorem packetInclusion_injective
33     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
34     (hK : P.Preserves K) (i : ι) :
35     Function.Injective (P.packetInclusion K hK i) := by
36   intro x y h
37   apply Subtype.ext
38   apply Subtype.ext
39   exact congrArg (fun z : LinearMap.range (P.proj i) ↦ (z : M)) h
40 
41 /-- The packet sequence is exact at its middle term. -/
42 theorem packet_sequence_exact
43     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
44     (hK : P.Preserves K) (i : ι) :
45     LinearMap.range (P.packetInclusion K hK i) =
46       LinearMap.ker (P.packetQuotientMap K hK i) := by
47   rw [P.packetQuotientMap_ker]
48   ext x
49   constructor
50   · rintro ⟨y, rfl⟩
51     exact (y : K).property
52   · intro hx
53     let y : K := ⟨(x : M), hx⟩
54     have hy : y ∈ LinearMap.range ((P.restrictTo K hK).proj i) := by
55       rw [P.restrictTo_range]
56       exact x.property
57     exact ⟨⟨y, hy⟩, rfl⟩
58 
59 /-- All three conditions for the actual short exact sequence of one packet. -/
60 theorem packet_shortExact
61     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
62     (hK : P.Preserves K) (i : ι) :
63     Function.Injective (P.packetInclusion K hK i) ∧
64       LinearMap.range (P.packetInclusion K hK i) =
65         LinearMap.ker (P.packetQuotientMap K hK i) ∧
66       Function.Surjective (P.packetQuotientMap K hK i) :=
67   ⟨P.packetInclusion_injective K hK i, P.packet_sequence_exact K hK i,
68     P.packetQuotientMap_surjective K hK i⟩
69 
70 /-- The finite product of the packet inclusions (equal to the finite direct
71 sum under the canonical finite-product/direct-sum equivalence). -/
72 def packetCoordinateInclusion
73     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
74     (hK : P.Preserves K) :
75     (P.restrictTo K hK).PacketSpace →ₗ[R] P.PacketSpace where
76   toFun x i := P.packetInclusion K hK i (x i)
77   map_add' x y := by funext i; exact (P.packetInclusion K hK i).map_add _ _
78   map_smul' a x := by funext i; exact (P.packetInclusion K hK i).map_smul _ _
79 
80 /-- The finite product of the actual packet quotient maps. -/
81 def packetCoordinateQuotient
82     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
83     (hK : P.Preserves K) :
84     P.PacketSpace →ₗ[R] (P.descendTo K hK).PacketSpace where
85   toFun x i := P.packetQuotientMap K hK i (x i)
86   map_add' x y := by funext i; exact (P.packetQuotientMap K hK i).map_add _ _
87   map_smul' a x := by funext i; exact (P.packetQuotientMap K hK i).map_smul _ _
88 
89 /-- Exact packet coordinates identify the original inclusion with the product
90 of the packetwise inclusions. -/
91 theorem packetCoordinateInclusion_natural
92     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
93     (hK : P.Preserves K) :
94     (P.packetCoordinateInclusion K hK).comp (P.restrictTo K hK).rangeAnalysis =
95       P.rangeAnalysis.comp K.subtype := by
96   ext x i
97   rfl
98 
99 /-- Exact packet coordinates identify the original quotient map with the
100 product of the packetwise quotient maps. -/
101 theorem packetCoordinateQuotient_natural
102     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
103     (hK : P.Preserves K) :
104     (P.packetCoordinateQuotient K hK).comp P.rangeAnalysis =
105       (P.descendTo K hK).rangeAnalysis.comp K.mkQ := by
106   ext x i
107   rfl
108 
109 /-- The finite product of the packet sequences is itself short exact. Together
110 with the two naturality identities and `exactPacketCoordinates`, this is the
111 decomposition of the entire exact sequence into its packet sequences. -/
112 theorem packetCoordinate_shortExact
113     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
114     (hK : P.Preserves K) :
115     Function.Injective (P.packetCoordinateInclusion K hK) ∧
116       LinearMap.range (P.packetCoordinateInclusion K hK) =
117         LinearMap.ker (P.packetCoordinateQuotient K hK) ∧
118       Function.Surjective (P.packetCoordinateQuotient K hK) := by
119   classical
120   refine ⟨?_, ?_, ?_⟩
121   · intro x y h
122     funext i
123     exact P.packetInclusion_injective K hK i (congrFun h i)
124   · ext x
125     constructor
126     · rintro ⟨y, rfl⟩
127       change (P.packetCoordinateQuotient K hK)
128         ((P.packetCoordinateInclusion K hK) y) = 0
129       funext i
130       have hi : P.packetInclusion K hK i (y i) ∈
131           LinearMap.ker (P.packetQuotientMap K hK i) := by
132         rw [← P.packet_sequence_exact]
133         exact ⟨y i, rfl⟩
134       exact hi
135     · intro hx
136       have hi (i : ι) : ∃ y, P.packetInclusion K hK i y = x i := by
137         have hz : P.packetQuotientMap K hK i (x i) = 0 :=
138           congrFun hx i
139         have hm : x i ∈ LinearMap.range (P.packetInclusion K hK i) := by
140           rw [P.packet_sequence_exact]
141           exact hz
142         exact hm
143       exact ⟨fun i ↦ Classical.choose (hi i),
144         funext (fun i ↦ Classical.choose_spec (hi i))⟩
145   · intro y
146     choose x hx using fun i ↦ P.packetQuotientMap_surjective K hK i (y i)
147     exact ⟨x, funext hx⟩
148 
149 end Komorebi.Foundation.LinearProjectorFamily
150 
151 #print axioms Komorebi.Foundation.LinearProjectorFamily.packet_shortExact
152 #print axioms Komorebi.Foundation.LinearProjectorFamily.packetCoordinate_shortExact
153 #print axioms Komorebi.Foundation.LinearProjectorFamily.packetCoordinateInclusion_natural
154 #print axioms Komorebi.Foundation.LinearProjectorFamily.packetCoordinateQuotient_natural

Back to source controls