DirectedGlobeFaces.lean`

82 declarations, 0 contain sorry, 0 declared as axioms

Ordered atoms of globes and their right cylinders

The two lower rows of a globe atom are singleton faces. Their linear rank orders all negative faces before the atom and all positive faces after it. This supplies generation of each actual globe-cylinder piece.

def OAI.Thomason.Construction.DirectedGlobeComplex.basisAtom line 27
theorem OAI.Thomason.Construction.DirectedGlobeComplex.basisAtom_top line 30
theorem OAI.Thomason.Construction.DirectedGlobeComplex.basisAtom_above line 36
theorem OAI.Thomason.Construction.DirectedGlobeComplex.basisAtom_below line 41
def OAI.Thomason.Construction.DirectedGlobeComplex.basisHeight line 51
theorem OAI.Thomason.Construction.DirectedGlobeComplex.basisAtom_sideHeight line 54
def OAI.Thomason.Construction.DirectedGlobeComplex.orderedAtomBasis line 70
theorem OAI.Thomason.Construction.DirectedGlobeComplex.orderedAtomBasis_sideHeight line 92
def OAI.Thomason.Construction.DirectedGlobeComplex.cylinderOrderedAtomBasis line 95
theorem OAI.Thomason.Construction.DirectedGlobeComplex.cylinder_generated line 98
def OAI.Thomason.Construction.SimplicialCylinder.ends line 124
Source documentation
Two disjoint copies of a simplicial set, in each degree.
```
def ends (X : SSet.{u}) : SSet.{u} where
…
```
def OAI.Thomason.Construction.SimplicialCylinder.desc line 131
Source documentation
The map specified independently on the two ends.
```
def desc {X Y : SSet.{u}} (f g : X ⟶ Y) : ends X ⟶ Y where
…
```
Mentions: OAI.Thomason.Construction.SimplicialCylinder.ends
def OAI.Thomason.Construction.SimplicialCylinder.zero line 139
def OAI.Thomason.Construction.SimplicialCylinder.one line 142
theorem OAI.Thomason.Construction.SimplicialCylinder.zero_desc line 146
theorem OAI.Thomason.Construction.SimplicialCylinder.one_desc line 149
def OAI.Thomason.Construction.SimplicialCylinder.inclusion line 152
Source documentation
The actual inclusion of the two cylinder ends.
```
noncomputable def inclusion (X : SSet.{u}) : ends X ⟶ X ⊗ Δ[1] :=
…
```
Mentions: OAI.Thomason.Construction.SimplicialCylinder.ends
theorem OAI.Thomason.Construction.SimplicialCylinder.zero_inclusion line 156
theorem OAI.Thomason.Construction.SimplicialCylinder.one_inclusion line 159
instance OAI.Thomason.Construction.SimplicialCylinder.inclusion_mono line 162
Source documentation
The two ends are disjoint, and each includes injectively.
```
instance inclusion_mono (X : SSet.{u}) : Mono (inclusion X) := by
…
```
Mentions: OAI.Thomason.Construction.SimplicialCylinder.inclusion
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.faceGenerator_of_dimension line 206
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.faceGenerator_zero line 211
def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unitCell line 221
Source documentation
The finite table of the additive classes of a strict cell's faces.
```
def unitCell (x : C) : DirectedComplex.Cell (complex C) where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unitCell_table line 234
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unitCell_face line 237
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.face_comp_below line 256
Source documentation
Lower faces of a composite are the common lower faces of its factors.
```
theorem face_comp_below (a : Bool) {m n : ℕ} (hmn : m < n) (x y : C)
    (h : C.target n x = C.source n y) :
    C.face a m (C.comp n x y h) = C.face a m x := by
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unitCell_comp line 262
def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unit line 288
Source documentation
The concrete unit into the realization of lambda.
```
def unit : C ⟶ (complex C).realization where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex
def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluate line 317
Source documentation
The degree n component extracted from a strict functor to nu K.
```
def evaluate (f : C ⟶ K.realization) (n : ℕ) : Chains C n →+ K.group n :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Chains
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluate_generator line 328
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluate_faceGenerator line 332
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluate_differential line 339
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluate_augmentation line 350
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluate_positive line 359
def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluateHom line 370
Source documentation
The augmented positive chain map obtained from an arbitrary strict map.
```
def evaluateHom (f : C ⟶ K.realization) : DirectedComplex.Hom (complex C) K where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unit_evaluate line 377
Source documentation
Evaluation followed by the constructed unit recovers every strict cell.
```
theorem unit_evaluate (f : C ⟶ K.realization) :
    StrictOmegaCategory.Hom.comp (unit C) (evaluateHom f).realization = f := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom.comp, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unit, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluateHom
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unitCell_top line 386
Source documentation
The generator of any bounded cell is its unit table at that degree.
```
theorem unitCell_top (n : ℕ) (x : Bounded C n) :
    (unitCell C x.val).table false n = generator C n x :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Bounded, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unitCell, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.generator
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluate_unit line 391
Source documentation
Every positive chain map is uniquely recovered from its realized unit.
```
theorem evaluate_unit (g : DirectedComplex.Hom (complex C) K) :
    evaluateHom (StrictOmegaCategory.Hom.comp (unit C) g.realization) = g := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluateHom, OAI.Thomason.Construction.StrictOmegaCategory.Hom.comp, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unit
def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.homEquiv line 406
Source documentation
The actual lambda-nu hom-set equivalence.
```
def homEquiv (C : StrictOmegaCategory.{0}) (K : DirectedComplex.{0}) :
    DirectedComplex.Hom (complex C) K ≃ (C ⟶ K.realization) where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex
def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.map line 437
Source documentation
The chain map induced by an arbitrary strict functor.
```
def map (f : C ⟶ D) : DirectedComplex.Hom (complex C) (complex D) :=
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.map_generator line 440
def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.functor line 447
Source documentation
The concrete strict abelianization functor.
```
def functor : StrictOmegaCategory.{0} ⥤ DirectedComplex.{0} where
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluate_naturality line 470
Source documentation
Naturality in the strict source, checked on actual bounded-cell generators.
```
theorem evaluate_naturality {K : DirectedComplex.{0}} (f : C ⟶ D) (g : D ⟶ K.realization) :
    DirectedComplex.Hom.comp (map f) (evaluateHom g) = evaluateHom (f ≫ g) := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom.comp, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.map, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.evaluateHom
def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.adjunction line 485
Source documentation
Lambda is left adjoint to the actual positive-table realization nu.
```
def adjunction : functor ⊣ realizationFunctor :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.functor
theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.preservesColimits line 497
Source documentation
The abelianization carries every existing strict colimit to the corresponding directed-complex colimit, including the pasted globe squares.
```
theorem preservesColimits : Limits.PreservesColimitsOfSize.{0, 0} functor := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.functor
def OAI.Thomason.Construction.DirectedGlobeComplex.abelianizationToGlobe line 524
Source documentation
Evaluation from the additive strict-cell presentation to the explicit positive globe chains.
```
def abelianizationToGlobe (n : ℕ) :
    DirectedComplex.Hom (StrictOmegaCategory.Abelianization.complex (StrictOmegaCategory.Globe.category n)) (complex n) :=
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.DirectedGlobeComplex.complex
def OAI.Thomason.Construction.DirectedGlobeComplex.globeToAbelianization line 529
Source documentation
The universal top cell supplies the reverse positive chain map.
```
def globeToAbelianization (n : ℕ) :
    DirectedComplex.Hom (complex n) (StrictOmegaCategory.Abelianization.complex (StrictOmegaCategory.Globe.category n)) :=
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedGlobeComplex.complex, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category
theorem OAI.Thomason.Construction.DirectedGlobeComplex.globeToAbelianization_top line 533
theorem OAI.Thomason.Construction.DirectedGlobeComplex.abelianizationToGlobe_top line 540
theorem OAI.Thomason.Construction.DirectedGlobeComplex.abelianizationToGlobe_inverse line 547
theorem OAI.Thomason.Construction.DirectedGlobeComplex.globeToAbelianization_inverse line 557
def OAI.Thomason.Construction.DirectedGlobeComplex.abelianizationIso line 568
Source documentation
The positive chain presentation of a strict globe is exactly the explicit globe complex, not an additional comparison input.
```
def abelianizationIso (n : ℕ) : StrictOmegaCategory.Abelianization.complex (StrictOmegaCategory.Globe.category n) ≅ complex n where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.DirectedGlobeComplex.complex
def OAI.Thomason.Construction.DirectedGlobeComplex.abelianizationGlobeIso line 598
Source documentation
Naturality is proved through the actual lambda-nu adjunction, whose unit followed by globe evaluation is the canonical globe isomorphism.
```
def abelianizationGlobeIso :
    StrictOmegaCategory.Globe.inclusion ⋙ StrictOmegaCategory.Abelianization.functor ≅
      chainFunctor :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.inclusion, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.functor, OAI.Thomason.Construction.DirectedGlobeComplex.chainFunctor
def OAI.Thomason.Construction.DirectedGlobeComplex.rightCylinderAbelianizationGlobeIso line 629
Source documentation
Tensoring the natural chain presentations with the right interval and realizing gives the exact globe restriction of the chain model.
```
def rightCylinderAbelianizationGlobeIso :
    StrictOmegaCategory.Globe.inclusion ⋙
        (StrictOmegaCategory.Abelianization.functor ⋙ rightCylinderFunctor ⋙ realizationFunctor) ≅
      rightGlobeCylinder :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.inclusion, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.functor, OAI.Thomason.Construction.DirectedGlobeComplex.rightGlobeCylinder
theorem OAI.Thomason.Construction.SimplexAtomsInput.atom_top line 661
Source documentation
The top chain of the chosen atom is its literal normalized basis element.
```
theorem atom_top {m p : ℕ} (b : Basis m p) (side : Bool) :
    (a.atom b).table side p = Finsupp.single b 1 := by
…
```
theorem OAI.Thomason.Construction.SimplexAtomsInput.atom_above_zero line 670
Source documentation
There are no atom chains above its basis dimension.
```
theorem atom_above_zero {m p : ℕ} (b : Basis m p) {n : ℕ} (hpn : p < n) (side : Bool) :
    (a.atom b).table side n = 0 := by
…
```
theorem OAI.Thomason.Construction.SimplexAtomsInput.atom_dimension line 675
theorem OAI.Thomason.Construction.SimplexAtomsInput.atom_dimension_iff line 680
Source documentation
The nonzero top chain detects the exact dimension of an atom.
```
theorem atom_dimension_iff {m p n : ℕ} (b : Basis m p) :
    (h.object m).DimensionLE n (a.atom b) ↔ p ≤ n := by
…
```

theorem OAI.Thomason.Construction.SimplexAtomsInput.positive_add_zero line 692

Source documentation

A normalized simplex's positive cone admits no nonzero cancellation.

theorem positive_add_zero {m p : ℕ} (x y : (directedComplex m (h.squared m)).group p)
    (hx : x ∈ (directedComplex m (h.squared m)).positive p)
    (hy : y ∈ (directedComplex m (h.squared m)).positive p) (he : x + y = 0) :
    x = 0 ∧ y = 0 := by
…

def OAI.Thomason.Construction.SimplexAtomsInput.basisLift line 705
Source documentation
Lift a normalized basis element to the corresponding actual strict cell.
```
def basisLift (m p : ℕ) : Chains m p →+ StrictOmegaCategory.Abelianization.Chains (h.object m) p :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Chains
theorem OAI.Thomason.Construction.SimplexAtomsInput.basisLift_single line 710
theorem OAI.Thomason.Construction.SimplexAtomsInput.basisLift_cell line 718
Source documentation
The basis lift recovers every bounded strict cell, using composition generation of the simplex atoms.
```
theorem basisLift_cell (m : ℕ) : ∀ x : h.object m, ∀ n (hx : (h.object m).DimensionLE n x),
    a.basisLift m n (x.table false n) =
      StrictOmegaCategory.Abelianization.generator (h.object m) n ⟨x, hx⟩ := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.generator
def OAI.Thomason.Construction.SimplexAtomsInput.toSimplexChains line 781
Source documentation
Evaluate the additive classes of strict cells in their original chains.
```
def toSimplexChains (_a : SimplexAtomsInput h) (m : ℕ) :
    Hom (StrictOmegaCategory.Abelianization.complex (h.object m))
      (directedComplex m (h.squared m)) :=
…
```
Mentions: OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex
def OAI.Thomason.Construction.SimplexAtomsInput.toSimplexApp line 787
Source documentation
Evaluation with explicit unbundled chain-group types.
```
def toSimplexApp (m n : ℕ) :
    StrictOmegaCategory.Abelianization.Chains (h.object m) n →+ Chains m n :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Chains
theorem OAI.Thomason.Construction.SimplexAtomsInput.toSimplexChains_generator line 791
theorem OAI.Thomason.Construction.SimplexAtomsInput.toSimplexChains_basisLift line 799
Source documentation
The strict-cell relations impose no additional normalized-chain relation.
```
theorem toSimplexChains_basisLift (m n : ℕ) (z : Chains m n) :
    a.toSimplexApp m n (a.basisLift m n z) = z := by
…
```
theorem OAI.Thomason.Construction.SimplexAtomsInput.basisLift_toSimplexChains line 809
Source documentation
Every additive strict-cell class is recovered by the basis inverse.
```
theorem basisLift_toSimplexChains (m n : ℕ)
    (z : StrictOmegaCategory.Abelianization.Chains (h.object m) n) :
    a.basisLift m n (a.toSimplexApp m n z) = z := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Chains
theorem OAI.Thomason.Construction.SimplexAtomsInput.toSimplexChains_injective line 822
Source documentation
In particular evaluation is injective in every degree.
```
theorem toSimplexChains_injective (m n : ℕ) :
    Function.Injective (a.toSimplexApp m n) := by
…
```
theorem OAI.Thomason.Construction.SimplexAtomsInput.basisLift_positive line 829
Source documentation
The inverse sends positive basis combinations to positive strict-cell classes.
```
theorem basisLift_positive (m n : ℕ) {z : Chains m n} (hz : z ∈ positive m n) :
    a.basisLift m n z ∈ StrictOmegaCategory.Abelianization.positive (h.object m) n := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.positive
def OAI.Thomason.Construction.SimplexAtomsInput.fromSimplexChains line 845
Source documentation
Differential compatibility follows from injectivity of the evaluated chains; the basis construction already gives both inverse equations.
```
def fromSimplexChains (m : ℕ) :
    Hom (directedComplex m (h.squared m))
      (StrictOmegaCategory.Abelianization.complex (h.object m)) where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex
def OAI.Thomason.Construction.SimplexAtomsInput.abelianizationIso line 863
Source documentation
The actual directed-complex isomorphism, with all positivity and augmentation information retained.
```
def abelianizationIso (m : ℕ) :
    StrictOmegaCategory.Abelianization.complex (h.object m) ≅
      directedComplex m (h.squared m) where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex
def OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap line 898
Source documentation
The chosen m-face of the universal n-cell. For m ≥ n this is its identity extension, so the same definition covers every pair of indices.
```
def faceMap (a : Bool) (m n : ℕ) : category m ⟶ category n :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap_top line 902
theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap_self line 905
theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap_comp line 910
Source documentation
The two iterated faces of a higher globe obey the strict globular law.
```
theorem faceMap_comp (a b : Bool) (m k n : ℕ) (hmk : m < k) :
    faceMap a m k ≫ faceMap b k n = faceMap a m n := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap
theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap_lift line 919
Source documentation
Precomposing the universal cell map with a face gives its actual source or target cell.
```
theorem faceMap_lift (C : StrictOmegaCategory) {n : ℕ} (x : C) (hx : C.DimensionLE n x)
    (a : Bool) (m : ℕ) :
    faceMap a m n ≫ lift C x hx =
      lift C (C.face a m x) (C.face_dimensionLE a m x) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory, OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.StrictOmegaCategory.Globe.lift
theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.truncated_iff_globe_test line 928
Source documentation
Truncation is exactly the pointwise n-boundary test on all universal finite cells. This supplies the dimension interface for an internal hom.
```
theorem truncated_iff_globe_test (C : StrictOmegaCategory) (n : ℕ) :
    C.IsTruncated n ↔ ∀ (m : ℕ) (f : category m ⟶ C) (a : Bool),
      f.toFun ((category m).face a n Cell.top) = f.toFun Cell.top := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.face
def OAI.Thomason.Construction.DirectedGlobeComplex.faceMap line 964
theorem OAI.Thomason.Construction.DirectedGlobeComplex.faceMap_top line 967
theorem OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe_faceMap line 974
Source documentation
The square from the actual free globe to its chain realization commutes on each source and target map.
```
theorem fromGlobe_faceMap (a : Bool) (m n : ℕ) :
    StrictOmegaCategory.Globe.faceMap a m n ≫ fromGlobe n =
      fromGlobe m ≫ (faceMap a m n).realization := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe, OAI.Thomason.Construction.DirectedGlobeComplex.faceMap
theorem OAI.Thomason.Construction.DirectedGlobeComplex.faceMap_right_endpoint line 985
Source documentation
The right-cylinder face maps preserve the two strict endpoint maps.
```
theorem faceMap_right_endpoint (a e : Bool) (m n : ℕ) :
    StrictOmegaCategory.Hom.comp (faceMap a m n).realization
      (RightCylinder.endpoint (complex n) e).realization =
      StrictOmegaCategory.Hom.comp (RightCylinder.endpoint (complex m) e).realization
        (RightCylinder.map (faceMap a m n)).realization := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom.comp, OAI.Thomason.Construction.DirectedGlobeComplex.faceMap, OAI.Thomason.Construction.DirectedGlobeComplex.complex
theorem OAI.Thomason.Construction.DirectedGlobeComplex.faceMap_right_projection line 997
Source documentation
Interval collapse also commutes with the concrete chain face map.
```
theorem faceMap_right_projection (a : Bool) (m n : ℕ) :
    StrictOmegaCategory.Hom.comp (RightCylinder.map (faceMap a m n)).realization
      (RightCylinder.projection (complex n)).realization =
      StrictOmegaCategory.Hom.comp (RightCylinder.projection (complex m)).realization
        (faceMap a m n).realization := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom.comp, OAI.Thomason.Construction.DirectedGlobeComplex.faceMap, OAI.Thomason.Construction.DirectedGlobeComplex.complex