Raising supports to higher levels #
def
ConNF.raiseIndex
[ConNF.Params]
{β : ConNF.Λ}
{γ : ConNF.Λ}
(hγ : ↑γ < ↑β)
(A : ConNF.ExtendedIndex ↑γ)
:
Equations
- ConNF.raiseIndex hγ A = (Quiver.Hom.toPath hγ).comp A
Instances For
Equations
- ConNF.raise hγ c = { path := ConNF.raiseIndex hγ c.path, value := c.value }
Instances For
@[simp]
theorem
ConNF.raise_path
[ConNF.Params]
{β : ConNF.Λ}
{γ : ConNF.Λ}
(hγ : ↑γ < ↑β)
(c : ConNF.Address ↑γ)
:
(ConNF.raise hγ c).path = ConNF.raiseIndex hγ c.path
@[simp]
theorem
ConNF.raise_value
[ConNF.Params]
{β : ConNF.Λ}
{γ : ConNF.Λ}
(hγ : ↑γ < ↑β)
(c : ConNF.Address ↑γ)
:
(ConNF.raise hγ c).value = c.value
theorem
ConNF.raiseIndex_injective
[ConNF.Params]
{β : ConNF.Λ}
{γ : ConNF.Λ}
(hγ : ↑γ < ↑β)
{A : ConNF.ExtendedIndex ↑γ}
{B : ConNF.ExtendedIndex ↑γ}
(h : ConNF.raiseIndex hγ A = ConNF.raiseIndex hγ B)
:
A = B
theorem
Quiver.Path.comp_injective'
{V : Type u_1}
[Quiver V]
{a : V}
{b : V}
{c : V}
{d : V}
{p₁ : Quiver.Path a b}
{p₂ : Quiver.Path a c}
{q₁ : Quiver.Path b d}
{q₂ : Quiver.Path c d}
(h₁ : p₁.length = p₂.length)
(h₂ : p₁.comp q₁ = p₂.comp q₂)
:
b = c
theorem
ConNF.raiseIndex_index_injective
[ConNF.Params]
{β : ConNF.Λ}
{γ : ConNF.Λ}
{δ : ConNF.Λ}
(hγ : ↑γ < ↑β)
(hδ : ↑δ < ↑β)
{A : ConNF.ExtendedIndex ↑γ}
{B : ConNF.ExtendedIndex ↑δ}
(h : ConNF.raiseIndex hγ A = ConNF.raiseIndex hδ B)
:
γ = δ
theorem
ConNF.raise_injective
[ConNF.Params]
{β : ConNF.Λ}
{γ : ConNF.Λ}
(hγ : ↑γ < ↑β)
{c : ConNF.Address ↑γ}
{d : ConNF.Address ↑γ}
(h : ConNF.raise hγ c = ConNF.raise hγ d)
:
c = d
theorem
ConNF.smul_raise_eq_iff
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(c : ConNF.Address ↑γ)
(ρ : ConNF.Allowable ↑β)
:
ρ • ConNF.raise hγ c = ConNF.raise hγ c ↔ (ConNF.Allowable.comp (Quiver.Hom.toPath hγ)) ρ • c = c
def
ConNF.Appears
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
(hγ : ↑γ < ↑β)
(s : Set (ConNF.StructSet ↑γ))
:
A set s of γ-structSets appears at level α if it occurs as the γ-extension of some
α-tangle.
Equations
- ConNF.Appears hγ s = ∃ (t : ConNF.TSet ↑β), s = ConNF.StructSet.ofCoe (ConNF.toStructSet t) (↑γ) hγ
Instances For
def
ConNF.AppearsRaised
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
(hγ : ↑γ < ↑β)
(χs : Set (ConNF.CodingFunction β))
(U : ConNF.Support ↑β)
:
Equations
- ConNF.AppearsRaised hγ χs U = ConNF.Appears hγ {u : ConNF.StructSet ↑γ | ∃ χ ∈ χs, ∃ V ≥ U, ∃ (hV : V ∈ χ), u ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet ((χ.decode V).get hV)) (↑γ) hγ}
Instances For
noncomputable def
ConNF.decodeRaised
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
(hγ : ↑γ < ↑β)
(χs : Set (ConNF.CodingFunction β))
(U : ConNF.Support ↑β)
(hU : ConNF.AppearsRaised hγ χs U)
:
ConNF.TSet ↑β
Equations
- ConNF.decodeRaised hγ χs U hU = Exists.choose hU
Instances For
We now aim to show that decodeRaised is a coding function.
theorem
ConNF.decodeRaised_spec
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
(hγ : ↑γ < ↑β)
(χs : Set (ConNF.CodingFunction β))
(U : ConNF.Support ↑β)
(hU : ConNF.AppearsRaised hγ χs U)
:
ConNF.StructSet.ofCoe (ConNF.toStructSet (ConNF.decodeRaised hγ χs U hU)) (↑γ) hγ = {u : ConNF.StructSet ↑γ |
∃ χ ∈ χs, ∃ V ≥ U, ∃ (hV : V ∈ χ), u ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet ((χ.decode V).get hV)) (↑γ) hγ}
theorem
ConNF.appearsRaised_smul
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
(hγ : ↑γ < ↑β)
{χs : Set (ConNF.CodingFunction β)}
(U : ConNF.Support ↑β)
(hU : ConNF.AppearsRaised hγ χs U)
(ρ : ConNF.Allowable ↑β)
:
ConNF.AppearsRaised hγ χs (ρ • U)
theorem
ConNF.decodeRaised_smul
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
{χs : Set (ConNF.CodingFunction β)}
(U : ConNF.Support ↑β)
(hU : ConNF.AppearsRaised hγ χs U)
(ρ : ConNF.Allowable ↑β)
:
ConNF.decodeRaised hγ χs (ρ • U) ⋯ = ρ • ConNF.decodeRaised hγ χs U hU
def
ConNF.tangleExtension
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(t : ConNF.TSet ↑β)
:
Set (ConNF.TSet ↑γ)
The tangles in the γ-extension of a given β-tangle.
Equations
- ConNF.tangleExtension hγ t = {u : ConNF.TSet ↑γ | ConNF.toStructSet u ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet t) (↑γ) hγ}
Instances For
noncomputable def
ConNF.raisedSupport
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(u : ConNF.TSet ↑γ)
:
A support for a γ-tangle, expressed as a set of β-support conditions.
Equations
- ConNF.raisedSupport hγ S u = S + ConNF.Enumeration.image u.support (ConNF.raise hγ)
Instances For
theorem
ConNF.le_raisedSupport
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(u : ConNF.TSet ↑γ)
:
S ≤ ConNF.raisedSupport hγ S u
theorem
ConNF.raisedSupport_supports
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(u : ConNF.TSet ↑γ)
:
MulAction.Supports (ConNF.Allowable ↑β) (ConNF.Enumeration.carrier (ConNF.raisedSupport hγ S u))
(ConNF.singleton β γ hγ u)
noncomputable def
ConNF.raiseSingleton
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(u : ConNF.TSet ↑γ)
:
Equations
- ConNF.raiseSingleton hγ S u = ConNF.CodingFunction.code (ConNF.raisedSupport hγ S u) (ConNF.singleton β γ hγ u) ⋯
Instances For
def
ConNF.RaisedSingleton
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
:
Type u
Equations
- ConNF.RaisedSingleton hγ = { χ : ConNF.CodingFunction β // ∃ (S : ConNF.Support ↑β) (u : ConNF.TSet ↑γ), χ = ConNF.raiseSingleton hγ S u }
Instances For
theorem
ConNF.smul_raise_eq
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(ρ : ConNF.Allowable ↑β)
(c : ConNF.Address ↑γ)
:
ρ • ConNF.raise hγ c = ConNF.raise hγ ((ConNF.Allowable.comp (Quiver.Hom.toPath hγ)) ρ • c)
theorem
ConNF.smul_image_raise_eq
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(ρ : ConNF.Allowable ↑β)
(T : ConNF.Support ↑γ)
:
ρ • ConNF.Enumeration.image T (ConNF.raise hγ) = ConNF.Enumeration.image ((ConNF.Allowable.comp (Quiver.Hom.toPath hγ)) ρ • T) (ConNF.raise hγ)
def
ConNF.raiseSingletons
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(t : ConNF.TSet ↑β)
:
Take the γ-extension of t, treated as a set of α-level singletons, and turn them into
coding functions.
Equations
- ConNF.raiseSingletons hγ S t = ConNF.raiseSingleton hγ S '' ConNF.tangleExtension hγ t
Instances For
theorem
ConNF.raiseSingletons_subset_range
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
{S : ConNF.Support ↑β}
{t : ConNF.TSet ↑β}
:
ConNF.raiseSingletons hγ S t ⊆ Set.range Subtype.val
theorem
ConNF.smul_reducedSupport_eq
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(v : ConNF.TSet ↑γ)
(ρ : ConNF.Allowable ↑β)
(hUV : S ≤ ρ • ConNF.raisedSupport hγ S v)
(c : ConNF.Address ↑β)
(hc : c ∈ S)
:
theorem
ConNF.raiseSingletons_reducedSupport
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(t : ConNF.TSet ↑β)
(hSt : MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ S} t)
:
{u : ConNF.StructSet ↑γ |
∃ χ ∈ ConNF.raiseSingletons hγ S t,
∃ V ≥ S, ∃ (hV : V ∈ χ), u ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet ((χ.decode V).get hV)) (↑γ) hγ} = ConNF.StructSet.ofCoe (ConNF.toStructSet t) (↑γ) hγ
theorem
ConNF.appearsRaised_raiseSingletons
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(t : ConNF.TSet ↑β)
(hSt : MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ S} t)
:
ConNF.AppearsRaised hγ (ConNF.raiseSingletons hγ S t) S
theorem
ConNF.decodeRaised_raiseSingletons
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(t : ConNF.TSet ↑β)
(hSt : MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ S} t)
:
ConNF.decodeRaised hγ (ConNF.raiseSingletons hγ S t) S ⋯ = t
noncomputable def
ConNF.raisedCodingFunction
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(χs : Set (ConNF.CodingFunction β))
(o : ConNF.SupportOrbit β)
(ho : ∀ U ∈ o, ConNF.AppearsRaised hγ χs U)
(ho' : ∀ (U : ConNF.Support ↑β) (hU : U ∈ o),
MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ U} (ConNF.decodeRaised hγ χs U ⋯))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ConNF.decode_raisedCodingFunction
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(χs : Set (ConNF.CodingFunction β))
(o : ConNF.SupportOrbit β)
(ho : ∀ U ∈ o, ConNF.AppearsRaised hγ χs U)
(ho' : ∀ (U : ConNF.Support ↑β) (hU : U ∈ o),
MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ U} (ConNF.decodeRaised hγ χs U ⋯))
(U : ConNF.Support ↑β)
(hU : U ∈ ConNF.raisedCodingFunction hγ χs o ho ho')
:
((ConNF.raisedCodingFunction hγ χs o ho ho').decode U).get hU = ConNF.decodeRaised hγ χs U ⋯
theorem
ConNF.mem_raisedCodingFunction_iff
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(χs : Set (ConNF.CodingFunction β))
(o : ConNF.SupportOrbit β)
(ho : ∀ U ∈ o, ConNF.AppearsRaised hγ χs U)
(ho' : ∀ (U : ConNF.Support ↑β) (hU : U ∈ o),
MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ U} (ConNF.decodeRaised hγ χs U ⋯))
(U : ConNF.Support ↑β)
:
U ∈ ConNF.raisedCodingFunction hγ χs o ho ho' ↔ U ∈ o
theorem
ConNF.appearsRaised_of_mem_orbit
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(t : ConNF.TSet ↑β)
(hSt : MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ S} t)
(U : ConNF.Support ↑β)
(hU : U ∈ ConNF.SupportOrbit.mk S)
:
ConNF.AppearsRaised hγ (ConNF.raiseSingletons hγ S t) U
theorem
ConNF.supports_decodeRaised_of_mem_orbit
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(t : ConNF.TSet ↑β)
(hSt : MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ S} t)
(U : ConNF.Support ↑β)
(hU : U ∈ ConNF.SupportOrbit.mk S)
:
MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ U}
(ConNF.decodeRaised hγ (ConNF.raiseSingletons hγ S t) U ⋯)
noncomputable def
ConNF.recode
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(t : ConNF.TSet ↑β)
(hSt : MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ S} t)
:
Converts a tangle to a coding class by going via raisedCodingFunction γ.
Equations
- ConNF.recode hγ S t hSt = ConNF.raisedCodingFunction hγ (ConNF.raiseSingletons hγ S t) (ConNF.SupportOrbit.mk S) ⋯ ⋯
Instances For
theorem
ConNF.decode_recode
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(t : ConNF.TSet ↑β)
(hSt : MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ S} t)
:
((ConNF.recode hγ S t hSt).decode S).get ⋯ = t
theorem
ConNF.recode_eq
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑β)
(t : ConNF.TSet ↑β)
(hSt : MulAction.Supports (ConNF.Allowable ↑β) {c : ConNF.Address ↑β | c ∈ S} t)
:
ConNF.recode hγ S t hSt = ConNF.CodingFunction.code S t hSt
The recode function yields the original coding function on t.