English
The basis representation of a quadratic map along a basis is the composition with the basis change map.
Русский
Базисное представление квадратичной карты вдоль базиса есть композиция с базисным переходом.
LaTeX
$$basisRepr(Q, v) = Q.comp v.equivFun.symm$$
Lean4
/-- Given a symmetric bilinear form `B` on some vector space `V` over a field `K`
in which `2` is invertible, there exists an orthogonal basis with respect to `B`. -/
theorem exists_orthogonal_basis [hK : Invertible (2 : K)] {B : LinearMap.BilinForm K V} (hB₂ : B.IsSymm) :
∃ v : Basis (Fin (finrank K V)) K V, B.IsOrthoᵢ v :=
by
suffices ∀ d, finrank K V = d → ∃ v : Basis (Fin d) K V, B.IsOrthoᵢ v by exact this _ rfl
intro d hd
induction d generalizing V with
| zero => exact ⟨basisOfFinrankZero hd, fun _ _ _ => map_zero _⟩
| succ d
ih =>
haveI :=
finrank_pos_iff.1
(hd.symm ▸ Nat.succ_pos d : 0 < finrank K V)
-- either the bilinear form is trivial or we can pick a non-null `x`
obtain rfl | hB₁ := eq_or_ne B 0
· let b := Module.finBasis K V
rw [hd] at b
exact ⟨b, fun i j _ => rfl⟩
obtain ⟨x, hx⟩ := exists_bilinForm_self_ne_zero hB₁ hB₂
rw [← Submodule.finrank_add_eq_of_isCompl (isCompl_span_singleton_orthogonal hx).symm,
finrank_span_singleton (ne_zero_of_map hx)] at hd
let B' := B.domRestrict₁₂ (Submodule.orthogonalBilin (K ∙ x) B) (Submodule.orthogonalBilin (K ∙ x) B)
obtain ⟨v', hv₁⟩ :=
ih (hB₂.domRestrict _ : B'.IsSymm)
(Nat.succ.inj hd)
-- concatenate `x` with the basis obtained by induction
let b :=
Basis.mkFinCons x v'
(by
rintro c y hy hc
rw [add_eq_zero_iff_neg_eq] at hc
rw [← hc, Submodule.neg_mem_iff] at hy
have := (isCompl_span_singleton_orthogonal hx).disjoint
rw [Submodule.disjoint_def] at this
have := this (c • x) (Submodule.smul_mem _ _ <| Submodule.mem_span_singleton_self _) hy
exact (smul_eq_zero.1 this).resolve_right fun h => hx <| h.symm ▸ map_zero _)
(by
intro y
refine ⟨-B x y / B x x, fun z hz => ?_⟩
obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hz
rw [IsOrtho, map_smul, smul_apply, map_add, map_smul, smul_eq_mul, smul_eq_mul, div_mul_cancel₀ _ hx,
add_neg_cancel, mul_zero])
refine ⟨b, ?_⟩
rw [Basis.coe_mkFinCons]
intro j i
refine Fin.cases ?_ (fun i => ?_) i <;> refine Fin.cases ?_ (fun j => ?_) j <;> intro hij <;>
simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]
· exact (hij rfl).elim
· rw [IsOrtho, ← hB₂.eq]
exact (v' j).prop _ (Submodule.mem_span_singleton_self x)
· exact (v' i).prop _ (Submodule.mem_span_singleton_self x)
· exact hv₁ (ne_of_apply_ne _ hij)
