ReleaseGluingPacketBridge.lean

1 import KomorebiVerification.PaperII.ReleaseGluingDVR
2 import KomorebiVerification.PaperII.NestedRefinement
3 
4 /-! The genuine lattice quotient construction consumes the existing packet/refinement interface. -/
5 
6 set_option autoImplicit false
7 
8 namespace Komorebi.PaperII.ReleaseGluing
9 
10 open Komorebi.Foundation
11 
12 universe u v w
13 variable {O : Type u} {K : Type v} {V : Type w}
14 variable [CommRing O] [Field K] [Algebra O K]
15 variable [AddCommGroup V] [Module O V] [Module K V] [IsScalarTower O K V]
16 variable {I J : Type*} [Fintype I] [Fintype J]
17 
18 def ofLinearProjectorFamily (P : LinearProjectorFamily K V I) : Projectors K V I where
19   proj := P.proj
20   idem i := by ext x; exact P.idempotent i x
21   orthogonal i j hij := by ext x; exact P.orthogonal hij x
22   complete := by
23     ext x
24     simpa only [LinearMap.sum_apply, Module.End.one_apply] using P.complete x
25 
26 /-- Existing refinement, rather than an assumed range-containment conclusion, supplies the lattice inclusion. -/
27 theorem original_refinement_range_containment
28     (P : LinearProjectorFamily K V I) (Q : LinearProjectorFamily K V J)
29     (parent : J → I) (h : NestedRefinement.Refines P Q parent) (j : J) :
30     LinearMap.range (((ofLinearProjectorFamily Q).restrictScalars (O := O)).proj j) ≤
31       LinearMap.range (((ofLinearProjectorFamily P).restrictScalars (O := O)).proj (parent j)) := by
32   rintro x ⟨y, rfl⟩
33   refine ⟨Q.proj j y, ?_⟩
34   exact h.coarse_fine_apply_eq_self j y
35 
36 /-- The displayed quotient exact sequence under the original refinement relation. -/
37 theorem original_refinement_gluing_short_exact
38     (P : LinearProjectorFamily K V I) (Q : LinearProjectorFamily K V J)
39     (parent : J → I) (h : NestedRefinement.Refines P Q parent) (Λ : Submodule O V) :
40     let P' := (ofLinearProjectorFamily P).restrictScalars (O := O)
41     let Q' := (ofLinearProjectorFamily Q).restrictScalars (O := O)
42     let incl := splitInside_le_of_refines P' Λ Q' parent
43       (original_refinement_range_containment P Q parent h)
44     Function.Injective (quotientInclusion (splitInside Q' Λ) (splitInside P' Λ)) ∧
45     LinearMap.range (quotientInclusion (splitInside Q' Λ) (splitInside P' Λ)) =
46       LinearMap.ker (Submodule.factor incl) ∧
47     Function.Surjective (Submodule.factor incl) := by
48   exact gluing_refinement_short_exact _ _ _ parent
49     (original_refinement_range_containment P Q parent h)
50 
51 /-- The original refinement relation gives monotonicity of the genuine least gluing weights. -/
52 theorem original_refinement_globalWeight_mono
53     (P : LinearProjectorFamily K V I) (Q : LinearProjectorFamily K V J)
54     (parent : J → I) (h : NestedRefinement.Refines P Q parent) (Λ : Submodule O V) (pi : O)
55     (finiteP : ∀ i, ∃ s, ClearsPacket
56       ((ofLinearProjectorFamily P).restrictScalars (O := O)) Λ pi i s)
57     (finiteQ : ∀ j, ∃ s, ClearsPacket
58       ((ofLinearProjectorFamily Q).restrictScalars (O := O)) Λ pi j s) :
59     globalWeight ((ofLinearProjectorFamily P).restrictScalars (O := O)) Λ pi finiteP ≤
60       globalWeight ((ofLinearProjectorFamily Q).restrictScalars (O := O)) Λ pi finiteQ := by
61   exact globalWeight_mono_of_refines _ _ _ pi finiteP finiteQ parent
62     (original_refinement_range_containment P Q parent h)
63 
64 end Komorebi.PaperII.ReleaseGluing

Back to source controls