IntegralCellularBoundary.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Integral chains for a polygon incidence system, with all lifted edges independent. This is the algebraic cellular boundary needed for the source's cycle producer. It does not identify these chains with a topological homology theory.

def OAI.HyperbolicObstruction.IntegralIncidence.reverse line 20
Source documentation
Formal dart reversal. Loop edges and parallel indexed edges remain distinct.
```
def reverse (e : E × Bool) : E × Bool := (e.1, !e.2)
```
theorem OAI.HyperbolicObstruction.IntegralIncidence.reverse_reverse line 22
def OAI.HyperbolicObstruction.IntegralIncidence.liftedStart line 27
def OAI.HyperbolicObstruction.IntegralIncidence.liftedReverse line 28
theorem OAI.HyperbolicObstruction.IntegralIncidence.liftedReverse_reverse line 34
def OAI.HyperbolicObstruction.IntegralIncidence.edgeChain line 42
Source documentation
Signed contribution of a lifted dart to the free integral edge module. A negative dart is indexed at the start of its positive reverse.
```
def edgeChain (e : G × (E × Bool)) : (G × E) →₀ ℤ :=
…
```
theorem OAI.HyperbolicObstruction.IntegralIncidence.edgeChain_reverse line 47
def OAI.HyperbolicObstruction.IntegralIncidence.edgeBoundary line 54
Source documentation
The boundary of a positive lifted edge.
```
def edgeBoundary (e : G × E) : (G × V) →₀ ℤ :=
…
```
def OAI.HyperbolicObstruction.IntegralIncidence.d₁ line 58
lemma OAI.HyperbolicObstruction.IntegralIncidence.boundary_edgeChain line 62
structure OAI.HyperbolicObstruction.IntegralIncidence.Polygons line 72
Source documentation
An indexed polygonal attaching system, before topological realization.
```
structure Polygons (E V C : Type*) where
…
```
lemma OAI.HyperbolicObstruction.IntegralIncidence.group_prefix_rotate line 79