GraySimplexProjection.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Actual realization equivalences on the finite Gray parameters

The constructed global collapse restricts to the literal weak chain collapse on every globe and binary pasting. Both surrounding comparison maps are proved strict isomorphisms.

theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.projection_parameter line 22
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.projection_parameter_weak line 36
Source documentation
The constructed collapse is an actual Street-realization weak equivalence on every finite parameter used by its extension.
```
theorem projection_parameter_weak (h : NormalizedSimplexIdentities)
    (i : GlobePasting.Shape) :
    h.streetWeakEquivalences (projection.app (GlobePasting.object i)) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.object
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.orderedRealizationCylinderIso line 78
Source documentation
The actual extended cylinder agrees with the positive chain cylinder on every ordered atomic realization whose cylinder basis has the proved order.
```
def orderedRealizationCylinderIso {K : DirectedComplex.{0}} (B : OrderedAtomBasis K)
    (hs : B.SideHeight) : cylinder.obj K.realization ≅ (rightCylinder K).realization :=
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.orderedRealizationCylinderIso_hom line 84
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.comparisonToRealization_isIso line 88
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.simplexCylinderIso line 95
Source documentation
In particular, the actual cylinder of each oriental is its literal normalized-chain right cylinder.
```
def simplexCylinderIso (h : NormalizedSimplexIdentities) (m : ℕ) :
    cylinder.obj (h.object m) ≅
      (rightCylinder (SimplexComplex.directedComplex m (h.squared m))).realization :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.directedComplex
def OAI.Thomason.Construction.NormalizedSimplexIdentities.orientalUnitIso line 123
Source documentation
On an actual oriental, the abelianization unit is a strict isomorphism.
```
def orientalUnitIso (m : ℕ) :
    h.object m ≅ (StrictOmegaCategory.Abelianization.complex (h.object m)).realization :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.orientalUnitIso_hom line 127

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.constructedChainModelComparison_projection line 132

Source documentation

The concrete chain comparison commutes with interval collapse.

theorem constructedChainModelComparison_projection (m : SimplexCategory) :
    h.constructedChainModelComparison.hom.app m ≫
        StrictOmegaCategory.GrayChainExtension.modelCollapse.app (h.object m.len) =
      h.cylinderProjection.app m ≫ StrictOmegaCategory.Abelianization.unit (h.object m.len) := by
…

Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unit

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.extendedComparison_projection line 157

Source documentation

A map into the extended cylinder with the actual chain comparison has the prescribed collapse. No invertibility of that map is needed here.

theorem extendedComparison_projection (m : SimplexCategory)
    (f : h.cylinderObject m.len ⟶ StrictOmegaCategory.GrayChainExtension.cylinder.obj
      (h.object m.len))
    (hf : f ≫ StrictOmegaCategory.GrayChainExtension.comparison.app (h.object m.len) =
      h.constructedChainModelComparison.hom.app m) :
    f ≫ StrictOmegaCategory.GrayChainExtension.projection.app (h.object m.len) =
      h.cylinderProjection.app m := by
…