Coherent data

In this file, we define the type of coherent data below a particular proper type index.

Main declarations

• ConNF.ModelDataData: Coherent data below a given level α.

TODO: We're going to try allowing model data at level ⊥ to vary. That is, we use (β : TypeIndex) → [LeLevel β] → ModelData β instead of (β : Λ) → [LeLevel β] → ModelData β.

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

A convenience typeclass to hold data below the current level.

• data (β : TypeIndex) [LeLevel β] : ModelData β
• positions (β : TypeIndex) [LtLevel β] : Position (Tangle β)

theorem ConNF.LeData.ext_iff {inst✝ : Params} {inst✝¹ : Level} {x y : LeData} : x = y ↔ data = data ∧ positions ≍ positions

theorem ConNF.LeData.ext {inst✝ : Params} {inst✝¹ : Level} {x y : LeData} (data : data = data) (positions : positions ≍ positions) : x = y

instance ConNF.instModelDataOfLeDataOfLeLevel [Params] [Level] [LeData] (β : TypeIndex) [LeLevel β] : ModelData β

Equations

• ConNF.instModelDataOfLeDataOfLeLevel = ConNF.LeData.data

instance ConNF.instPositionTangle [Params] [Level] [LeData] (β : TypeIndex) [LtLevel β] : Position (Tangle β)

Equations

• ConNF.instPositionTangle = ConNF.LeData.positions

class ConNF.PreCoherentData [Params] [Level] extends ConNF.LeData : Type (u + 1)

• data (β : TypeIndex) [LeLevel β] : ModelData β
• positions (β : TypeIndex) [LtLevel β] : Position (Tangle β)
• allPermSderiv {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) : AllPerm β → AllPerm γ
• singleton {β γ : Λ} [LeLevel ↑β] [LeLevel ↑γ] (h : ↑γ < ↑β) : TSet ↑γ → TSet ↑β

theorem ConNF.PreCoherentData.ext {inst✝ : Params} {inst✝¹ : Level} {x y : PreCoherentData} (data : LeData.data = LeData.data) (positions : LeData.positions ≍ LeData.positions) (allPermSderiv : @allPermSderiv inst✝ inst✝¹ x ≍ @allPermSderiv inst✝ inst✝¹ y) (singleton : @singleton inst✝ inst✝¹ x ≍ @singleton inst✝ inst✝¹ y) : x = y

theorem ConNF.PreCoherentData.ext_iff {inst✝ : Params} {inst✝¹ : Level} {x y : PreCoherentData} : x = y ↔ LeData.data = LeData.data ∧ LeData.positions ≍ LeData.positions ∧ @allPermSderiv inst✝ inst✝¹ x ≍ @allPermSderiv inst✝ inst✝¹ y ∧ @singleton inst✝ inst✝¹ x ≍ @singleton inst✝ inst✝¹ y

instance ConNF.instDerivativeAllPerm [Params] [Level] [PreCoherentData] {β γ : TypeIndex} [LeLevel β] [LeLevel γ] : Derivative (AllPerm β) (AllPerm γ) β γ

Equations

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

@[simp]

theorem ConNF.allPerm_deriv_nil [Params] [Level] [PreCoherentData] {β : TypeIndex} [LeLevel β] (ρ : AllPerm β) : ρ ⇘ Path.nil = ρ

@[simp]

theorem ConNF.allPerm_deriv_sderiv [Params] [Level] [PreCoherentData] {β γ δ : TypeIndex} [LeLevel β] [LeLevel γ] [LeLevel δ] (ρ : AllPerm β) (A : β ↝ γ) (h : δ < γ) : ρ ⇘ (A ↘ h) = ρ ⇘ A ↘ h

class ConNF.CoherentData [Params] [Level] extends ConNF.PreCoherentData : Type (u + 1)

Note that in earlier versions of the proof we additionally used the following assumption.

typedMem_tSetForget {β : Λ} {γ : TypeIndex} [LeLevel β] [LeLevel γ]
  (hγ : γ < β) (x : TSet β) (y : StrSet γ) :
  y ∈[hγ] xᵁ → ∃ z : TSet γ, y = zᵁ

• data (β : TypeIndex) [LeLevel β] : ModelData β
• positions (β : TypeIndex) [LtLevel β] : Position (Tangle β)
• allPermSderiv {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) : AllPerm β → AllPerm γ
• singleton {β γ : Λ} [LeLevel ↑β] [LeLevel ↑γ] (h : ↑γ < ↑β) : TSet ↑γ → TSet ↑β
• allPermSderiv_forget {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) (ρ : AllPerm β) : (ρ ↘ h)ᵁ = ρᵁ ↘ h
• pos_atom_lt_pos {β : TypeIndex} [LtLevel β] (t : Tangle β) (A : β ↝ ⊥) (a : Atom) : a ∈ (t.support ⇘. A)ᴬ → pos a < pos t
• pos_nearLitter_lt_pos {β : TypeIndex} [LtLevel β] (t : Tangle β) (A : β ↝ ⊥) (N : NearLitter) : N ∈ (t.support ⇘. A)ᴺ → pos N < pos t
• smul_fuzz {γ : Λ} {δ : TypeIndex} {ε : Λ} [LeLevel ↑γ] [LtLevel δ] [LtLevel ↑ε] (hδ : δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : δ ≠ ↑ε) (ρ : AllPerm ↑γ) (t : Tangle δ) : ρᵁ ↘ hε ↘. • fuzz hδε t = fuzz hδε (ρ ↘ hδ • t)
• allPerm_of_basePerm (π : BasePerm) : ∃ (ρ : AllPerm ⊥), ρᵁ Path.nil = π
• allPerm_of_smulFuzz {γ : Λ} [LeLevel ↑γ] (ρs : {δ : TypeIndex} → [inst : LtLevel δ] → δ < ↑γ → AllPerm δ) (h : ∀ {δ : TypeIndex} {ε : Λ} [inst : LtLevel δ] [inst_1 : LtLevel ↑ε] (hδ : δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : δ ≠ ↑ε) (t : Tangle δ), (ρs hε)ᵁ ↘. • fuzz hδε t = fuzz hδε (ρs hδ • t)) : ∃ (ρ : AllPerm ↑γ), ∀ (δ : TypeIndex) [inst : LtLevel δ] (hδ : δ < ↑γ), ρ ↘ hδ = ρs hδ
• tSet_ext {β γ : Λ} [LeLevel ↑β] [LeLevel ↑γ] (hγ : ↑γ < ↑β) (x y : TSet ↑β) (h : ∀ (z : TSet ↑γ), z ∈[hγ] x ↔ z ∈[hγ] y) : x = y
• typedMem_singleton_iff {β γ : Λ} [LeLevel ↑β] [LeLevel ↑γ] (hγ : ↑γ < ↑β) (x y : TSet ↑γ) : y ∈[hγ] singleton hγ x ↔ y = x

theorem ConNF.CoherentData.ext {inst✝ : Params} {inst✝¹ : Level} {x y : CoherentData} (data : LeData.data = LeData.data) (positions : LeData.positions ≍ LeData.positions) (allPermSderiv : @PreCoherentData.allPermSderiv inst✝ inst✝¹ x.toPreCoherentData ≍ @PreCoherentData.allPermSderiv inst✝ inst✝¹ y.toPreCoherentData) (singleton : @singleton inst✝ inst✝¹ x.toPreCoherentData ≍ @singleton inst✝ inst✝¹ y.toPreCoherentData) : x = y

theorem ConNF.CoherentData.ext_iff {inst✝ : Params} {inst✝¹ : Level} {x y : CoherentData} : x = y ↔ LeData.data = LeData.data ∧ LeData.positions ≍ LeData.positions ∧ @PreCoherentData.allPermSderiv inst✝ inst✝¹ x.toPreCoherentData ≍ @PreCoherentData.allPermSderiv inst✝ inst✝¹ y.toPreCoherentData ∧ @singleton inst✝ inst✝¹ x.toPreCoherentData ≍ @singleton inst✝ inst✝¹ y.toPreCoherentData

@[simp]

theorem ConNF.allPermDeriv_forget [Params] [Level] [CoherentData] {β γ : TypeIndex} [LeLevel β] [iγ : LeLevel γ] (A : β ↝ γ) (ρ : AllPerm β) : (ρ ⇘ A)ᵁ = ρᵁ ⇘ A

theorem ConNF.allPerm_inv_sderiv [Params] [Level] [CoherentData] {β γ : TypeIndex} [LeLevel β] [iγ : LeLevel γ] (h : γ < β) (ρ : AllPerm β) : ρ⁻¹ ↘ h = (ρ ↘ h)⁻¹

theorem ConNF.TSet.mem_smul_iff [Params] [Level] [CoherentData] {β γ : TypeIndex} [LeLevel β] [iγ : LeLevel γ] {x : TSet γ} {y : TSet β} (h : γ < β) (ρ : AllPerm β) : x ∈[h] ρ • y ↔ ρ⁻¹ ↘ h • x ∈[h] y

@[simp]

theorem ConNF.CoherentData.smul_singleton [Params] [Level] [CoherentData] {β γ : Λ} [LeLevel ↑β] [LeLevel ↑γ] (hγ : ↑γ < ↑β) (x : TSet ↑γ) (ρ : AllPerm ↑β) : ρ • singleton hγ x = singleton hγ (ρ ↘ hγ • x)