class NominalSets.PermAction (𝔸 : Type u_1) (X : Type u_2) : Type (max u_1 u_2)

A permutable type X has a Perm-action.

• perm : Perm 𝔸 → X → X

  Applies a permutation to an element.

• perm_one (x : X) : perm 1 x = x

  The identity permutation acts as the identity.

• perm_mul (π₁ π₂ : Perm 𝔸) (x : X) : perm π₁ (perm π₂ x) = perm (π₁ * π₂) x

  Composition of permutations is composition of actions.

class NominalSets.DiscretePermAction (𝔸 : Type u_1) (X : Type u_2) [PermAction 𝔸 X] : Prop

A discrete permutable type's elements are not affected by permutation.

• perm_discrete (π : Perm 𝔸) (x : X) : perm π x = x

  Permutation does nothing.

def NominalSets.«termDiscretePermAction[_]» : Lean.ParserDescr

A discrete permutable type's elements are not affected by permutation.

Equations

• One or more equations did not get rendered due to their size.

def NominalSets.PermAction.lift (𝔸 : Type u_1) {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] (eq : X ≃ Y) : PermAction 𝔸 Y

We can construct PermAction instances via a bijection.

Equations

• NominalSets.PermAction.lift 𝔸 eq = { perm := fun (π : NominalSets.Perm 𝔸) (x : Y) => eq (NominalSets.perm π (eq.invFun x)), perm_one := ⋯, perm_mul := ⋯ }

instance NominalSets.PermAction.instInhabited {𝔸 : Type u_1} {X : Type u_2} : Inhabited (PermAction 𝔸 X)

Equations

• NominalSets.PermAction.instInhabited = { default := { perm := fun (x : NominalSets.Perm 𝔸) (x_1 : X) => x_1, perm_one := ⋯, perm_mul := ⋯ } }

instance NominalSets.PermAction.inst {𝔸 : Type u_1} : PermAction 𝔸 𝔸

Equations

• NominalSets.PermAction.inst = { perm := fun (π : NominalSets.Perm 𝔸) (x : 𝔸) => π x, perm_one := ⋯, perm_mul := ⋯ }

@[simp]

theorem NominalSets.PermAction.perm_def {𝔸 : Type u_1} (π : Perm 𝔸) (x : 𝔸) : perm π x = π x

instance NominalSets.Bool.instPermActionBool {𝔸 : Type u_1} : PermAction 𝔸 Bool

Equations

• NominalSets.Bool.instPermActionBool = default

instance NominalSets.Empty.instPermActionEmpty {𝔸 : Type u_1} : PermAction 𝔸 Empty

Equations

• NominalSets.Empty.instPermActionEmpty = default

instance NominalSets.PEmpty.instPermActionPEmpty {𝔸 : Type u_1} : PermAction 𝔸 PEmpty.{u_4 + 1}

Equations

• NominalSets.PEmpty.instPermActionPEmpty = default

instance NominalSets.Unit.instPermActionUnit {𝔸 : Type u_1} : PermAction 𝔸 Unit

Equations

• NominalSets.Unit.instPermActionUnit = default

instance NominalSets.PUnit.instPermActionPUnit {𝔸 : Type u_1} : PermAction 𝔸 PUnit.{u_4 + 1}

Equations

• NominalSets.PUnit.instPermActionPUnit = default

instance NominalSets.Function.instPermActionForall {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : PermAction 𝔸 (X → Y)

Equations

• NominalSets.Function.instPermActionForall = { perm := fun (π : NominalSets.Perm 𝔸) (f : X → Y) (x : X) => NominalSets.perm π (f (NominalSets.perm π⁻¹ x)), perm_one := ⋯, perm_mul := ⋯ }

@[simp]

theorem NominalSets.Function.perm_def {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (π : Perm 𝔸) (f : X → Y) (x : X) : perm π f x = perm π (f (perm π⁻¹ x))