Disjoint blocks embed in the Hecke tower

The disjoint block map places two Hecke stages on consecutive blocks of strands. This file proves that it is injective over every commutative coefficient ring and at every unit parameter. Thus the two coefficient algebras embed as their tensor product, including at singular parameters, as required for induction from disjoint blocks.

The proof reuses cosetEquiv and shift_cosetRep from the coset-basis construction. The coset representatives for the second block become the representatives with indices shifted by the size of the first block, so uniqueness of the larger stage's coset coordinates recovers every tensor coefficient.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.blockIncl_injective {R : Type u_1} [CommRing R] {q : Rˣ} (a b : ℕ) : Function.Injective ⇑(blockIncl R q a b)

The disjoint block map is an embedding, over every commutative ring and at every unit parameter. No semisimplicity or invertibility of a quantum integer is required.