FiniteCarrierSummands.lean

1 import PaperX.MatrixProjector
2 import PaperX.PrecisionIdempotent
3 
4 /-! End-to-end lifting of an actual summand inside a supplied finite-group carrier.
5 Only one sufficiently deep equivariant quotient projector is required. -/
6 set_option autoImplicit false
7 namespace PaperX.FiniteCarrierSummands
8 open PaperX.RepresentationLimits PaperX.MatrixProjector
9 
10 variable {R Γ ι : Type*} [CommRing R] [IsDomain R]
11   [Group Γ] [Fintype Γ] [Fintype ι] [DecidableEq ι]
12 
13 /-- The carrier's integral projector is constructed, not an input. -/
14 theorem exists_split_projector (π : R) [IsAdicComplete (Ideal.span {π}) R]
15     (e k : ℕ) (ρ : MatrixRep R Γ ι)
16     (hΓ : (Fintype.card Γ : R) ≠ 0) (hdiv : (Fintype.card Γ : R) ∣ π^e)
17     (hk : 0 < k) (B : Matrix ι ι (R ⧸ (Ideal.span {π})^(e+k)))
18     (hB : B * B = B)
19     (hcomm : ∀ g, (ρ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k))) * B =
20       B * (ρ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k)))) :
21     ∃ P : Projector ρ,
22       P.matrix.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) =
23         B.map (Ideal.Quotient.factorPow (Ideal.span {π}) (Nat.le_add_left k e)) := by
24   obtain ⟨E, hE, hred, hρ⟩ := PrecisionIdempotent.exists_idempotent_lift
25     π e k ρ hΓ hdiv hk B hB hcomm
26   exact ⟨⟨E, hE, hρ⟩, hred⟩
27 
28 /-- Equivariant inclusion and retraction are actual maps of the actual image.
29 Their projection and the full carrier decomposition follow from the constructed
30 projector. Both summands reduce onto exactly the prescribed quotient submodules. -/
31 theorem exists_lifted_summand (π : R) [IsAdicComplete (Ideal.span {π}) R]
32     (e k : ℕ) (ρ : MatrixRep R Γ ι)
33     (hΓ : (Fintype.card Γ : R) ≠ 0) (hdiv : (Fintype.card Γ : R) ∣ π^e)
34     (hk : 0 < k) (B : Matrix ι ι (R ⧸ (Ideal.span {π})^(e+k)))
35     (hB : B * B = B)
36     (hcomm : ∀ g, (ρ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k))) * B =
37       B * (ρ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k)))) :
38     ∃ P : Projector ρ,
39       P.matrix.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) =
40         B.map (Ideal.Quotient.factorPow (Ideal.span {π}) (Nat.le_add_left k e)) ∧
41       P.retraction.comp P.inclusion = LinearMap.id ∧
42       P.inclusion.comp P.retraction = P.linear ∧
43       (∀ g v, P.inclusion (P.image.toRepresentation g v) = carrier ρ g (P.inclusion v)) ∧
44       (∀ g v, P.retraction (carrier ρ g v) = P.image.toRepresentation g (P.retraction v)) ∧
45       (∀ w : ι → R ⧸ (Ideal.span {π})^k,
46         (∃ v : P.image.toSubmodule,
47           (Ideal.Quotient.mk ((Ideal.span {π})^k)) ∘ (v : ι → R) = w) ↔
48         (B.map (Ideal.Quotient.factorPow (Ideal.span {π}) (Nat.le_add_left k e))).mulVec w = w) ∧
49       (∀ w : ι → R ⧸ (Ideal.span {π})^k,
50         (∃ v : P.kernel.toSubmodule,
51           (Ideal.Quotient.mk ((Ideal.span {π})^k)) ∘ (v : ι → R) = w) ↔
52         (B.map (Ideal.Quotient.factorPow (Ideal.span {π}) (Nat.le_add_left k e))).mulVec w = 0) := by
53   obtain ⟨P, hP⟩ := exists_split_projector π e k ρ hΓ hdiv hk B hB hcomm
54   refine ⟨P, hP, P.split_law, P.inclusion_retraction,
55     P.inclusion_equivariant, P.retraction_equivariant, ?_, ?_⟩
56   · intro w
57     rw [P.image_reduction_iff _ Ideal.Quotient.mk_surjective,
58       (P.changeCoefficients (Ideal.Quotient.mk ((Ideal.span {π})^k))).image_iff]
59     change (P.matrix.map _).mulVec w = w ↔ _
60     rw [hP]
61   · intro w
62     rw [P.kernel_reduction_iff _ Ideal.Quotient.mk_surjective]
63     change (P.matrix.map _).mulVec w = 0 ↔ _
64     rw [hP]
65 
66 /-- The same projector defines a summand of any pullback through the finite group. -/
67 def pullback {G : Type*} [Group G] (ρ : MatrixRep R Γ ι)
68     (P : Projector ρ) (q : G →* Γ) : Projector (ρ.comp q) where
69   matrix := P.matrix
70   idempotent := P.idempotent
71   commutes g := P.commutes (q g)
72 
73 omit [IsDomain R] [Fintype Γ] in
74 theorem pullback_projection (ρ : MatrixRep R Γ ι) (P : Projector ρ)
75     {G : Type*} [Group G] (q : G →* Γ) : (pullback ρ P q).matrix = P.matrix := rfl
76 
77 end PaperX.FiniteCarrierSummands

Back to source controls