FibreRefinement.lean

1 import KomorebiVerification.ProjectorCore
2 
3 /-!
4 # Concrete fibre projectors and exact refinement
5 
6 This file upgrades the pointwise masks from `ProjectorCore` to genuine linear
7 projectors.  It also proves the refinement law from independently defined
8 coarse and fine masks: a coarse fibre is the sum of the fine fibres mapping to
9 it.  In particular, the conclusion is not stored as a structure field.
10 -/
11 
12 set_option autoImplicit false
13 
14 namespace Komorebi.Packet
15 
16 universe u v w x
17 
18 variable {R : Type u} {M : Type v} {α : Type w} {β : Type x}
19 
20 /-- The pointwise fibre mask, regarded as an `R`-linear endomorphism. -/
21 def fibreLinearProj
22     [Semiring R] [AddCommMonoid M] [Module R M] [DecidableEq β]
23     (address : α → β) (b : β) : Module.End R (α → M) where
24   toFun := fibreProj address b
25   map_add' x y := by
26     funext a
27     by_cases h : address a = b <;> simp [fibreProj, h]
28   map_smul' r x := by
29     funext a
30     by_cases h : address a = b <;> simp [fibreProj, h]
31 
32 @[simp] theorem fibreLinearProj_apply
33     [Semiring R] [AddCommMonoid M] [Module R M] [DecidableEq β]
34     (address : α → β) (b : β) (x : α → M) :
35     fibreLinearProj (R := R) address b x = fibreProj address b x :=
36   rfl
37 
38 /-- Every finite address map induces a complete orthogonal projector family. -/
39 def fibreLinearProjectorFamily
40     [Semiring R] [AddCommMonoid M] [Module R M]
41     [DecidableEq β] [Fintype β]
42     (address : α → β) :
43     Komorebi.Foundation.LinearProjectorFamily R (α → M) β where
44   proj := fibreLinearProj (R := R) address
45   idempotent b x := fibreProj_idempotent address b x
46   orthogonal hbc x := fibreProj_orthogonal address hbc x
47   complete x := fibreProj_reconstruction address x
48 
49 /--
50 Exact nested refinement for fibre masks.  The coarse mask on `merge ∘ fine`
51 equals the sum of all independently defined fine masks in the selected fibre.
52 -/
53 theorem fibreProj_refinement
54     {γ : Type*}
55     [DecidableEq β] [DecidableEq γ] [Fintype γ] [AddCommMonoid M]
56     (fine : α → γ) (merge : γ → β) (b : β) (x : α → M) :
57     fibreProj (fun a => merge (fine a)) b x =
58       ∑ c, if merge c = b then fibreProj fine c x else 0 := by
59   funext a
60   classical
61   simp only [fibreProj]
62   rw [Finset.sum_apply]
63   simp only [ite_apply, Pi.zero_apply]
64   simp only [fibreProj]
65   symm
66   have hzero : ∀ c : γ, c ≠ fine a →
67       (if merge c = b then if fine a = c then x a else 0 else 0) = 0 := by
68     intro c hca
69     simp [Ne.symm hca]
70   simpa using
71     (Fintype.sum_eq_single
72       (f := fun c : γ =>
73         if merge c = b then if fine a = c then x a else 0 else 0)
74       (fine a) hzero)
75 
76 /-- The same refinement law, expressed for the corresponding linear maps. -/
77 theorem fibreLinearProj_refinement
78     {γ : Type*}
79     [Semiring R] [AddCommMonoid M] [Module R M]
80     [DecidableEq β] [DecidableEq γ] [Fintype γ]
81     (fine : α → γ) (merge : γ → β) (b : β) :
82     fibreLinearProj (R := R) (M := M) (fun a => merge (fine a)) b =
83       ∑ c, if merge c = b then fibreLinearProj (R := R) (M := M) fine c else 0 := by
84   apply LinearMap.ext
85   intro (x : α → M)
86   apply funext
87   intro a
88   change fibreProj (fun a => merge (fine a)) b x a =
89     ((∑ c ∈ Finset.univ,
90       if merge c = b then fibreLinearProj (R := R) (M := M) fine c else 0) x) a
91   rw [LinearMap.sum_apply, Finset.sum_apply]
92   calc
93     fibreProj (fun a => merge (fine a)) b x a =
94         ∑ c, if merge c = b then fibreProj fine c x a else 0 := by
95       simpa only [Fintype.sum_apply, ite_apply, Pi.zero_apply] using
96         congrFun (fibreProj_refinement fine merge b x) a
97     _ = ∑ c, (if merge c = b then
98           fibreLinearProj (R := R) (M := M) fine c else 0) x a := by
99       apply Fintype.sum_congr
100       intro c
101       by_cases hc : merge c = b <;> simp [hc, fibreLinearProj_apply]
102 
103 end Komorebi.Packet

Back to source controls