@[reducible, inline]

abbrev SignedPerm.SignGroup (n : ℕ) : Type

The sign group $(\{\pm 1\})^n$ realized multiplicatively as $\operatorname{Fin}(n) \to (\mathbb{Z}/2)^\times$.

noncomputable def SignedPerm.signGroupPermAction (n : ℕ) : Equiv.Perm (Fin n) →* MulAut (SignGroup n)

The permutation action of $S_n$ on the sign group $(\{\pm 1\})^n$ by index permutation, encoded as a group homomorphism into $\operatorname{MulAut}$.

@[reducible, inline]

abbrev SignedPerm.SignedPermGroup (n : ℕ) : Type

The signed permutation group (hyperoctahedral group) $S_n^\pm = (\{\pm 1\})^n \rtimes S_n$, the Coxeter group of type $C_n$ (Section 10.2).

def SignedPerm.signedPermGroupEquivProd (n : ℕ) : SignedPermGroup n ≃ SignGroup n × Equiv.Perm (Fin n)

As a set, $S_n^\pm$ is in bijection with $(\{\pm 1\})^n \times S_n$.

theorem SignedPerm.signedPermGroup_card (n : ℕ) : Nat.card (SignedPermGroup n) = 2 ^ n * n.factorial

The cardinality of the signed permutation group is $|S_n^\pm| = 2^n \cdot n!$.

def SignedPerm.signChangeAt (n : ℕ) (j : Fin n) : SignGroup n

The generator $\varepsilon_j \in (\{\pm 1\})^n$ that flips the sign at coordinate $j$ only.

theorem SignedPerm.signGroupPermAction_signChangeAt (n : ℕ) (σ : Equiv.Perm (Fin n)) (j : Fin n) : ((signGroupPermAction n) σ) (signChangeAt n j) = signChangeAt n (σ j)

The $S_n$-action permutes the single-coordinate sign flips: $\sigma \cdot \varepsilon_j = \varepsilon_{\sigma j}$.

theorem SignedPerm.inr_conj_inl (n : ℕ) (σ : Equiv.Perm (Fin n)) (ε : SignGroup n) : SemidirectProduct.inr σ * SemidirectProduct.inl ε * (SemidirectProduct.inr σ)⁻¹ = SemidirectProduct.inl (((signGroupPermAction n) σ) ε)

Conjugation of a sign vector by a permutation in the semidirect product: $\sigma \varepsilon \sigma^{-1} = \sigma \cdot \varepsilon$.

noncomputable def SignedPerm.generators (n : ℕ) : Set (SignedPermGroup (n + 1))

The Coxeter generators of $S_{n+1}^\pm$: the $n$ adjacent transpositions plus the sign flip at the last coordinate.

theorem SignedPerm.ZMod2_eq_zero_or_one (x : ZMod 2) : x = 0 ∨ x = 1

Every element of $\mathbb{Z}/2$ is either $0$ or $1$.

theorem SignedPerm.Multiplicative_ZMod2_cases (x : Multiplicative (ZMod 2)) : x = 1 ∨ x = Multiplicative.ofAdd 1

Every element of $(\mathbb{Z}/2)^\times$ (multiplicative form) is either the identity or $\operatorname{ofAdd} 1$.

theorem SignedPerm.signGroup_closure_signChangeAt (n : ℕ) : Subgroup.closure (Set.range (signChangeAt n)) = ⊤

The single-coordinate sign flips generate the whole sign group $(\{\pm 1\})^n$.

theorem SignedPerm.inl_mem_of_signChangeAt_mem (n : ℕ) (ε : SignGroup n) (S : Subgroup (SignedPermGroup n)) (h : ∀ (j : Fin n), SemidirectProduct.inl (signChangeAt n j) ∈ S) : SemidirectProduct.inl ε ∈ S

A subgroup containing every single-coordinate sign flip contains every signed-coordinate element from the $\inl$ embedding.

theorem SignedPerm.inr_mem_of_adj_swaps_mem (n : ℕ) (σ : Equiv.Perm (Fin (n + 1))) (S : Subgroup (SignedPermGroup (n + 1))) (hS : ∀ (i : Fin n), SemidirectProduct.inr (Equiv.swap i.castSucc i.succ) ∈ S) : SemidirectProduct.inr σ ∈ S

A subgroup containing all adjacent transpositions (via the $\inr$ embedding) contains every permutation in $S_{n+1}$.