Coding functions

structure ConNF.CodingFunction [ConNF.Params] (β : ConNF.Λ) [ConNF.ModelData ↑β] : Type u

• decode : ConNF.Support ↑β →. ConNF.TSet ↑β
• dom_nonempty : self.decode.Dom.Nonempty
• supports_decode' : ∀ (S : ConNF.Support ↑β) (hS : (self.decode S).Dom), MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier S) ((self.decode S).get hS)
• dom_iff : ∀ (S T : ConNF.Support ↑β), (self.decode S).Dom → ((self.decode T).Dom ↔ ∃ (ρ : ConNF.Allowable ↑β), T = ρ • S)
• decode_smul' : ∀ (S : ConNF.Support ↑β) (ρ : ConNF.Allowable ↑β) (h₁ : (self.decode S).Dom) (h₂ : (self.decode (ρ • S)).Dom), (self.decode (ρ • S)).get h₂ = ρ • (self.decode S).get h₁

theorem ConNF.CodingFunction.dom_nonempty [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (self : ConNF.CodingFunction β) : self.decode.Dom.Nonempty

theorem ConNF.CodingFunction.supports_decode' [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (self : ConNF.CodingFunction β) (S : ConNF.Support ↑β) (hS : (self.decode S).Dom) : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier S) ((self.decode S).get hS)

theorem ConNF.CodingFunction.dom_iff [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (self : ConNF.CodingFunction β) (S : ConNF.Support ↑β) (T : ConNF.Support ↑β) (hS : (self.decode S).Dom) : (self.decode T).Dom ↔ ∃ (ρ : ConNF.Allowable ↑β), T = ρ • S

theorem ConNF.CodingFunction.decode_smul' [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (self : ConNF.CodingFunction β) (S : ConNF.Support ↑β) (ρ : ConNF.Allowable ↑β) (h₁ : (self.decode S).Dom) (h₂ : (self.decode (ρ • S)).Dom) : (self.decode (ρ • S)).get h₂ = ρ • (self.decode S).get h₁

instance ConNF.CodingFunction.instMembershipSupportSomeΛ [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] : Membership (ConNF.Support ↑β) (ConNF.CodingFunction β)

Equations

• ConNF.CodingFunction.instMembershipSupportSomeΛ = { mem := fun (S : ConNF.Support ↑β) (χ : ConNF.CodingFunction β) => (χ.decode S).Dom }

theorem ConNF.CodingFunction.mem_iff [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {χ : ConNF.CodingFunction β} {S : ConNF.Support ↑β} : S ∈ χ ↔ (χ.decode S).Dom

theorem ConNF.CodingFunction.mem_iff_of_mem [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {χ : ConNF.CodingFunction β} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} (h : S ∈ χ) : T ∈ χ ↔ ∃ (ρ : ConNF.Allowable ↑β), T = ρ • S

theorem ConNF.CodingFunction.smul_mem [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {χ : ConNF.CodingFunction β} {S : ConNF.Support ↑β} (ρ : ConNF.Allowable ↑β) (h : S ∈ χ) : ρ • S ∈ χ

theorem ConNF.CodingFunction.mem_of_smul_mem [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {χ : ConNF.CodingFunction β} {S : ConNF.Support ↑β} {ρ : ConNF.Allowable ↑β} (h : ρ • S ∈ χ) : S ∈ χ

theorem ConNF.CodingFunction.exists_mem [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (χ : ConNF.CodingFunction β) : ∃ (S : ConNF.Support ↑β), S ∈ χ

theorem ConNF.CodingFunction.supports_decode [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {χ : ConNF.CodingFunction β} (S : ConNF.Support ↑β) (hS : S ∈ χ) : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier S) ((χ.decode S).get hS)

theorem ConNF.CodingFunction.decode_smul [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {χ : ConNF.CodingFunction β} (S : ConNF.Support ↑β) (ρ : ConNF.Allowable ↑β) (h : ρ • S ∈ χ) : (χ.decode (ρ • S)).get h = ρ • (χ.decode S).get ⋯

theorem ConNF.CodingFunction.ext [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {χ₁ : ConNF.CodingFunction β} {χ₂ : ConNF.CodingFunction β} (S : ConNF.Support ↑β) (h₁ : S ∈ χ₁) (h₂ : S ∈ χ₂) (h : (χ₁.decode S).get h₁ = (χ₂.decode S).get h₂) : χ₁ = χ₂

Two coding functions are equal if they decode a single ordered support to the same tangle.

theorem ConNF.CodingFunction.smul_supports [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {S : ConNF.Support ↑β} {t : ConNF.TSet ↑β} (h : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier S) t) (ρ : ConNF.Allowable ↑β) : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier (ρ • S)) (ρ • t)

theorem ConNF.CodingFunction.decode_congr [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {χ : ConNF.CodingFunction β} {S₁ : ConNF.Support ↑β} {S₂ : ConNF.Support ↑β} {h₁ : S₁ ∈ χ} {h₂ : S₂ ∈ χ} (h : S₁ = S₂) : (χ.decode S₁).get h₁ = (χ.decode S₂).get h₂

noncomputable def ConNF.CodingFunction.code [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (S : ConNF.Support ↑β) (t : ConNF.TSet ↑β) (h : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier S) t) : ConNF.CodingFunction β

Produce a coding function for a given ordered support and tangle it supports.

Equations

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

@[simp]

theorem ConNF.CodingFunction.code_decode [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (S : ConNF.Support ↑β) (t : ConNF.TSet ↑β) (h : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier S) t) : (ConNF.CodingFunction.code S t h).decode S = Part.some t

@[simp]

theorem ConNF.CodingFunction.mem_code_self [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {S : ConNF.Support ↑β} {t : ConNF.TSet ↑β} {h : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier S) t} : S ∈ ConNF.CodingFunction.code S t h

@[simp]

theorem ConNF.CodingFunction.mem_code [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {S : ConNF.Support ↑β} {t : ConNF.TSet ↑β} {h : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier S) t} (T : ConNF.Support ↑β) : T ∈ ConNF.CodingFunction.code S t h ↔ ∃ (ρ : ConNF.Allowable ↑β), T = ρ • S

theorem ConNF.CodingFunction.eq_code [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] {χ : ConNF.CodingFunction β} {S : ConNF.Support ↑β} (h : S ∈ χ) : χ = ConNF.CodingFunction.code S ((χ.decode S).get h) ⋯

Every coding function can be obtained by invoking code with an ordered support in its domain.

theorem ConNF.CodingFunction.code_smul [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (S : ConNF.Support ↑β) (t : ConNF.TSet ↑β) (ρ : ConNF.Allowable ↑β) (h₁ : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier (ρ • S)) (ρ • t)) (h₂ : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier S) t) : ConNF.CodingFunction.code (ρ • S) (ρ • t) h₁ = ConNF.CodingFunction.code S t h₂

@[simp]

theorem ConNF.CodingFunction.code_eq_code_iff [ConNF.Params] {β : ConNF.Λ} [ConNF.ModelData ↑β] (S : ConNF.Support ↑β) (S' : ConNF.Support ↑β) (t : ConNF.TSet ↑β) (t' : ConNF.TSet ↑β) (h : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier S) t) (h' : MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier S') t') : ConNF.CodingFunction.code S t h = ConNF.CodingFunction.code S' t' h' ↔ ∃ (ρ : ConNF.Allowable ↑β), S' = ρ • S ∧ t' = ρ • t