FiniteCarrier.lean

1 import Mathlib.RingTheory.Artinian.Module
2 import Mathlib.LinearAlgebra.FiniteDimensional.Basic
3 
4 /-! Paper XII, 8.7–8.8. Index zero is the manuscript's first level. -/
5 namespace PaperXII.FiniteCarrier
6 
7 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V]
8 
9 /-- The entire descending submodule chain eventually stabilizes. -/
10 theorem descending_stabilizes (W : ℕ → Submodule K V) (hW : Antitone W) :
11     ∃ N, ∀ n, N ≤ n → W n = W N := by
12   obtain ⟨N, hN⟩ := IsArtinian.monotone_stabilizes (R := K) (M := V) ⟨W, hW⟩
13   exact ⟨N, fun n hn ↦ (hN n hn).symm⟩
14 
15 /-- The stable value equals the intersection of all levels. -/
16 theorem exists_iInf_eq (W : ℕ → Submodule K V) (hW : Antitone W) :
17     ∃ N, (⨅ n, W n) = W N ∧ ∀ n, N ≤ n → W n = W N := by
18   obtain ⟨N, hN⟩ := descending_stabilizes W hW
19   refine ⟨N, le_antisymm (iInf_le W N) ?_, hN⟩
20   apply le_iInf
21   intro n
22   rcases le_total n N with hn | hn
23   · exact hW hn
24   · exact (hN n hn).symm.le
25 
26 /-- Nonzero levels in a descending finite-dimensional chain have nonzero intersection. -/
27 theorem iInf_ne_bot (W : ℕ → Submodule K V) (hW : Antitone W)
28     (hne : ∀ n, W n ≠ ⊥) : (⨅ n, W n) ≠ ⊥ := by
29   obtain ⟨N, hN, _⟩ := exists_iInf_eq W hW
30   rw [hN]
31   exact hne N
32 
33 /-- A zero intersection is witnessed at a finite level. -/
34 theorem exists_eq_bot_of_iInf_eq_bot (W : ℕ → Submodule K V) (hW : Antitone W)
35     (hzero : (⨅ n, W n) = ⊥) : ∃ n, W n = ⊥ := by
36   obtain ⟨N, hN, _⟩ := exists_iInf_eq W hW
37   exact ⟨N, hN.symm.trans hzero⟩
38 
39 omit [FiniteDimensional K V] in
40 /-- The absorption relation forces the packet ranges to descend.
41 Idempotence and the reverse absorption relation are not needed for this implication. -/
42 theorem ranges_antitone (e : ℕ → Module.End K V)
43     (habs : ∀ n, (e n).comp (e (n + 1)) = e (n + 1)) :
44     Antitone (fun n ↦ LinearMap.range (e n)) := by
45   apply antitone_nat_of_succ_le
46   intro n y hy
47   obtain ⟨v, rfl⟩ := hy
48   refine ⟨e (n + 1) v, ?_⟩
49   exact LinearMap.congr_fun (habs n) v
50 
51 /-- Manuscript 8.7, with stabilization and nonzero intersection in one statement. -/
52 theorem nested_packets (e : ℕ → Module.End K V)
53     (habs : ∀ n, (e n).comp (e (n + 1)) = e (n + 1))
54     (hne : ∀ n, LinearMap.range (e n) ≠ ⊥) :
55     (∃ N, ∀ n, N ≤ n → LinearMap.range (e n) = LinearMap.range (e N)) ∧
56       (⨅ n, LinearMap.range (e n)) ≠ ⊥ :=
57   ⟨descending_stabilizes _ (ranges_antitone e habs),
58     iInf_ne_bot _ (ranges_antitone e habs) hne⟩
59 
60 /-- Manuscript 8.8. This holds without assuming the individual ranges are nonzero. -/
61 theorem finite_incompatibility_witness (e : ℕ → Module.End K V)
62     (habs : ∀ n, (e n).comp (e (n + 1)) = e (n + 1))
63     (hzero : (⨅ n, LinearMap.range (e n)) = ⊥) :
64     ∃ n, LinearMap.range (e n) = ⊥ :=
65   exists_eq_bot_of_iInf_eq_bot _ (ranges_antitone e habs) hzero
66 
67 end PaperXII.FiniteCarrier

Back to source controls