Correction.lean

1 import Mathlib.GroupTheory.QuotientGroup.Basic
2 import Mathlib.Data.Int.Basic
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Semantic constraints and a genuine obstruction quotient
8 
9 A raw linear defect d(f) is always removable by subtracting f. A nontrivial
10 problem must restrict admissible corrections. Here p records semantics and
11 corrections must lie in ker p. The obstruction is [d(f)] in R / d(ker p).
12 -/
13 universe u v w z
14 namespace KomorebiSpace
15 
16 structure CorrectionProblem (E : Type u) (R : Type v) (S : Type w)
17     [AddCommGroup E] [AddCommGroup R] [AddCommGroup S] where
18   residual : E →+ R
19   semantics : E →+ S
20 
21 namespace CorrectionProblem
22 variable {E : Type u} {R : Type v} {S : Type w}
23 variable [AddCommGroup E] [AddCommGroup R] [AddCommGroup S]
24 
25 def boundaries (P : CorrectionProblem E R S) : AddSubgroup R :=
26   P.semantics.ker.map P.residual
27 
28 abbrev Obstruction (P : CorrectionProblem E R S) := R ⧸ P.boundaries
29 
30 def obstruction (P : CorrectionProblem E R S) (x : E) : P.Obstruction :=
31   (P.residual x : R ⧸ P.boundaries)
32 
33 /-- Quotient vanishing is precisely solvability by an admissible correction. -/
34 theorem obstruction_zero_iff (P : CorrectionProblem E R S) (x : E) :
35     P.obstruction x = 0 ↔
36       ∃ a : E, P.semantics a = 0 ∧ P.residual a = P.residual x := by
37   change (P.residual x : R ⧸ P.boundaries) = 0 ↔ _
38   rw [QuotientAddGroup.eq_zero_iff]
39   rfl
40 
41 /-- Main constrained exactification equivalence, with semantics preserved. -/
42 theorem flatten_iff (P : CorrectionProblem E R S) (x : E) :
43     P.obstruction x = 0 ↔
44       ∃ y : E, P.residual y = 0 ∧ P.semantics y = P.semantics x := by
45   rw [P.obstruction_zero_iff]
46   constructor
47   · rintro ⟨a, ha, hd⟩
48     refine ⟨x-a, ?_, ?_⟩
49     · rw [map_sub, hd, sub_self]
50     · rw [map_sub, ha, sub_zero]
51   · rintro ⟨y, hy, hs⟩
52     refine ⟨x-y, ?_, ?_⟩
53     · rw [map_sub, hs, sub_self]
54     · rw [map_sub, hy, sub_zero]
55 
56 theorem obstruction_invariant (P : CorrectionProblem E R S) (x a : E)
57     (ha : P.semantics a = 0) : P.obstruction (x-a) = P.obstruction x := by
58   have hz : (P.residual a : R ⧸ P.boundaries) = 0 :=
59     (QuotientAddGroup.eq_zero_iff _).2 ⟨a, ha, rfl⟩
60   change (P.residual (x-a) : R ⧸ P.boundaries) = (P.residual x : R ⧸ P.boundaries)
61   rw [map_sub, QuotientAddGroup.mk_sub, hz, sub_zero]
62 
63 /-- A dual witness rules out every semantics-preserving exact correction. -/
64 theorem nonzero_certificate (P : CorrectionProblem E R S)
65     {D : Type z} [AddCommGroup D] (L : R →+ D) (x : E)
66     (annihilate : ∀ a, P.semantics a = 0 → L (P.residual a) = 0)
67     (witness : L (P.residual x) ≠ 0) : P.obstruction x ≠ 0 := by
68   intro h
69   rcases (P.obstruction_zero_iff x).1 h with ⟨a, ha, he⟩
70   apply witness
71   rw [← he]
72   exact annihilate a ha
73 
74 /-- With no semantic restriction every linear primary defect is correctable. -/
75 theorem unrestricted_correction (d : E →+ R) (x : E) :
76     ∃ a : E, d x - d a = 0 := ⟨x, sub_self _⟩
77 
78 /-- An explicit nontrivial model: the residual itself is the protected semantics. -/
79 def rigidInteger : CorrectionProblem ℤ ℤ ℤ :=
80   ⟨AddMonoidHom.id ℤ, AddMonoidHom.id ℤ⟩
81 
82 theorem rigid_one_obstructed : rigidInteger.obstruction 1 ≠ 0 := by
83   intro h
84   have hx := (rigidInteger.flatten_iff 1).1 h
85   change ∃ y : ℤ, y = 0 ∧ y = 1 at hx
86   obtain ⟨y, h0, h1⟩ := hx
87   omega
88 
89 end CorrectionProblem
90 end KomorebiSpace

Back to source controls