OrthogonalProjectors.lean

1 import PaperX.MatrixProjector
2 import Mathlib.Algebra.BigOperators.Ring.Finset
3 
4 /-! A complete labeled orthogonal family of actual equivariant projectors. -/
5 set_option autoImplicit false
6 namespace PaperX.OrthogonalProjectors
7 open PaperX.RepresentationLimits PaperX.MatrixProjector
8 open scoped BigOperators
9 
10 variable {R Γ ι : Type*} [CommRing R] [Group Γ]
11   [Fintype ι] [DecidableEq ι]
12 
13 structure Family (ρ : MatrixRep R Γ ι) (J : Type*) [Fintype J] where
14   projector : J → Projector ρ
15   orthogonal : ∀ i j, i ≠ j → (projector i).matrix * (projector j).matrix = 0
16   total : ∑ i, (projector i).matrix = 1
17 
18 namespace Family
19 variable {ρ : MatrixRep R Γ ι} {J : Type*} [Fintype J] (E : Family ρ J)
20 
21 theorem product [DecidableEq J] (i j : J) :
22     (E.projector i).matrix * (E.projector j).matrix =
23       if i = j then (E.projector i).matrix else 0 := by
24   split
25   · rename_i h
26     subst j
27     exact (E.projector i).idempotent
28   · exact E.orthogonal i j ‹i ≠ j›
29 
30 def changeCoefficients {S : Type*} [CommRing S] (f : R →+* S) :
31     Family (RepresentationLimits.changeCoefficients f ρ) J where
32   projector i := (E.projector i).changeCoefficients f
33   orthogonal i j hij := by
34     change ((E.projector i).matrix.map f) * ((E.projector j).matrix.map f) = 0
35     rw [← Matrix.map_mul, E.orthogonal i j hij]
36     exact f.mapMatrix.map_zero
37   total := by
38     change ∑ i, f.mapMatrix (E.projector i).matrix = 1
39     rw [← map_sum, E.total, map_one]
40 
41 end Family
42 end PaperX.OrthogonalProjectors

Back to source controls