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

A linear automorphism Φ : V ≃ₗ V is a global isometry of the bilinear form B if it preserves all values of B.

theorem Garrett.IsGlobalIsometry.refl {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : IsGlobalIsometry B (LinearEquiv.refl k V)

The identity automorphism is always a global isometry.

theorem Garrett.IsGlobalIsometry.symm {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] {B : LinearMap.BilinForm k V} {Φ : V ≃ₗ[k] V} (hΦ : IsGlobalIsometry B Φ) : IsGlobalIsometry B Φ.symm

The inverse of a global isometry is again a global isometry.

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

An isotropic flag in a formed space (V, B) is a strictly increasing chain of totally isotropic subspaces.

• len : ℕ
• spaces : Fin self.len → Submodule k V
• strictMono : StrictMono self.spaces
• isotropic (i : Fin self.len) : IsTotallyIsotropic B (self.spaces i)

noncomputable def Garrett.IsotropicFlag.flagType {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] {B : LinearMap.BilinForm k V} (F : IsotropicFlag B) : Fin F.len → ℕ

The type of an isotropic flag is the sequence of dimensions of its spaces.

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

Two isotropic flags have the same type if they have the same length and the same dimension sequence.

def Garrett.IsotropicFlag.parabolicSubgroup {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] {B : LinearMap.BilinForm k V} (F : IsotropicFlag B) : Set (V ≃ₗ[k] V)

The parabolic subgroup of an isotropic flag F consists of all global isometries of B that stabilize every space of F setwise.

theorem Garrett.isometry_between_isotropic_subspaces {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] {B : LinearMap.BilinForm k V} (U W : Submodule k V) (hU : IsTotallyIsotropic B U) (hW : IsTotallyIsotropic B W) (φ : ↥U ≃ₗ[k] ↥W) : IsSubspaceIsometry B U W φ

Any linear equivalence between two totally isotropic subspaces is automatically an isometry of the restricted bilinear form (both forms are zero).

noncomputable def Garrett.LinearEquiv.restrictSubmodule {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) (U W : Submodule R M) (h : Submodule.map (↑e) U = W) : ↥U ≃ₗ[R] ↥W

Restriction of a linear automorphism e : M ≃ₗ M to a linear equivalence U ≃ₗ W between subspaces U and W = e(U).

theorem Garrett.LinearEquiv.restrictSubmodule_val {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) (U W : Submodule R M) (h : Submodule.map (↑e) U = W) (u : ↥U) : ↑((restrictSubmodule e U W h) u) = e ↑u

The underlying value of LinearEquiv.restrictSubmodule agrees with the ambient automorphism e.

theorem Garrett.LinearEquiv.symm_stabilizes {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (g : M ≃ₗ[R] M) (U : Submodule R M) (h : Submodule.map (↑g) U = U) : Submodule.map (↑g.symm) U = U

If a linear automorphism g stabilizes a submodule U, then so does its inverse g.symm.

theorem Garrett.isotropicFlag_equiv_of_sameType {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] {B : LinearMap.BilinForm k V} [FiniteDimensional k V] (hBsymm : ∀ (x y : V), (B x) y = (B y) x) (hnd : B.orthogonal ⊤ = ⊥) (F₁ F₂ : IsotropicFlag B) (hst : F₁.sameType F₂) : ∃ (Φ : V ≃ₗ[k] V), IsGlobalIsometry B Φ ∧ ∀ (i : Fin F₁.len), Submodule.map (↑Φ) (F₁.spaces i) = F₂.spaces (Fin.cast ⋯ i)

Two isotropic flags of the same type are conjugate by a global isometry of the bilinear form B. Built using Witt's Extension Theorem.

theorem Garrett.parabolicSubgroup_conjugate_of_flag_map {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] {B : LinearMap.BilinForm k V} (F₁ F₂ : IsotropicFlag B) (Φ : V ≃ₗ[k] V) (hΦ_isom : IsGlobalIsometry B Φ) (hlen : F₁.len = F₂.len) (hΦ_maps : ∀ (i : Fin F₁.len), Submodule.map (↑Φ) (F₁.spaces i) = F₂.spaces (Fin.cast hlen i)) (g : V ≃ₗ[k] V) : g ∈ F₂.parabolicSubgroup ↔ Φ ≪≫ₗ (g ≪≫ₗ Φ.symm) ∈ F₁.parabolicSubgroup

Conjugation by a global isometry Φ mapping F₁ to F₂ provides a bijection between the parabolic subgroups of F₁ and F₂.

theorem Garrett.isotropicFlag_parabolics_conjugate {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] {B : LinearMap.BilinForm k V} [FiniteDimensional k V] (hBsymm : ∀ (x y : V), (B x) y = (B y) x) (hnd : B.orthogonal ⊤ = ⊥) (F₁ F₂ : IsotropicFlag B) (hst : F₁.sameType F₂) : ∃ (Φ : V ≃ₗ[k] V), IsGlobalIsometry B Φ ∧ ∀ (g : V ≃ₗ[k] V), g ∈ F₂.parabolicSubgroup ↔ Φ ≪≫ₗ (g ≪≫ₗ Φ.symm) ∈ F₁.parabolicSubgroup

Main theorem: parabolic subgroups of any two isotropic flags of the same type are conjugate by a global isometry of B.