AcceptedComplexes.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The bundled-group and carrier-and-instance presentations of augmented directed complexes have the same positive tables and strict realization.

def OAI.Thomason.Construction.DirectedComplex.toAccepted line 16
Source documentation
Express a directed complex using its chain carriers and group instances.
```
def toAccepted (K : DirectedComplex.{u}) : Thomason.DirectedComplex.{u} where
…
```
def OAI.Thomason.Construction.DirectedComplex.ofAccepted line 26
Source documentation
Bundle the chain groups of a carrier-and-instance directed complex.
```
def ofAccepted (K : Thomason.DirectedComplex.{u}) : DirectedComplex.{u} where
…
```
def OAI.Thomason.Construction.DirectedComplex.Hom.toAccepted line 35
Source documentation
A positive chain map is unchanged on each chain group by the conversion.
```
def Hom.toAccepted {K L : DirectedComplex.{u}} (f : Hom K L) :
    Thomason.DirectedComplex.Hom K.toAccepted L.toAccepted where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.DirectedComplex.Hom
def OAI.Thomason.Construction.DirectedComplex.Hom.ofAccepted line 43
Source documentation
Positive chain maps also admit the bundled-group presentation.
```
def Hom.ofAccepted {K L : Thomason.DirectedComplex.{u}} (f : Thomason.DirectedComplex.Hom K L) :
    Hom (ofAccepted K) (ofAccepted L) where
…
```
Mentions: OAI.Thomason.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.Hom
def OAI.Thomason.Construction.DirectedComplex.Cell.toAccepted line 55
Source documentation
Transpose the degree and boundary indices of a positive globular table.
```
def toAccepted (x : Cell K) : Thomason.DirectedComplex.Table K.toAccepted where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.DirectedComplex.Table
def OAI.Thomason.Construction.DirectedComplex.Cell.ofAccepted line 63
Source documentation
Express a positive table in the Boolean-face presentation.
```
def ofAccepted (x : Thomason.DirectedComplex.Table K.toAccepted) : Cell K where
…
```
Mentions: OAI.Thomason.DirectedComplex.Table, OAI.Thomason.Construction.DirectedComplex.Cell
def OAI.Thomason.Construction.DirectedComplex.Cell.acceptedEquiv line 71
Source documentation
The table conversion preserves all chains, including zero upper chains.
```
def acceptedEquiv (K : DirectedComplex.{u}) : Cell K ≃ Thomason.DirectedComplex.Table K.toAccepted where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.DirectedComplex.Table
theorem OAI.Thomason.Construction.DirectedComplex.Cell.toAccepted_face line 77
theorem OAI.Thomason.Construction.DirectedComplex.Cell.ofAccepted_truncate line 82
theorem OAI.Thomason.Construction.DirectedComplex.Cell.toAccepted_comp line 88
theorem OAI.Thomason.Construction.DirectedComplex.Cell.toAccepted_map line 97
def OAI.Thomason.Construction.DirectedComplex.realizationIso line 103
Source documentation
The two positive-table realizations are isomorphic as strict omega-categories.
```
def realizationIso (K : DirectedComplex.{u}) :
    toOmega.obj K.realization ≅ K.toAccepted.nu where
…
```
theorem OAI.Thomason.Construction.DirectedComplex.realizationIso_naturality line 125
Source documentation
Realization of a positive chain map commutes with the presentation isomorphism.
```
theorem realizationIso_naturality {K L : DirectedComplex.{u}} (f : Hom K L) :
    toOmega.map f.realization ≫ (realizationIso L).hom =
      (realizationIso K).hom ≫ f.toAccepted.nu := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.realizationIso