Recoding

In this file, we show that all coding functions of level β > γ can be expressed in terms of a set of a particular class of γ-coding functions, called raised coding functions.

Main declarations

• ConNF.exists_combination_raisedSingleton: Each coding function at a level β > γ can be expressed in terms of a set of γ-coding functions and a β-support orbit.

def ConNF.Combination [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (x : ConNF.TSet ↑β) (S : ConNF.Support ↑β) (χs : Set (ConNF.CodingFunction ↑β)) : Prop

Equations

• ConNF.Combination hγ x S χs = ∀ (y : ConNF.TSet ↑γ), y ∈[hγ] x ↔ ∃ χ ∈ χs, ∃ (T : ConNF.Support ↑β) (z : ConNF.TSet ↑β), χ.rel T z ∧ S.Subsupport T ∧ y ∈[hγ] z

theorem ConNF.combination_unique [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) {x₁ x₂ : ConNF.TSet ↑β} {S : ConNF.Support ↑β} {χs : Set (ConNF.CodingFunction ↑β)} (hx₁ : ConNF.Combination hγ x₁ S χs) (hx₂ : ConNF.Combination hγ x₂ S χs) : x₁ = x₂

theorem ConNF.Combination.smul [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) {x : ConNF.TSet ↑β} {S : ConNF.Support ↑β} {χs : Set (ConNF.CodingFunction ↑β)} (h : ConNF.Combination hγ x S χs) (ρ : ConNF.AllPerm ↑β) : ConNF.Combination hγ (ρ • x) (ρᵁ • S) χs

inductive ConNF.RaisedRel [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (s : Set (ConNF.CodingFunction ↑β)) (o : ConNF.SupportOrbit ↑β) : Rel (ConNF.Support ↑β) (ConNF.TSet ↑β)

• mk: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.CoherentData] {β γ : ConNF.Λ} [inst_3 : ConNF.LeLevel ↑β] [inst_4 : ConNF.LeLevel ↑γ] {hγ : ↑γ < ↑β} {s : Set (ConNF.CodingFunction ↑β)} {o : ConNF.SupportOrbit ↑β} (S : ConNF.Support ↑β), S.orbit = o → ∀ (x : ConNF.TSet ↑β), ConNF.Combination hγ x S s → ConNF.RaisedRel hγ s o S x

theorem ConNF.raisedRel_coinjective [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (s : Set (ConNF.CodingFunction ↑β)) (o : ConNF.SupportOrbit ↑β) : (ConNF.RaisedRel hγ s o).Coinjective

theorem ConNF.raisedRel_dom_nonempty [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) {s : Set (ConNF.CodingFunction ↑β)} {o : ConNF.SupportOrbit ↑β} (hso : ∀ (S : ConNF.Support ↑β), S.orbit = o → ∃ (x : ConNF.TSet ↑β), ConNF.Combination hγ x S s ∧ S.Supports x) : (ConNF.RaisedRel hγ s o).dom.Nonempty

theorem ConNF.supports_of_raisedRel [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) {s : Set (ConNF.CodingFunction ↑β)} {o : ConNF.SupportOrbit ↑β} (hso : ∀ (S : ConNF.Support ↑β), S.orbit = o → ∃ (x : ConNF.TSet ↑β), ConNF.Combination hγ x S s ∧ S.Supports x) {S : ConNF.Support ↑β} {x : ConNF.TSet ↑β} : ConNF.RaisedRel hγ s o S x → S.Supports x

theorem ConNF.orbit_eq_of_mem_dom_raisedRel [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (s : Set (ConNF.CodingFunction ↑β)) (o : ConNF.SupportOrbit ↑β) {S : ConNF.Support ↑β} (hS : S ∈ (ConNF.RaisedRel hγ s o).dom) : S.orbit = o

theorem ConNF.smul_raisedRel [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (s : Set (ConNF.CodingFunction ↑β)) (o : ConNF.SupportOrbit ↑β) {S : ConNF.Support ↑β} {x : ConNF.TSet ↑β} (h : ConNF.RaisedRel hγ s o S x) (ρ : ConNF.AllPerm ↑β) : ConNF.RaisedRel hγ s o (ρᵁ • S) (ρ • x)

def ConNF.raisedCodingFunction [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (s : Set (ConNF.CodingFunction ↑β)) (o : ConNF.SupportOrbit ↑β) (hso : ∀ (S : ConNF.Support ↑β), S.orbit = o → ∃ (x : ConNF.TSet ↑β), ConNF.Combination hγ x S s ∧ S.Supports x) : ConNF.CodingFunction ↑β

Equations

• ConNF.raisedCodingFunction hγ s o hso = { rel := ConNF.RaisedRel hγ s o, rel_coinjective := ⋯, rel_dom_nonempty := ⋯, supports_of_rel := ⋯, orbit_eq_of_mem_dom := ⋯, smul_rel := ⋯ }

theorem ConNF.scoderiv_supports_singleton [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (S : ConNF.Support ↑γ) (y : ConNF.TSet ↑γ) (h : S.Supports y) : (S ↗ hγ).Supports (ConNF.singleton hγ y)

theorem ConNF.raisedSingleton_supports [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (S : ConNF.Support ↑β) (y : ConNF.TSet ↑γ) : (S + ConNF.designatedSupport y ↗ hγ).Supports (ConNF.singleton hγ y)

def ConNF.raisedSingleton [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (S : ConNF.Support ↑β) (y : ConNF.TSet ↑γ) : ConNF.CodingFunction ↑β

Equations

• ConNF.raisedSingleton hγ S y = { set := ConNF.singleton hγ y, support := S + ConNF.designatedSupport y ↗ hγ, support_supports := ⋯ }.code

theorem ConNF.combination_raisedSingleton [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (x : ConNF.TSet ↑β) (S : ConNF.Support ↑β) (hxS : S.Supports x) : ConNF.Combination hγ x S (ConNF.raisedSingleton hγ S '' {y : ConNF.TSet ↑γ | y ∈[hγ] x})

def ConNF.RaisedSingleton [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) : Type u

Equations

• ConNF.RaisedSingleton hγ = { χ : ConNF.CodingFunction ↑β // ∃ (S : ConNF.Support ↑β) (y : ConNF.TSet ↑γ), χ = ConNF.raisedSingleton hγ S y }

theorem ConNF.exists_combination_raisedSingleton [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (χ : ConNF.CodingFunction ↑β) : ∃ (s : Set (ConNF.RaisedSingleton hγ)) (o : ConNF.SupportOrbit ↑β) (hso : ∀ (S : ConNF.Support ↑β), S.orbit = o → ∃ (x : ConNF.TSet ↑β), ConNF.Combination hγ x S (Subtype.val '' s) ∧ S.Supports x), χ = ConNF.raisedCodingFunction hγ (Subtype.val '' s) o hso

structure ConNF.RaisedSingletonData [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (β γ : ConNF.Λ) [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] : Type u

• ba : ConNF.κ
• bN : ConNF.κ
• o : ConNF.SupportOrbit ↑β
• χ : ConNF.CodingFunction ↑γ

def ConNF.RaisedSingletonData.mk' [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (S : ConNF.Support ↑β) (y : ConNF.TSet ↑γ) : ConNF.RaisedSingletonData β γ

Equations

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

theorem ConNF.RaisedSingletonData.mk'_eq_mk' [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) {S₁ S₂ : ConNF.Support ↑β} {y₁ y₂ : ConNF.TSet ↑γ} (h : ConNF.RaisedSingletonData.mk' hγ S₁ y₁ = ConNF.RaisedSingletonData.mk' hγ S₂ y₂) : ConNF.raisedSingleton hγ S₁ y₁ = ConNF.raisedSingleton hγ S₂ y₂

theorem ConNF.card_raisedSingleton_lt' [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) : Cardinal.mk (ConNF.RaisedSingleton hγ) ≤ Cardinal.mk (ConNF.RaisedSingletonData β γ)

def ConNF.raisedSingletonDataEquiv [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (β γ : ConNF.Λ) [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] : ConNF.RaisedSingletonData β γ ≃ ConNF.κ × ConNF.κ × ConNF.SupportOrbit ↑β × ConNF.CodingFunction ↑γ

Equations

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

theorem ConNF.card_raisedSingleton_lt [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (h₁ : Cardinal.mk (ConNF.SupportOrbit ↑β) < Cardinal.mk ConNF.μ) (h₂ : ∀ δ < ↑β, ∀ [inst : ConNF.LeLevel δ], Cardinal.mk (ConNF.CodingFunction δ) < Cardinal.mk ConNF.μ) : Cardinal.mk (ConNF.RaisedSingleton hγ) < Cardinal.mk ConNF.μ