PathImages.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Iterated images of the arrow coefficient maps.

def OAI.HarmonicArtin.ParabolicIntersections.pathImages line 10
lemma OAI.HarmonicArtin.ParabolicIntersections.mem_pathImages_zero line 14
lemma OAI.HarmonicArtin.ParabolicIntersections.pathImages_step line 18
lemma OAI.HarmonicArtin.ParabolicIntersections.pathImages_eq_bot line 37
lemma OAI.HarmonicArtin.ParabolicIntersections.supported_mem_of_single line 47
Source documentation
An arbitrary supported vector belongs to a subspace as soon as all its occupied coordinate vectors do.
```
lemma supported_mem_of_single {P : Submodule ℂ (I → ℂ)} (x : I → ℂ)
    (h : ∀ i, x i ≠ 0 → Pi.single i (1 : ℂ) ∈ P) : x ∈ P := by
…
```

theorem OAI.HarmonicArtin.ParabolicIntersections.incoming_spanning_pathImages line 64

Source documentation

Iterating incoming spanning equations lands in the image of paths of length n. The lower bound on the placement prevents leaving the range where the spanning equations hold.

theorem incoming_spanning_pathImages (degree : I → ℤ) (lower : ℤ)
    (hspan : ∀ i, lower < degree i → ∃ y : A → (I → ℂ),
      (∀ a j, y a j ≠ 0 → degree j = degree i - 1) ∧
      (∃ t : Finset A, Pi.single i (1 : ℂ) = ∑ a ∈ t, Matrix.vecMul (y a) (B a))) :
    ∀ n : ℕ, ∀ i, lower + n ≤ degree i → Pi.single i (1 : ℂ) ∈ pathImages B n := by
…

Mentions: OAI.HarmonicArtin.ParabolicIntersections.pathImages