IntervalAdjunction.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The globe-and-pasting construction gives a right interval adjunction on strict omega-categories. The equivalence of cell presentations transports its ordered simplex comparisons, endpoints, collapse and finite truncations.

def OAI.Thomason.ConstructedInterval.tensor line 17
Source documentation
The global right interval tensor in the separate-boundary presentation.
```
def tensor : OmegaCategory.{0} ⥤ OmegaCategory.{0} :=
…
```
def OAI.Thomason.ConstructedInterval.internalHom line 21
Source documentation
The right internal hom whose cells are maps from concrete globe cylinders.
```
def internalHom : OmegaCategory.{0} ⥤ OmegaCategory.{0} :=
…
```
def OAI.Thomason.ConstructedInterval.adjunction line 25
Source documentation
Transport of the global right interval adjunction preserves its actual functors.
```
def adjunction : tensor ⊣ internalHom :=
…
```
Mentions: OAI.Thomason.ConstructedInterval.tensor, OAI.Thomason.ConstructedInterval.internalHom
def OAI.Thomason.ConstructedInterval.endpoint line 30
Source documentation
The two oriented endpoint maps of the transported cylinder.
```
def endpoint (side : Bool) : 𝟭 OmegaCategory.{0} ⟶ tensor :=
…
```
Mentions: OAI.Thomason.ConstructedInterval.tensor
def OAI.Thomason.ConstructedInterval.projection line 35
Source documentation
Collapse of the transported cylinder to its source.
```
def projection : tensor ⟶ 𝟭 OmegaCategory.{0} :=
…
```
Mentions: OAI.Thomason.ConstructedInterval.tensor
theorem OAI.Thomason.ConstructedInterval.endpoint_projection line 39
def OAI.Thomason.ConstructedInterval.representationComparison line 51
Source documentation
Conversion of the source presentation commutes naturally with the tensor.
```
def representationComparison :
    toOmega ⋙ tensor ≅ GrayChainExtension.cylinder ⋙ toOmega :=
…
```
Mentions: OAI.Thomason.ConstructedInterval.tensor
theorem OAI.Thomason.ConstructedInterval.representationComparison_endpoint line 55
theorem OAI.Thomason.ConstructedInterval.representationComparison_projection line 67
theorem OAI.Thomason.ConstructedInterval.internalHom_isTruncated line 82
Source documentation
The same right internal hom preserves each finite dimension bound.
```
theorem internalHom_isTruncated {Y : OmegaCategory.{0}} {n : ℕ}
    (hY : Y.IsTruncated n) : (internalHom.obj Y).IsTruncated n := by
…
```
def OAI.Thomason.ConstructedInterval.simplexComparison line 92
Source documentation
The ordered simplex cylinder compares naturally with the global right tensor.
```
def simplexComparison :
    h.cylinderCosimplicial ⋙ toOmega ≅ (h.cosimplicial ⋙ toOmega) ⋙ tensor :=
…
```
Mentions: OAI.Thomason.ConstructedInterval.tensor
theorem OAI.Thomason.ConstructedInterval.simplexComparison_endpoint line 98
Source documentation
The ordered comparison respects both endpoint conventions.
```
theorem simplexComparison_endpoint (side : Bool) (m : SimplexCategory) :
    toOmega.map ((h.cylinderEndpoint side).app m) ≫ (simplexComparison h).hom.app m =
      (endpoint side).app (toOmega.obj (h.object m.len)) := by
…
```
Mentions: OAI.Thomason.ConstructedInterval.simplexComparison, OAI.Thomason.ConstructedInterval.endpoint
theorem OAI.Thomason.ConstructedInterval.simplexComparison_projection line 109
Source documentation
The ordered comparison respects collapse of the interval.
```
theorem simplexComparison_projection (m : SimplexCategory) :
    (simplexComparison h).hom.app m ≫ projection.app (toOmega.obj (h.object m.len)) =
      toOmega.map (h.cylinderProjection.app m) := by
…
```
Mentions: OAI.Thomason.ConstructedInterval.simplexComparison