English
The application of stabilizerMulEquiv at i to g yields the corresponding fibre permutation at a, matching h.
Русский
Применение stabilizerMulEquiv к i и g даёт соответствующую перестановку на волокне, сопоставляющую a.
LaTeX
$$stabilizerMulEquiv g i ⟨a, h⟩ = mk.symm g.unop a$$
Lean4
/-- The `invFun` component of `MulEquiv` from `MulAction.stabilizer (Perm α) p`
to the product of the `Equiv.Perm {a | f a = i} (as an `Equiv.Perm α`) -/
def stabilizerEquiv_invFun_aux (g : ∀ i, Perm { a // f a = i }) : Perm α
where
toFun := stabilizerEquiv_invFun g
invFun := stabilizerEquiv_invFun (fun i ↦ (g i).symm)
left_inv
a := by
rw [stabilizerEquiv_invFun_eq _ (comp_stabilizerEquiv_invFun g a)]
exact congr_arg Subtype.val ((g <| f a).left_inv _)
right_inv
a := by
rw [stabilizerEquiv_invFun_eq _ (comp_stabilizerEquiv_invFun _ a)]
exact congr_arg Subtype.val ((g <| f a).right_inv _)
