CoefficientPaths.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The path-algebra relations satisfied by actual minimal differentials.

def OAI.HarmonicArtin.ParabolicIntersections.arrowMatrix line 14
lemma OAI.HarmonicArtin.ParabolicIntersections.differential_arrow_left_support line 18
lemma OAI.HarmonicArtin.ParabolicIntersections.arrowMatrix_noncomposable line 26
lemma OAI.HarmonicArtin.ParabolicIntersections.arrowMatrix_outside line 37
lemma OAI.HarmonicArtin.ParabolicIntersections.arrowMatrix_mesh line 48
Source documentation
The mesh relation is precisely the token coefficient of d²=0; minimality eliminates the other two terms in that coefficient.
```
lemma arrowMatrix_mesh (E : BasedComplex Q (K := ℂ) I) (hE : E.IsMinimal Q) (v : V) :
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.coefficient_paths_nilpotent line 79
Source documentation
The published abstract mesh input applies to the coefficient maps of any actual minimal complex supported in the given colors.
```
theorem coefficient_paths_nilpotent (U : Set V) (hmesh : MeshNilpotent Q U)
    (E : BasedComplex Q (K := ℂ) I) (hE : E.IsMinimal Q)
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent
lemma OAI.HarmonicArtin.ParabolicIntersections.cochain_interval_restrict line 90
Source documentation
Truncating to a cochain interval gives a complex. No differential can leave and re-enter the interval because it increases cochain degree by one.
```
lemma cochain_interval_restrict (E : BasedComplex Q (K := ℂ) I) (l r : ℤ) :
…
```
def OAI.HarmonicArtin.ParabolicIntersections.cochainInterval line 110
theorem OAI.HarmonicArtin.ParabolicIntersections.interval_coefficient_paths_nilpotent line 117
Source documentation
Lemma 7.1 in its interval form. The fixed exponent works for every minimal complex and every interval; coefficient maps may vary with placement.
```
theorem interval_coefficient_paths_nilpotent (U : Set V) (hmesh : MeshNilpotent Q U) :
    ∃ N : ℕ, 0 < N ∧ ∀ (I : Type) [Fintype I]
      (E : BasedComplex Q (K := ℂ) I), E.IsMinimal Q → ∀ l r : ℤ,
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent