noncomputable def GeometricAlgebra.complIsomOfIsCompl {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W C₁ C₂ : Submodule k V) (hc₁ : IsCompl W C₁) (hc₂ : IsCompl W C₂) : ↥C₁ ≃ₗ[k] ↥C₂

Two complements C₁ and C₂ to the same subspace W are linearly isomorphic, via the composition of inclusion C₁ ↪ V with the linear projection V ↠ C₂ along W.

noncomputable def GeometricAlgebra.swapComplement {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W C₁ C₂ : Submodule k V) (hc₁ : IsCompl W C₁) (hc₂ : IsCompl W C₂) : V ≃ₗ[k] V

The linear automorphism of V that fixes W pointwise and sends the complement C₁ to the complement C₂ via complIsomOfIsCompl.

theorem GeometricAlgebra.swapComplement_fix_W {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W C₁ C₂ : Submodule k V) (hc₁ : IsCompl W C₁) (hc₂ : IsCompl W C₂) (w : V) (hw : w ∈ W) : (swapComplement W C₁ C₂ hc₁ hc₂) w = w

The swapComplement automorphism fixes every vector of W pointwise.

theorem GeometricAlgebra.swapComplement_map_C {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W C₁ C₂ : Submodule k V) (hc₁ : IsCompl W C₁) (hc₂ : IsCompl W C₂) : Submodule.map (↑(swapComplement W C₁ C₂ hc₁ hc₂)) C₁ = C₂

The swapComplement automorphism maps the complement C₁ onto the complement C₂.

theorem GeometricAlgebra.swapComplement_preserves_sub {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W C₁ C₂ S : Submodule k V) (hc₁ : IsCompl W C₁) (hc₂ : IsCompl W C₂) (hle : S ≤ W) : Submodule.map (↑(swapComplement W C₁ C₂ hc₁ hc₂)) S = S

Any subspace S contained in W is preserved by the swapComplement automorphism (since it acts as the identity on W).

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

Hypothesis bundling the composition step needed for the conjugacy-of-opposite flags theorem: given a flag F and two opposite flags F'₁, F'₂, there exists a linear automorphism preserving F and mapping F'₁ to F'₂.

• compose_swaps (F F'₁ F'₂ : Flag k V) : F.isOppositeFlag F'₁ → 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.opposite_systems_conjugacy_theorem (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] [FiniteDimensional k V] (hyp : OppositeConjugacyCompositionHyp k V) (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)

The conjugacy theorem for opposite flags: given the composition hypothesis, any two flags opposite to F are conjugate by a linear automorphism that fixes the spaces of F.

def GeometricAlgebra.instOppositeSystemsConjugacyProperty' {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (hyp : OppositeConjugacyCompositionHyp k V) : OppositeSystemsConjugacyProperty k V

Bundles opposite_systems_conjugacy_theorem as an instance of the OppositeSystemsConjugacyProperty typeclass.