FixedMovingSource.lean

1 import PaperXI.FixedMoving
2 import PaperXI.FiniteFieldAverage
3 import PaperXI.OddPhase
4 import Mathlib.RingTheory.Finiteness.Cardinality
5 
6 /-! The source fixed/moving theorem, with the decomposition and restricted
7 invertibility derived from the actual finite order prime to the characteristic. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.FixedMoving
11 
12 variable {F V : Type*} [Field F] [AddCommGroup V] [Module F V]
13 
14 /-- Finite order with invertible order scalar gives the actual complementary subspaces. -/
15 theorem isCompl_of_period (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1) (hm : (m : F) ≠ 0) :
16     IsCompl (fixed g) (moving g) := FiniteFieldAverage.isCompl g m hpow hm
17 
18 /-- The constructed decomposition equivalence has the literal sum as its forward map. -/
19 def decomposition (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1) (hm : (m : F) ≠ 0) :
20     (fixed g × moving g) ≃ₗ[F] V := FiniteFieldAverage.decomposition g m hpow hm
21 
22 @[simp] theorem decomposition_apply (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
23     (hm : (m : F) ≠ 0) (v : fixed g × moving g) :
24     decomposition g m hpow hm v = (v.1 : V) + (v.2 : V) := rfl
25 
26 /-- The fixed projection is the actual finite average. -/
27 theorem decomposition_fixed (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
28     (hm : (m : F) ≠ 0) (v : V) :
29     (((decomposition g m hpow hm).symm v).1 : V) = FiniteFieldAverage.average g m v :=
30   FiniteFieldAverage.decomposition_symm_fst g m hpow hm v
31 
32 /-- The moving projection is the remainder after the actual finite average. -/
33 theorem decomposition_moving (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
34     (hm : (m : F) ≠ 0) (v : V) :
35     (((decomposition g m hpow hm).symm v).2 : V) = v - FiniteFieldAverage.average g m v :=
36   FiniteFieldAverage.decomposition_symm_snd g m hpow hm v
37 
38 theorem movingForm_nondegenerate (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
39     (hm : (m : F) ≠ 0) (b : LinearMap.BilinForm F V) (hb : b.IsAlt)
40     (hbn : b.Nondegenerate) (hg : ∀ x y, b (g x) (g y) = b x y) :
41     (movingForm g b).Nondegenerate :=
42   movingForm_nondegenerate_of_isCompl g b hb hbn hg (isCompl_of_period g m hpow hm)
43 
44 theorem fixedForm_nondegenerate (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
45     (hm : (m : F) ≠ 0) (b : LinearMap.BilinForm F V) (hb : b.IsAlt)
46     (hbn : b.Nondegenerate) (hg : ∀ x y, b (g x) (g y) = b x y) :
47     (fixedForm g b).Nondegenerate :=
48   fixedForm_nondegenerate_of_isCompl g b hb hbn hg (isCompl_of_period g m hpow hm)
49 
50 section PrimeField
51 variable {p : ℕ} [Fact p.Prime]
52 variable {U : Type*} [AddCommGroup U] [Module (ZMod p) U]
53 
54 /-- Finite dimension over the actual finite field makes the automorphism order positive. -/
55 theorem source_order_pos [FiniteDimensional (ZMod p) U] (g : U ≃ₗ[ZMod p] U) : 0 < orderOf g := by
56   let : Finite U := Module.finite_of_finite (ZMod p)
57   let : Finite (U ≃ₗ[ZMod p] U) :=
58     Finite.of_injective (fun e : U ≃ₗ[ZMod p] U => (e : U → U))
59       (fun _ _ he => LinearEquiv.ext (congrFun he))
60   exact orderOf_pos g
61 
62 /-- The source prime-to-characteristic order condition supplies an invertible field scalar. -/
63 theorem source_order_ne_zero (g : U ≃ₗ[ZMod p] U) (horder : Nat.Coprime (orderOf g) p) :
64     (orderOf g : ZMod p) ≠ 0 := by
65   rw [Ne, ZMod.natCast_eq_zero_iff]
66   exact (Fact.out : p.Prime).coprime_iff_not_dvd.mp horder.symm
67 
68 theorem source_isCompl (g : U ≃ₗ[ZMod p] U) (horder : Nat.Coprime (orderOf g) p) :
69     IsCompl (fixed g) (moving g) :=
70   isCompl_of_period g (orderOf g) (pow_orderOf_eq_one g) (source_order_ne_zero g horder)
71 
72 /-- The source decomposition, constructed from the actual order of the automorphism. -/
73 def sourceDecomposition (g : U ≃ₗ[ZMod p] U) (horder : Nat.Coprime (orderOf g) p) :
74     (fixed g × moving g) ≃ₗ[ZMod p] U :=
75   decomposition g (orderOf g) (pow_orderOf_eq_one g) (source_order_ne_zero g horder)
76 
77 @[simp] theorem sourceDecomposition_apply (g : U ≃ₗ[ZMod p] U)
78     (horder : Nat.Coprime (orderOf g) p) (v : fixed g × moving g) :
79     sourceDecomposition g horder v = (v.1 : U) + (v.2 : U) := rfl
80 
81 theorem source_moving_fixedPointFree (g : U ≃ₗ[ZMod p] U)
82     (horder : Nat.Coprime (orderOf g) p) : OddPhase.FixedPointFree (movingAction g) :=
83   movingAction_fixedPointFree_of_isCompl g (source_isCompl g horder)
84 
85 /-- The source's actual restricted difference as a linear equivalence. -/
86 def sourceMovingDifference [FiniteDimensional (ZMod p) U] (g : U ≃ₗ[ZMod p] U) (horder : Nat.Coprime (orderOf g) p) :
87     moving g ≃ₗ[ZMod p] moving g := movingDifferenceEquiv g (source_isCompl g horder)
88 
89 @[simp] theorem sourceMovingDifference_apply [FiniteDimensional (ZMod p) U] (g : U ≃ₗ[ZMod p] U)
90     (horder : Nat.Coprime (orderOf g) p) (v : moving g) :
91     sourceMovingDifference g horder v = movingAction g v - v := rfl
92 
93 /-- Source 12.6: the actual orthogonal decomposition, nondegenerate restrictions,
94 and invertibility of the actual moving difference all follow from the source hypotheses. -/
95 theorem source [FiniteDimensional (ZMod p) U] (g : U ≃ₗ[ZMod p] U) (horder : Nat.Coprime (orderOf g) p)
96     (b : LinearMap.BilinForm (ZMod p) U) (hb : b.IsAlt) (hbn : b.Nondegenerate)
97     (hg : ∀ x y, b (g x) (g y) = b x y) :
98     0 < orderOf g ∧ IsCompl (fixed g) (moving g) ∧
99       (∀ x ∈ fixed g, ∀ y ∈ moving g, b x y = 0) ∧
100       (fixedForm g b).Nondegenerate ∧ (movingForm g b).Nondegenerate ∧
101       OddPhase.FixedPointFree (movingAction g) ∧
102       Function.Bijective (OddPhase.difference (movingAction g)) := by
103   have hc := source_isCompl g horder
104   have hfree := source_moving_fixedPointFree g horder
105   exact ⟨source_order_pos g, hc, fun _ hx _ hy => orthogonal g b hg hx hy,
106     fixedForm_nondegenerate_of_isCompl g b hb hbn hg hc,
107     movingForm_nondegenerate_of_isCompl g b hb hbn hg hc,
108     hfree, (OddPhase.fixedPointFree_iff_bijective (movingAction g)).mp hfree⟩
109 
110 end PrimeField
111 end PaperXI.FixedMoving

Back to source controls