Countable closure under triangular dependencies

For a code c, dependency c is the countable set of basis coordinates occurring in its prepared sequence. Because code indices are injective, closing a countable set under all codes whose indices it contains still takes only countably many new coordinates at each finite stage.

def Wallace.dependencyClosureStep {I : Type u} {Code : Type v} (index : Code ↪ I) (dependency : Code → Set I) (D : Set I) : Set I

One closure step under a family of countable dependencies.

Equations

• Wallace.dependencyClosureStep index dependency D = D ∪ ⋃ (c : Code), ⋃ (_ : index c ∈ D), dependency c

def Wallace.dependencyClosureStages {I : Type u} {Code : Type v} (index : Code ↪ I) (dependency : Code → Set I) (D₀ : Set I) : ℕ → Set I

Finite stages of the dependency closure.

Equations

• Wallace.dependencyClosureStages index dependency D₀ 0 = D₀
• Wallace.dependencyClosureStages index dependency D₀ n.succ = Wallace.dependencyClosureStep index dependency (Wallace.dependencyClosureStages index dependency D₀ n)

def Wallace.dependencyClosure {I : Type u} {Code : Type v} (index : Code ↪ I) (dependency : Code → Set I) (D₀ : Set I) : Set I

Closure after all finite stages.

Equations

• Wallace.dependencyClosure index dependency D₀ = ⋃ (n : ℕ), Wallace.dependencyClosureStages index dependency D₀ n

theorem Wallace.subset_dependencyClosure {I : Type u} {Code : Type v} (index : Code ↪ I) (dependency : Code → Set I) (D₀ : Set I) : D₀ ⊆ dependencyClosure index dependency D₀

theorem Wallace.dependency_subset_closure_of_index_mem {I : Type u} {Code : Type v} (index : Code ↪ I) (dependency : Code → Set I) (D₀ : Set I) {c : Code} (hc : index c ∈ dependencyClosure index dependency D₀) : dependency c ⊆ dependencyClosure index dependency D₀

The closure is closed under every dependency whose code index it contains.

theorem Wallace.countable_preimage_of_injective {I : Type u} {Code : Type v} (index : Code ↪ I) {D : Set I} (hD : D.Countable) : {c : Code | index c ∈ D}.Countable

theorem Wallace.countable_dependencyClosureStep {I : Type u} {Code : Type v} (index : Code ↪ I) (dependency : Code → Set I) (hdep : ∀ (c : Code), (dependency c).Countable) {D : Set I} (hD : D.Countable) : (dependencyClosureStep index dependency D).Countable

A countable set remains countable after one dependency-closure step.

theorem Wallace.countable_dependencyClosure {I : Type u} {Code : Type v} (index : Code ↪ I) (dependency : Code → Set I) (hdep : ∀ (c : Code), (dependency c).Countable) {D₀ : Set I} (hD₀ : D₀.Countable) : (dependencyClosure index dependency D₀).Countable

Closing a countable set under countable triangular dependencies is countable.

Prepared-support specialization

def Wallace.preparedDependency {I : Type u} {Code : Type v} {R : Type w} [Zero R] (prepared : Code → ℕ → I →₀ R) (c : Code) : Set I

All coordinates occurring in the prepared sequence attached to a code.

Equations

• Wallace.preparedDependency prepared c = ⋃ (n : ℕ), ↑(prepared c n).support

theorem Wallace.preparedDependency_countable {I : Type u} {Code : Type v} {R : Type w} [Zero R] (prepared : Code → ℕ → I →₀ R) (c : Code) : (preparedDependency prepared c).Countable

def Wallace.preparedClosure {I : Type u} {Code : Type v} {R : Type w} [Zero R] (index : Code ↪ I) (prepared : Code → ℕ → I →₀ R) (x : I →₀ R) : Set I

The dependency closure generated by the support of a finitely supported vector.

Equations

• Wallace.preparedClosure index prepared x = Wallace.dependencyClosure index (Wallace.preparedDependency prepared) ↑x.support

theorem Wallace.support_subset_preparedClosure {I : Type u} {Code : Type v} {R : Type w} [Zero R] (index : Code ↪ I) (prepared : Code → ℕ → I →₀ R) (x : I →₀ R) : ↑x.support ⊆ preparedClosure index prepared x

theorem Wallace.preparedClosure_countable {I : Type u} {Code : Type v} {R : Type w} [Zero R] (index : Code ↪ I) (prepared : Code → ℕ → I →₀ R) (x : I →₀ R) : (preparedClosure index prepared x).Countable

theorem Wallace.preparedSupport_subset_preparedClosure {I : Type u} {Code : Type v} {R : Type w} [Zero R] (index : Code ↪ I) (prepared : Code → ℕ → I →₀ R) (x : I →₀ R) (c : Code) (hc : index c ∈ preparedClosure index prepared x) (n : ℕ) : ↑(prepared c n).support ⊆ preparedClosure index prepared x

The closure contains every coordinate in a prepared sequence whose code index it contains.