Base permutations

In this file, we define base permutations, their group structure, and their actions on atoms, litters, and near-litters.

Main declarations

• ConNF.BasePerm: The type of base permutations.
• ConNF.BasePerm.smul_nearLitter_coe: The action of a base permutation on a near-litter agrees with the pointwise action that treats it as a set of atoms.
• ConNF.BasePerm.smul_nearLitter_eq_smul_symmDiff_smul: We can determine the action of a base permutation on a near-litter by knowing its precise action on the relevant litter, as well as the action on all atoms in the symmetric difference between that near-litter and its corresponding litter.

structure ConNF.BasePerm [ConNF.Params] : Type u

A base permutation is a permutation of atoms which sends near-litters to near-litters. Then, the images of near-litters near the same litter must be near the same litter. Hence a base permutation induces a permutation of litters, and we keep that as data for simplicity.

This is sometimes called a -1-allowable permutation. The proposition near can be interpreted as saying that if s is an L-near-litter, then its image under the permutation (atomPerm) is near the litter that L is mapped to under the litter permutation (litterPerm).

The definition ↑atomPerm⁻¹ ⁻¹' s is used instead of ↑atomPerm '' s because it has better definitional properties. For instance, x ∈ ↑atomPerm⁻¹ ⁻¹' s is definitionally equal to atomPerm⁻¹ x ∈ s.

• atomPerm : Equiv.Perm ConNF.Atom
• litterPerm : Equiv.Perm ConNF.Litter
• near : ∀ ⦃L : ConNF.Litter⦄ ⦃s : Set ConNF.Atom⦄, ConNF.IsNearLitter L s → ConNF.IsNearLitter (self.litterPerm L) (⇑self.atomPerm⁻¹ ⁻¹' s)

theorem ConNF.BasePerm.near [ConNF.Params] (self : ConNF.BasePerm) ⦃L : ConNF.Litter⦄ ⦃s : Set ConNF.Atom⦄ : ConNF.IsNearLitter L s → ConNF.IsNearLitter (self.litterPerm L) (⇑self.atomPerm⁻¹ ⁻¹' s)

theorem ConNF.IsNearLitter.map [ConNF.Params] {L : ConNF.Litter} {π : ConNF.BasePerm} {s : Set ConNF.Atom} (h : ConNF.IsNearLitter L s) : ConNF.IsNearLitter (π.litterPerm L) (π.atomPerm⁻¹.toFun ⁻¹' s)

This is the condition that relates the atomPerm and the litterPerm. This is essentially the field near in the structure BasePerm, but presented here as a lemma.

theorem ConNF.BasePerm.atomPerm_injective [ConNF.Params] : Function.Injective ConNF.BasePerm.atomPerm

The map from the type of base permutations to the type of permutations of atoms is injective. That is, if two base permutations have the same action on atoms, they are equal.

theorem ConNF.BasePerm.ext [ConNF.Params] {π : ConNF.BasePerm} {π' : ConNF.BasePerm} (h : π.atomPerm = π'.atomPerm) : π = π'

An extensionality result for base permutations. If two base permutations have the same action on atoms, they are equal.

We are going to show that the set of base permutations forms a group. To do this, we construct several instances, such as the existence of an identity element or inverse elements.

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

The identity base permutation.

Equations

• ConNF.BasePerm.instOne = { one := { atomPerm := 1, litterPerm := 1, near := ⋯ } }

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

Any base permutation admits an inverse, which is also a base permutation.

Equations

• ConNF.BasePerm.instInv = { inv := fun (π : ConNF.BasePerm) => { atomPerm := π.atomPerm⁻¹, litterPerm := π.litterPerm⁻¹, near := ⋯ } }

instance ConNF.BasePerm.instMul [ConNF.Params] : Mul ConNF.BasePerm

Base permutations can be composed.

Equations

• ConNF.BasePerm.instMul = { mul := fun (π π' : ConNF.BasePerm) => { atomPerm := π.atomPerm * π'.atomPerm, litterPerm := π.litterPerm * π'.litterPerm, near := ⋯ } }

instance ConNF.BasePerm.instDiv [ConNF.Params] : Div ConNF.BasePerm

Dividing two permutations π / π' can be interpreted as π * π'⁻¹.

Equations

• ConNF.BasePerm.instDiv = { div := fun (π π' : ConNF.BasePerm) => { atomPerm := π.atomPerm / π'.atomPerm, litterPerm := π.litterPerm / π'.litterPerm, near := ⋯ } }

instance ConNF.BasePerm.instPowNat [ConNF.Params] : Pow ConNF.BasePerm ℕ

We can raise base permutations to a natural power since we can do this to permutations of atoms and litters.

Equations

• ConNF.BasePerm.instPowNat = { pow := fun (π : ConNF.BasePerm) (n : ℕ) => { atomPerm := π.atomPerm ^ n, litterPerm := π.litterPerm ^ n, near := ⋯ } }

instance ConNF.BasePerm.instPowInt [ConNF.Params] : Pow ConNF.BasePerm ℤ

We can raise base permutations to an integer power since we can do this to permutations of atoms and litters.

Equations

• ConNF.BasePerm.instPowInt = { pow := fun (π : ConNF.BasePerm) (n : ℤ) => { atomPerm := π.atomPerm ^ n, litterPerm := π.litterPerm ^ n, near := ⋯ } }

instance ConNF.BasePerm.instInhabited [ConNF.Params] : Inhabited ConNF.BasePerm

Equations

• ConNF.BasePerm.instInhabited = { default := 1 }

The following lemmas describe how the group of base permutations interacts with the group of base type permutations and the group of litter permutations. In particular, many group operations, such as taking the inverse, can be moved out of the near-litter context and into the (simpler) base permutation or litter permutation context.

The @[simp] attribute teaches these results to the simp tactic. This means that simp will (for example) prefer group operations to be applied after extracting the base permutation, not before.

@[simp]

theorem ConNF.BasePerm.atomPerm_one [ConNF.Params] : ConNF.BasePerm.atomPerm 1 = 1

@[simp]

theorem ConNF.BasePerm.atomPerm_inv [ConNF.Params] (π : ConNF.BasePerm) : π⁻¹.atomPerm = π.atomPerm⁻¹

@[simp]

theorem ConNF.BasePerm.atomPerm_hMul [ConNF.Params] (π : ConNF.BasePerm) (π' : ConNF.BasePerm) : (π * π').atomPerm = π.atomPerm * π'.atomPerm

@[simp]

theorem ConNF.BasePerm.atomPerm_div [ConNF.Params] (π : ConNF.BasePerm) (π' : ConNF.BasePerm) : (π / π').atomPerm = π.atomPerm / π'.atomPerm

@[simp]

theorem ConNF.BasePerm.atomPerm_pow [ConNF.Params] (π : ConNF.BasePerm) (n : ℕ) : (π ^ n).atomPerm = π.atomPerm ^ n

@[simp]

theorem ConNF.BasePerm.atomPerm_zpow [ConNF.Params] (π : ConNF.BasePerm) (n : ℤ) : (π ^ n).atomPerm = π.atomPerm ^ n

@[simp]

theorem ConNF.BasePerm.litterPerm_one [ConNF.Params] : ConNF.BasePerm.litterPerm 1 = 1

@[simp]

theorem ConNF.BasePerm.litterPerm_inv [ConNF.Params] (π : ConNF.BasePerm) : π⁻¹.litterPerm = π.litterPerm⁻¹

@[simp]

theorem ConNF.BasePerm.litterPerm_hMul [ConNF.Params] (π : ConNF.BasePerm) (π' : ConNF.BasePerm) : (π * π').litterPerm = π.litterPerm * π'.litterPerm

@[simp]

theorem ConNF.BasePerm.litterPerm_div [ConNF.Params] (π : ConNF.BasePerm) (π' : ConNF.BasePerm) : (π / π').litterPerm = π.litterPerm / π'.litterPerm

@[simp]

theorem ConNF.BasePerm.litterPerm_pow [ConNF.Params] (π : ConNF.BasePerm) (n : ℕ) : (π ^ n).litterPerm = π.litterPerm ^ n

@[simp]

theorem ConNF.BasePerm.litterPerm_zpow [ConNF.Params] (π : ConNF.BasePerm) (n : ℤ) : (π ^ n).litterPerm = π.litterPerm ^ n

instance ConNF.BasePerm.instGroup [ConNF.Params] : Group ConNF.BasePerm

Base permutations form a group.

Equations

• ConNF.BasePerm.instGroup = Function.Injective.group ConNF.BasePerm.atomPerm ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Base permutations act on atoms via the atom permutation.

Equations

• ConNF.BasePerm.instMulActionAtom = MulAction.mk ⋯ ⋯

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

Base permutations act on litters via the litter permutation.

Equations

• ConNF.BasePerm.instMulActionLitter = MulAction.mk ⋯ ⋯

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

Base permutations act on near-litters.

Equations

• ConNF.BasePerm.instMulActionNearLitter = MulAction.mk ⋯ ⋯

theorem ConNF.BasePerm.smul_nearLitter_def [ConNF.Params] (π : ConNF.BasePerm) (N : ConNF.NearLitter) : π • N = ⟨π • N.fst, ⟨⇑π.atomPerm⁻¹ ⁻¹' ↑N, ⋯⟩⟩

@[simp]

theorem ConNF.BasePerm.smul_nearLitter_fst [ConNF.Params] (π : ConNF.BasePerm) (N : ConNF.NearLitter) : (π • N).fst = π • N.fst

theorem ConNF.BasePerm.smul_nearLitter_coe_preimage [ConNF.Params] (π : ConNF.BasePerm) (N : ConNF.NearLitter) : ↑(π • N) = ⇑π.atomPerm⁻¹ ⁻¹' ↑N

theorem ConNF.BasePerm.smul_nearLitter_coe [ConNF.Params] (π : ConNF.BasePerm) (N : ConNF.NearLitter) : ↑(π • N) = π • ↑N

The action of a base permutation on a near-litter agrees with the pointwise action on its atoms.

theorem ConNF.BasePerm.smul_nearLitter_snd [ConNF.Params] (π : ConNF.BasePerm) (N : ConNF.NearLitter) : ↑(π • N).snd = π • ↑N.snd

@[simp]

theorem ConNF.BasePerm.NearLitter.mem_snd_iff [ConNF.Params] (N : ConNF.NearLitter) (a : ConNF.Atom) : a ∈ ↑N.snd ↔ a ∈ N

@[simp]

theorem ConNF.BasePerm.NearLitter.not_mem_snd_iff [ConNF.Params] (N : ConNF.NearLitter) (a : ConNF.Atom) : a ∉ ↑N.snd ↔ a ∉ N

theorem ConNF.BasePerm.smul_nearLitter_eq_smul_symmDiff_smul [ConNF.Params] (π : ConNF.BasePerm) (N : ConNF.NearLitter) : ↑(π • N) = symmDiff (↑(π • N.fst.toNearLitter)) (π • symmDiff (ConNF.litterSet N.fst) ↑N.snd)