Mathlib.GroupTheory.Perm.Option

Equiv.optionCongr_one theorem

{α : Type*} : (1 : Perm α).optionCongr = 1

Full source

@[simp]
theorem Equiv.optionCongr_one {α : Type*} : (1 : Perm α).optionCongr = 1 :=
  Equiv.optionCongr_refl

Identity Permutation Preserved under `optionCongr`

Informal description

For any type $\alpha$, the permutation of the `Option α` type obtained by applying the `optionCongr` function to the identity permutation `1` of $\alpha$ is equal to the identity permutation of `Option α`.

Equiv.optionCongr_swap theorem

{α : Type*} [DecidableEq α] (x y : α) : optionCongr (swap x y) = swap (some x) (some y)

Full source

@[simp]
theorem Equiv.optionCongr_swap {α : Type*} [DecidableEq α] (x y : α) :
    optionCongr (swap x y) = swap (some x) (some y) := by
  ext (_ | i)
  · simp [swap_apply_of_ne_of_ne]
  · by_cases hx : i = x
    · simp only [hx, optionCongr_apply, Option.map_some', swap_apply_left, Option.mem_def,
             Option.some.injEq]
    by_cases hy : i = y <;> simp [hx, hy, swap_apply_of_ne_of_ne]

`optionCongr` Preserves Transpositions: `optionCongr (swap x y) = swap (some x) (some y)`

Informal description

For any type $\alpha$ with decidable equality and for any elements $x, y \in \alpha$, the permutation of `Option α` obtained by applying `optionCongr` to the transposition swapping $x$ and $y$ is equal to the transposition swapping `some x` and `some y`.

Equiv.optionCongr_sign theorem

{α : Type*} [DecidableEq α] [Fintype α] (e : Perm α) : Perm.sign e.optionCongr = Perm.sign e

Full source

@[simp]
theorem Equiv.optionCongr_sign {α : Type*} [DecidableEq α] [Fintype α] (e : Perm α) :
    Perm.sign e.optionCongr = Perm.sign e := by
  induction e using Perm.swap_induction_on with
  | one => simp [Perm.one_def]
  | swap_mul f x y hne h =>
    simp [h, hne, Perm.mul_def, ← Equiv.optionCongr_trans]

Sign Preservation under `optionCongr`: $\operatorname{sign}(\operatorname{optionCongr}(e)) = \operatorname{sign}(e)$

Informal description

For any finite type $\alpha$ with decidable equality and any permutation $e$ of $\alpha$, the sign of the permutation $\operatorname{optionCongr}(e)$ of $\operatorname{Option} \alpha$ is equal to the sign of $e$.

map_equiv_removeNone theorem

{α : Type*} [DecidableEq α] (σ : Perm (Option α)) : (removeNone σ).optionCongr = swap none (σ none) * σ

Full source

@[simp]
theorem map_equiv_removeNone {α : Type*} [DecidableEq α] (σ : Perm (Option α)) :
    (removeNone σ).optionCongr = swap none (σ none) * σ := by
  ext1 x
  have : Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x) := by
    obtain - | x := x
    · simp
    · cases h : σ (some _)
      · simp [removeNone_none _ h]
      · have hn : σ (some x) ≠ none := by simp [h]
        have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
        simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]
  simpa using this

Factorization of $\operatorname{optionCongr} \circ \operatorname{removeNone}$ via transposition and permutation

Informal description

For any type $\alpha$ with decidable equality and any permutation $\sigma$ of $\operatorname{Option} \alpha$, the permutation obtained by applying $\operatorname{optionCongr}$ to $\operatorname{removeNone} \sigma$ is equal to the composition of the transposition swapping $\operatorname{none}$ and $\sigma(\operatorname{none})$ with $\sigma$.

Equiv.Perm.decomposeOption definition

{α : Type*} [DecidableEq α] : Perm (Option α) ≃ Option α × Perm α

Full source

/-- Permutations of `Option α` are equivalent to fixing an
`Option α` and permuting the remaining with a `Perm α`.
The fixed `Option α` is swapped with `none`. -/
@[simps]
def Equiv.Perm.decomposeOption {α : Type*} [DecidableEq α] :
    PermPerm (Option α) ≃ Option α × Perm α where
  toFun σ := (σ none, removeNone σ)
  invFun i := swap none i.1 * i.2.optionCongr
  left_inv σ := by simp
  right_inv := fun ⟨x, σ⟩ => by
    have : removeNone (swap none x * σ.optionCongr) = σ :=
      Equiv.optionCongr_injective (by simp [← mul_assoc])
    simp [← Perm.eq_inv_iff_eq, this]

Decomposition of permutations of `Option α`

Informal description

The equivalence between permutations of `Option α` and pairs consisting of an element of `Option α` and a permutation of `α`. Specifically, a permutation `σ` of `Option α` is mapped to the pair `(σ none, removeNone σ)`, where `removeNone σ` is the permutation of `α` obtained by restricting `σ` to `α` (viewed as a subset of `Option α`). The inverse operation constructs a permutation of `Option α` by swapping `none` with the given element of `Option α` and applying the given permutation of `α` to the remaining elements.

Equiv.Perm.decomposeOption_symm_of_none_apply theorem

{α : Type*} [DecidableEq α] (e : Perm α) (i : Option α) : Equiv.Perm.decomposeOption.symm (none, e) i = i.map e

Full source

theorem Equiv.Perm.decomposeOption_symm_of_none_apply {α : Type*} [DecidableEq α] (e : Perm α)
    (i : Option α) : Equiv.Perm.decomposeOption.symm (none, e) i = i.map e := by simp

Application of Inverse Decomposition Equivalence for Permutations of $\operatorname{Option} \alpha$ with $\operatorname{none}$

Informal description

For any type $\alpha$ with decidable equality, given a permutation $e$ of $\alpha$ and an element $i$ of $\operatorname{Option} \alpha$, the application of the inverse of the decomposition equivalence $\operatorname{Equiv.Perm.decomposeOption}$ to the pair $(\operatorname{none}, e)$ evaluated at $i$ is equal to the image of $i$ under the permutation $e$ (where $\operatorname{none}$ is mapped to itself).

Equiv.Perm.decomposeOption_symm_sign theorem

 {α : Type*} [DecidableEq α] [Fintype α] (e : Perm α) :
  Perm.sign (Equiv.Perm.decomposeOption.symm (none, e)) = Perm.sign e

Full source

theorem Equiv.Perm.decomposeOption_symm_sign {α : Type*} [DecidableEq α] [Fintype α] (e : Perm α) :
    Perm.sign (Equiv.Perm.decomposeOption.symm (none, e)) = Perm.sign e := by simp

Sign Preservation under Inverse Decomposition for $\operatorname{Option} \alpha$: $\operatorname{sign}(\operatorname{decomposeOption.symm}(\operatorname{none}, e)) = \operatorname{sign}(e)$

Informal description

For any finite type $\alpha$ with decidable equality and any permutation $e$ of $\alpha$, the sign of the permutation $\operatorname{decomposeOption.symm}(\operatorname{none}, e)$ of $\operatorname{Option} \alpha$ is equal to the sign of $e$.

Finset.univ_perm_option theorem

 {α : Type*} [DecidableEq α] [Fintype α] :
  @Finset.univ (Perm <| Option α) _ =
    (Finset.univ : Finset <| Option α × Perm α).map Equiv.Perm.decomposeOption.symm.toEmbedding

Full source

/-- The set of all permutations of `Option α` can be constructed by augmenting the set of
permutations of `α` by each element of `Option α` in turn. -/
theorem Finset.univ_perm_option {α : Type*} [DecidableEq α] [Fintype α] :
    @Finset.univ (Perm <| Option α) _ =
      (Finset.univ : Finset <| OptionOption α × Perm α).map Equiv.Perm.decomposeOption.symm.toEmbedding :=
  (Finset.univ_map_equiv_to_embedding _).symm

Characterization of Permutations of $\mathrm{Option}\,\alpha$ via Decomposition

Informal description

For a finite type $\alpha$ with decidable equality, the set of all permutations of $\mathrm{Option}\,\alpha$ is equal to the image of the set of all pairs $(x, \sigma)$ where $x \in \mathrm{Option}\,\alpha$ and $\sigma$ is a permutation of $\alpha$, under the inverse of the decomposition equivalence $\mathrm{Equiv.Perm.decomposeOption}$.