def GLnBuilding.joinSub {k : Type u_1} [Field k] {n : ℕ} (F : Frame k n) (S : Finset (Fin n)) : Submodule k (Vec k n)

Frame-indexed join: $\mathrm{joinSub}\ F\ S = \bigoplus_{i \in S} F.\mathrm{lines}\ i$.

theorem GLnBuilding.joinSub_injective {k : Type u_1} [Field k] {n : ℕ} (F : Frame k n) : Function.Injective (joinSub F)

The map $S \mapsto \mathrm{joinSub}\ F\ S$ is injective.

theorem GLnBuilding.joinSub_isCompatible {k : Type u_1} [Field k] {n : ℕ} (F : Frame k n) (S : Finset (Fin n)) : Frame.IsCompatible k n F (joinSub F S)

Every joinSub F S is $F$-compatible by definition.

theorem GLnBuilding.extractFinset_of_joinSub {k : Type u_1} [Field k] {n : ℕ} (F : Frame k n) (S : Finset (Fin n)) : extractFinset k n F (joinSub F S) = S

Round-trip identity: extractFinset F (joinSub F S) = S.

theorem GLnBuilding.joinSub_extractFinset {k : Type u_1} [Field k] {n : ℕ} (F : Frame k n) (V : Submodule k (Vec k n)) (h : Frame.IsCompatible k n F V) : joinSub F (extractFinset k n F V) = V

Round-trip identity: joinSub F (extractFinset F V) = V for any $F$-compatible $V$.

noncomputable def GLnBuilding.apartmentIsoHypUnconditional (k : Type u_2) [Field k] (n : ℕ) : ApartmentIsoHyp k n

Unconditional construction of the apartment isomorphism: given two apartments sharing two chambers, build a bijection $f$ on subspaces that sends $F_1$-compatible subspaces to $F_2$-compatible ones, fixes the shared chambers, and is the identity on the intersection. The construction matches "only-$F_1$" finsets bijectively to "only-$F_2$" finsets via a cardinality argument.