Coding functions

def ConNF.ModelData.TSet.Orbit [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] (β : ConNF.Λ) [ConNF.LeLevel ↑β] : Type u

Equations

• ConNF.ModelData.TSet.Orbit β = MulAction.orbitRel.Quotient (ConNF.Allowable ↑β) (ConNF.TSet ↑β)

def ConNF.ModelData.TSet.Orbit.mk [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) : ConNF.ModelData.TSet.Orbit β

Equations

• ConNF.ModelData.TSet.Orbit.mk s = ⟦s⟧

theorem ConNF.ModelData.TSet.Orbit.eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {s₁ : ConNF.TSet ↑β} {s₂ : ConNF.TSet ↑β} : ConNF.ModelData.TSet.Orbit.mk s₁ = ConNF.ModelData.TSet.Orbit.mk s₂ ↔ s₁ ∈ MulAction.orbit (ConNF.Allowable ↑β) s₂

theorem ConNF.ModelData.TSet.Orbit.mk_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) (ρ : ConNF.Allowable ↑β) : ConNF.ModelData.TSet.Orbit.mk (ρ • s) = ConNF.ModelData.TSet.Orbit.mk s

theorem ConNF.ModelData.TSet.Orbit.has_repr [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (o : ConNF.ModelData.TSet.Orbit β) : ∃ (t : ConNF.Tangle ↑β), o = ConNF.ModelData.TSet.Orbit.mk t.set

noncomputable def ConNF.ModelData.TSet.Orbit.repr [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (o : ConNF.ModelData.TSet.Orbit β) : ConNF.Tangle ↑β

Equations

• o.repr = ⋯.choose

theorem ConNF.ModelData.TSet.Orbit.repr_spec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (o : ConNF.ModelData.TSet.Orbit β) : o = ConNF.ModelData.TSet.Orbit.mk o.repr.set

theorem ConNF.ModelData.TSet.has_twist [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) : ∃ (ρ : ConNF.Allowable ↑β), ρ • (ConNF.ModelData.TSet.Orbit.mk s).repr.set = s

noncomputable def ConNF.ModelData.TSet.twist [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) : ConNF.Allowable ↑β

An allowable permutation that turns the representing tangle into s.

Equations

• s.twist = ⋯.choose

theorem ConNF.ModelData.TSet.eq_twist_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) : s.twist • (ConNF.ModelData.TSet.Orbit.mk s).repr.set = s

theorem ConNF.ModelData.TSet.twist_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) (ρ : ConNF.Allowable ↑β) : ρ • s = (ρ • s).twist • s.twist⁻¹ • s

noncomputable def ConNF.ModelData.TSet.out [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) : ConNF.Tangle ↑β

A canonical tangle chosen for this TSet.

Equations

• s.out = s.twist • (ConNF.ModelData.TSet.Orbit.mk s).repr

theorem ConNF.ModelData.TSet.eq_set_out [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) : s = s.out.set

theorem ConNF.ModelData.TSet.out_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s₁ : ConNF.TSet ↑β) (s₂ : ConNF.TSet ↑β) (h : s₁.out = s₂.out) : s₁ = s₂

noncomputable def ConNF.ModelData.TSet.support [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) : ConNF.Support ↑β

Equations

• s.support = s.twist • (ConNF.ModelData.TSet.Orbit.mk s).repr.support

theorem ConNF.ModelData.TSet.support_supports [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier s.support) s

theorem ConNF.ModelData.TSet.smul_support_max [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) (ρ : ConNF.Allowable ↑β) : (ρ • s).support.max = s.support.max

theorem ConNF.ModelData.TSet.smul_support [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (s : ConNF.TSet ↑β) (ρ : ConNF.Allowable ↑β) : (ρ • s).support = (ρ • s).twist • s.twist⁻¹ • s.support