OrthogonalSummands.lean

1 import PaperXI.OddSymplectic
2 import Mathlib.LinearAlgebra.FiniteDimensional.Basic
3 import Mathlib.Algebra.Module.Submodule.LinearMap
4 import Mathlib.Algebra.BigOperators.Module
5 
6 /-! Actual restricted forms and automorphisms on an internal orthogonal
7 family. Nondegeneracy is derived from orthogonality and spanning. Inverse
8 invariance is derived from finite-dimensionality and forward invariance. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.OrthogonalSummands
12 open scoped BigOperators
13 
14 variable {K V ι : Type*} [Field K] [AddCommGroup V] [Module K V]
15 
16 /-- The restriction of the actual alternating form remains alternating. -/
17 theorem restricted_isAlt (b : LinearMap.BilinForm K V) (ha : b.IsAlt)
18     (S : Submodule K V) : (b.restrict S).IsAlt := fun x => ha x
19 
20 /-- Every summand in an orthogonal spanning family inherits nondegeneracy.
21 Neither finite-dimensionality nor an assumed restricted form is used. -/
22 theorem restricted_form_nondegenerate (b : LinearMap.BilinForm K V) (hn : b.Nondegenerate)
23     (S : ι → Submodule K V) (hspan : (⨆ i, S i) = ⊤)
24     (horth : ∀ i j, i ≠ j → ∀ x ∈ S i, ∀ y ∈ S j, b x y = 0) (i : ι) :
25     (b.restrict (S i)).Nondegenerate := by
26   constructor
27   · intro x hx
28     apply Subtype.ext
29     apply hn.1 (x : V)
30     have hk : (⨆ j, S j) ≤ (b x).ker := by
31       apply iSup_le
32       intro j y hy
33       change b x y = 0
34       by_cases hji : j = i
35       · subst j
36         exact hx ⟨y, hy⟩
37       · exact horth i j (Ne.symm hji) x x.property y hy
38     rw [hspan] at hk
39     intro y
40     exact hk (Submodule.mem_top : y ∈ (⊤ : Submodule K V))
41   · intro x hx
42     apply Subtype.ext
43     apply hn.2 (x : V)
44     have hk : (⨆ j, S j) ≤ (b.flip x).ker := by
45       apply iSup_le
46       intro j y hy
47       change b y x = 0
48       by_cases hji : j = i
49       · subst j
50         exact hx ⟨y, hy⟩
51       · exact horth j i hji y hy x x.property
52     rw [hspan] at hk
53     intro y
54     exact hk (Submodule.mem_top : y ∈ (⊤ : Submodule K V))
55 
56 /-- A finite internal sum equivalence with the literal summation equation
57 supplies the spanning hypothesis used above. -/
58 theorem iSup_eq_top_of_equiv_sum [Fintype ι] (S : ι → Submodule K V)
59     (E : (∀ i, S i) ≃ₗ[K] V) (hE : ∀ x, E x = ∑ i, (x i : V)) :
60     (⨆ i, S i) = ⊤ := by
61   apply top_unique
62   intro v _
63   obtain ⟨x, rfl⟩ := E.surjective v
64   rw [hE]
65   exact Submodule.sum_mem _ (fun i _ => (le_iSup S i) (x i).property)
66 
67 variable [FiniteDimensional K V]
68 
69 /-- Actual restriction of an invertible ambient map to a forward-invariant
70 subspace. Surjectivity of the restriction is proved from its injectivity. -/
71 def restrictionEquiv (g : V ≃ₗ[K] V) (S : Submodule K V)
72     (hg : ∀ x ∈ S, g x ∈ S) : S ≃ₗ[K] S :=
73   LinearEquiv.ofInjectiveEndo (g.toLinearMap.restrict hg) (by
74     intro x y h
75     apply Subtype.ext
76     exact g.injective (congrArg Subtype.val h))
77 
78 @[simp] theorem restrictionEquiv_coe (g : V ≃ₗ[K] V) (S : Submodule K V)
79     (hg : ∀ x ∈ S, g x ∈ S) (x : S) : (restrictionEquiv g S hg x : V) = g x := rfl
80 
81 /-- The inverse of the restricted equivalence is the actual ambient inverse. -/
82 theorem restrictionEquiv_symm_coe (g : V ≃ₗ[K] V) (S : Submodule K V)
83     (hg : ∀ x ∈ S, g x ∈ S) (x : S) :
84     ((restrictionEquiv g S hg).symm x : V) = g.symm x := by
85   apply g.injective
86   rw [g.apply_symm_apply]
87   exact congrArg Subtype.val ((restrictionEquiv g S hg).apply_symm_apply x)
88 
89 /-- Forward invariance under an invertible finite-dimensional map also gives
90 inverse invariance; it is not an extra source hypothesis. -/
91 theorem inverse_mem (g : V ≃ₗ[K] V) (S : Submodule K V)
92     (hg : ∀ x ∈ S, g x ∈ S) (x : V) (hx : x ∈ S) : g.symm x ∈ S := by
93   rw [← restrictionEquiv_symm_coe g S hg ⟨x, hx⟩]
94   exact ((restrictionEquiv g S hg).symm ⟨x, hx⟩).property
95 
96 /-- Preservation of the ambient form gives preservation of its actual restriction. -/
97 theorem restrictionEquiv_form (b : LinearMap.BilinForm K V) (g : V ≃ₗ[K] V)
98     (hform : ∀ x y, b (g x) (g y) = b x y)
99     (S : Submodule K V) (hg : ∀ x ∈ S, g x ∈ S) (x y : S) :
100     b.restrict S (restrictionEquiv g S hg x) (restrictionEquiv g S hg y) =
101       b.restrict S x y := hform x y
102 
103 /-- A fixed-point-free ambient automorphism remains so on each invariant summand. -/
104 theorem restrictionEquiv_fixed_eq_zero (g : V ≃ₗ[K] V)
105     (hfix : ∀ x, g x = x → x = 0) (S : Submodule K V)
106     (hg : ∀ x ∈ S, g x ∈ S) (x : S) (hx : restrictionEquiv g S hg x = x) : x = 0 := by
107   apply Subtype.ext
108   exact hfix x (congrArg Subtype.val hx)
109 
110 /-- Each actual orthogonal summand has even dimension under the odd-characteristic
111 symplectic hypotheses. -/
112 theorem restricted_even_finrank (b : LinearMap.BilinForm K V) (ha : b.IsAlt)
113     (hn : b.Nondegenerate) (h2 : (2 : K) ≠ 0) (S : ι → Submodule K V)
114     (hspan : (⨆ i, S i) = ⊤)
115     (horth : ∀ i j, i ≠ j → ∀ x ∈ S i, ∀ y ∈ S j, b x y = 0) (i : ι) :
116     Even (Module.finrank K (S i)) :=
117   OddSymplectic.even_finrank (b.restrict (S i)) (restricted_isAlt b ha (S i))
118     (restricted_form_nondegenerate b hn S hspan horth i) h2
119 
120 end PaperXI.OrthogonalSummands

Back to source controls