noncomputable def Garrett.BilinForm.orthogonalSum {k : Type u_1} [Field k] {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) : LinearMap.BilinForm k (V₁ × V₂)

The orthogonal direct sum of two bilinear forms B₁ on V₁ and B₂ on V₂, defined on the product space by (p, q) ↦ B₁ p.1 q.1 + B₂ p.2 q.2.

@[simp]

theorem Garrett.BilinForm.orthogonalSum_apply {k : Type u_1} [Field k] {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) (v w : V₁ × V₂) : ((orthogonalSum B₁ B₂) v) w = (B₁ v.1) w.1 + (B₂ v.2) w.2

Evaluation formula for the orthogonal direct sum of bilinear forms.

theorem Garrett.neg_orthogonalSum_eq {k : Type u_1} [Field k] {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) : -BilinForm.orthogonalSum B₁ B₂ = BilinForm.orthogonalSum (-B₁) (-B₂)

Negation distributes over the orthogonal direct sum of bilinear forms.

def Garrett.BilinForm.IsNondegenerate' {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Prop

A bilinear form is nondegenerate (in the orthogonal-complement sense) when the orthogonal complement of the whole space is trivial.

def Garrett.BilinForm.IsHyperbolic {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Prop

A bilinear form B is hyperbolic if it is nondegenerate and admits a Lagrangian subspace W (a totally isotropic subspace equal to its own orthogonal complement).

def Garrett.IsFormedSpaceIsometry {k : Type u_1} [Field k] {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) (φ : V₁ ≃ₗ[k] V₂) : Prop

A linear equivalence φ : V₁ ≃ₗ V₂ is an isometry of formed spaces if it preserves the corresponding bilinear forms B₁ and B₂.

def Garrett.FormedSpacesIsometric {k : Type u_1} [Field k] {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) : Prop

Two formed spaces (V₁, B₁) and (V₂, B₂) are isometric if there exists a linear equivalence between them preserving the bilinear forms.

theorem Garrett.orthogonalSum_nondegenerate {k : Type u_1} [Field k] {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) (h₁ : BilinForm.IsNondegenerate' B₁) (h₂ : BilinForm.IsNondegenerate' B₂) : BilinForm.IsNondegenerate' (BilinForm.orthogonalSum B₁ B₂)

The orthogonal direct sum of two nondegenerate bilinear forms is nondegenerate.

theorem Garrett.neg_nondegenerate {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hnd : BilinForm.IsNondegenerate' B) : BilinForm.IsNondegenerate' (-B)

The negation of a nondegenerate bilinear form is nondegenerate.

def Garrett.diagonal {k : Type u_1} [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] : Submodule k (V × V)

The diagonal subspace {(v, v) | v ∈ V} of V × V.

theorem Garrett.directSum_neg_isHyperbolic {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hnd : BilinForm.IsNondegenerate' B) : BilinForm.IsHyperbolic (BilinForm.orthogonalSum B (-B))

For any nondegenerate bilinear form B, the orthogonal direct sum B ⊕ (-B) is hyperbolic, with Lagrangian given by the diagonal subspace.

theorem Garrett.nondegenerate_fst_of_orthogonalSum {k : Type u_1} [Field k] {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) (hnd : BilinForm.IsNondegenerate' (BilinForm.orthogonalSum B₁ B₂)) : BilinForm.IsNondegenerate' B₁

If the orthogonal direct sum B₁ ⊕ B₂ is nondegenerate, then so is B₁.

theorem Garrett.lagrangian_W1_isotropic {k : Type u_2} [Field k] {V₁ : Type u_3} {V₂ : Type u_4} [AddCommGroup V₁] [Module k V₁] [FiniteDimensional k V₁] [AddCommGroup V₂] [Module k V₂] [FiniteDimensional k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) (W₁₂ : Submodule k (V₁ × V₂)) (W₂ : Submodule k V₂) (hW₁₂_iso : ∀ w₁ ∈ W₁₂, ∀ w₂ ∈ W₁₂, ((BilinForm.orthogonalSum B₁ B₂) w₁) w₂ = 0) (hW₂_iso : ∀ w₁ ∈ W₂, ∀ w₂ ∈ W₂, (B₂ w₁) w₂ = 0) : have W₁ := Submodule.map (LinearMap.fst k V₁ V₂) (W₁₂ ⊓ ⊤.prod W₂); W₁ ≤ B₁.orthogonal W₁

Given a totally isotropic subspace W₁₂ for B₁ ⊕ B₂ and a totally isotropic subspace W₂ for B₂, the projection of W₁₂ ∩ (V₁ × W₂) onto V₁ is a totally isotropic subspace for B₁.

theorem Garrett.IsNondegenerate'_to_Nondegenerate_inline {k₀ : Type u_2} [Field k₀] {V : Type u_3} [AddCommGroup V] [Module k₀ V] [FiniteDimensional k₀ V] {B : LinearMap.BilinForm k₀ V} (h : BilinForm.IsNondegenerate' B) : B.Nondegenerate

Convert the orthogonal-complement formulation of nondegeneracy into Mathlib's BilinForm.Nondegenerate predicate.

theorem Garrett.lagrangian_finrank_inline {k₀ : Type u_2} [Field k₀] {V : Type u_3} [AddCommGroup V] [Module k₀ V] [FiniteDimensional k₀ V] (B : LinearMap.BilinForm k₀ V) (W : Submodule k₀ V) (hW_lagrangian : B.orthogonal W = W) (hB_nd : BilinForm.IsNondegenerate' B) : 2 * Module.finrank k₀ ↥W = Module.finrank k₀ V

A Lagrangian subspace of a nondegenerate bilinear form has dimension equal to half the dimension of the ambient space.

theorem Garrett.lagrangian_extraction_hard_direction {k : Type u_2} [Field k] {V₁ : Type u_3} {V₂ : Type u_4} [AddCommGroup V₁] [Module k V₁] [FiniteDimensional k V₁] [AddCommGroup V₂] [Module k V₂] [FiniteDimensional k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) (W₁₂ : Submodule k (V₁ × V₂)) (W₂ : Submodule k V₂) (hW₁₂_iso : ∀ w₁ ∈ W₁₂, ∀ w₂ ∈ W₁₂, ((BilinForm.orthogonalSum B₁ B₂) w₁) w₂ = 0) (hW₁₂_orth : (BilinForm.orthogonalSum B₁ B₂).orthogonal W₁₂ = W₁₂) (hW₁₂_nd : BilinForm.IsNondegenerate' (BilinForm.orthogonalSum B₁ B₂)) (hW₂_iso : ∀ w₁ ∈ W₂, ∀ w₂ ∈ W₂, (B₂ w₁) w₂ = 0) (hW₂_orth : B₂.orthogonal W₂ = W₂) (hW₂_nd : BilinForm.IsNondegenerate' B₂) : have W₁ := Submodule.map (LinearMap.fst k V₁ V₂) (W₁₂ ⊓ ⊤.prod W₂); B₁.orthogonal W₁ ≤ W₁

Hard direction of the Lagrangian extraction lemma: with the same data as in lagrangian_W1_isotropic, the projection W₁ not only is contained in its orthogonal complement (the easy direction), but actually equals it. This step of the proof currently contains a sorry.

theorem Garrett.hyperbolic_cancel_summand {k : Type u_1} [Field k] {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module k V₁] [FiniteDimensional k V₁] [AddCommGroup V₂] [Module k V₂] [FiniteDimensional k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) (h_sum : BilinForm.IsHyperbolic (BilinForm.orthogonalSum B₁ B₂)) (h₂ : BilinForm.IsHyperbolic B₂) : BilinForm.IsHyperbolic B₁

Hyperbolic cancellation: if B₁ ⊕ B₂ is hyperbolic and B₂ is hyperbolic, then B₁ is hyperbolic.

theorem Garrett.isHyperbolic_of_isometric {k : Type u_1} [Field k] {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) (φ : V₁ ≃ₗ[k] V₂) (hiso : IsFormedSpaceIsometry B₁ B₂ φ) (hH : BilinForm.IsHyperbolic B₂) : BilinForm.IsHyperbolic B₁

Hyperbolicity is preserved under isometry: if (V₁, B₁) is isometric to a hyperbolic formed space (V₂, B₂), then B₁ is hyperbolic.

theorem Garrett.isHyperbolic_of_orthogonalSum_hyperbolic_isometric {k : Type u_1} [Field k] {X : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [AddCommGroup X] [Module k X] [FiniteDimensional k X] [AddCommGroup H₁] [Module k H₁] [FiniteDimensional k H₁] [AddCommGroup H₂] [Module k H₂] (B_X : LinearMap.BilinForm k X) (B_H₁ : LinearMap.BilinForm k H₁) (B_H₂ : LinearMap.BilinForm k H₂) (hH₁ : BilinForm.IsHyperbolic B_H₁) (hH₂ : BilinForm.IsHyperbolic B_H₂) (hiso : FormedSpacesIsometric (BilinForm.orthogonalSum B_X B_H₁) B_H₂) : BilinForm.IsHyperbolic B_X

Combination of cancellation and isometry-preservation: if X ⊕ H₁ is isometric to a hyperbolic space H₂ and H₁ is hyperbolic, then X is hyperbolic.

noncomputable def Garrett.rearrangeEquiv {k : Type u_1} [Field k] {U : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module k U] [AddCommGroup X] [Module k X] [AddCommGroup Y] [Module k Y] : ((X × Y) × U × U) ≃ₗ[k] (U × X) × U × Y

A rearrangement linear equivalence permuting the four factors of (X × Y) × (U × U) into (U × X) × (U × Y).

theorem Garrett.orthogonal_direct_sum_neg_isHyperbolic {k : Type u_1} [Field k] {U : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module k U] [FiniteDimensional k U] [AddCommGroup X] [Module k X] [FiniteDimensional k X] [AddCommGroup Y] [Module k Y] [FiniteDimensional k Y] (B_U : LinearMap.BilinForm k U) (B_X : LinearMap.BilinForm k X) (B_Y : LinearMap.BilinForm k Y) (hU_nd : BilinForm.IsNondegenerate' B_U) (_hX_nd : BilinForm.IsNondegenerate' B_X) (hY_nd : BilinForm.IsNondegenerate' B_Y) (φ : (U × X) ≃ₗ[k] U × Y) (hφ : IsFormedSpaceIsometry (BilinForm.orthogonalSum B_U B_X) (BilinForm.orthogonalSum B_U B_Y) φ) : BilinForm.IsHyperbolic (BilinForm.orthogonalSum B_X (-B_Y))

Garrett's Chapter 7 hyperbolicity result: if (U ⊕ X) ≃ (U ⊕ Y) is an isometry of nondegenerate formed spaces, then the orthogonal direct sum X ⊕ (-Y) is hyperbolic.

theorem Formalization.ch7_directSum_neg_hyperbolic {k : Type u_1} [Field k] {U : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module k U] [FiniteDimensional k U] [AddCommGroup X] [Module k X] [FiniteDimensional k X] [AddCommGroup Y] [Module k Y] [FiniteDimensional k Y] (B_U : LinearMap.BilinForm k U) (B_X : LinearMap.BilinForm k X) (B_Y : LinearMap.BilinForm k Y) (hU_nd : Garrett.BilinForm.IsNondegenerate' B_U) (hX_nd : Garrett.BilinForm.IsNondegenerate' B_X) (hY_nd : Garrett.BilinForm.IsNondegenerate' B_Y) (φ : (U × X) ≃ₗ[k] U × Y) (hφ : Garrett.IsFormedSpaceIsometry (Garrett.BilinForm.orthogonalSum B_U B_X) (Garrett.BilinForm.orthogonalSum B_U B_Y) φ) : Garrett.BilinForm.IsHyperbolic (Garrett.BilinForm.orthogonalSum B_X (-B_Y))

Formalization-namespace wrapper for orthogonal_direct_sum_neg_isHyperbolic, exposing the Chapter 7 hyperbolicity result under the Formalization namespace.