Base permutations #
In this file, we define the group of base permutations, and their actions on atoms, litters, and
near-litters. In the paper, these are called -1
-allowable permutations, but that term has a
different meaning in this formalisation.
Definitions #
A base permutation consists of a permutation of atoms, a permutation of litters, and a proof
that if some set s
is near the litter set of some litter L
, then when we apply the permutation
of atoms pointwise to s
, the resulting set of atoms is near the litter obtained by applying the
permutation of litters to L
. This condition means that the pointwise image of a near-litter N
under the permutation of atoms is a near-litter, and that the litter it is near to is just the image
of Nᴸ
under the permutation of litters. It is easy to see that it is not necessary to include
the litter permutation in this definition, because the image of some litter L
under the
permutation of litters must be the unique litter near the pointwise image of Lᴬ
under the map of
atoms; we simply include the data of this extra permutation for definitional convenience.
- atoms : Equiv.Perm ConNF.Atom
- litters : Equiv.Perm ConNF.Litter
Instances For
If π
is a base permutation, we write πᴬ
for its associated permutation of atoms.
Equations
- ConNF.BasePerm.instSuperAPermAtom = { superA := ConNF.BasePerm.atoms }
If π
is a base permutation, we write πᴸ
for its associated permutation of litters.
Equations
- ConNF.BasePerm.instSuperLPermLitter = { superL := ConNF.BasePerm.litters }
For a base permutation π
and an atom a
, we write π • a
for πᴬ a
.
We will later show that this is a group action.
For a base permutation π
and a litter L
, we write π • L
for πᴸ L
.
We will later show that this is a group action.
A restatement of apply_near_apply
using the new notations.
For a base permutation π
and an atom N
, we write π • N
for the near-litter N'
such that
N'ᴸ = π • Nᴸ
and N'ᴬ = π • Nᴬ
, where the latter group action on sets of atoms is the pointwise
action. We will later show that this is a group action.
We establish some useful definitional equalities.
An extensionality principle for base permutations: if two base permutations have the same
action on atoms, then they coincide. This is because we can recover the data of πᴸ
from πᴬ
,
given that π
is a base permutation.
Group structure #
The identity permutation.
Equations
- ConNF.BasePerm.instOne = { one := { atoms := 1, litters := 1, apply_near_apply := ⋯ } }
The relevant instance of smul_near_smul
for the inverse of a base permutation.
The inverse of a permutation.
The group structure on base permutations.
The action of base permutations on atoms is a group action.
Equations
- ConNF.BasePerm.instMulActionAtom = MulAction.mk ⋯ ⋯
The action of base permutations on litters is a group action.
Equations
- ConNF.BasePerm.instMulActionLitter = MulAction.mk ⋯ ⋯
The action of base permutations on near-litters is a group action.
Equations
- ConNF.BasePerm.instMulActionNearLitter = MulAction.mk ⋯ ⋯
Base permutations commute with the interference of near-litters.