noncomputable def typeCGen {n : ℕ} (i : Fin n) : SignedPerm.SignedPermGroup n

The $i$-th Coxeter generator of type $C_n$: an adjacent transposition for $i < n-1$, or the sign change at the last coordinate when $i = n-1$.

theorem typeC_coxeterGroup_finite (n : ℕ) : Finite (CoxeterMatrix.B n).Group

The type-$C_n$ Coxeter group is finite.

theorem typeC_coxeterGroup_card_le (n : ℕ) : Nat.card (CoxeterMatrix.B n).Group ≤ 2 ^ n * n.factorial

Upper bound on the type-$C_n$ Coxeter group: $|W(C_n)| \le 2^n \cdot n!$.

theorem typeC_generators_isLiftable (n : ℕ) : (CoxeterMatrix.B n).IsLiftable fun (i : Fin n) => typeCGen i

The chosen signed permutations $\{\text{typeCGen}\ i\}$ satisfy all type-$C_n$ Coxeter relations.

theorem typeC_relations_satisfied (n : ℕ) (r : FreeGroup (Fin n)) : r ∈ (CoxeterMatrix.B n).relationsSet → (FreeGroup.lift fun (i : Fin n) => typeCGen i) r = 1

Every type-$C_n$ Coxeter relation evaluates to $1$ under the assignment to typeCGen.

noncomputable def typeCHom (n : ℕ) : (CoxeterMatrix.B n).Group →* SignedPerm.SignedPermGroup n

Canonical homomorphism $W(C_n) \to S_n^\pm$ sending each Coxeter generator to the corresponding typeCGen.

theorem typeCHom_of (n : ℕ) (i : Fin n) : (typeCHom n) (PresentedGroup.of i) = typeCGen i

The presented-group hom sends the $i$-th simple generator to typeCGen i.

theorem typeCHom_inr_mem_range (n : ℕ) (σ : Equiv.Perm (Fin n)) : SemidirectProduct.inr σ ∈ (typeCHom n).range

Every permutation $\sigma \in S_n$, viewed inside $S_n^\pm$ via $\inr$, lies in the range of typeCHom.

theorem typeCHom_inl_mem_range (n : ℕ) (ε : SignedPerm.SignGroup n) : SemidirectProduct.inl ε ∈ (typeCHom n).range

Every sign vector $\varepsilon \in (\{\pm 1\})^n$, viewed via $\inl$, lies in the range of typeCHom.

theorem typeCHom_surjective (n : ℕ) : Function.Surjective ⇑(typeCHom n)

typeCHom n is surjective onto $S_n^\pm$.

theorem typeC_coxeterGroup_card_eq (n : ℕ) : Nat.card (CoxeterMatrix.B n).Group = 2 ^ n * n.factorial

Exact cardinality: $|W(C_n)| = 2^n \cdot n!$, matching $|S_n^\pm|$.

theorem typeCHom_injective (n : ℕ) : Function.Injective ⇑(typeCHom n)

typeCHom n is injective: it is therefore a group isomorphism $W(C_n) \cong S_n^\pm$.

noncomputable def typeC_mulEquiv_forward (n : ℕ) : (CoxeterMatrix.B n).Group ≃* SignedPerm.SignedPermGroup n

Group isomorphism $W(C_n) \cong S_n^\pm$, packaging typeCHom as a MulEquiv.

noncomputable def typeC_signedPerm_mulEquiv (n : ℕ) : SignedPerm.SignedPermGroup n ≃* (CoxeterMatrix.B n).Group

Reverse isomorphism $S_n^\pm \cong W(C_n)$.