Documentation

ConNF.Base.BasePerm

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
  • apply_near_apply : ∀ (s : Set ConNF.Atom) (L : ConNF.Litter), s ~ Lself.atoms '' s ~ (self.litters L)
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 }
    instance ConNF.BasePerm.instSMulAtom [ConNF.Params] :
    SMul ConNF.BasePerm ConNF.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 }
    instance ConNF.BasePerm.instSMulLitter [ConNF.Params] :
    SMul ConNF.BasePerm ConNF.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 }
    theorem ConNF.BasePerm.smul_near_smul [ConNF.Params] (π : ConNF.BasePerm) (s : Set ConNF.Atom) (L : ConNF.Litter) :
    s ~ Lπ s ~ (π L)

    A restatement of apply_near_apply using the new notations.

    instance ConNF.BasePerm.instSMulNearLitter [ConNF.Params] :
    SMul ConNF.BasePerm ConNF.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.

    theorem ConNF.BasePerm.smul_atom_def [ConNF.Params] (π : ConNF.BasePerm) (a : ConNF.Atom) :
    π a = π a
    theorem ConNF.BasePerm.smul_litter_def [ConNF.Params] (π : ConNF.BasePerm) (L : ConNF.Litter) :
    π L = π L
    @[simp]
    theorem ConNF.BasePerm.smul_nearLitter_atoms [ConNF.Params] (π : ConNF.BasePerm) (N : ConNF.NearLitter) :
    (π N) = π N
    @[simp]
    theorem ConNF.BasePerm.smul_nearLitter_litter [ConNF.Params] (π : ConNF.BasePerm) (N : ConNF.NearLitter) :
    (π N) = π N
    theorem ConNF.BasePerm.ext [ConNF.Params] {π₁ π₂ : ConNF.BasePerm} (h : ∀ (a : ConNF.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.

    Group structure #

    instance ConNF.BasePerm.instOne [ConNF.Params] :
    One ConNF.BasePerm

    The identity permutation.

    Equations
    • ConNF.BasePerm.instOne = { one := { atoms := 1, litters := 1, apply_near_apply := } }
    instance ConNF.BasePerm.instMul [ConNF.Params] :
    Mul ConNF.BasePerm

    The composition of permutations.

    Equations
    • ConNF.BasePerm.instMul = { mul := fun (π₁ π₂ : ConNF.BasePerm) => { atoms := π₁ * π₂, litters := π₁ * π₂, apply_near_apply := } }
    @[simp]
    theorem ConNF.BasePerm.mul_atom [ConNF.Params] (π₁ π₂ : ConNF.BasePerm) :
    (π₁ * π₂) = π₁ * π₂
    @[simp]
    theorem ConNF.BasePerm.mul_litter [ConNF.Params] (π₁ π₂ : ConNF.BasePerm) :
    (π₁ * π₂) = π₁ * π₂
    theorem ConNF.BasePerm.inv_smul_near_inv_smul [ConNF.Params] (π : ConNF.BasePerm) (s : Set ConNF.Atom) (L : ConNF.Litter) :
    s ~ Lπ⁻¹ s ~ (π⁻¹ L)

    The relevant instance of smul_near_smul for the inverse of a base permutation.

    instance ConNF.BasePerm.instInv [ConNF.Params] :
    Inv ConNF.BasePerm

    The inverse of a permutation.

    Equations
    • ConNF.BasePerm.instInv = { inv := fun (π : ConNF.BasePerm) => { atoms := π⁻¹, litters := π⁻¹, apply_near_apply := } }
    @[simp]
    theorem ConNF.BasePerm.inv_atom [ConNF.Params] (π : ConNF.BasePerm) :
    @[simp]
    theorem ConNF.BasePerm.inv_litter [ConNF.Params] (π : ConNF.BasePerm) :
    instance ConNF.BasePerm.instGroup [ConNF.Params] :
    Group ConNF.BasePerm

    The group structure on base permutations.

    Equations
    instance ConNF.BasePerm.instMulActionAtom [ConNF.Params] :
    MulAction ConNF.BasePerm ConNF.Atom

    The action of base permutations on atoms is a group action.

    Equations
    instance ConNF.BasePerm.instMulActionLitter [ConNF.Params] :
    MulAction ConNF.BasePerm ConNF.Litter

    The action of base permutations on litters is a group action.

    Equations
    instance ConNF.BasePerm.instMulActionNearLitter [ConNF.Params] :
    MulAction ConNF.BasePerm ConNF.NearLitter

    The action of base permutations on near-litters is a group action.

    Equations
    @[simp]
    theorem ConNF.BasePerm.smul_interference [ConNF.Params] (π : ConNF.BasePerm) (N₁ N₂ : ConNF.NearLitter) :
    π ConNF.interference N₁ N₂ = ConNF.interference (π N₁) (π N₂)

    Base permutations commute with the interference of near-litters.