NormalFormTransport.lean

1 import RealizationBoundaries.SelectorClassification
2 import RealizationBoundaries.NormalForms
3 
4 /-! # Exact coordinate transport under finite selector changes -/
5 set_option autoImplicit false
6 set_option backward.isDefEq.respectTransparency false
7 noncomputable section
8 namespace RealizationBoundaries
9 
10 /-- The section difference is genuinely finite, without a nonzero-rational hypothesis. -/
11 theorem section_difference_finite (a b : ℕ → Bool)
12     (h : {n : ℕ | a n ≠ b n}.Finite) (r : ℚ) :
13     rationalSection (pairedSelector a) r - rationalSection (pairedSelector b) r ∈ finiteSupport := by
14   classical
15   obtain ⟨E, hE, he⟩ := pairedSelectors_agree_off_finite a b h
16   apply hE.subset
17   intro p hp
18   by_contra hn
19   apply hp
20   change rationalSection (pairedSelector a) r p - rationalSection (pairedSelector b) r p = 0
21   simp [rationalSection, he p hn]
22 
23 /-- Finite correction converting the source normal-form section into the target section. -/
24 def selectorCorrection (a b : ℕ → Bool)
25     (h : {n : ℕ | a n ≠ b n}.Finite) (r : ℚ) : finiteSupport :=
26   ⟨rationalSection (pairedSelector a) r - rationalSection (pairedSelector b) r,
27     section_difference_finite a b h r⟩
28 
29 /-- The coordinate formula is typed in the twisted normal-form groups, not split products. -/
30 def normalFormTransport (a b : ℕ → Bool) (h : {n : ℕ | a n ≠ b n}.Finite)
31     (x : NormalForm (pairedSelector a)) : NormalForm (pairedSelector b) :=
32   ⟨x.rational, x.finite + selectorCorrection a b h x.rational⟩
33 
34 @[simp] theorem normalFormTransport_rational (a b : ℕ → Bool)
35     (h : {n : ℕ | a n ≠ b n}.Finite) (x : NormalForm (pairedSelector a)) :
36     (normalFormTransport a b h x).rational = x.rational := rfl
37 
38 @[simp] theorem normalFormTransport_finite (a b : ℕ → Bool)
39     (h : {n : ℕ | a n ≠ b n}.Finite) (x : NormalForm (pairedSelector a)) :
40     (normalFormTransport a b h x).finite = x.finite + selectorCorrection a b h x.rational := rfl
41 
42 /-- Transport fixes the represented ambient vector exactly, not merely its tail class. -/
43 theorem normalFormTransport_realization (a b : ℕ → Bool)
44     (h : {n : ℕ | a n ≠ b n}.Finite) (x : NormalForm (pairedSelector a)) :
45     (NormalForm.realizationEquiv (pairedSelector_infinite b)
46       (normalFormTransport a b h x)).val =
47     (NormalForm.realizationEquiv (pairedSelector_infinite a) x).val := by
48   simp only [NormalForm.realizationEquiv_coe, normalFormTransport_rational,
49     normalFormTransport_finite]
50   change rationalSection (pairedSelector b) x.rational +
51     (x.finite.val + (rationalSection (pairedSelector a) x.rational -
52       rationalSection (pairedSelector b) x.rational)) = _
53   abel
54 
55 /-- The same coordinate transformation as an actual additive equivalence. -/
56 def normalFormTransportEquiv (a b : ℕ → Bool) (h : {n : ℕ | a n ≠ b n}.Finite) :
57     NormalForm (pairedSelector a) ≃+ NormalForm (pairedSelector b) :=
58   ((NormalForm.realizationEquiv (pairedSelector_infinite a)).trans
59     (pairedEquivOfFiniteDisagreement a b h)).trans
60       (NormalForm.realizationEquiv (pairedSelector_infinite b)).symm
61 
62 /-- The abstractly composed equivalence has precisely the finite-correction formula. -/
63 theorem normalFormTransportEquiv_apply (a b : ℕ → Bool)
64     (h : {n : ℕ | a n ≠ b n}.Finite) (x : NormalForm (pairedSelector a)) :
65     normalFormTransportEquiv a b h x = normalFormTransport a b h x := by
66   apply (NormalForm.realizationEquiv (pairedSelector_infinite b)).injective
67   apply Subtype.ext
68   change (NormalForm.realizationEquiv (pairedSelector_infinite b)
69     ((NormalForm.realizationEquiv (pairedSelector_infinite b)).symm
70       (pairedEquivOfFiniteDisagreement a b h
71         (NormalForm.realizationEquiv (pairedSelector_infinite a) x)))).val = _
72   rw [AddEquiv.apply_symm_apply, pairedEquivOfFiniteDisagreement_val]
73   exact (normalFormTransport_realization a b h x).symm
74 
75 /-- Addition is preserved for the actual twisted laws. -/
76 theorem normalFormTransport_add (a b : ℕ → Bool)
77     (h : {n : ℕ | a n ≠ b n}.Finite) (x y : NormalForm (pairedSelector a)) :
78     normalFormTransport a b h (x+y) =
79       normalFormTransport a b h x + normalFormTransport a b h y := by
80   simpa only [normalFormTransportEquiv_apply] using (normalFormTransportEquiv a b h).map_add x y
81 
82 end RealizationBoundaries

Back to source controls