SummandExamples.lean

1 import PaperX.PrecisionIdempotent
2 import PaperX.SummandBoundary
3 
4 /-! A concrete application of precision idempotent lifting to an actual
5 continuous C2 carrier over Z_2.  The supplied projector lives modulo four;
6 the theorem constructs an exact nonzero proper equivariant projector. -/
7 set_option autoImplicit false
8 namespace PaperX.SummandExamples
9 open scoped Matrix
10 open PaperX.RepresentationLimits PaperX.CompletionExamples
11 open PaperX.PrecisionExamples PaperX.SummandBoundary
12 
13 /-- The prescribed mod-four projector is idempotent. -/
14 theorem skew_two_quotient_idempotent :
15     (skewProjector 2).map (Ideal.Quotient.mk (twoIdeal^2)) *
16         (skewProjector 2).map (Ideal.Quotient.mk (twoIdeal^2)) =
17       (skewProjector 2).map (Ideal.Quotient.mk (twoIdeal^2)) := by
18   rw [← Matrix.map_mul, skewProjector_idempotent]
19 
20 theorem skew_two_commutes_quotient (g : C2) :
21     (tau g).map (Ideal.Quotient.mk (twoIdeal^2)) *
22         (skewProjector 2).map (Ideal.Quotient.mk (twoIdeal^2)) =
23       (skewProjector 2).map (Ideal.Quotient.mk (twoIdeal^2)) *
24         (tau g).map (Ideal.Quotient.mk (twoIdeal^2)) := by
25   rw [← Matrix.map_mul, ← Matrix.map_mul]
26   apply (quotient_matrices_eq_iff 2 _ _).mpr
27   simpa only [Matrix.map_mul] using skew_two_commutes_mod_four g
28 
29 /-- This uses the general lifting theorem on finite quotient input.  An exact
30 projector is obtained as a conclusion, not supplied as an input. -/
31 theorem actual_two_adic_projector_lift :
32     ∃ E : Matrix (Fin 2) (Fin 2) ℤ_[2], E * E = E ∧
33       E.map (Ideal.Quotient.mk (twoIdeal^1)) =
34         (skewProjector 2).map (Ideal.Quotient.mk (twoIdeal^1)) ∧
35       (∀ g : C2, tau g * E = E * tau g) ∧ E ≠ 0 ∧ E ≠ 1 := by
36   let B := (skewProjector 2).map (Ideal.Quotient.mk (twoIdeal^2))
37   obtain ⟨E, hid, hred, hcomm⟩ := PrecisionIdempotent.exists_idempotent_lift
38     (2 : ℤ_[2]) 1 1 tau group_order_nonzero group_order_divides_two (by decide)
39     B skew_two_quotient_idempotent skew_two_commutes_quotient
40   have hE : E.map (Ideal.Quotient.mk (twoIdeal^1)) =
41       (skewProjector 2).map (Ideal.Quotient.mk (twoIdeal^1)) := by
42     rw [hred]
43     ext i j
44     simp [B]
45   refine ⟨E, hid, hE, hcomm, ?_, ?_⟩
46   · intro hz
47     have h := (quotient_matrices_eq_iff 1 E (skewProjector 2)).mp hE
48     have h00 := congrArg (fun M : Matrix (Fin 2) (Fin 2) (ZMod (2^1)) => M 0 0) h
49     norm_num [hz, skewProjector] at h00
50     exact (by decide : (0 : ZMod (2^1)) ≠ 1) h00
51   · intro hi
52     have h := (quotient_matrices_eq_iff 1 E (skewProjector 2)).mp hE
53     have h11 := congrArg (fun M : Matrix (Fin 2) (Fin 2) (ZMod (2^1)) => M 1 1) h
54     norm_num [hi, skewProjector] at h11
55     exact (by decide : (1 : ZMod (2^1)) ≠ 0) h11
56 
57 end PaperX.SummandExamples

Back to source controls