CoordinateTransport.lean

1 import PaperIRelease.AlgebraSupport
2 import KomorebiVerification.PaperITransport
3 set_option autoImplicit false
4 noncomputable section
5 namespace Komorebi.PaperIRelease.CoordinateTransport
6 open Komorebi.Foundation
7 universe u v w x
8 variable {K : Type u} [Field K]
9 variable {X : Type v} [AddCommGroup X] [Module K X]
10 variable {Y : Type w} [AddCommGroup Y] [Module K Y]
11 variable {I : Type x} [Fintype I]
12 
13 /-- Conjugation restricts to an actual linear equivalence of each packet range. -/
14 def packetRangeEquiv (P : LinearProjectorFamily K X I) (U : X ≃ₗ[K] Y) (i : I) :
15     (P.proj i).range ≃ₗ[K] ((P.conjugate U).proj i).range where
16   toFun x := ⟨U x, by
17     obtain ⟨z, hz⟩ := x.property
18     exact ⟨U z, by simp [← hz]⟩⟩
19   invFun y := ⟨U.symm y, by
20     obtain ⟨z, hz⟩ := y.property
21     exact ⟨U.symm z, by simp [← hz]⟩⟩
22   left_inv _ := by apply Subtype.ext; exact U.symm_apply_apply _
23   right_inv _ := by apply Subtype.ext; exact U.apply_symm_apply _
24   map_add' _ _ := by apply Subtype.ext; exact U.map_add _ _
25   map_smul' _ _ := by apply Subtype.ext; exact U.map_smul _ _
26 
27 /-- Packet dimension is invariant, with explicit lifts for different universes. -/
28 theorem packet_rank_invariant (P : LinearProjectorFamily K X I) (U : X ≃ₗ[K] Y) (i : I) :
29     Cardinal.lift.{w} (Module.rank K (P.proj i).range) =
30       Cardinal.lift.{v} (Module.rank K ((P.conjugate U).proj i).range) :=
31   (packetRangeEquiv P U i).lift_rank_eq
32 
33 /-- Every support relation, in particular a support preorder, is preserved literally. -/
34 theorem support_pattern_invariant (P : LinearProjectorFamily K X I) (U : X ≃ₗ[K] Y)
35     (rel : I → I → Prop) (T : Module.End K X) :
36     OperatorSupported (P.conjugate U) rel (conjugateEnd U T) ↔ OperatorSupported P rel T := by
37   rw [operatorSupported_iff_ambient, operatorSupported_iff_ambient]
38   constructor
39   · intro h b a hab
40     have hz := h b a hab
41     rw [conjugate_transferBlock] at hz
42     exact Komorebi.PacketNaturalityCompletion.Reachability.conjugateEnd_eq_zero_iff U _ |>.mp hz
43   · intro h b a hab
44     rw [conjugate_transferBlock, h b a hab]
45     ext y
46     simp [conjugateEnd]
47 
48 end Komorebi.PaperIRelease.CoordinateTransport

Back to source controls