AtomicNaturality.lean

1 import PaperXI.AtomicReconstruction
2 
3 /-! Naturality and the exact information-preservation boundary for Theorem 2.5.
4 Twist laws are attached to the primitive decomposition and ordered quotient
5 relations. Equivariance of the final candidate is then a theorem, not an input. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.AtomicNaturality
9 open PaperXI.AtomicMultiset PaperXI.AtomicReconstruction
10 
11 variable {P A B T : Type*} {sP : Setoid P}
12 
13 /-- The initial assignment can be stated on representatives. Isomorphism
14 compatibility suffices to descend it before performing any block reconstruction. -/
15 theorem reconstruction_from_representatives {A₀ B₀ : Type*}
16     (sA : Setoid A₀) (sB : Setoid B₀) (f : A₀ → B₀)
17     (hf : ∀ a a', sA.r a a' → sB.r (f a) (f a'))
18     (D : Decomposition sP (Quotient sA)) (L : OrderedQuotient (Quotient sB) T) :
19     ∃! F : Quotient sP → T, Reconstructs (descend f hf) D L F :=
20   formal_atomic_reconstruction (descend f hf) D L
21 
22 theorem blocks_twist (D : Decomposition sP A) (tP : P → P) (tA : A → A)
23     (hP : ∀ p q, sP.r p q → sP.r (tP p) (tP q))
24     (hD : ∀ p xs, D.displays p xs → D.displays (tP p) (xs.map (blockMap tA)))
25     (p : Quotient sP) :
26     blocks D (Quotient.map tP hP p) = extend tA (blocks D p) := by
27   refine Quotient.inductionOn p ?_
28   intro p
29   obtain ⟨xs, hxs⟩ := D.exists_display p
30   change blocks D (Quotient.mk sP (tP p)) = extend tA (blocks D (Quotient.mk sP p))
31   rw [blocks_of_display D (tP p) _ (hD p xs hxs), blocks_of_display D p xs hxs]
32   rfl
33 
34 /-- Twisting a valid ordered quotient yields the quotient of the twisted factors.
35 The sorting itself is not assumed to commute: ties may choose different displays. -/
36 theorem realize_twist (L : OrderedQuotient B T) (tB : B → B) (tT : T → T)
37     (horder : ∀ a b, L.precedes a b → L.precedes (blockMap tB a) (blockMap tB b))
38     (hquot : ∀ xs t, xs.Pairwise L.precedes → L.quotient xs t →
39       L.quotient (xs.map (blockMap tB)) (tT t))
40     (s : Multiset (Block B)) : realize L (extend tB s) = tT (realize L s) := by
41   have hs : ((ordered L s).map (blockMap tB)).Pairwise L.precedes := by
42     rw [List.pairwise_map]
43     exact (ordered_pairwise L s).imp (fun h => horder _ _ h)
44   have hm : (((ordered L s).map (blockMap tB)) : Multiset (Block B)) = extend tB s := by
45     rw [← Multiset.map_coe, ordered_multiset]
46     rfl
47   exact realize_eq L (extend tB s) _ hs hm _
48     (hquot _ _ (ordered_pairwise L s)
49       (realize_spec L s _ (ordered_pairwise L s) (ordered_multiset L s)))
50 
51 /-- The final reconstruction commutes with unramified-type twists when the
52 atomic assignment and the two classical interfaces have the declared twist laws. -/
53 theorem candidate_twist (f : A → B) (D : Decomposition sP A)
54     (L : OrderedQuotient B T) (tP : P → P) (tA : A → A) (tB : B → B) (tT : T → T)
55     (hP : ∀ p q, sP.r p q → sP.r (tP p) (tP q))
56     (hD : ∀ p xs, D.displays p xs → D.displays (tP p) (xs.map (blockMap tA)))
57     (hf : ∀ a, f (tA a) = tB (f a))
58     (horder : ∀ a b, L.precedes a b → L.precedes (blockMap tB a) (blockMap tB b))
59     (hquot : ∀ xs t, xs.Pairwise L.precedes → L.quotient xs t →
60       L.quotient (xs.map (blockMap tB)) (tT t)) (p : Quotient sP) :
61     candidate f D L (Quotient.map tP hP p) = tT (candidate f D L p) := by
62   change realize L (extend f (blocks D (Quotient.map tP hP p))) = _
63   rw [blocks_twist D tP tA hP hD, extend_natural f tA tB hf]
64   exact realize_twist L tB tT horder hquot _
65 
66 /-- Injectivity of the formal block assembly is exactly injectivity on atoms. -/
67 theorem extend_injective_iff (f : A → B) :
68     Function.Injective (extend f) ↔ Function.Injective f := by
69   constructor
70   · intro h a b hab
71     let x : Block A := ⟨a, 1, by omega⟩
72     let y : Block A := ⟨b, 1, by omega⟩
73     have hm : extend f ({x} : Multiset (Block A)) = extend f {y} := by
74       simp only [extend_singleton]
75       congr 1
76       exact Block.ext hab rfl
77     have he : x = y := by simpa only [Multiset.singleton_inj] using h hm
78     exact congrArg Block.atom he
79   · exact extend_injective f
80 
81 /-- Full output injectivity needs both source classification and target
82 classification, in addition to atomic injectivity. None follows from uniqueness
83 of the reconstruction map alone. -/
84 theorem candidate_injective (f : A → B) (D : Decomposition sP A)
85     (L : OrderedQuotient B T) (hf : Function.Injective f)
86     (hD : Function.Injective (blocks D)) (hL : Function.Injective (realize L)) :
87     Function.Injective (candidate f D L) := by
88   exact hL.comp ((extend_injective f hf).comp hD)
89 
90 /-- Different display choices satisfying a common intrinsic-decomposition
91 contract produce identical candidates. -/
92 theorem decomposition_independence (f : A → B) (D E : Decomposition sP A)
93     (L : OrderedQuotient B T)
94     (hDE : ∀ p xs ys, D.displays p xs → E.displays p ys → xs.Perm ys) :
95     candidate f D L = candidate f E L := by
96   funext p
97   refine Quotient.inductionOn p ?_
98   intro p
99   obtain ⟨xs, hx⟩ := D.exists_display p
100   obtain ⟨ys, hy⟩ := E.exists_display p
101   change realize L (extend f (blocks D (Quotient.mk sP p))) =
102     realize L (extend f (blocks E (Quotient.mk sP p)))
103   rw [blocks_of_display D p xs hx, blocks_of_display E p ys hy,
104       Multiset.coe_eq_coe.mpr (hDE p xs ys hx hy)]
105 
106 end PaperXI.AtomicNaturality

Back to source controls