DirectedComplex.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Augmented directed complexes and their globular cells

An augmented directed complex consists of chain groups, differentials, an augmentation and positive submonoids. A globular cell is a finite table of positive chains, with the boundary and augmentation equations in Steiner's construction nu. Its faces are truncations of this table.

structure OAI.Thomason.Construction.DirectedComplex line 22
structure OAI.Thomason.Construction.DirectedComplex.Hom line 34
Source documentation
A chain map preserving the augmentation and positive submonoids.
```
structure Hom (K L : DirectedComplex.{u}) where
…
```
structure OAI.Thomason.Construction.DirectedComplex.Cell line 43
Source documentation
The finite positive chain table defining a cell of nu K.
```
structure Cell (K : DirectedComplex.{u}) where
…
```
def OAI.Thomason.Construction.DirectedComplex.Cell.map line 57
Source documentation
Applying a positive chain map in every degree preserves the full table equations, including the boundary data below any vanishing top chain.
```
def map (f : Hom K L) (x : Cell K) : Cell L where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.Cell
theorem OAI.Thomason.Construction.DirectedComplex.Cell.map_table line 68
def OAI.Thomason.Construction.DirectedComplex.Cell.cutTable line 73
Source documentation
Truncate a table at degree n, retaining the chosen boundary twice in that degree. The lower-dimensional entries remain unchanged.
```
def cutTable (x : Cell K) (a : Bool) (n : ℕ) (b : Bool) (m : ℕ) : K.group m :=
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell
def OAI.Thomason.Construction.DirectedComplex.Cell.face line 76
theorem OAI.Thomason.Construction.DirectedComplex.Cell.face_table line 109
theorem OAI.Thomason.Construction.DirectedComplex.Cell.map_face line 113
Source documentation
Positive chain maps preserve globular source and target truncation.
```
theorem map_face (f : Hom K L) (x : Cell K) (a : Bool) (n : ℕ) :
    map f (x.face a n) = (map f x).face a n := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.map, OAI.Thomason.Construction.DirectedComplex.Cell.face
theorem OAI.Thomason.Construction.DirectedComplex.Cell.face_face line 120
Source documentation
The face operations satisfy the strict globular identities.
```
theorem face_face (x : Cell K) (a b : Bool) (m n : ℕ) :
    (x.face b n).face a m = if m < n then x.face a m else x.face b n := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.face
theorem OAI.Thomason.Construction.DirectedComplex.Cell.matching_top line 133
theorem OAI.Thomason.Construction.DirectedComplex.Cell.matching_below line 138
def OAI.Thomason.Construction.DirectedComplex.Cell.pasteTable line 145
Source documentation
The table for composition along dimension n: retain common lower data, take the exterior boundaries at n, and add the higher chains.
```
def pasteTable (x y : Cell K) (n : ℕ) (a : Bool) (m : ℕ) : K.group m :=
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell
def OAI.Thomason.Construction.DirectedComplex.Cell.comp line 150
theorem OAI.Thomason.Construction.DirectedComplex.Cell.comp_table line 203
theorem OAI.Thomason.Construction.DirectedComplex.Cell.map_comp line 208
Source documentation
Positive chain maps respect composition of globular tables. This includes maps sending generators to sums or zero.
```
theorem map_comp (f : Hom K L) (x y : Cell K) (n : ℕ)
    (h : x.face true n = y.face false n)
    (h' : (map f x).face true n = (map f y).face false n) :
    map f (comp x y n h) = comp (map f x) (map f y) n h' := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.map, OAI.Thomason.Construction.DirectedComplex.Cell.face, OAI.Thomason.Construction.DirectedComplex.Cell.comp