Representation.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The equivalence between separate-boundary and Boolean-face presentations of strict omega-categories preserves every cell and every composition.

theorem OAI.Thomason.Construction.StrictOmegaCategory.source_comp_le line 15
theorem OAI.Thomason.Construction.StrictOmegaCategory.target_comp_le line 23
def OAI.Thomason.Construction.StrictOmegaCategory.toOmegaCategory line 32
Source documentation
Interpret Boolean faces as separate source and target operations.
```
def toOmegaCategory (C : StrictOmegaCategory.{u}) : Thomason.OmegaCategory.{u} where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.Hom.toOmegaFunctor line 65
Source documentation
The same cell function is a functor in the separate-boundary presentation.
```
def Hom.toOmegaFunctor {C : StrictOmegaCategory.{u}} {D : StrictOmegaCategory.{v}}
    (f : Hom C D) : Thomason.OmegaCategory.Functor C.toOmegaCategory D.toOmegaCategory where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom, OAI.Thomason.OmegaCategory.Functor
theorem OAI.Thomason.Construction.StrictOmegaCategory.toOmegaCategory_isTruncated line 72
def OAI.Thomason.OmegaCategory.toStrictOmegaCategory line 85
Source documentation
Combine source and target into a Boolean-indexed boundary operation.
```
def toStrictOmegaCategory (C : OmegaCategory.{u}) : Construction.StrictOmegaCategory.{u} where
…
```
def OAI.Thomason.OmegaCategory.Functor.toStrictHom line 117
Source documentation
Strict functors preserve the combined Boolean face operation.
```
def Functor.toStrictHom {C : OmegaCategory.{u}} {D : OmegaCategory.{v}}
    (f : Functor C D) : Construction.StrictOmegaCategory.Hom
      C.toStrictOmegaCategory D.toStrictOmegaCategory where
…
```
Mentions: OAI.Thomason.OmegaCategory.Functor, OAI.Thomason.Construction.StrictOmegaCategory.Hom
theorem OAI.Thomason.OmegaCategory.toStrictOmegaCategory_isTruncated line 127
def OAI.Thomason.Construction.toOmega line 142
Source documentation
The cell-preserving conversion to separate source and target.
```
def toOmega : StrictOmegaCategory.{u} ⥤ OmegaCategory.{u} where
…
```
def OAI.Thomason.Construction.fromOmega line 149
Source documentation
The cell-preserving conversion to Boolean-indexed boundaries.
```
def fromOmega : OmegaCategory.{u} ⥤ StrictOmegaCategory.{u} where
…
```
def OAI.Thomason.Construction.strictRoundtripIso line 155
def OAI.Thomason.Construction.omegaRoundtripIso line 168
def OAI.Thomason.Construction.representationEquivalence line 184
Source documentation
The two presentations describe equivalent categories of strict omega-categories.
```
noncomputable def representationEquivalence : StrictOmegaCategory.{u} ≌ OmegaCategory.{u} where
…
```
def OAI.Thomason.Construction.toFiniteOmega line 192
Source documentation
Conversion restricted to categories with a uniform finite dimension bound.
```
def toFiniteOmega (n : ℕ) : StrictOmegaCategory.Truncated.{u} n ⥤
    OmegaCategory.NCategory.{u} n where
…
```
def OAI.Thomason.Construction.fromFiniteOmega line 200
Source documentation
The inverse conversion also preserves the same finite dimension bound.
```
def fromFiniteOmega (n : ℕ) : OmegaCategory.NCategory.{u} n ⥤
    StrictOmegaCategory.Truncated.{u} n where
…
```
def OAI.Thomason.Construction.finiteRepresentationEquivalence line 208
Source documentation
The presentation equivalence restricts in every finite dimension.
```
noncomputable def finiteRepresentationEquivalence (n : ℕ) : StrictOmegaCategory.Truncated.{u} n ≌
    OmegaCategory.NCategory.{u} n where
…
```