OrthogonalPhase.lean

1 import PaperXI.OddPhaseSum
2 import PaperXI.OrthogonalSummands
3 import Mathlib.Algebra.DirectSum.Module
4 
5 /-! Source 12.4 for an actual finite internal orthogonal decomposition. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.OrthogonalPhase
9 open scoped BigOperators Classical
10 
11 variable {K X ι : Type*} [Field K] [AddCommGroup X] [Module K X] [Fintype ι]
12 
13 /-- The actual internal direct-sum map becomes a finite-product equivalence. -/
14 def decomposition (S : ι → Submodule K X) (hS : DirectSum.IsInternal S) :
15     (∀ i, S i) ≃ₗ[K] X :=
16   (DirectSum.linearEquivFunOnFintype K ι (fun i => S i)).symm.trans
17     (LinearEquiv.ofBijective (DirectSum.coeLinearMap S) hS)
18 
19 theorem decomposition_sum (S : ι → Submodule K X) (hS : DirectSum.IsInternal S)
20     (x : ∀ i, S i) : decomposition S hS x = ∑ i, (x i : X) := by
21   classical
22   have he : (decomposition S hS).toLinearMap =
23       ∑ i, (S i).subtype.comp (LinearMap.proj i) := by
24     apply LinearMap.pi_ext
25     intro i y
26     simp only [LinearMap.sum_apply, LinearMap.comp_apply, LinearMap.proj_apply,
27       Submodule.subtype_apply]
28     change (DirectSum.coeLinearMap S)
29       ((DirectSum.linearEquivFunOnFintype K ι (fun i => S i)).symm (Pi.single i y)) = _
30     rw [DirectSum.linearEquivFunOnFintype_symm_single, DirectSum.coeLinearMap_lof]
31     symm
32     have hs : ∑ j, ((Pi.single i y : ∀ j, S j) j : X) =
33         ((Pi.single i y : ∀ j, S j) i : X) := by
34       apply Finset.sum_eq_single i
35       · intro j _ hji
36         rw [Pi.single_eq_of_ne hji]
37         rfl
38       · intro hi
39         exact (hi (Finset.mem_univ i)).elim
40     simpa using hs
41   simpa only [LinearMap.sum_apply, LinearMap.comp_apply, LinearMap.proj_apply,
42     Submodule.subtype_apply, LinearEquiv.coe_coe] using
43     congrArg (fun f : (∀ i, S i) →ₗ[K] X => f x) he
44 
45 variable [FiniteDimensional K X]
46 
47 def restricted (G : X ≃ₗ[K] X) (S : ι → Submodule K X)
48     (hstable : ∀ i, ∀ x ∈ S i, G x ∈ S i) (i : ι) : S i ≃ₗ[K] S i :=
49   OrthogonalSummands.restrictionEquiv G (S i) (hstable i)
50 
51 omit [Fintype ι] in
52 @[simp] theorem restricted_coe (G : X ≃ₗ[K] X) (S : ι → Submodule K X)
53     (hstable : ∀ i, ∀ x ∈ S i, G x ∈ S i) (i : ι) (x : S i) :
54     (restricted G S hstable i x : X) = G x := rfl
55 
56 theorem intertwines (G : X ≃ₗ[K] X) (S : ι → Submodule K X)
57     (hS : DirectSum.IsInternal S) (hstable : ∀ i, ∀ x ∈ S i, G x ∈ S i)
58     (x : ∀ i, S i) :
59     decomposition S hS (LinearEquiv.piCongrRight (restricted G S hstable) x) =
60       G (decomposition S hS x) := by
61   simp only [decomposition_sum, map_sum, LinearEquiv.piCongrRight_apply, restricted_coe]
62 
63 section PrimeField
64 variable {p : ℕ} [Fact p.Prime]
65 variable {V : Type*} [AddCommGroup V] [Module (ZMod p) V]
66 variable [FiniteDimensional (ZMod p) V]
67 
68 theorem phase_product (hp : p ≠ 2) (b : LinearMap.BilinForm (ZMod p) V)
69     (ha : b.IsAlt) (hn : b.Nondegenerate) (G : V ≃ₗ[ZMod p] V)
70     (S : ι → Submodule (ZMod p) V) (hS : DirectSum.IsInternal S)
71     (horth : ∀ i j, i ≠ j → ∀ x ∈ S i, ∀ y ∈ S j, b x y = 0)
72     (hstable : ∀ i, ∀ x ∈ S i, G x ∈ S i) :
73     OddPhase.phase G = ∏ i, OddPhase.phase (restricted G S hstable i) := by
74   apply OddPhaseSum.of_decomposition hp (fun i => b.restrict (S i))
75     (fun i => OrthogonalSummands.restricted_isAlt b ha (S i))
76     (fun i => OrthogonalSummands.restricted_form_nondegenerate b hn S
77       hS.submodule_iSup_eq_top horth i)
78     (restricted G S hstable) G (decomposition S hS)
79   exact intertwines G S hS hstable
80 
81 theorem fixedPointFree (G : V ≃ₗ[ZMod p] V)
82     (S : ι → Submodule (ZMod p) V) (hS : DirectSum.IsInternal S)
83     (hstable : ∀ i, ∀ x ∈ S i, G x ∈ S i)
84     (hfix : ∀ i, OddPhase.FixedPointFree (restricted G S hstable i)) :
85     OddPhase.FixedPointFree G :=
86   OddPhaseSum.fixedPointFree_of_decomposition (restricted G S hstable) hfix G
87     (decomposition S hS) (intertwines G S hS hstable)
88 
89 /-- Full finite orthogonal multiplicativity: the restricted forms and actions
90 are constructed from the ambient data, and all fixed-point-free conditions hold. -/
91 theorem source (hp : p ≠ 2) (b : LinearMap.BilinForm (ZMod p) V)
92     (ha : b.IsAlt) (hn : b.Nondegenerate) (G : V ≃ₗ[ZMod p] V)
93     (hform : ∀ x y, b (G x) (G y) = b x y)
94     (S : ι → Submodule (ZMod p) V) (hS : DirectSum.IsInternal S)
95     (horth : ∀ i j, i ≠ j → ∀ x ∈ S i, ∀ y ∈ S j, b x y = 0)
96     (hstable : ∀ i, ∀ x ∈ S i, G x ∈ S i)
97     (hfix : ∀ i, OddPhase.FixedPointFree (restricted G S hstable i)) :
98     (∀ i, (b.restrict (S i)).IsAlt ∧ (b.restrict (S i)).Nondegenerate) ∧
99       (∀ i (x y : S i), b.restrict (S i) (restricted G S hstable i x)
100         (restricted G S hstable i y) = b.restrict (S i) x y) ∧
101       OddPhase.FixedPointFree G ∧
102       OddPhase.phase G = ∏ i, OddPhase.phase (restricted G S hstable i) := by
103   refine ⟨fun i => ⟨OrthogonalSummands.restricted_isAlt b ha (S i),
104     OrthogonalSummands.restricted_form_nondegenerate b hn S
105       hS.submodule_iSup_eq_top horth i⟩, ?_, fixedPointFree G S hS hstable hfix,
106     phase_product hp b ha hn G S hS horth hstable⟩
107   intro i x y
108   exact OrthogonalSummands.restrictionEquiv_form b G hform (S i) (hstable i) x y
109 
110 end PrimeField
111 end PaperXI.OrthogonalPhase

Back to source controls