Hypotheses for constructing tangles

In this file we state the conditions required to generate the fuzz maps at all levels below a given proper type index α : Λ. Using these inductive hypotheses we can build the t-sets and allowable permutations at level α. However, with such weak hypotheses (in particular, the lack of any coherence between type levels) we cannot prove many facts about these new types.

Main declarations

• ConNF.ModelDataLt: The ModelData for each β < α.
• ConNF.PositionedTanglesLt: The PositionedTangles for each β < α.
• ConNF.TypedObjectsLt: The TypedObjects for each β < α.
• ConNF.PositionedObjectsLt: The PositionedObjects for each β < α.

theorem ConNF.ModelDataLt.ext_iff : ∀ {inst : ConNF.Params} {inst_1 : ConNF.Level} (x y : ConNF.ModelDataLt), x = y ↔ ConNF.ModelDataLt.data = ConNF.ModelDataLt.data

theorem ConNF.ModelDataLt.ext : ∀ {inst : ConNF.Params} {inst_1 : ConNF.Level} (x y : ConNF.ModelDataLt), ConNF.ModelDataLt.data = ConNF.ModelDataLt.data → x = y

class ConNF.ModelDataLt [ConNF.Params] [ConNF.Level] : Type (u + 1)

The ModelData for each β < α.

• data : (β : ConNF.Λ) → [inst : ConNF.LtLevel ↑β] → ConNF.ModelData ↑β

instance ConNF.ModelDataLt.toModelData [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (β : ConNF.TypeIndex) [ConNF.LtLevel β] : ConNF.ModelData β

Equations

• ConNF.ModelDataLt.toModelData x✝ = match x✝, x with | none, x => ConNF.Bot.modelData | some β, x => ConNF.ModelDataLt.data β

theorem ConNF.PositionedTanglesLt.ext : ∀ {inst : ConNF.Params} {inst_1 : ConNF.Level} {inst_2 : ConNF.ModelDataLt} (x y : ConNF.PositionedTanglesLt), ConNF.PositionedTanglesLt.data = ConNF.PositionedTanglesLt.data → x = y

theorem ConNF.PositionedTanglesLt.ext_iff : ∀ {inst : ConNF.Params} {inst_1 : ConNF.Level} {inst_2 : ConNF.ModelDataLt} (x y : ConNF.PositionedTanglesLt), x = y ↔ ConNF.PositionedTanglesLt.data = ConNF.PositionedTanglesLt.data

class ConNF.PositionedTanglesLt [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : Type u

The PositionedTangles for each β < α.

• data : (β : ConNF.Λ) → [inst : ConNF.LtLevel ↑β] → ConNF.PositionedTangles ↑β

noncomputable instance ConNF.PositionedTanglesLt.toPositionedTangles [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] (β : ConNF.TypeIndex) [ConNF.LtLevel β] : ConNF.PositionedTangles β

Equations

• ConNF.PositionedTanglesLt.toPositionedTangles x✝ = match x✝, x with | none, x => ConNF.Bot.positionedTangles | some β, x => ConNF.PositionedTanglesLt.data β

@[reducible, inline]

abbrev ConNF.TypedObjectsLt [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : Type u

The TypedObjects for each β < α.

Equations

• ConNF.TypedObjectsLt = ((β : ConNF.Λ) → [inst_1 : ConNF.LtLevel ↑β] → ConNF.TypedObjects β)

@[reducible, inline]

abbrev ConNF.PositionedObjectsLt [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] : Prop

The PositionedObjects for each β < α.

Equations

• ConNF.PositionedObjectsLt = ∀ (β : ConNF.Λ) [inst_1 : ConNF.LtLevel ↑β], ConNF.PositionedObjects β

We have to give the following things different names in the two places we define them: here, and in the FOA hypothesis file.

def ConNF.Tangle.set_lt [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] {β : ConNF.TypeIndex} [ConNF.LtLevel β] : ConNF.Tangle β → ConNF.TSet β

Equations

• x.set_lt = match x✝¹, x✝, x with | some β, x, t => t.set | none, _i, a => a

theorem ConNF.Tangle.set_lt_smul [ConNF.Params] [ConNF.Level] [i : ConNF.ModelDataLt] {β : ConNF.TypeIndex} [iβ : ConNF.LtLevel β] (ρ : ConNF.Allowable β) (t : ConNF.Tangle β) : (ρ • t).set_lt = ρ • t.set_lt

theorem ConNF.exists_tangle_lt [ConNF.Params] [ConNF.Level] [i : ConNF.ModelDataLt] {β : ConNF.TypeIndex} [iβ : ConNF.LtLevel β] (t : ConNF.TSet β) : ∃ (u : ConNF.Tangle β), u.set_lt = t

theorem ConNF.Tangle.ext_lt [ConNF.Params] [ConNF.Level] [i : ConNF.ModelDataLt] {β : ConNF.TypeIndex} [iβ : ConNF.LtLevel β] (t₁ : ConNF.Tangle β) (t₂ : ConNF.Tangle β) (hs : t₁.set_lt = t₂.set_lt) (hS : t₁.support = t₂.support) : t₁ = t₂

theorem ConNF.Tangle.smul_set_lt [ConNF.Params] [ConNF.Level] [i : ConNF.ModelDataLt] {β : ConNF.TypeIndex} [iβ : ConNF.LtLevel β] (t : ConNF.Tangle β) (ρ : ConNF.Allowable β) : (ρ • t).set_lt = ρ • t.set_lt

theorem ConNF.Tangle.support_supports_lt [ConNF.Params] [ConNF.Level] [i : ConNF.ModelDataLt] {β : ConNF.TypeIndex} [iβ : ConNF.LtLevel β] (t : ConNF.Tangle β) : MulAction.Supports (ConNF.Allowable β) (ConNF.Enumeration.carrier t.support) t