theorem GeometricAlgebra.submodule_map_of_finrank_eq {k : Type u_1} [Field k] {M : Type u_3} [AddCommGroup M] [Module k M] [FiniteDimensional k M] (W₁ W₂ : Submodule k M) (hdim : Module.finrank k ↥W₁ = Module.finrank k ↥W₂) : ∃ (e : M ≃ₗ[k] M), Submodule.map (↑e) W₁ = W₂

Any two subspaces of the same finite dimension are related by a global linear automorphism mapping one onto the other.

theorem GeometricAlgebra.adjustment_equiv {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (W U₁ U₂ : Submodule k V) (hle₁ : W ≤ U₁) (hle₂ : W ≤ U₂) (hdim : Module.finrank k ↥U₁ = Module.finrank k ↥U₂) : ∃ (e : V ≃ₗ[k] V), (∀ w ∈ W, e w = w) ∧ Submodule.map (↑e) U₁ = U₂

Given a common subspace W ≤ U₁, W ≤ U₂ with U₁ and U₂ of equal dimension, there is a linear automorphism fixing W pointwise that sends U₁ onto U₂.

theorem GeometricAlgebra.map_eq_of_pointwise_fix {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (S W : Submodule k V) (e : V ≃ₗ[k] V) (hfix : ∀ w ∈ W, e w = w) (hle : S ≤ W) : Submodule.map (↑e) S = S

If e fixes every element of W pointwise, then e also fixes every subspace S ≤ W setwise: S.map e = S.

theorem GeometricAlgebra.map_trans_eq {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (S : Submodule k V) (e₁ e₂ : V ≃ₗ[k] V) : Submodule.map (↑(e₁ ≪≫ₗ e₂)) S = Submodule.map (↑e₂) (Submodule.map (↑e₁) S)

Mapping a submodule under a composition of linear equivalences agrees with applying the maps successively.

theorem GeometricAlgebra.flag_equiv_aux {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (n : ℕ) (spaces₁ spaces₂ : Fin n → Submodule k V) : StrictMono spaces₁ → StrictMono spaces₂ → (∀ (i : Fin n), Module.finrank k ↥(spaces₁ i) = Module.finrank k ↥(spaces₂ i)) → ∃ (e : V ≃ₗ[k] V), ∀ (i : Fin n), Submodule.map (↑e) (spaces₁ i) = spaces₂ i

Inductive helper: two strictly ascending sequences of subspaces of the same length, with matching dimensions stage by stage, are related by a single linear automorphism that sends each spaces₁ i onto spaces₂ i.

theorem GeometricAlgebra.flag_equiv_of_sameType (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] [FiniteDimensional k V] (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)

Two flags of the same type (same length and same dimensions at each stage) are GL(V)-equivalent: there is a single linear automorphism that sends each subspace of one flag to the corresponding subspace of the other.

instance GeometricAlgebra.instFlagEquivalenceProperty {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] : FlagEquivalenceProperty k V

The FlagEquivalenceProperty instance: over any field, on a finite-dimensional vector space, flags of the same type are GL(V)-equivalent.