Protected.lean

1 import Mathlib.LinearAlgebra.Dual.Lemmas
2 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
3 import Mathlib.FieldTheory.Finite.Basic
4 
5 /-!
6 Protected realization and exact observation counts.  The source proves
7 statements about declared linear maps, not soundness of arbitrary annotations.
8 -/
9 namespace ProofPath
10 open Module
11 
12 variable {K E R S W : Type*} [Field K]
13   [AddCommGroup E] [Module K E] [AddCommGroup R] [Module K R]
14   [AddCommGroup S] [Module K S] [AddCommGroup W] [Module K W]
15 
16 def CorrectionImage (D : E →ₗ[K] R) (p : E →ₗ[K] S) : Submodule K R :=
17   p.ker.map D
18 
19 theorem protected_iff_correction (D : E →ₗ[K] R) (p : E →ₗ[K] S) (x : E) :
20     (∃ y, D y = 0 ∧ p y = p x) ↔ D x ∈ CorrectionImage D p := by
21   constructor
22   · rintro ⟨y, hy, hpy⟩
23     exact ⟨x - y, by simp [hpy], by simp [hy]⟩
24   · rintro ⟨h, hh, he⟩
25     have hp : p h = 0 := hh
26     exact ⟨x - h, by simp [he], by simp [hp]⟩
27 
28 theorem obstruction_sound (D : E →ₗ[K] R) (p : E →ₗ[K] S) (x : E)
29     (l : R →ₗ[K] K) (hz : ∀ h, p h = 0 → l (D h) = 0)
30     (hne : l (D x) ≠ 0) : ¬ ∃ y, D y = 0 ∧ p y = p x := by
31   intro h
32   rcases (protected_iff_correction D p x).mp h with ⟨v, hv, he⟩
33   exact hne (he ▸ hz v hv)
34 
35 theorem protected_alternative (D : E →ₗ[K] R) (p : E →ₗ[K] S) (x : E) :
36     (¬ ∃ y, D y = 0 ∧ p y = p x) ↔
37     ∃ l : R →ₗ[K] K, (∀ h, p h = 0 → l (D h) = 0) ∧ l (D x) = 1 := by
38   constructor
39   · intro hn
40     have hx : D x ∉ CorrectionImage D p :=
41       fun h => hn ((protected_iff_correction D p x).mpr h)
42     obtain ⟨l, hl, hz⟩ :=
43       Submodule.exists_dual_map_eq_bot_of_notMem hx inferInstance
44     have vanish : ∀ h, p h = 0 → l (D h) = 0 := by
45       intro h hp
46       have hm : l (D h) ∈ (CorrectionImage D p).map l :=
47         ⟨D h, ⟨h, hp, rfl⟩, rfl⟩
48       simpa [hz] using hm
49     refine ⟨(l (D x))⁻¹ • l, ?_, ?_⟩
50     · intro h hp
51       simp [vanish h hp]
52     · simp [hl]
53   · rintro ⟨l, hz, hone⟩
54     exact obstruction_sound D p x l hz (by rw [hone]; exact one_ne_zero)
55 
56 /-- Translation by a chosen point classifies a nonempty linear fiber. -/
57 def kernelEquivFiber (T : E →ₗ[K] R) (x₀ : E) :
58     T.ker ≃ {y : E // T y = T x₀} where
59   toFun h := ⟨x₀ + h, by simp⟩
60   invFun y := ⟨y - x₀, by simp [y.property]⟩
61   left_inv h := by ext; simp
62   right_inv y := by ext; simp
63 
64 theorem fiber_card [Fintype K] [Fintype E] (T : E →ₗ[K] R) (x₀ : E) :
65     Nat.card {y : E // T y = T x₀} =
66       Fintype.card K ^ finrank K T.ker := by
67   classical
68   rw [← Nat.card_congr (kernelEquivFiber T x₀), Nat.card_eq_fintype_card]
69   exact Module.card_eq_pow_finrank
70 
71 def observationMap (T : E →ₗ[K] R) (Q : E →ₗ[K] W) : T.ker →ₗ[K] W :=
72   Q.comp T.ker.subtype
73 
74 /-- Every attained observation fiber is a translate of the same kernel. -/
75 def observationKernelEquiv (T : E →ₗ[K] R) (Q : E →ₗ[K] W) (x₀ : E) :
76     (observationMap T Q).ker ≃ {y : E // T y = T x₀ ∧ Q y = Q x₀} where
77   toFun h := ⟨x₀ + h.val.val, by
78     have ht : T h.val.val = 0 := h.val.property
79     have hq : Q h.val.val = 0 := h.property
80     simp [ht, hq]⟩
81   invFun y := ⟨⟨y - x₀, by simp [y.property.1]⟩, by
82     change Q (y.val - x₀) = 0
83     simp [y.property.2]⟩
84   left_inv h := by ext; simp
85   right_inv y := by ext; simp
86 
87 theorem observation_fiber_card [Fintype K] [Fintype E]
88     (T : E →ₗ[K] R) (Q : E →ₗ[K] W) (x₀ : E) :
89     Nat.card {y : E // T y = T x₀ ∧ Q y = Q x₀} =
90       Fintype.card K ^ finrank K (observationMap T Q).ker := by
91   classical
92   rw [← Nat.card_congr (observationKernelEquiv T Q x₀), Nat.card_eq_fintype_card]
93   exact Module.card_eq_pow_finrank
94 
95 theorem observation_rank_nullity [FiniteDimensional K E]
96     (T : E →ₗ[K] R) (Q : E →ₗ[K] W) :
97     finrank K (observationMap T Q).range + finrank K (observationMap T Q).ker =
98       finrank K T.ker :=
99   (observationMap T Q).finrank_range_add_finrank_ker
100 
101 theorem exact_observation_count [Fintype K] [Fintype E]
102     (T : E →ₗ[K] R) (Q : E →ₗ[K] W) (x₀ : E) :
103     Nat.card {y : E // T y = T x₀} =
104       Nat.card {y : E // T y = T x₀ ∧ Q y = Q x₀} *
105         Fintype.card K ^ finrank K (observationMap T Q).range := by
106   classical
107   rw [fiber_card, observation_fiber_card,
108     ← observation_rank_nullity T Q, pow_add, mul_comm]
109 
110 /-- Original protected constraints are exactly a fiber of the stacked map. -/
111 theorem stacked_fiber (D : E →ₗ[K] R) (p : E →ₗ[K] S) (x y : E) :
112     (D.prod p) y = (0, p x) ↔ D y = 0 ∧ p y = p x := by
113   simp
114 
115 end ProofPath

Back to source controls