DomMulAct.comp_stabilizerEquiv_invFun
theorem DomMulAct.comp_stabilizerEquiv_invFun :
∀ {α : Type u_1} {ι : Type u_2} {f : α → ι} (g : (i : ι) → Equiv.Perm { a // f a = i }) (a : α),
f (DomMulAct.stabilizerEquiv_invFun g a) = f a
The theorem `DomMulAct.comp_stabilizerEquiv_invFun` states that for any types `α` and `ι`, and any function `f` from `α` to `ι`, and any function `g` that associates each element `i` of `ι` with a permutation on the subset of `α` that `f` maps to `i`, applying the stabilizer's inverse function `DomMulAct.stabilizerEquiv_invFun` to an element `a` from `α` and then applying `f` to the result is the same as simply applying `f` to `a` directly. In other words, the operation of `DomMulAct.stabilizerEquiv_invFun` preserves the value of `f`.
More concisely: For any function `f: α → ι` and permutation association `g: ι → Σ (a: α) (i: ι) (f a = i),` applying the inverse stabilizer function `DomMulAct.stabilizerEquiv_invFun` to an element `a` in `α` and then applying `f` is equal to directly applying `f` to `a.` In other words, `DomMulAct.stabilizerEquiv_invFun` preserves the value of `f.`
|
DomMulAct.stabilizer_card
theorem DomMulAct.stabilizer_card :
∀ {α : Type u_1} {ι : Type u_2} (f : α → ι) [inst : Fintype α] [inst_1 : Fintype ι] [inst_2 : DecidableEq α]
[inst_3 : DecidableEq ι],
Fintype.card { g // f ∘ ⇑g = f } = Finset.univ.prod fun i => (Fintype.card { a // f a = i }).factorial
The theorem `DomMulAct.stabilizer_card` states that for any types `α` and `ι`, given a function `f` from `α` to `ι`, assuming `α` and `ι` are finite types and their equality is decidable, the cardinality or number of elements of the set of permutations that preserve the function `f` (meaning that the function `f` remains the same after applying the permutation) is equal to the product of the factorials of the cardinalities of the sets `{ a // f a = i }` for all `i` in the universal finite set of type `ι`. This universal set includes all possible values of type `ι`.
In simpler terms, this theorem counts the number of permutations of `α` that leave `f` unchanged. It calculates this by taking the product of the factorials of the sizes of the preimage sets of `f`.
More concisely: The theorem states that the number of permutations of a finite type preserving a function to another finite type equals the product of the factorials of the sizes of the preimage sets of the function values.
|
DomMulAct.stabilizerEquiv_invFun_eq
theorem DomMulAct.stabilizerEquiv_invFun_eq :
∀ {α : Type u_1} {ι : Type u_2} {f : α → ι} (g : (i : ι) → Equiv.Perm { a // f a = i }) {a : α} {i : ι}
(h : f a = i), DomMulAct.stabilizerEquiv_invFun g a = ↑((g i) ⟨a, h⟩)
The theorem `DomMulAct.stabilizerEquiv_invFun_eq` states that for any types `α` and `ι`, and any function `f` from `α` to `ι`, along with a function `g` which associates each element of `ι` to a permutation of the subset of `α` where `f` equals that element, for any given elements `a` in `α` and `i` in `ι` such that `f(a)` equals `i`, the `invFun` of the `stabilizerEquiv` applied to `g` and `a` is equal to the application of the permutation `g(i)` to the element `a` with the proof that `f(a)` equals `i`.
More concisely: For any function `f: α → ι` and permutation function `g: ι → permission (α × α)`, if `a ∈ α` and `i ∈ ι` satisfy `f(a) = i`, then `(stabilizerEquiv g a).invFun a = g(i)(a)`.
|