Allowable permutations

In this file, we define the type of allowable permutations at level α, assuming that they exist for all type indices β < α.

Main declarations

• ConNF.Derivatives: A collection of allowable permutations at every level β < α, which are the one-step derivatives of the newly defined allowable permutations at level α.
• ConNF.NewAllowable: A collection of Derivatives that commutes with the fuzz map.
• ConNF.Code.smul_code: Allowable permutations preserve code equivalence.

def ConNF.Derivatives [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : Type u

A collection of derivatives is a collection of allowable permutations at every type index β < α. The type of allowable permutations is a subtype of this type.

Equations

• ConNF.Derivatives = ((β : ConNF.TypeIndex) → [inst_1 : ConNF.LtLevel β] → ConNF.Allowable β)

instance ConNF.instGroupDerivatives [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : Group ConNF.Derivatives

Equations

• ConNF.instGroupDerivatives = Pi.group

@[simp]

theorem ConNF.Derivatives.one_apply [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (β : ConNF.TypeIndex) [ConNF.LtLevel β] : 1 β = 1

@[simp]

theorem ConNF.Derivatives.mul_apply [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (β : ConNF.TypeIndex) [ConNF.LtLevel β] (ρ : ConNF.Derivatives) (ρ' : ConNF.Derivatives) : (ρ * ρ') β = ρ β * ρ' β

@[simp]

theorem ConNF.Derivatives.inv_apply [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (β : ConNF.TypeIndex) [ConNF.LtLevel β] (ρ : ConNF.Derivatives) : ρ⁻¹ β = (ρ β)⁻¹

The bottom of a path can be easily manipulated with operations such as cons. We now need to introduce machinery for manipulating the top of a path. This allows us to convert collections of derivatives structural permutations, whose derivative maps are more naturally expressed in the other direction.

def ConNF.Derivatives.pathTop {V : Type u_1} [Quiver V] {x : V} {y : V} : Quiver.Path x y → V

If the path is nonempty, extract the second element of the path. This requires induction over paths because paths in quivers are expressed with their cons operation at the end, not the start.

Equations

• ConNF.Derivatives.pathTop (Quiver.Path.nil.cons e) = y
• ConNF.Derivatives.pathTop ((p.cons e).cons a) = ConNF.Derivatives.pathTop (p.cons e)
• ConNF.Derivatives.pathTop Quiver.Path.nil = x

theorem ConNF.Derivatives.pathTop_toPath_comp {V : Type u_2} [Quiver V] {x : V} {y : V} {z : V} (e : x ⟶ y) (p : Quiver.Path y z) : ConNF.Derivatives.pathTop (e.toPath.comp p) = y

def ConNF.Derivatives.pathTop_hom {V : Type u_1} [Quiver V] {x : V} {y : V} (p : Quiver.Path x y) (h : p.length ≠ 0) : x ⟶ ConNF.Derivatives.pathTop p

Equations

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

def ConNF.Derivatives.pathTail {V : Type u_1} [Quiver V] {x : V} {y : V} (p : Quiver.Path x y) : Quiver.Path (ConNF.Derivatives.pathTop p) y

Extract the portion of the path after the first morphism.

Equations

• ConNF.Derivatives.pathTail (Quiver.Path.nil.cons e) = Quiver.Path.nil
• ConNF.Derivatives.pathTail ((p.cons e).cons a) = (ConNF.Derivatives.pathTail (p.cons e)).cons a
• ConNF.Derivatives.pathTail Quiver.Path.nil = Quiver.Path.nil

theorem ConNF.Derivatives.pathTop_pathTail {V : Type u_2} [Quiver V] {x : V} {y : V} (p : Quiver.Path x y) (h : p.length ≠ 0) : (ConNF.Derivatives.pathTop_hom p h).toPath.comp (ConNF.Derivatives.pathTail p) = p

We can remove the first morphism from a path and compose it back to form the original path.

theorem ConNF.Derivatives.ExtendedIndex.pathTop_pathTail [ConNF.Params] {α : ConNF.Λ} (A : ConNF.ExtendedIndex ↑α) : ⋯.toPath.comp (ConNF.Derivatives.pathTail A) = A

theorem ConNF.Derivatives.cons_heq {V : Type u_2} [Quiver V] {x₁ : V} {x₂ : V} {y : V} {z : V} (p₁ : Quiver.Path x₁ y) (p₂ : Quiver.Path x₂ y) (hx : x₁ = x₂) (hp : HEq p₁ p₂) (e : y ⟶ z) : HEq (p₁.cons e) (p₂.cons e)

theorem ConNF.Derivatives.pathTail_comp {V : Type u_2} [Quiver V] {x : V} {y : V} {z : V} (f : x ⟶ y) (p : Quiver.Path y z) : HEq (ConNF.Derivatives.pathTail (f.toPath.comp p)) p

Adding and removing a morphism from the top of a path doesn't change anything.

instance ConNF.Derivatives.instLtLevelPathTopTypeIndex [ConNF.Params] [ConNF.Level] (A : ConNF.ExtendedIndex ↑ConNF.α) : ConNF.LtLevel (ConNF.Derivatives.pathTop A)

Equations

• ⋯ = ⋯

def ConNF.Derivatives.toStructPerm' [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (ρ : ConNF.Derivatives) : ConNF.StructPerm ↑ConNF.α

Convert a collection of derivatives to a structural permutation. To work out the A-derivative, we extract the first morphism in the path A and use it to determine which of the β-allowable permutations in ρ we will use.

Equations

• ρ.toStructPerm' A = ConNF.Allowable.toStructPerm (ρ (ConNF.Derivatives.pathTop A)) (ConNF.Derivatives.pathTail A)

def ConNF.Derivatives.toStructPerm [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : ConNF.Derivatives →* ConNF.StructPerm ↑ConNF.α

Convert a collection of derivatives to a structural permutation.

Equations

• ConNF.Derivatives.toStructPerm = { toFun := ConNF.Derivatives.toStructPerm', map_one' := ⋯, map_mul' := ⋯ }

theorem ConNF.Derivatives.toStructPerm_congr [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (ρ : ConNF.Derivatives) {β₁ : ConNF.TypeIndex} {β₂ : ConNF.TypeIndex} [ConNF.LtLevel β₁] [ConNF.LtLevel β₂] (hβ : β₁ = β₂) {A₁ : ConNF.ExtendedIndex β₁} {A₂ : ConNF.ExtendedIndex β₂} (hA : HEq A₁ A₂) : ConNF.Allowable.toStructPerm (ρ β₁) A₁ = ConNF.Allowable.toStructPerm (ρ β₂) A₂

theorem ConNF.Derivatives.toStructPerm'_injective [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : Function.Injective ConNF.Derivatives.toStructPerm'

theorem ConNF.Derivatives.toStructPerm_injective [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : Function.Injective ⇑ConNF.Derivatives.toStructPerm

theorem ConNF.Derivatives.comp_toPath_toStructPerm [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (ρ : ConNF.Derivatives) (β : ConNF.TypeIndex) [i : ConNF.LtLevel β] : ConNF.Tree.comp (Quiver.Hom.toPath ⋯) (ConNF.Derivatives.toStructPerm ρ) = ConNF.Allowable.toStructPerm (ρ β)

theorem ConNF.Derivatives.coe_apply_bot [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (ρ : ConNF.Derivatives) : ρ ⊥ = ConNF.Derivatives.toStructPerm ρ (Quiver.Hom.toPath ⋯)

instance ConNF.Derivatives.instMulAction [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] {X : Type u_1} [MulAction (ConNF.StructPerm ↑ConNF.α) X] : MulAction ConNF.Derivatives X

Equations

• ConNF.Derivatives.instMulAction = MulAction.compHom X ConNF.Derivatives.toStructPerm

@[simp]

theorem ConNF.Derivatives.toStructPerm_smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] {X : Type u_1} [MulAction (ConNF.StructPerm ↑ConNF.α) X] (ρ : ConNF.Derivatives) (x : X) : ρ • x = ConNF.Derivatives.toStructPerm ρ • x

instance ConNF.Derivatives.instMulActionCode [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : MulAction ConNF.Derivatives ConNF.Code

In the same way that structural permutations act on addresses, collections of derivatives act on codes.

Equations

• ConNF.Derivatives.instMulActionCode = MulAction.mk ⋯ ⋯

@[simp]

theorem ConNF.Derivatives.β_smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (ρ : ConNF.Derivatives) (c : ConNF.Code) : (ρ • c).β = c.β

@[simp]

theorem ConNF.Derivatives.members_smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (ρ : ConNF.Derivatives) (c : ConNF.Code) : (ρ • c).members = ρ c.β • c.members

@[simp]

theorem ConNF.Derivatives.smul_mk [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (f : ConNF.Derivatives) (γ : ConNF.TypeIndex) [ConNF.LtLevel γ] (s : Set (ConNF.TSet γ)) : f • ConNF.Code.mk γ s = ConNF.Code.mk γ (f γ • s)

instance ConNF.Derivatives.instSMulNonemptyCode [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : SMul ConNF.Derivatives ConNF.NonemptyCode

Equations

• ConNF.Derivatives.instSMulNonemptyCode = { smul := fun (ρ : ConNF.Derivatives) (c : ConNF.NonemptyCode) => ⟨ρ • ↑c, ⋯⟩ }

@[simp]

theorem ConNF.Derivatives.coe_smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (ρ : ConNF.Derivatives) (c : ConNF.NonemptyCode) : ↑(ρ • c) = ρ • ↑c

instance ConNF.Derivatives.instMulActionNonemptyCode [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : MulAction ConNF.Derivatives ConNF.NonemptyCode

Equations

• ConNF.Derivatives.instMulActionNonemptyCode = Function.Injective.mulAction (fun (a : { c : ConNF.Code // c.members.Nonempty }) => ↑a) ⋯ ⋯

def ConNF.Derivatives.IsAllowable [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] (ρ : ConNF.Derivatives) : Prop

We say that a collection of derivatives is allowable if its one-step derivatives commute with the fuzz maps.

Equations

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

theorem ConNF.isAllowable_one [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : ConNF.Derivatives.IsAllowable 1

theorem ConNF.isAllowable_inv [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] {ρ : ConNF.Derivatives} (h : ρ.IsAllowable) : ρ⁻¹.IsAllowable

theorem ConNF.isAllowable_mul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] {ρ : ConNF.Derivatives} {ρ' : ConNF.Derivatives} (h : ρ.IsAllowable) (h' : ρ'.IsAllowable) : (ρ * ρ').IsAllowable

theorem ConNF.isAllowable_div [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] {ρ : ConNF.Derivatives} {ρ' : ConNF.Derivatives} (h : ρ.IsAllowable) (h' : ρ'.IsAllowable) : (ρ / ρ').IsAllowable

theorem ConNF.isAllowable_pow [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] {ρ : ConNF.Derivatives} (h : ρ.IsAllowable) (n : ℕ) : (ρ ^ n).IsAllowable

theorem ConNF.isAllowable_zpow [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] {ρ : ConNF.Derivatives} (h : ρ.IsAllowable) (n : ℤ) : (ρ ^ n).IsAllowable

def ConNF.NewAllowable [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : Type u

An allowable permutation is a collection of derivatives that commutes with the fuzz maps.

Equations

• ConNF.NewAllowable = { ρ : ConNF.Derivatives // ρ.IsAllowable }

instance ConNF.NewAllowable.instCoeTCDerivatives [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : CoeTC ConNF.NewAllowable ConNF.Derivatives

Equations

• ConNF.NewAllowable.instCoeTCDerivatives = { coe := Subtype.val }

theorem ConNF.NewAllowable.coe_injective [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : Function.Injective Subtype.val

instance ConNF.NewAllowable.instOne [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : One ConNF.NewAllowable

Equations

• ConNF.NewAllowable.instOne = { one := ⟨1, ⋯⟩ }

instance ConNF.NewAllowable.instInv [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : Inv ConNF.NewAllowable

Equations

• ConNF.NewAllowable.instInv = { inv := fun (ρ : ConNF.NewAllowable) => ⟨(↑ρ)⁻¹, ⋯⟩ }

instance ConNF.NewAllowable.instMul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : Mul ConNF.NewAllowable

Equations

• ConNF.NewAllowable.instMul = { mul := fun (ρ ρ' : ConNF.NewAllowable) => ⟨↑ρ * ↑ρ', ⋯⟩ }

instance ConNF.NewAllowable.instDiv [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : Div ConNF.NewAllowable

Equations

• ConNF.NewAllowable.instDiv = { div := fun (ρ ρ' : ConNF.NewAllowable) => ⟨↑ρ / ↑ρ', ⋯⟩ }

instance ConNF.NewAllowable.instPowNat [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : Pow ConNF.NewAllowable ℕ

Equations

• ConNF.NewAllowable.instPowNat = { pow := fun (ρ : ConNF.NewAllowable) (n : ℕ) => ⟨↑ρ ^ n, ⋯⟩ }

instance ConNF.NewAllowable.instPowInt [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : Pow ConNF.NewAllowable ℤ

Equations

• ConNF.NewAllowable.instPowInt = { pow := fun (ρ : ConNF.NewAllowable) (n : ℤ) => ⟨↑ρ ^ n, ⋯⟩ }

@[simp]

theorem ConNF.NewAllowable.coe_one [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : ↑1 = 1

@[simp]

theorem ConNF.NewAllowable.coe_inv [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] (ρ : ConNF.NewAllowable) : ↑ρ⁻¹ = (↑ρ)⁻¹

@[simp]

theorem ConNF.NewAllowable.coe_mul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] (ρ : ConNF.NewAllowable) (ρ' : ConNF.NewAllowable) : ↑(ρ * ρ') = ↑ρ * ↑ρ'

@[simp]

theorem ConNF.NewAllowable.coe_div [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] (ρ : ConNF.NewAllowable) (ρ' : ConNF.NewAllowable) : ↑(ρ / ρ') = ↑ρ / ↑ρ'

@[simp]

theorem ConNF.NewAllowable.coe_pow [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] (ρ : ConNF.NewAllowable) (n : ℕ) : ↑(ρ ^ n) = ↑ρ ^ n

@[simp]

theorem ConNF.NewAllowable.coe_zpow [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] (ρ : ConNF.NewAllowable) (n : ℤ) : ↑(ρ ^ n) = ↑ρ ^ n

instance ConNF.NewAllowable.instGroup [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : Group ConNF.NewAllowable

Equations

• ConNF.NewAllowable.instGroup = Function.Injective.group Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem ConNF.NewAllowable.coeHom_apply [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] (self : { ρ : ConNF.Derivatives // ρ.IsAllowable }) : ConNF.NewAllowable.coeHom self = ↑self

def ConNF.NewAllowable.coeHom [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : ConNF.NewAllowable →* ConNF.Derivatives

The coercion from allowable permutations to their derivatives as a monoid homomorphism.

Equations

• ConNF.NewAllowable.coeHom = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }

def ConNF.NewAllowable.toStructPerm [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : ConNF.NewAllowable →* ConNF.StructPerm ↑ConNF.α

Turn an allowable permutation into a structural permutation.

Equations

• ConNF.NewAllowable.toStructPerm = ConNF.Derivatives.toStructPerm.comp ConNF.NewAllowable.coeHom

theorem ConNF.NewAllowable.toStructPerm_injective [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] : Function.Injective ⇑ConNF.NewAllowable.toStructPerm

theorem ConNF.NewAllowable.comp_toPath_toStructPerm [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] (ρ : ConNF.NewAllowable) (β : ConNF.TypeIndex) [i : ConNF.LtLevel β] : ConNF.Tree.comp (Quiver.Hom.toPath ⋯) (ConNF.NewAllowable.toStructPerm ρ) = ConNF.Allowable.toStructPerm (↑ρ β)

instance ConNF.NewAllowable.instMulAction [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] {X : Type u_1} [MulAction ConNF.Derivatives X] : MulAction ConNF.NewAllowable X

Equations

• ConNF.NewAllowable.instMulAction = MulAction.compHom X ConNF.NewAllowable.coeHom

@[simp]

theorem ConNF.NewAllowable.coe_smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] {X : Type u_1} [MulAction ConNF.Derivatives X] (ρ : ConNF.NewAllowable) (x : X) : ↑ρ • x = ρ • x

@[simp]

theorem ConNF.NewAllowable.smul_typedNearLitter [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (γ : ConNF.Λ) [ConNF.LtLevel ↑γ] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (ρ : ConNF.NewAllowable) (N : ConNF.NearLitter) : ↑ρ ↑γ • ConNF.typedNearLitter N = ConNF.typedNearLitter (ConNF.Allowable.toStructPerm (↑ρ ↑γ) (Quiver.Hom.toPath ⋯) • N)

@[simp]

theorem ConNF.NewAllowable.β_smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] (ρ : ConNF.NewAllowable) (c : ConNF.Code) : (ρ • c).β = c.β

@[simp]

theorem ConNF.NewAllowable.members_smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] (ρ : ConNF.NewAllowable) (c : ConNF.Code) : (ρ • c).members = ↑ρ c.β • c.members

@[simp]

theorem ConNF.NewAllowable.smul_mk [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] (ρ : ConNF.NewAllowable) (γ : ConNF.TypeIndex) [ConNF.LtLevel γ] (s : Set (ConNF.TSet γ)) : ρ • ConNF.Code.mk γ s = ConNF.Code.mk γ (↑ρ γ • s)

theorem ConNF.NewAllowable.smul_cloud [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] {β : ConNF.TypeIndex} [ConNF.LtLevel β] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (ρ : ConNF.NewAllowable) (s : Set (ConNF.TSet β)) (hβγ : β ≠ ↑γ) : ↑ρ ↑γ • ConNF.cloud hβγ s = ConNF.cloud hβγ (↑ρ β • s)

Allowable permutations commute with the cloud map.

theorem ConNF.NewAllowable.smul_cloudCode [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {c : ConNF.Code} (ρ : ConNF.NewAllowable) (hc : c.β ≠ ↑γ) : ρ • ConNF.cloudCode γ c = ConNF.cloudCode γ (ρ • c)

Allowable permutations commute with the cloudCode map.

theorem ConNF.CloudRel.smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {ρ : ConNF.NewAllowable} {c : ConNF.Code} {d : ConNF.Code} : c ↝₀ d → ρ • c ↝₀ ρ • d

@[simp]

theorem ConNF.smul_cloudRel [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {ρ : ConNF.NewAllowable} {c : ConNF.Code} {d : ConNF.Code} : ρ • c ↝₀ ρ • d ↔ c ↝₀ d

@[irreducible]

theorem ConNF.Code.isEven_smul_nonempty [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {ρ : ConNF.NewAllowable} (c : ConNF.NonemptyCode) : (ρ • ↑c).IsEven ↔ (↑c).IsEven

@[simp]

theorem ConNF.Code.isEven_smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {ρ : ConNF.NewAllowable} {c : ConNF.Code} : (ρ • c).IsEven ↔ c.IsEven

@[simp]

theorem ConNF.Code.isOdd_smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {ρ : ConNF.NewAllowable} {c : ConNF.Code} : (ρ • c).IsOdd ↔ c.IsOdd

theorem ConNF.Code.isEven.smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {ρ : ConNF.NewAllowable} {c : ConNF.Code} : c.IsEven → (ρ • c).IsEven

Alias of the reverse direction of ConNF.Code.isEven_smul.

theorem ConNF.Code.isOdd.smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {ρ : ConNF.NewAllowable} {c : ConNF.Code} : c.IsOdd → (ρ • c).IsOdd

Alias of the reverse direction of ConNF.Code.isOdd_smul.

theorem ConNF.Code.Equiv.smul [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {ρ : ConNF.NewAllowable} {c : ConNF.Code} {d : ConNF.Code} : c ≡ d → ρ • c ≡ ρ • d

theorem ConNF.Code.smul_code [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] [ConNF.BasePositions] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {ρ : ConNF.NewAllowable} {c : ConNF.Code} {d : ConNF.Code} : ρ • c ≡ ρ • d ↔ c ≡ d

Allowable permutations preserve code equivalence.