ReleaseGluingBinary.lean

1 import KomorebiVerification.PaperII.ReleaseGluing
2 import Mathlib.Tactic.FinCases
3 import Mathlib.Algebra.BigOperators.Fin
4 
5 set_option autoImplicit false
6 open scoped BigOperators
7 
8 namespace Komorebi.PaperII.ReleaseGluing
9 
10 universe u v
11 variable {O : Type u} {V : Type v}
12 variable [CommRing O] [AddCommGroup V] [Module O V]
13 
14 /-- With two complementary packets, either coordinate already detects the gluing class. -/
15 theorem gluingCoordinate_injective_binary
16     (P : Projectors O V (Fin 2)) (Λ : Submodule O V) (i : Fin 2) :
17     Function.Injective (gluingCoordinate P Λ i) := by
18   apply LinearMap.ker_eq_bot.mp
19   apply le_antisymm
20   · intro z hz
21     obtain ⟨x, rfl⟩ := (splitInside P Λ).mkQ_surjective z
22     have hi : P.proj i x ∈ Λ := (rawCoordinate_eq_zero_iff P Λ i x).mp hz
23     have hsum : P.proj 0 x + P.proj 1 x = x := by
24       simpa only [Fin.sum_univ_two] using reconstruct P x
25     have hall : ∀ j, P.proj j x ∈ Λ := by
26       intro j
27       fin_cases i <;> fin_cases j
28       · exact hi
29       · have heq : P.proj 1 x = x - P.proj 0 x := by
30           apply eq_sub_iff_add_eq.mpr
31           simpa only [add_comm] using hsum
32         change P.proj 1 x ∈ Λ
33         rw [heq]
34         exact Λ.sub_mem x.property hi
35       · have heq : P.proj 0 x = x - P.proj 1 x :=
36           eq_sub_iff_add_eq.mpr hsum
37         change P.proj 0 x ∈ Λ
38         rw [heq]
39         exact Λ.sub_mem x.property hi
40       · exact hi
41     have hx : x ∈ splitInside P Λ := (mem_splitLattice_iff P Λ x).mpr hall
42     simpa only [Submodule.mem_bot, Submodule.mkQ_apply,
43       Submodule.Quotient.mk_eq_zero] using hx
44   · exact bot_le
45 
46 /-- The actual binary gluing quotient is isomorphic to either packet quotient. -/
47 noncomputable def binaryGluingEquivCoordinate
48     (P : Projectors O V (Fin 2)) (Λ : Submodule O V) (i : Fin 2) :
49     GluingModule P Λ ≃ₗ[O] CoordinateQuotient P Λ i :=
50   LinearEquiv.ofBijective (gluingCoordinate P Λ i)
51     ⟨gluingCoordinate_injective_binary P Λ i, gluingCoordinate_surjective P Λ i⟩
52 
53 /-- In the binary case, either least packet weight equals the global gluing weight. -/
54 theorem binary_packetWeight_eq_globalWeight
55     (P : Projectors O V (Fin 2)) (Λ : Submodule O V) (pi : O)
56     (finite : ∀ i, ∃ s, ClearsPacket P Λ pi i s) (i : Fin 2) :
57     packetWeight P Λ pi i (finite i) = globalWeight P Λ pi finite := by
58   have hequiv (s : ℕ) : ClearsPacket P Λ pi i s ↔
59       ∀ z : GluingModule P Λ, (pi ^ s) • z = 0 := by
60     rw [← annihilates_coordinate_iff_clears P Λ pi i s]
61     constructor
62     · intro h z
63       apply gluingCoordinate_injective_binary P Λ i
64       rw [map_smul, h _, map_zero]
65     · intro h z
66       obtain ⟨x, rfl⟩ := gluingCoordinate_surjective P Λ i z
67       rw [← map_smul, h _, map_zero]
68   apply le_antisymm
69   · apply (clearsPacket_iff_weight_le P Λ pi i (finite i) _).mp
70     exact (hequiv _).mpr ((gluing_annihilated_iff_globalWeight_le P Λ pi finite _).mpr le_rfl)
71   · apply (gluing_annihilated_iff_globalWeight_le P Λ pi finite _).mp
72     exact (hequiv _).mp ((clearsPacket_iff_weight_le P Λ pi i (finite i) _).mpr le_rfl)
73 
74 /-- Complementary binary projectors have exactly the same least separation weight. -/
75 theorem binary_packetWeights_equal
76     (P : Projectors O V (Fin 2)) (Λ : Submodule O V) (pi : O)
77     (finite : ∀ i, ∃ s, ClearsPacket P Λ pi i s) :
78     packetWeight P Λ pi 0 (finite 0) = packetWeight P Λ pi 1 (finite 1) := by
79   rw [binary_packetWeight_eq_globalWeight, binary_packetWeight_eq_globalWeight]
80 
81 end Komorebi.PaperII.ReleaseGluing

Back to source controls