Coding functions

In this file, we define coding functions.

Main declarations

• ConNF.CodingFunction: The type of coding functions.

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

• S.orbit = ⟦S⟧

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

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

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

@[simp]

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

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

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

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

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

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

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

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

Equations

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

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

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

@[simp]

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