Permutations preserving the fibers of a map #
Given f : α → ι, the permutations σ of α with f (σ a) = f a for every a form a subgroup
of Equiv.Perm α, here called TauCeti.fiberSubgroup f. This file records that subgroup, the
transpositions it contains, the behaviour of the construction under conjugation and pairing two
maps, the criteria for it to be trivial and for it to be a point stabilizer, and the isomorphism
restricting a fiber-preserving permutation to each fiber,
fiberSubgroup f ≃* ∀ i, Equiv.Perm {a // f a = i},
together with the two formulas reading that isomorphism, and its inverse, through a family of
equivalences {a // f a = i} ≃ β i of the fibers, which is how a concrete description of the
fibers is fed into it.
For finite α the cosets of fiberSubgroup f are the rearrangements of f: the coset of g
records the map f ∘ g⁻¹, and this identifies Equiv.Perm α ⧸ fiberSubgroup f, equivariantly,
with the maps α → ι having fibers of the same sizes as those of f
(TauCeti.quotientFiberSubgroupEquiv). When the fibers of f are the rows of a tabloid this is
the description of the tabloids as the row-colourings of α, and the fixed points of a
permutation π on the cosets are the rearrangements c with c ∘ π = c
(TauCeti.card_fixedPoints_quotient_fiberSubgroup).
The order of fiberSubgroup f is the product of the factorials of the fiber sizes
(TauCeti.natCard_fiberSubgroup). Summing these orders over all colourings α → ι, each
weighted by a function of its fiber sizes, therefore gives (card α)! times the sum of the weight
over the fiber-size functions of total card α (TauCeti.sum_natCard_fiberSubgroup_smul), the
orbit-stabilizer count that averages power sums over the symmetric group.
Mathlib already studies these permutations, but through the domain action of Equiv.Perm α on
α → ι: DomMulAct.stabilizerMulEquiv is the same isomorphism stated on
(MulAction.stabilizer (Equiv.Perm α)ᵈᵐᵃ f)ᵐᵒᵖ. The ᵈᵐᵃ/ᵐᵒᵖ wrapping makes it awkward to use
where the object of interest is a subgroup of Equiv.Perm α itself, as it is for the row and
column groups of a Young tableau; fiberSubgroup is that subgroup. The two presentations are
identified by fiberSubgroupMulEquivStabilizer, and the isomorphism above is Mathlib's
DomMulAct.stabilizerMulEquiv transported along it.
The subgroup of permutations of α that preserve every fiber of f : α → ι, that is, those
moving each point within its own fiber.
Equations
- TauCeti.fiberSubgroup f = { carrier := {σ : Equiv.Perm α | ∀ (a : α), f (σ a) = f a}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
The transposition of two points lying in a common fiber of f preserves every fiber of f:
it moves each of the two points to the other, inside their shared fiber, and fixes the rest.
Conjugation by e transports the subgroup preserving the fibers of f to the subgroup
preserving the fibers of g when e identifies their fiber equivalence relations.
Composing with an injective map does not change the fibers of f, hence neither the
permutations preserving them.
Preserving the fibers of two maps at once is preserving the fibers of the paired map.
A map whose fibers are {a} and at most one other makes the fiber subgroup a point
stabilizer. If f separates a from every other point and identifies all the others with one
another, then a permutation preserves the fibers of f exactly when it fixes a: the fiber {a}
can only be mapped to itself, and its complement -- a second fiber when it is nonempty, and empty
when α = {a} -- then takes care of itself.
Only the identity preserves the fibers of an injective map, its fibers being singletons.
If the identity is the only permutation preserving the fibers of f, then f is injective:
two points in a common fiber would be exchanged by a nontrivial fiber-preserving transposition.
The fibers of f are preserved only by the identity exactly when f is injective.
The permutations preserving the fibers of f are the stabilizer of f for the domain action
of Equiv.Perm α on α → ι, read as a subgroup of Equiv.Perm α itself: the ᵈᵐᵃ and ᵐᵒᵖ
synonyms reverse multiplication twice, so σ ↦ DomMulAct.mk σ is an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Read in (Equiv.Perm α)ᵈᵐᵃ, the stabilizer element attached to a fiber-preserving permutation
is that permutation.
Read in Equiv.Perm α, the fiber-preserving permutation attached to an element of the
stabilizer is that element.
Restricting a fiber-preserving permutation of α to each fiber of f is an isomorphism onto
the product of the permutation groups of the fibers.
This is Mathlib's DomMulAct.stabilizerMulEquiv transported along
fiberSubgroupMulEquivStabilizer.
Equations
Instances For
The fiber-preserving permutation assembled from a family of permutations of the fibers of f
moves each point by the permutation of its own fiber.
Reading fiberSubgroupMulEquivPiPerm f through equivalences e i : {a // f a = i} ≃ β i of
the fibers of f: the i-th component takes the point of β i matching a to the one matching
σ a. Specialising this to a concrete family of fibers gives the component formula for the
transported isomorphism.
Reading the inverse of fiberSubgroupMulEquivPiPerm f through equivalences
e i : {a // f a = i} ≃ β i of the fibers of f: the assembled permutation moves each point by
the permutation of its own fiber, read through e.
Local decidable equality for computing fiber cardinalities without an API constraint.
Equations
Instances For
The cosets of the fiber subgroup of f are the rearrangements of f. The coset of g
in Equiv.Perm α ⧸ fiberSubgroup f is sent to the map f ∘ g⁻¹
(TauCeti.quotientFiberSubgroupEquiv_mk), and every map with fibers of the same sizes as those of
f arises in exactly one way. The equivalence intertwines the left action of Equiv.Perm α on
the cosets with its action c ↦ c ∘ π⁻¹ on maps (TauCeti.quotientFiberSubgroupEquiv_smul).
Equations
- TauCeti.quotientFiberSubgroupEquiv f = Equiv.ofBijective (Quotient.lift (fun (g : Equiv.Perm α) => ⟨f ∘ ⇑g⁻¹, ⋯⟩) ⋯) ⋯
Instances For
The coset of g is sent to the rearrangement f ∘ g⁻¹ of f.
The rearrangement equivalence is equivariant: moving a coset by π precomposes the
corresponding rearrangement with π⁻¹.
A coset is fixed by π exactly when the corresponding rearrangement of f is invariant
under π.
The fixed cosets of π count the π-invariant rearrangements of f: the number of cosets
of the fiber subgroup of f fixed by π is the number of maps c : α → ι with fibers of the same
sizes as those of f and with c ∘ π = c. For the rows of a tabloid this is the value at π of
the permutation character on the tabloids.
The order of the fiber subgroup is the product of the factorials of the fiber sizes: a fiber-preserving permutation is an independent permutation of each fiber.
Every distribution of the points of α among the colours is the fiber-size function of some
colouring: a function d : ι → ℕ with total card α is i ↦ #{a | f a = i} for some
f : α → ι.
Summing the orders of the fiber subgroups over all colourings, each colouring weighted by
a function of its fiber sizes: the colourings with a given fiber-size function d form one orbit
of Equiv.Perm α, whose stabilizers are their fiber subgroups, so together they contribute
(card α)! times the weight of d, and every d of total card α occurs.