@[reducible, inline]

abbrev GeometricAlgebra.GLV (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] : Type u_2

Abbreviation for the general linear group GL(V) of a k-module V.

noncomputable def GeometricAlgebra.linearEquivToGLV {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (e : V ≃ₗ[k] V) : GLV k V

Convert a linear equivalence V ≃ₗ[k] V to an element of the general linear group GLV k V.

@[simp]

theorem GeometricAlgebra.linearEquivToGLV_val {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (e : V ≃ₗ[k] V) : ↑(linearEquivToGLV e) = ↑e

The underlying linear map of linearEquivToGLV e is e.toLinearMap.

noncomputable def GeometricAlgebra.glvToLinearEquiv {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (g : GLV k V) : V ≃ₗ[k] V

Convert an element of the general linear group GLV k V back to a linear equivalence V ≃ₗ[k] V.

@[simp]

theorem GeometricAlgebra.glvToLinearEquiv_toLinearMap {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (g : GLV k V) : ↑(glvToLinearEquiv g) = ↑g

The linear map underlying glvToLinearEquiv g is the underlying map of g.

theorem GeometricAlgebra.linearEquivToGLV_glvToLinearEquiv {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (g : GLV k V) : linearEquivToGLV (glvToLinearEquiv g) = g

Round-trip lemma: converting g : GLV k V to a linear equivalence and back recovers g.

theorem GeometricAlgebra.linearEquivToGLV_mul_val {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (d u : V ≃ₗ[k] V) : ↑(linearEquivToGLV d * linearEquivToGLV u) = ↑d ∘ₗ ↑u

The product linearEquivToGLV d * linearEquivToGLV u in GLV k V has underlying linear map equal to the composition d ∘ u.

theorem GeometricAlgebra.map_inv_of_map_eq {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (e : V ≃ₗ[k] V) (W : Submodule k V) (h : Submodule.map (↑e) W = W) : Submodule.map (↑e.symm) W = W

If a linear equivalence e preserves a submodule W, then so does its inverse e.symm.

theorem GeometricAlgebra.map_inv_of_map_to {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (g : GLV k V) (W₁ W₂ : Submodule k V) (h : Submodule.map (↑g) W₁ = W₂) : Submodule.map (↑g⁻¹) W₂ = W₁

If g ∈ GLV k V sends a submodule W₁ to W₂, then g⁻¹ sends W₂ back to W₁.

structure GeometricAlgebra.Flag (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] : Type u_4

A flag in a k-vector space V is a strictly increasing sequence of submodules spaces : Fin len → Submodule k V.

• len : ℕ
• spaces : Fin self.len → Submodule k V
• strictMono : StrictMono self.spaces

noncomputable def GeometricAlgebra.Flag.type {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F : Flag k V) : Fin F.len → ℕ

The type of a flag F is the sequence of dimensions of its constituent submodules.

def GeometricAlgebra.Flag.sameType {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F₁ F₂ : Flag k V) : Prop

Two flags have the same type when they have the same length and the same sequence of dimensions.

theorem GeometricAlgebra.Flag.submodule_map_mul_eq {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (a b : GLV k V) (W : Submodule k V) : Submodule.map (↑(a * b)) W = Submodule.map (↑a) (Submodule.map (↑b) W)

The image of a submodule under the product of two GL elements equals the iterated image: W.map (a * b) = (W.map b).map a.

def GeometricAlgebra.Flag.parabolicSubgroup {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F : Flag k V) : Subgroup (GLV k V)

The parabolic subgroup of GL(V) stabilizing a flag F: the elements preserving every space in the flag.

def GeometricAlgebra.Flag.unipotentRadical {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F : Flag k V) : Set (GLV k V)

The unipotent radical of the parabolic subgroup of F: elements in the parabolic that act as the identity on each successive quotient F.spaces i / F.spaces (i-1) (and as the identity on F.spaces 0).

theorem GeometricAlgebra.Flag.parabolic_mem_preserves {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] {F : Flag k V} {g : GLV k V} (hg : g ∈ F.parabolicSubgroup) (i : Fin F.len) {v : V} (hv : v ∈ F.spaces i) : ↑g v ∈ F.spaces i

An element of the parabolic subgroup of F maps each flag level into itself pointwise.

theorem GeometricAlgebra.Flag.gl_mul_inv_cancel {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (g : GLV k V) (v : V) : ↑g (↑g⁻¹ v) = v

Multiplication by g then g⁻¹ (as linear maps) cancels: g (g⁻¹ v) = v.

theorem GeometricAlgebra.Flag.gl_conj_apply {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (g u : GLV k V) (v : V) : ↑(g * u * g⁻¹) v = ↑g (↑u (↑g⁻¹ v))

Conjugation in GLV k V translates to threefold application of underlying linear maps: (g u g⁻¹) v = g (u (g⁻¹ v)).

theorem GeometricAlgebra.Flag.conj_minus_eq {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (g u : GLV k V) (v : V) : ↑(g * u * g⁻¹) v - v = ↑g (↑u (↑g⁻¹ v) - ↑g⁻¹ v)

Difference identity for conjugation: (g u g⁻¹) v - v = g (u (g⁻¹ v) - g⁻¹ v).

theorem GeometricAlgebra.Flag.parabolic_conj {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F₁ F₂ : Flag k V) (g : GLV k V) (hlen : F₁.len = F₂.len) (hg : ∀ (i : Fin F₁.len), Submodule.map (↑g) (F₁.spaces i) = F₂.spaces (Fin.cast hlen i)) : F₂.parabolicSubgroup = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) F₁.parabolicSubgroup

If g ∈ GL(V) maps the flag F₁ to F₂ (level-wise), then the parabolic subgroup of F₂ is the g-conjugate of the parabolic subgroup of F₁.

theorem GeometricAlgebra.Flag.inf_map_conj_of_mem {G : Type u_3} [Group G] (H K : Subgroup G) (g : G) (hg : g ∈ H) : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (H ⊓ K) = H ⊓ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) K

For g ∈ H, conjugation by g preserves H and distributes over intersections: (H ⊓ K)^g = H ⊓ K^g.

theorem GeometricAlgebra.Flag.conj_map_inf {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (H K : Subgroup (GLV k V)) (g : GLV k V) : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (H ⊓ K) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H ⊓ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) K

Conjugation in GLV k V distributes over intersection of subgroups.

def GeometricAlgebra.Flag.isOppositeFlag {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F' : Flag k V) : Prop

Two flags are opposite if they have the same length and type, and each matched pair of levels (F.spaces i, F'.spaces (F'.len - 1 - i)) is complementary.

def GeometricAlgebra.Flag.oppositeParabolic {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F' : Flag k V) : Subgroup (GLV k V)

The parabolic subgroup attached to the opposite flag F'.

def GeometricAlgebra.Flag.leviComponent {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F' : Flag k V) : F.isOppositeFlag F' → Subgroup (GLV k V)

The Levi component associated with an opposite pair of flags (F, F'): the intersection of their parabolic subgroups.

def GeometricAlgebra.Flag.ParabolicsSemidirectProduct {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F' : Flag k V) (h : F.isOppositeFlag F') : Prop

The parabolic subgroup of F is a semidirect product of its Levi component (with respect to the opposite flag F') and its unipotent radical: every element of the parabolic factors uniquely as a Levi times unipotent.

def GeometricAlgebra.Flag.truncate {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F : Flag k V) (h : 1 ≤ F.len) : Flag k V

Drop the top space from a flag, keeping the first F.len - 1 levels.

def GeometricAlgebra.Flag.truncateStart {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F : Flag k V) (h : 1 ≤ F.len) : Flag k V

Drop the bottom space from a flag, keeping levels from index 1 onwards.

@[simp]

theorem GeometricAlgebra.Flag.truncate_len {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F : Flag k V) (h : 1 ≤ F.len) : (F.truncate h).len = F.len - 1

The length of F.truncate h is F.len - 1.

@[simp]

theorem GeometricAlgebra.Flag.truncateStart_len {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F : Flag k V) (h : 1 ≤ F.len) : (F.truncateStart h).len = F.len - 1

The length of F.truncateStart h is F.len - 1.

theorem GeometricAlgebra.Flag.truncate_spaces {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F : Flag k V) (h : 1 ≤ F.len) (i : Fin (F.len - 1)) : (F.truncate h).spaces i = F.spaces ⟨↑i, ⋯⟩

The spaces of F.truncate h agree with those of F at the same indices.

theorem GeometricAlgebra.Flag.truncateStart_spaces {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F : Flag k V) (h : 1 ≤ F.len) (i : Fin (F.len - 1)) : (F.truncateStart h).spaces i = F.spaces ⟨↑i + 1, ⋯⟩

The spaces of F.truncateStart h are F.spaces ⟨i + 1, …⟩.

def GeometricAlgebra.Flag.IsCoveringOppositePair {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F' : Flag k V) : F.isOppositeFlag F' → Prop

A pair of opposite flags is a "covering" pair when F is nonempty and its top space is all of V.

class GeometricAlgebra.SemidirectExistenceProperty (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] : Prop

Existence property: for every covering opposite pair (F, F') and every flag stabilizer p of F, there exists a Levi-unipotent factorization p = d ∘ u.

• exists_decomp_linear (F F' : Flag k V) (_h : F.isOppositeFlag F') (hlen : 0 < F.len) (_hcov : F.spaces ⟨F.len - 1, ⋯⟩ = ⊤) (p : V ≃ₗ[k] V) : (∀ (i : Fin F.len), Submodule.map (↑p) (F.spaces i) = F.spaces i) → ∃ (d : V ≃ₗ[k] V) (u : V ≃ₗ[k] V), (∀ (i : Fin F.len), Submodule.map (↑d) (F.spaces i) = F.spaces i) ∧ (∀ (i : Fin F'.len), Submodule.map (↑d) (F'.spaces i) = F'.spaces i) ∧ (∀ (i : Fin F.len), Submodule.map (↑u) (F.spaces i) = F.spaces i) ∧ (∀ (i : Fin F.len), ∀ v ∈ F.spaces i, ↑u v - v ∈ if x : ↑i = 0 then ⊥ else F.spaces ⟨↑i - 1, ⋯⟩) ∧ ↑p = ↑d ∘ₗ ↑u

theorem GeometricAlgebra.Flag.unipotent_levi_is_id {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F' : Flag k V) (hopp : F.isOppositeFlag F') (hlen : 0 < F.len) (hcov : F.spaces ⟨F.len - 1, ⋯⟩ = ⊤) (e : V ≃ₗ[k] V) (he_F' : ∀ (i : Fin F'.len), Submodule.map (↑e) (F'.spaces i) = F'.spaces i) (hunip : ∀ (i : Fin F.len), ∀ v ∈ F.spaces i, ↑e v - v ∈ if _hh : ↑i = 0 then ⊥ else F.spaces ⟨↑i - 1, ⋯⟩) : e = LinearEquiv.refl k V

Uniqueness in M ∩ U = {1}: a linear equivalence that simultaneously preserves the opposite flag F' levelwise and is unipotent along F must be the identity.

theorem GeometricAlgebra.Flag.unique_decomp_linear_proof {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F' : Flag k V) (hopp : F.isOppositeFlag F') (hlen : 0 < F.len) (hcov : F.spaces ⟨F.len - 1, ⋯⟩ = ⊤) (d₁ d₂ u₁ u₂ : V ≃ₗ[k] V) (_hd₁_F : ∀ (i : Fin F.len), Submodule.map (↑d₁) (F.spaces i) = F.spaces i) (hd₁_F' : ∀ (i : Fin F'.len), Submodule.map (↑d₁) (F'.spaces i) = F'.spaces i) (_hd₂_F : ∀ (i : Fin F.len), Submodule.map (↑d₂) (F.spaces i) = F.spaces i) (hd₂_F' : ∀ (i : Fin F'.len), Submodule.map (↑d₂) (F'.spaces i) = F'.spaces i) (hu₁_F : ∀ (i : Fin F.len), Submodule.map (↑u₁) (F.spaces i) = F.spaces i) (hu₁_unip : ∀ (i : Fin F.len), ∀ v ∈ F.spaces i, ↑u₁ v - v ∈ if _hh : ↑i = 0 then ⊥ else F.spaces ⟨↑i - 1, ⋯⟩) (_hu₂_F : ∀ (i : Fin F.len), Submodule.map (↑u₂) (F.spaces i) = F.spaces i) (hu₂_unip : ∀ (i : Fin F.len), ∀ v ∈ F.spaces i, ↑u₂ v - v ∈ if _hh : ↑i = 0 then ⊥ else F.spaces ⟨↑i - 1, ⋯⟩) (hcomp : ↑d₁ ∘ₗ ↑u₁ = ↑d₂ ∘ₗ ↑u₂) : d₁ = d₂ ∧ u₁ = u₂

Uniqueness of the Levi-unipotent factorization at the linear-equivalence level: if d₁ ∘ u₁ = d₂ ∘ u₂ with both factors lying in the appropriate Levi and unipotent subspaces, then d₁ = d₂ and u₁ = u₂.

class GeometricAlgebra.SemidirectDecompositionProperty (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] : Prop

Combined property packaging both existence and uniqueness of the Levi-unipotent decomposition of the flag stabilizer.

• exists_decomp_linear (F F' : Flag k V) (_h : F.isOppositeFlag F') (hlen : 0 < F.len) (_hcov : F.spaces ⟨F.len - 1, ⋯⟩ = ⊤) (p : V ≃ₗ[k] V) : (∀ (i : Fin F.len), Submodule.map (↑p) (F.spaces i) = F.spaces i) → ∃ (d : V ≃ₗ[k] V) (u : V ≃ₗ[k] V), (∀ (i : Fin F.len), Submodule.map (↑d) (F.spaces i) = F.spaces i) ∧ (∀ (i : Fin F'.len), Submodule.map (↑d) (F'.spaces i) = F'.spaces i) ∧ (∀ (i : Fin F.len), Submodule.map (↑u) (F.spaces i) = F.spaces i) ∧ (∀ (i : Fin F.len), ∀ v ∈ F.spaces i, ↑u v - v ∈ if x : ↑i = 0 then ⊥ else F.spaces ⟨↑i - 1, ⋯⟩) ∧ ↑p = ↑d ∘ₗ ↑u
• unique_decomp_linear (F F' : Flag k V) (_h : F.isOppositeFlag F') (hlen : 0 < F.len) (_hcov : F.spaces ⟨F.len - 1, ⋯⟩ = ⊤) (d₁ d₂ u₁ u₂ : V ≃ₗ[k] V) : (∀ (i : Fin F.len), Submodule.map (↑d₁) (F.spaces i) = F.spaces i) → (∀ (i : Fin F'.len), Submodule.map (↑d₁) (F'.spaces i) = F'.spaces i) → (∀ (i : Fin F.len), Submodule.map (↑d₂) (F.spaces i) = F.spaces i) → (∀ (i : Fin F'.len), Submodule.map (↑d₂) (F'.spaces i) = F'.spaces i) → (∀ (i : Fin F.len), Submodule.map (↑u₁) (F.spaces i) = F.spaces i) → (∀ (i : Fin F.len), ∀ v ∈ F.spaces i, ↑u₁ v - v ∈ if x : ↑i = 0 then ⊥ else F.spaces ⟨↑i - 1, ⋯⟩) → (∀ (i : Fin F.len), Submodule.map (↑u₂) (F.spaces i) = F.spaces i) → (∀ (i : Fin F.len), ∀ v ∈ F.spaces i, ↑u₂ v - v ∈ if x : ↑i = 0 then ⊥ else F.spaces ⟨↑i - 1, ⋯⟩) → ↑d₁ ∘ₗ ↑u₁ = ↑d₂ ∘ₗ ↑u₂ → d₁ = d₂ ∧ u₁ = u₂

instance GeometricAlgebra.instSemidirectDecompositionProperty {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [SemidirectExistenceProperty k V] : SemidirectDecompositionProperty k V

The existence property SemidirectExistenceProperty together with the unique-decomposition lemma Flag.unique_decomp_linear_proof yields the combined SemidirectDecompositionProperty.

class GeometricAlgebra.FlagEquivalenceProperty (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] : Prop

Two flags of the same type are linearly equivalent: there exists a linear automorphism of V mapping one to the other levelwise.

• equiv_linear (F₁ F₂ : Flag k V) : F₁.sameType F₂ → ∃ (e : V ≃ₗ[k] V) (hlen : F₁.len = F₂.len), ∀ (i : Fin F₁.len), Submodule.map (↑e) (F₁.spaces i) = F₂.spaces (Fin.cast hlen i)

theorem GeometricAlgebra.FlagsOfSameTypeAreGLEquivalent (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] [FlagEquivalenceProperty k V] (F₁ F₂ : Flag k V) : F₁.sameType F₂ → ∃ (g : GLV k V) (hlen : F₁.len = F₂.len), ∀ (i : Fin F₁.len), Submodule.map (↑g) (F₁.spaces i) = F₂.spaces (Fin.cast hlen i)

Group-level corollary of FlagEquivalenceProperty: same-type flags are conjugate under some element of GLV k V.

class GeometricAlgebra.OppositeSystemsConjugacyProperty (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] : Prop

For any flag F, any two flags opposite to F are conjugate via a linear automorphism that preserves F levelwise.

• conjugate_linear (F F'₁ F'₂ : Flag k V) (_h₁ : F.isOppositeFlag F'₁) (_h₂ : F.isOppositeFlag F'₂) : ∃ (e : V ≃ₗ[k] V) (hlen : F'₁.len = F'₂.len), (∀ (i : Fin F.len), Submodule.map (↑e) (F.spaces i) = F.spaces i) ∧ ∀ (i : Fin F'₁.len), Submodule.map (↑e) (F'₁.spaces i) = F'₂.spaces (Fin.cast hlen i)

theorem GeometricAlgebra.OppositeSystemsAreConjugate (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] [OppositeSystemsConjugacyProperty k V] (F F'₁ F'₂ : Flag k V) (_h₁ : F.isOppositeFlag F'₁) (_h₂ : F.isOppositeFlag F'₂) : ∃ (p : GLV k V) (_ : p ∈ F.parabolicSubgroup) (hlen : F'₁.len = F'₂.len), ∀ (i : Fin F'₁.len), Submodule.map (↑p) (F'₁.spaces i) = F'₂.spaces (Fin.cast hlen i)

Group-level corollary of OppositeSystemsConjugacyProperty: opposite flags to a fixed F are conjugate by an element of the parabolic subgroup of F.

theorem GeometricAlgebra.SemidirectDecompositionExists {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [SemidirectDecompositionProperty k V] (F F' : Flag k V) (h : F.isOppositeFlag F') (hlen : 0 < F.len) (_hcov : F.spaces ⟨F.len - 1, ⋯⟩ = ⊤) (p : GLV k V) : p ∈ F.parabolicSubgroup → ∃ (m : GLV k V) (u : GLV k V), m ∈ F.leviComponent F' h ∧ u ∈ F.unipotentRadical ∧ p = m * u

Group-level form of the semidirect existence: under SemidirectDecompositionProperty, any element of the parabolic subgroup of F factors as a Levi component times a unipotent radical element.

theorem GeometricAlgebra.SemidirectDecompositionUnique {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [SemidirectDecompositionProperty k V] (F F' : Flag k V) (h : F.isOppositeFlag F') (hlen : 0 < F.len) (_hcov : F.spaces ⟨F.len - 1, ⋯⟩ = ⊤) (m₁ m₂ u₁ u₂ : GLV k V) : m₁ ∈ F.leviComponent F' h → m₂ ∈ F.leviComponent F' h → u₁ ∈ F.unipotentRadical → u₂ ∈ F.unipotentRadical → m₁ * u₁ = m₂ * u₂ → m₁ = m₂ ∧ u₁ = u₂

Group-level uniqueness for the semidirect decomposition: the Levi-unipotent factorization of an element of the parabolic subgroup is unique.

class GeometricAlgebra.CompleteFlagPairEquivalenceProperty (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] : Prop

Any two same-type pairs of opposite flags (F₁, F'₁) and (F₂, F'₂) are linearly equivalent: one linear automorphism of V carries both F₁ ↦ F₂ and F'₁ ↦ F'₂ levelwise.

• equiv_linear (F₁ F₂ F'₁ F'₂ : Flag k V) : F₁.isOppositeFlag F'₁ → F₂.isOppositeFlag F'₂ → F₁.sameType F₂ → ∃ (e : V ≃ₗ[k] V) (hlen : F₁.len = F₂.len) (hlen' : F'₁.len = F'₂.len), (∀ (i : Fin F₁.len), Submodule.map (↑e) (F₁.spaces i) = F₂.spaces (Fin.cast hlen i)) ∧ ∀ (i : Fin F'₁.len), Submodule.map (↑e) (F'₁.spaces i) = F'₂.spaces (Fin.cast hlen' i)

theorem GeometricAlgebra.CompleteFlagPairsAreGLEquivalent (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] [CompleteFlagPairEquivalenceProperty k V] (F₁ F₂ F'₁ F'₂ : Flag k V) : F₁.isOppositeFlag F'₁ → F₂.isOppositeFlag F'₂ → F₁.sameType F₂ → ∃ (g : GLV k V) (hlen : F₁.len = F₂.len) (hlen' : F'₁.len = F'₂.len), (∀ (i : Fin F₁.len), Submodule.map (↑g) (F₁.spaces i) = F₂.spaces (Fin.cast hlen i)) ∧ ∀ (i : Fin F'₁.len), Submodule.map (↑g) (F'₁.spaces i) = F'₂.spaces (Fin.cast hlen' i)

Group-level corollary of CompleteFlagPairEquivalenceProperty: same-type opposite flag pairs are conjugate via an element of GLV k V.