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 #

source

structure ConNF.BasePerm [Params] :

Type u

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 Atom
litters : Equiv.Perm Litter
apply_near_apply (s : Set Atom) (L : Litter) : s ~ Lᴬ → ⇑self.atoms '' s ~ (self.litters L)ᴬ

Instances For

source

instance ConNF.BasePerm.instSuperAPermAtom [Params] :

SuperA BasePerm (Equiv.Perm Atom)

If π is a base permutation, we write πᴬ for its associated permutation of atoms.

Equations

ConNF.BasePerm.instSuperAPermAtom = { superA := ConNF.BasePerm.atoms }

source

instance ConNF.BasePerm.instSuperLPermLitter [Params] :

SuperL BasePerm (Equiv.Perm Litter)

If π is a base permutation, we write πᴸ for its associated permutation of litters.

Equations

ConNF.BasePerm.instSuperLPermLitter = { superL := ConNF.BasePerm.litters }

source

instance ConNF.BasePerm.instSMulAtom [Params] :

SMul BasePerm Atom

For a base permutation π and an atom a, we write π • a for πᴬ a. We will later show that this is a group action.

Equations

ConNF.BasePerm.instSMulAtom = { smul := fun (π : ConNF.BasePerm) (a : ConNF.Atom) => πᴬ a }

source

instance ConNF.BasePerm.instSMulLitter [Params] :

SMul BasePerm Litter

For a base permutation π and a litter L, we write π • L for πᴸ L. We will later show that this is a group action.

Equations

ConNF.BasePerm.instSMulLitter = { smul := fun (π : ConNF.BasePerm) (L : ConNF.Litter) => πᴸ L }

source

theorem ConNF.BasePerm.smul_near_smul [Params] (π : BasePerm) (s : Set Atom) (L : Litter) :

s ~ Lᴬ → π • s ~ (π • L)ᴬ

A restatement of apply_near_apply using the new notations.

source

instance ConNF.BasePerm.instSMulNearLitter [Params] :

SMul BasePerm NearLitter

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.

Equations

ConNF.BasePerm.instSMulNearLitter = { smul := fun (π : ConNF.BasePerm) (N : ConNF.NearLitter) => { litter := π • Nᴸ, atoms := π • Nᴬ, atoms_near_litter' := ⋯ } }

We establish some useful definitional equalities.

source

theorem ConNF.BasePerm.smul_atom_def [Params] (π : BasePerm) (a : Atom) :

π • a = πᴬ a

source

theorem ConNF.BasePerm.smul_litter_def [Params] (π : BasePerm) (L : Litter) :

π • L = πᴸ L

source

@[simp]

theorem ConNF.BasePerm.smul_nearLitter_atoms [Params] (π : BasePerm) (N : NearLitter) :

(π • N)ᴬ = π • Nᴬ

source

@[simp]

theorem ConNF.BasePerm.smul_nearLitter_litter [Params] (π : BasePerm) (N : NearLitter) :

(π • N)ᴸ = π • Nᴸ

source

theorem ConNF.BasePerm.ext [Params] {π₁ π₂ : BasePerm} (h : ∀ (a : Atom), π₁ • a = π₂ • a) :

π₁ = π₂

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.