Mathlib.GroupTheory.Perm.ViaEmbedding

Equiv.Perm.viaEmbedding definition

: Perm β

Full source

/-- Noncomputable version of `Equiv.Perm.viaFintypeEmbedding` that does not assume `Fintype` -/
noncomputable def viaEmbedding : Perm β :=
  extendDomain e (ofInjective ι.1 ι.2)

Permutation extension via embedding

Informal description

Given an embedding $\iota : \alpha \hookrightarrow \beta$ and a permutation $e$ of $\alpha$, the permutation `viaEmbedding` of $\beta$ extends $e$ by fixing all elements of $\beta$ not in the range of $\iota$. Specifically: - For $x \in \alpha$, $e.\text{viaEmbedding} \iota (\iota x) = \iota (e x)$. - For $x \in \beta$ not in the range of $\iota$, $e.\text{viaEmbedding} \iota x = x$.

Equiv.Perm.viaEmbedding_apply theorem

(x : α) : e.viaEmbedding ι (ι x) = ι (e x)

Full source

theorem viaEmbedding_apply (x : α) : e.viaEmbedding ι (ι x) = ι (e x) :=
  extendDomain_apply_image e (ofInjective ι.1 ι.2) x

Action of Extended Permutation on Embedded Elements

Informal description

For any permutation $e$ of a type $\alpha$ and any embedding $\iota : \alpha \hookrightarrow \beta$, the extended permutation $e.\text{viaEmbedding} \iota$ satisfies $(e.\text{viaEmbedding} \iota)(\iota x) = \iota (e x)$ for all $x \in \alpha$.

Equiv.Perm.viaEmbedding_apply_of_not_mem theorem

(x : β) (hx : x ∉ Set.range ι) : e.viaEmbedding ι x = x

Full source

theorem viaEmbedding_apply_of_not_mem (x : β) (hx : x ∉ Set.range ι) : e.viaEmbedding ι x = x :=
  extendDomain_apply_not_subtype e (ofInjective ι.1 ι.2) hx

Fixed Points Outside Embedding Range for Permutation Extension

Informal description

For any element $x \in \beta$ not in the range of the embedding $\iota : \alpha \hookrightarrow \beta$, the permutation $e.\text{viaEmbedding} \iota$ fixes $x$, i.e., $e.\text{viaEmbedding} \iota (x) = x$.

Equiv.Perm.viaEmbeddingHom definition

: Perm α →* Perm β

Full source

/-- `viaEmbedding` as a group homomorphism -/
noncomputable def viaEmbeddingHom : PermPerm α →* Perm β :=
  extendDomainHom (ofInjective ι.1 ι.2)

Permutation extension via embedding

Informal description

The group homomorphism that maps a permutation `e` of type `α` to a permutation of type `β` via an embedding `ι : α ↪ β`. For any element `x` in the range of `ι`, the permutation acts as `ι(e(ι⁻¹(x)))`, and for elements not in the range of `ι`, it acts as the identity.

Equiv.Perm.viaEmbeddingHom_apply theorem

: viaEmbeddingHom ι e = viaEmbedding e ι

Full source

theorem viaEmbeddingHom_apply : viaEmbeddingHom ι e = viaEmbedding e ι :=
  rfl

Equality of Permutation Extension via Embedding and its Homomorphism

Informal description

For any permutation $e$ of type $\alpha$ and any embedding $\iota : \alpha \hookrightarrow \beta$, the group homomorphism $\text{viaEmbeddingHom}$ applied to $e$ equals the permutation extension $\text{viaEmbedding}$ of $e$ via $\iota$, i.e., $\text{viaEmbeddingHom}(\iota)(e) = \text{viaEmbedding}(e, \iota)$.

Equiv.Perm.viaEmbeddingHom_injective theorem

: Function.Injective (viaEmbeddingHom ι)

Full source

theorem viaEmbeddingHom_injective : Function.Injective (viaEmbeddingHom ι) :=
  extendDomainHom_injective (ofInjective ι.1 ι.2)

Injectivity of Permutation Extension via Embedding Homomorphism

Informal description

The group homomorphism $\text{viaEmbeddingHom}(\iota) : \text{Perm}(\alpha) \to \text{Perm}(\beta)$, which extends permutations of $\alpha$ to permutations of $\beta$ via an embedding $\iota : \alpha \hookrightarrow \beta$, is injective.