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
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(x : TSet ↑β)
(S : Support ↑β)
(χs : Set (CodingFunction ↑β))
:
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
Instances For
theorem
ConNF.combination_unique
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
{x₁ x₂ : TSet ↑β}
{S : Support ↑β}
{χs : Set (CodingFunction ↑β)}
(hx₁ : Combination hγ x₁ S χs)
(hx₂ : Combination hγ x₂ S χs)
:
theorem
ConNF.Combination.smul
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
{x : TSet ↑β}
{S : Support ↑β}
{χs : Set (CodingFunction ↑β)}
(h : Combination hγ x S χs)
(ρ : AllPerm ↑β)
:
Combination hγ (ρ • x) (ρᵁ • S) χs
inductive
ConNF.RaisedRel
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(s : Set (CodingFunction ↑β))
(o : SupportOrbit ↑β)
:
- mk [Params] [Level] [CoherentData] {β γ : Λ} [LeLevel ↑β] [LeLevel ↑γ] {hγ : ↑γ < ↑β} {s : Set (CodingFunction ↑β)} {o : SupportOrbit ↑β} (S : Support ↑β) : S.orbit = o → ∀ (x : TSet ↑β), Combination hγ x S s → RaisedRel hγ s o S x
Instances For
theorem
ConNF.raisedRel_coinjective
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(s : Set (CodingFunction ↑β))
(o : SupportOrbit ↑β)
:
(RaisedRel hγ s o).Coinjective
theorem
ConNF.raisedRel_dom_nonempty
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
{s : Set (CodingFunction ↑β)}
{o : SupportOrbit ↑β}
(hso : ∀ (S : Support ↑β), S.orbit = o → ∃ (x : TSet ↑β), Combination hγ x S s ∧ S.Supports x)
:
theorem
ConNF.supports_of_raisedRel
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
{s : Set (CodingFunction ↑β)}
{o : SupportOrbit ↑β}
(hso : ∀ (S : Support ↑β), S.orbit = o → ∃ (x : TSet ↑β), Combination hγ x S s ∧ S.Supports x)
{S : Support ↑β}
{x : TSet ↑β}
:
theorem
ConNF.orbit_eq_of_mem_dom_raisedRel
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(s : Set (CodingFunction ↑β))
(o : SupportOrbit ↑β)
{S : Support ↑β}
(hS : S ∈ (RaisedRel hγ s o).dom)
:
theorem
ConNF.smul_raisedRel
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(s : Set (CodingFunction ↑β))
(o : SupportOrbit ↑β)
{S : Support ↑β}
{x : TSet ↑β}
(h : RaisedRel hγ s o S x)
(ρ : AllPerm ↑β)
:
def
ConNF.raisedCodingFunction
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(s : Set (CodingFunction ↑β))
(o : SupportOrbit ↑β)
(hso : ∀ (S : Support ↑β), S.orbit = o → ∃ (x : TSet ↑β), Combination hγ x S s ∧ S.Supports x)
:
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 := ⋯ }
Instances For
def
ConNF.raisedSingleton
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : Support ↑β)
(y : TSet ↑γ)
:
Equations
- ConNF.raisedSingleton hγ S y = { set := ConNF.singleton hγ y, support := S + ⋯.choose ↗ hγ, support_supports := ⋯ }.code
Instances For
def
ConNF.RaisedSingleton
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
:
Type u
Equations
- ConNF.RaisedSingleton hγ = { χ : ConNF.CodingFunction ↑β // ∃ (S : ConNF.Support ↑β) (y : ConNF.TSet ↑γ), χ = ConNF.raisedSingleton hγ S y }
Instances For
theorem
ConNF.exists_combination_raisedSingleton
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(χ : CodingFunction ↑β)
:
∃ (s : Set (RaisedSingleton hγ)) (o : SupportOrbit ↑β) (hso :
∀ (S : Support ↑β), S.orbit = o → ∃ (x : TSet ↑β), Combination hγ x S (Subtype.val '' s) ∧ S.Supports x),
χ = raisedCodingFunction hγ (Subtype.val '' s) o hso
structure
ConNF.RaisedSingletonData
[Params]
[Level]
[CoherentData]
(β γ : Λ)
[LeLevel ↑β]
[LeLevel ↑γ]
:
Type u
- ba : κ
- bN : κ
- o : SupportOrbit ↑β
- χ : CodingFunction ↑γ
Instances For
def
ConNF.RaisedSingletonData.mk'
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S : Support ↑β)
(y : TSet ↑γ)
:
Equations
Instances For
theorem
ConNF.card_raisedSingleton_lt'
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
:
def
ConNF.raisedSingletonDataEquiv
[Params]
[Level]
[CoherentData]
(β γ : Λ)
[LeLevel ↑β]
[LeLevel ↑γ]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ConNF.card_raisedSingleton_lt
[Params]
[Level]
[CoherentData]
{β γ : Λ}
[LeLevel ↑β]
[LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(h₁ : Cardinal.mk (SupportOrbit ↑β) < Cardinal.mk μ)
(h₂ : ∀ δ < ↑β, ∀ [inst : LeLevel δ], Cardinal.mk (CodingFunction δ) < Cardinal.mk μ)
: