Structural permutations

In this file, we define the ambient groups of structural permutations. These will later have recursively-constructed subgroups of allowable permutations which will act on t-sets; we define these larger ambient groups in advance in order to set up their infrastructure of derivatives and so on independently of the recursion.

We define structural permutations as trees of base permutations.

Main declarations

• ConNF.StructPerm: The type of structural permutations.

@[reducible, inline]

abbrev ConNF.StructPerm [ConNF.Params] : ConNF.TypeIndex → Type u

A structural permutation on a proper type index α is a base permutation for each α-extended index. This represents how the permutation acts along each path down the type levels in the model. Note that we define structural permutations as trees of near-litter permutations.

Equations

• ConNF.StructPerm = ConNF.Tree ConNF.BasePerm

instance ConNF.StructPerm.instInhabitedStructPerm [ConNF.Params] (α : ConNF.TypeIndex) : Inhabited (ConNF.StructPerm α)

Equations

• ConNF.StructPerm.instInhabitedStructPerm α = { default := fun (x : ConNF.ExtendedIndex α) => 1 }

The following lemmas show how the action of ⊥-structural permutations on near-litters behaves; this is exactly how base permutations behave.

@[simp]

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

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

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

@[simp]

theorem ConNF.StructPerm.comp_bot_smul_atom [ConNF.Params] {α : ConNF.TypeIndex} (π : ConNF.StructPerm α) (A : ConNF.ExtendedIndex α) (a : ConNF.Atom) : ConNF.Tree.comp A π • a = π A • a

@[simp]

theorem ConNF.StructPerm.comp_bot_smul_litter [ConNF.Params] {α : ConNF.TypeIndex} (π : ConNF.StructPerm α) (A : ConNF.ExtendedIndex α) (L : ConNF.Litter) : ConNF.Tree.comp A π • L = π A • L

@[simp]

theorem ConNF.StructPerm.comp_bot_smul_nearLitter [ConNF.Params] {α : ConNF.TypeIndex} (π : ConNF.StructPerm α) (A : ConNF.ExtendedIndex α) (N : ConNF.NearLitter) : ConNF.Tree.comp A π • N = π A • N

@[irreducible]

def ConNF.StructPerm.structSetAction [ConNF.Params] {α : ConNF.TypeIndex} : ConNF.StructPerm α → ConNF.StructSet α → ConNF.StructSet α

Equations

• One or more equations did not get rendered due to their size.
• π.structSetAction t = ConNF.StructSet.toBot (ConNF.Tree.ofBot π • ConNF.StructSet.ofBot t)

theorem ConNF.StructPerm.one_structSetAction [ConNF.Params] {α : ConNF.TypeIndex} (t : ConNF.StructSet α) : ConNF.StructPerm.structSetAction 1 t = t

theorem ConNF.StructPerm.mul_structSetAction [ConNF.Params] {α : ConNF.TypeIndex} (π₁ : ConNF.StructPerm α) (π₂ : ConNF.StructPerm α) (t : ConNF.StructSet α) : (π₁ * π₂).structSetAction t = π₁.structSetAction (π₂.structSetAction t)

instance ConNF.StructPerm.instMulActionStructSet [ConNF.Params] {α : ConNF.TypeIndex} : MulAction (ConNF.StructPerm α) (ConNF.StructSet α)

Equations

• ConNF.StructPerm.instMulActionStructSet = MulAction.mk ⋯ ⋯

theorem ConNF.StructPerm.smul_eq [ConNF.Params] {α : ConNF.TypeIndex} (π : ConNF.StructPerm α) (t : ConNF.StructSet α) : π • t = π.structSetAction t

theorem ConNF.StructPerm.smul_bot_eq [ConNF.Params] (π : ConNF.StructPerm ⊥) (t : ConNF.StructSet ⊥) : π • t = ConNF.StructSet.toBot (ConNF.Tree.ofBot π • ConNF.StructSet.ofBot t)

theorem ConNF.StructPerm.ofCoe_smul [ConNF.Params] {α : ConNF.Λ} {β : ConNF.TypeIndex} (π : ConNF.StructPerm ↑α) (t : ConNF.StructSet ↑α) (h : β < ↑α) : ConNF.StructSet.ofCoe (π • t) β h = ConNF.Tree.comp (Quiver.Hom.toPath h) π • ConNF.StructSet.ofCoe t β h