Coding functions

In this file, we define coding functions.

Main declarations

• ConNF.CodingFunction: The type of coding functions.

def ConNF.Support.orbitRel [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] : Rel (ConNF.Support β) (ConNF.Support β)

Equations

• S.orbitRel T = ∃ (ρ : ConNF.AllPerm β), ρᵁ • S = T

theorem ConNF.Support.orbitRel_isEquivalence [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] : Equivalence ConNF.Support.orbitRel

instance ConNF.Support.setoid [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] : Setoid (ConNF.Support β)

Equations

• ConNF.Support.setoid β = { r := ConNF.Support.orbitRel, iseqv := ⋯ }

def ConNF.SupportOrbit [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] : Type u

Equations

• ConNF.SupportOrbit β = Quotient (ConNF.Support.setoid β)

def ConNF.Support.orbit [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (S : ConNF.Support β) : ConNF.SupportOrbit β

Equations

• S.orbit = ⟦S⟧

theorem ConNF.SupportOrbit.out_orbit [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (o : ConNF.SupportOrbit β) : (Quotient.out o).orbit = o

theorem ConNF.SupportOrbit.exists_support [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (o : ConNF.SupportOrbit β) : ∃ (S : ConNF.Support β), S.orbit = o

theorem ConNF.Support.orbit_eq_iff [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {S T : ConNF.Support β} : S.orbit = T.orbit ↔ ∃ (ρ : ConNF.AllPerm β), ρᵁ • S = T

@[simp]

theorem ConNF.Support.smul_orbit [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {S : ConNF.Support β} {ρ : ConNF.AllPerm β} : (ρᵁ • S).orbit = S.orbit

structure ConNF.CodingFunction [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] : Type u

• rel : Rel (ConNF.Support β) (ConNF.TSet β)
• rel_coinjective : self.rel.Coinjective
• rel_dom_nonempty : self.rel.dom.Nonempty
• supports_of_rel : ∀ {S : ConNF.Support β} {x : ConNF.TSet β}, self.rel S x → S.Supports x
• orbit_eq_of_mem_dom : ∀ {S T : ConNF.Support β}, S ∈ self.rel.dom → T ∈ self.rel.dom → S.orbit = T.orbit
• smul_rel : ∀ {S : ConNF.Support β} {x : ConNF.TSet β}, self.rel S x → ∀ (ρ : ConNF.AllPerm β), self.rel (ρᵁ • S) (ρ • x)

theorem ConNF.CodingFunction.ext' [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {χ₁ χ₂ : ConNF.CodingFunction β} (h : ∀ (S : ConNF.Support β) (x : ConNF.TSet β), χ₁.rel S x ↔ χ₂.rel S x) : χ₁ = χ₂

theorem ConNF.CodingFunction.ext_aux [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {χ₁ χ₂ : ConNF.CodingFunction β} {S : ConNF.Support β} {x : ConNF.TSet β} (h₁ : χ₁.rel S x) (h₂ : χ₂.rel S x) : χ₁.rel ≤ χ₂.rel

theorem ConNF.CodingFunction.ext [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {χ₁ χ₂ : ConNF.CodingFunction β} (S : ConNF.Support β) (x : ConNF.TSet β) (h₁ : χ₁.rel S x) (h₂ : χ₂.rel S x) : χ₁ = χ₂

theorem ConNF.CodingFunction.exists_allPerm_of_rel [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {χ : ConNF.CodingFunction β} {S T : ConNF.Support β} {x y : ConNF.TSet β} (h₁ : χ.rel S x) (h₂ : χ.rel T y) : ∃ (ρ : ConNF.AllPerm β), ρᵁ • S = T ∧ ρ • x = y

def ConNF.Tangle.code [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (t : ConNF.Tangle β) : ConNF.CodingFunction β

Equations

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

theorem ConNF.Tangle.code_rel_self [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (t : ConNF.Tangle β) : t.code.rel t.support t.set

theorem ConNF.Tangle.code_eq_code_iff [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (t₁ t₂ : ConNF.Tangle β) : t₁.code = t₂.code ↔ ∃ (ρ : ConNF.AllPerm β), ρ • t₁ = t₂

@[simp]

theorem ConNF.Tangle.smul_code [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (t : ConNF.Tangle β) (ρ : ConNF.AllPerm β) : (ρ • t).code = t.code