English
Let α be a type and β: α → Type a family. For every a ∈ α we have the permutation group Perm(β(a)). There is a natural monoid hom σ from the product (over a ∈ α) of Perm(β(a)) to Perm(Σ a, β(a)) defined by σ((f_a)_{a})(a,b) = (a, f_a(b)). This hom preserves the identity and composition, and its range consists of those permutations of Σ a β(a) that do not exchange elements between different fibers.
Русский
Пусть α — множество, β: α → Type — семейство типов. Для каждого a ∈ α задано множество перестановок Perm(β(a)). Существует естественный гомоморфизм мономорфизм σ: ∏_{a∈α} Perm(β(a)) → Perm(Σ_{a∈α} β(a)), заданный на элементе (f_a) тем, что σ((f_a))(a,b) = (a, f_a(b)). Этот гомоморфизм сохраняет тождественный элемент и произведение; образ σ состоит из перестановок Σ a β(a), которые не меняют элементы между волокнами.
LaTeX
$$$$ \sigma_{\mathrm{Right}}:\left(\prod_{a\in\alpha} \mathrm{Perm}(\beta(a))\right) \to^* \mathrm{Perm}\left(\sum_{a\in\alpha} \beta(a)\right), \quad \sigma_{\mathrm{Right}}((f_a)_a)(a,b)=(a,f_a(b)). $$$$
Lean4
/-- `Equiv.Perm.sigmaCongrRight` as a `MonoidHom`.
This is particularly useful for its `MonoidHom.range` projection, which is the subgroup of
permutations which do not exchange elements between fibers. -/
@[simps]
def sigmaCongrRightHom {α : Type*} (β : α → Type*) : (∀ a, Perm (β a)) →* Perm (Σ a, β a)
where
toFun := sigmaCongrRight
map_one' := sigmaCongrRight_one
map_mul' _ _ := (sigmaCongrRight_mul _ _).symm
