AffineObstructionControls.lean

1 import FiniteAffineObstruction
2 
3 noncomputable section
4 set_option autoImplicit false
5 
6 namespace Komorebi.NativeAffine.Controls
7 open Komorebi.NativeAffine
8 
9 /-- An invertible coefficient map has no obstruction. -/
10 theorem identity_unobstructed (p n : ℕ) (r : Fin n → ℤ) :
11     obstruction p (LinearMap.id : (Fin n → ℤ) →ₗ[ℤ] (Fin n → ℤ)) r = 0 := by
12   rw [obstruction_zero_iff_correction]
13   refine ⟨-r, ?_⟩
14   simp
15 
16 /-- This obstruction can genuinely be nonzero. -/
17 theorem zero_map_residual_nonzero :
18     obstruction 2 (0 : (Fin 1 → ℤ) →ₗ[ℤ] (Fin 1 → ℤ)) (fun _ => 1) ≠ 0 := by
19   intro h
20   obtain ⟨t, ht⟩ := (obstruction_zero_iff_correction 2
21     (0 : (Fin 1 → ℤ) →ₗ[ℤ] (Fin 1 → ℤ)) (fun _ => 1)).mp h
22   have h0 : (1 : ZMod 2) = 0 := by
23     simpa [reduction] using congrFun ht (0 : Fin 1)
24   exact one_ne_zero h0
25 
26 /-- The singular constant system 0*x=-2 is satisfied modulo 2. -/
27 theorem singular_lower_solution :
28     ∀ i : Fin 1, (2 : ℤ) ∣
29       ((0 : (Fin 1 → ℤ) →ₗ[ℤ] (Fin 1 → ℤ)) 0 - (fun _ : Fin 1 => (-2 : ℤ))) i := by
30   intro i
31   exact dvd_refl 2
32 
33 /-- That same actual lower solution has no solution modulo 4. -/
34 theorem singular_no_lift :
35     ¬ ∃ y : Fin 1 → ℤ, ∀ i : Fin 1, (4 : ℤ) ∣
36       ((0 : (Fin 1 → ℤ) →ₗ[ℤ] (Fin 1 → ℤ)) y - (fun _ : Fin 1 => (-2 : ℤ))) i := by
37   rintro ⟨y, hy⟩
38   have h := hy 0
39   change (4 : ℤ) ∣ 2 at h
40   exact (by decide : ¬ (4 : ℤ) ∣ 2) h
41 
42 #print axioms identity_unobstructed
43 #print axioms zero_map_residual_nonzero
44 #print axioms singular_lower_solution
45 #print axioms singular_no_lift
46 
47 end Komorebi.NativeAffine.Controls

Back to source controls