PrecisionIdempotent.lean

1 import PaperX.AdicIdempotent
2 import PaperX.PrecisionAveraging
3 
4 /-! Finite-group equivariant idempotents lift from sufficiently deep reduction
5 inside an actual supplied integral carrier. Averaging loses at most `e` digits;
6 complete-ring polynomial correction preserves the retained positive precision. -/
7 set_option autoImplicit false
8 
9 namespace PaperX.PrecisionIdempotent
10 open PaperX.RepresentationLimits
11 
12 variable {R : Type*} [CommRing R] [IsDomain R]
13 variable {Γ : Type*} [Group Γ] [Fintype Γ]
14 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
15 
16 /-- An equivariant quotient idempotent lifts to an actual equivariant integral
17 idempotent. The given quotient data at depth `e+k` is retained at depth `k`.
18 No exact summand and no compatible family of quotient idempotents is assumed. -/
19 theorem exists_idempotent_lift (π : R) [IsAdicComplete (Ideal.span {π}) R]
20     (e k : ℕ) (ρ : MatrixRep R Γ ι)
21     (hΓ : (Fintype.card Γ : R) ≠ 0) (hdiv : (Fintype.card Γ : R) ∣ π^e)
22     (hk : 0 < k) (B : Matrix ι ι (R ⧸ (Ideal.span {π})^(e+k)))
23     (hB : B * B = B)
24     (hcomm : ∀ g, (ρ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k))) * B =
25       B * (ρ g).map (Ideal.Quotient.mk ((Ideal.span {π})^(e+k)))) :
26     ∃ E : Matrix ι ι R, E * E = E ∧
27       E.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) =
28         B.map (Ideal.Quotient.factorPow (Ideal.span {π}) (Nat.le_add_left k e)) ∧
29       ∀ g, ρ g * E = E * ρ g := by
30   obtain ⟨A, hA, hc⟩ := PrecisionAveraging.exists_intertwiner_lift π e k ρ ρ hΓ hdiv B hcomm
31   have ha : (A.map (Ideal.Quotient.mk ((Ideal.span {π})^k)))^2 =
32       A.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) := by
33     rw [hA, pow_two, ← Matrix.map_mul, hB]
34   obtain ⟨E, hE, heq, hi⟩ := AdicIdempotent.correct_commuting (Ideal.span {π}) k hk A ha
35   exact ⟨E, by simpa only [pow_two] using hE, heq.trans hA, fun g => hi (ρ g) (hc g)⟩
36 
37 end PaperX.PrecisionIdempotent

Back to source controls