OAI/CategoryTheory/Thomason/Gray/CylinderAssembly.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Composition generation by normalized simplex atoms

Steiner, Omega-categories and chain complexes (2004), Definition 3.2, Example 3.8 and Theorem 5.6 (arXiv:math/0403237v2), identify these exact normalized-chain atoms and prove composition generation. The principal atoms in this specialization are fixed by their entire chain tables.

  1. def OAI.Thomason.Construction.SimplexComplex.signedPart line 28

    Source documentation

    The positive or negative part of an integral chain, coefficient by coefficient.

    noncomputable def signedPart {m p : ℕ} (a : Bool) (x : Chains m p) : Chains m p :=
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains

  2. def OAI.Thomason.Construction.SimplexComplex.topBasis line 32

    Source documentation

    The distinguished top-dimensional simplex basis element.

    def topBasis (m : ℕ) : Basis m m := OrderEmbedding.ofStrictMono id strictMono_id

    Mentions: OAI.Thomason.Construction.SimplexComplex.Basis

  3. def OAI.Thomason.Construction.SimplexComplex.IsBasisAtom line 35

    Source documentation

    Steiner's downward-recursive formula specifies every entry of an atom.

    def IsBasisAtom (h : NormalizedSimplexIdentities) {m p : ℕ}
    (b : Basis m p) (x : h.object m) : Prop :=
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis

  4. theorem OAI.Thomason.Construction.SimplexComplex.IsBasisAtom.unique line 42

    Source documentation

    The full table formula characterizes an atom uniquely.

    theorem IsBasisAtom.unique (h : NormalizedSimplexIdentities) {m p : ℕ}
    {b : Basis m p} {x y : h.object m} (hx : IsBasisAtom h b x) (hy : IsBasisAtom h b y) : x = y := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.IsBasisAtom

  5. structure OAI.Thomason.Construction.SimplexAtomsInput line 68

    Source documentation

    Precisely the published atom facts used in the full-face argument.

    structure SimplexAtomsInput (h : NormalizedSimplexIdentities) where
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

  6. def OAI.Thomason.Construction.SimplexAtomsInput.atom line 84

    Source documentation

    The actual simplex atom indexed by an increasing tuple.

    noncomputable def atom {m p : ℕ} (b : SimplexComplex.Basis m p) : h.object m :=
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Basis

  7. theorem OAI.Thomason.Construction.SimplexAtomsInput.atom_source line 87
  8. theorem OAI.Thomason.Construction.SimplexAtomsInput.atom_target line 93
  9. theorem OAI.Thomason.Construction.StrictOmegaCategory.Hom.object_boundary line 122

    Source documentation

    Taking an object boundary commutes with every strict functor.

    theorem Hom.object_boundary (f : C ⟶ D) (a : Bool) (x : C) :
    f.toOneFunctor.obj (C.boundaryObject a x) = D.boundaryObject a (f.toFun x) :=
…
  10. def OAI.Thomason.Construction.StrictOmegaCategory.orderedLabel line 127

    Source documentation

    An ordered object function extends uniquely to a strict poset label.

    def orderedLabel {E : Type} [Preorder E] (f : Objects C → E)
    (hf : ∀ x : C, f (C.boundaryObject false x) ≤ f (C.boundaryObject true x)) :
    C ⟶ StrictPoset.category E where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Objects, OAI.Thomason.Construction.StrictPoset.category

  11. theorem OAI.Thomason.Construction.StrictOmegaCategory.orderedLabel_object line 164
  12. theorem OAI.Thomason.Construction.StrictOmegaCategory.hom_poset_ext line 173

    Source documentation

    A strict poset label is determined by its action on object cells.

    theorem hom_poset_ext {E : Type} [Preorder E] {f g : C ⟶ StrictPoset.category E}
    (he : ∀ x : Objects C, f.toFun x.val = g.toFun x.val) : f = g := by
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.Objects

  13. def OAI.Thomason.Construction.NormalizedSimplexIdentities.ordinalLabel line 196

    Source documentation

    The canonical strict map from an oriental to its ordered vertices.

    noncomputable def ordinalLabel (m : ℕ) : h.object m ⟶ StrictPoset.category (Fin (m + 1)) :=
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category

  14. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.ordinalLabel_vertex line 201
  15. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.ordinalLabel_naturality line 209

    Source documentation

    Ordinal labelling commutes with every simplex operator, including degeneracies.

    theorem ordinalLabel_naturality {m n : ℕ} (f : Fin (m + 1) →o Fin (n + 1)) :
    h.map f ≫ h.ordinalLabel n = h.ordinalLabel m ≫ StrictPoset.map f := by
…

    Mentions: OAI.Thomason.Construction.StrictPoset.map

  16. def OAI.Thomason.Construction.SimplexComplex.rise line 237
  17. def OAI.Thomason.Construction.SimplexComplex.prismBasis line 243

    Source documentation

    The image of a prism generator is the normalized tuple with the final upper endpoint appended.

    noncomputable def prismBasis {m n : ℕ} (f g : Fin (m + 1) →o Fin (n + 1))
    (hfg : ∀ i, f i ≤ g i) (p : ℕ) (s : Basis m p) : Chains n (p + 1) :=
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.Chains

  18. def OAI.Thomason.Construction.SimplexComplex.prism line 247
  19. theorem OAI.Thomason.Construction.SimplexComplex.prism_single line 252
  20. theorem OAI.Thomason.Construction.SimplexComplex.prismBasis_nonneg line 257
  21. theorem OAI.Thomason.Construction.SimplexComplex.prism_positive line 262

    Source documentation

    The new prism operator preserves the specified positive cones.

    theorem prism_positive {m n p : ℕ} (f g : Fin (m + 1) →o Fin (n + 1))
    (hfg : ∀ i, f i ≤ g i) {x : Chains m p} (hx : x ∈ positive m p) :
    prism f g hfg p x ∈ positive n (p + 1) := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, OAI.Thomason.Construction.SimplexComplex.prism

  22. theorem OAI.Thomason.Construction.SimplexComplex.prismBasis_stationary line 273

    Source documentation

    On any simplex whose final vertex is fixed, the whole prism generator vanishes by normalization.

    theorem prismBasis_stationary {m n p : ℕ} (f g : Fin (m + 1) →o Fin (n + 1))
    (hfg : ∀ i, f i ≤ g i) (s : Basis m p) (he : f (s (Fin.last p)) = g (s (Fin.last p))) :
    prismBasis f g hfg p s = 0 := tuple_append_eq_zero _ _ _ he

    Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.prismBasis, OAI.Thomason.Construction.SimplexComplex.tuple_append_eq_zero

  23. theorem OAI.Thomason.Construction.SimplexComplex.old_initial_or_constant_tail line 279

    Source documentation

    Sieve membership of the penultimate vertex gives an entirely old initial segment; otherwise both final vertices lie in the constant new part.

    theorem old_initial_or_constant_tail {E : Type*} [Preorder E] {A : Set E}
    (hA : IsLowerSet A) {n p : ℕ} (f g : E →o Fin (n + 1))
    (hagree : ∀ x ∈ A, f x = g x)
    (hconstant : ∀ x ∉ A, ∀ y ∉ A, g x = g y)
    (s : Fin (p + 2) →o E) :
    (∀ i : Fin (p + 1), f (s i.castSucc) = g (s i.castSucc)) ∨
      g (s (Fin.last (p + 1))) = g (s (Fin.last p).castSucc) := by
…
  24. theorem OAI.Thomason.Construction.SimplexComplex.relative_prism_last_face_cancel line 299

    Source documentation

    The exceptional-face identity needed in the differential of the prism, now derived from exactly the order/sieve hypotheses of the manuscript.

    theorem relative_prism_last_face_cancel {E : Type*} [Preorder E] {A : Set E}
    (hA : IsLowerSet A) {n p : ℕ} (f g : E →o Fin (n + 1))
    (hfg : ∀ x, f x ≤ g x) (hagree : ∀ x ∈ A, f x = g x)
    (hconstant : ∀ x ∉ A, ∀ y ∉ A, g x = g y)
    (s : Fin (p + 2) →o E) :
    tuple (append (initial (f.comp s)) (g (s (Fin.last (p + 1))))
      ((hfg _).trans (g.monotone (s.monotone (Fin.le_last _))))) -
    tuple (append (initial (f.comp s)) (g (s (Fin.last p).castSucc)) (hfg _)) =
      tuple (g.comp s) :=
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.tuple, OAI.Thomason.Construction.SimplexComplex.append, OAI.Thomason.Construction.SimplexComplex.initial

  25. theorem OAI.Thomason.Construction.SimplexComplex.deleteTuple_last line 324
  26. theorem OAI.Thomason.Construction.SimplexComplex.rise_delete_castSucc line 331
  27. theorem OAI.Thomason.Construction.SimplexComplex.rise_boundary line 351

    Source documentation

    The prism's boundary identity on weakly increasing tuples, with exactly its old-initial-segment/constant-final-segment hypothesis.

    theorem rise_boundary (h : NormalizedSimplexIdentities) {n p : ℕ}
    (f g : Fin (p + 2) →o Fin (n + 1)) (hfg : ∀ i, f i ≤ g i)
    (hcases : (∀ i : Fin (p + 1), f i.castSucc = g i.castSucc) ∨
      g (Fin.last (p + 1)) = g (Fin.last p).castSucc) :
    differential n (p + 1) (rise f g hfg) =
      (∑ i : Fin (p + 2), ((-1 : ℤ) ^ (i : ℕ)) •
        rise (deleteTuple f i) (deleteTuple g i) (fun j => hfg (i.succAbove j))) +
      ((-1 : ℤ) ^ (p + 1)) • (tuple g - tuple f) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.rise, OAI.Thomason.Construction.SimplexComplex.deleteTuple, OAI.Thomason.Construction.SimplexComplex.tuple

  28. theorem OAI.Thomason.Construction.SimplexComplex.prism_differentialBasis line 370
  29. theorem OAI.Thomason.Construction.SimplexComplex.prismBasis_boundary line 380

    Source documentation

    The signed differential formula for each basis prism, derived from the actual sieve hypotheses rather than assumed as a cylinder input.

    theorem prismBasis_boundary (h : NormalizedSimplexIdentities) {m n p : ℕ}
    {A : Set (Fin (m + 1))} (hA : IsLowerSet A)
    (f g : Fin (m + 1) →o Fin (n + 1)) (hfg : ∀ i, f i ≤ g i)
    (hagree : ∀ x ∈ A, f x = g x)
    (hconstant : ∀ x ∉ A, ∀ y ∉ A, g x = g y) (s : Basis m (p + 1)) :
    differential n (p + 1) (prismBasis f g hfg (p + 1) s) =
      prism f g hfg p (differentialBasis m p s) +
      ((-1 : ℤ) ^ (p + 1)) • (mapBasis g (p + 1) s - mapBasis f (p + 1) s) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.prismBasis, OAI.Thomason.Construction.SimplexComplex.prism, OAI.Thomason.Construction.SimplexComplex.differentialBasis, OAI.Thomason.Construction.SimplexComplex.mapBasis

  30. theorem OAI.Thomason.Construction.SimplexComplex.rise_boundary_zero line 398
  31. theorem OAI.Thomason.Construction.SimplexComplex.prism_boundary line 434

    Source documentation

    Extend the basis boundary identity by linearity in every positive degree.

    theorem prism_boundary (p : ℕ) (x : Chains m (p + 1)) :
    differential n (p + 1) (prism f g hfg (p + 1) x) =
      prism f g hfg p (differential m p x) +
        ((-1 : ℤ) ^ (p + 1)) • (mapChains g (p + 1) x - mapChains f (p + 1) x) := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.prism, OAI.Thomason.Construction.SimplexComplex.mapChains

  32. theorem OAI.Thomason.Construction.SimplexComplex.prism_boundary_zero line 450

    Source documentation

    Degree zero of the same boundary identity.

    theorem prism_boundary_zero (x : Chains m 0) :
    differential n 0 (prism f g hfg 0 x) = mapChains g 0 x - mapChains f 0 x := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.prism, OAI.Thomason.Construction.SimplexComplex.mapChains

  33. def OAI.Thomason.Construction.SimplexComplex.prismApp line 466

    Source documentation

    The generator formula on the actual right tensor chain groups.

    noncomputable def prismApp : (p : ℕ) →
    (RightCylinder.group (directedComplex m (h.squared m)) p) →+ Chains n p
  | 0 =>
    { toFun := fun x => mapChains f 0 x.1 + mapChains g 0 x.2
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.directedComplex, OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.mapChains

  34. def OAI.Thomason.Construction.SimplexComplex.prismChainMap line 479

    Source documentation

    The positive relative prism is a genuine augmented directed chain map.

    noncomputable def prismChainMap (h : NormalizedSimplexIdentities) {m n : ℕ}
    {A : Set (Fin (m + 1))} (hA : IsLowerSet A)
    (f g : Fin (m + 1) →o Fin (n + 1)) (hfg : ∀ i, f i ≤ g i)
    (hagree : ∀ x ∈ A, f x = g x)
    (hconstant : ∀ x ∉ A, ∀ y ∉ A, g x = g y) : Hom
    (rightCylinder (directedComplex m (h.squared m))) (directedComplex n (h.squared n)) where
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.directedComplex

  35. def OAI.Thomason.Construction.SimplexComplex.strictPrism line 523

    Source documentation

    Strict realization of the explicitly constructed positive prism map.

    noncomputable def strictPrism :
    StrictOmegaCategory.Hom
      (rightCylinder (directedComplex m (h.squared m))).realization
      (directedComplex n (h.squared n)).realization :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom, OAI.Thomason.Construction.SimplexComplex.directedComplex

  36. theorem OAI.Thomason.Construction.SimplexComplex.prismChainMap_endpoint line 530
  37. theorem OAI.Thomason.Construction.SimplexComplex.strictPrism_endpoint line 539

    Source documentation

    The realized prism has exactly the two prescribed strict endpoint functors.

    theorem strictPrism_endpoint (a : Bool)
    (x : (directedComplex m (h.squared m)).realization) :
    strictPrism h hA f g hfg hagree hconstant
      ((RightCylinder.endpoint (directedComplex m (h.squared m)) a).realization x) =
      (directedMap (h.squared m) (h.squared n) (if a then g else f)
        (h.naturality _)).realization x := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.directedComplex, OAI.Thomason.Construction.SimplexComplex.strictPrism, OAI.Thomason.Construction.SimplexComplex.directedMap

  38. theorem OAI.Thomason.Construction.SimplexComplex.rise_eq_zero_of_not_strictMono line 560

    Source documentation

    A repeated lower image makes the entire normalized prism tuple zero.

    theorem rise_eq_zero_of_not_strictMono {m n : ℕ}
    (f g : Fin (m + 1) →o Fin (n + 1)) (hfg : ∀ i, f i ≤ g i)
    (hf : ¬StrictMono f) : rise f g hfg = 0 := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.rise

  39. theorem OAI.Thomason.Construction.SimplexComplex.prism_precomp line 575

    Source documentation

    The prism operator commutes with all simplex maps, including degeneracies. This is an equality in every chain degree, not just on top-dimensional atoms.

    theorem prism_precomp {l m n : ℕ} (f g : Fin (m + 1) →o Fin (n + 1))
    (hfg : ∀ i, f i ≤ g i) (a : Fin (l + 1) →o Fin (m + 1)) (p : ℕ)
    (x : Chains l p) :
    prism f g hfg p (mapChains a p x) =
      prism (f.comp a) (g.comp a) (fun i => hfg (a i)) p x := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.prism, OAI.Thomason.Construction.SimplexComplex.mapChains

  40. theorem OAI.Thomason.Construction.SimplexComplex.prism_eq_zero_of_eq line 603

    Source documentation

    A pointwise fixed pair has a zero prism in every degree.

    theorem prism_eq_zero_of_eq {m n : ℕ} (f g : Fin (m + 1) →o Fin (n + 1))
    (hfg : ∀ i, f i ≤ g i) (he : ∀ i, f i = g i) (p : ℕ) (x : Chains m p) :
    prism f g hfg p x = 0 := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.prism

  41. theorem OAI.Thomason.Construction.SimplexComplex.prism_stationary line 612

    Source documentation

    Restricting to any simplex in the old part gives strict chain stationarity.

    theorem prism_stationary {l m n : ℕ} {A : Set (Fin (m + 1))}
    (f g : Fin (m + 1) →o Fin (n + 1)) (hfg : ∀ i, f i ≤ g i)
    (hagree : ∀ i ∈ A, f i = g i) (a : Fin (l + 1) →o Fin (m + 1))
    (ha : ∀ i, a i ∈ A) (p : ℕ) (x : Chains l p) :
    prism f g hfg p (mapChains a p x) = 0 := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.prism, OAI.Thomason.Construction.SimplexComplex.mapChains

  42. theorem OAI.Thomason.Construction.SimplexComplex.prismChainMap_stationary line 624

    Source documentation

    Stationarity is an equality of the complete directed chain maps on the old cylinder, including all lower-dimensional entries.

    theorem prismChainMap_stationary (h : NormalizedSimplexIdentities) {l m n : ℕ}
    {A : Set (Fin (m + 1))} (hA : IsLowerSet A)
    (f g : Fin (m + 1) →o Fin (n + 1)) (hfg : ∀ i, f i ≤ g i)
    (hagree : ∀ i ∈ A, f i = g i)
    (hconstant : ∀ x ∉ A, ∀ y ∉ A, g x = g y)
    (a : Fin (l + 1) →o Fin (m + 1)) (ha : ∀ i, a i ∈ A)
    (p : ℕ) (x : RightCylinder.group (directedComplex l (h.squared l)) p) :
    (prismChainMap h hA f g hfg hagree hconstant).app p
      ((RightCylinder.map (directedMap (h.squared l) (h.squared m) a (h.naturality a))).app p x) =
      mapChains (f.comp a) p ((RightCylinder.projection (directedComplex l (h.squared l))).app p x) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.directedComplex, OAI.Thomason.Construction.SimplexComplex.prismChainMap, OAI.Thomason.Construction.SimplexComplex.directedMap, OAI.Thomason.Construction.SimplexComplex.mapChains

  43. theorem OAI.Thomason.Construction.SimplexComplex.strictPrism_stationary line 648

    Source documentation

    The new relative prism is stationary as a strict functor after applying Steiner realization; it is not merely zero on top chains.

    theorem strictPrism_stationary (h : NormalizedSimplexIdentities) {l m n : ℕ}
    {A : Set (Fin (m + 1))} (hA : IsLowerSet A)
    (f g : Fin (m + 1) →o Fin (n + 1)) (hfg : ∀ i, f i ≤ g i)
    (hagree : ∀ i ∈ A, f i = g i)
    (hconstant : ∀ x ∉ A, ∀ y ∉ A, g x = g y)
    (a : Fin (l + 1) →o Fin (m + 1)) (ha : ∀ i, a i ∈ A)
    (x : (rightCylinder (directedComplex l (h.squared l))).realization) :
    strictPrism h hA f g hfg hagree hconstant
      ((RightCylinder.map (directedMap (h.squared l) (h.squared m) a (h.naturality a))).realization x) =
    (directedMap (h.squared l) (h.squared n) (f.comp a) (h.naturality _)).realization
      ((RightCylinder.projection (directedComplex l (h.squared l))).realization x) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.directedComplex, OAI.Thomason.Construction.SimplexComplex.strictPrism, OAI.Thomason.Construction.SimplexComplex.directedMap

  44. def OAI.Thomason.Construction.NormalizedSimplexIdentities.cylinderObject line 689
  45. def OAI.Thomason.Construction.NormalizedSimplexIdentities.cylinderMap line 692
  46. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.cylinderMap_id line 697
  47. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.cylinderMap_comp line 714
  48. def OAI.Thomason.Construction.NormalizedSimplexIdentities.cylinderCosimplicial line 731

    Source documentation

    The cosimplicial diagram of the actual strict chain cylinders.

    noncomputable def cylinderCosimplicial : SimplexCategory ⥤ StrictOmegaCategory.{0} where
…
  49. def OAI.Thomason.Construction.NormalizedSimplexIdentities.cylinderEndpoint line 737
  50. def OAI.Thomason.Construction.NormalizedSimplexIdentities.cylinderProjection line 748
  51. structure OAI.Thomason.Construction.RightGrayInput line 764

    Source documentation

    The exact published input about tensoring with the oriented interval. The natural isomorphism compares to the explicitly constructed chain tensor; its endpoint and projection equations fix the right-tensor convention.

    structure RightGrayInput (h : NormalizedSimplexIdentities) where
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

  52. theorem OAI.Thomason.Construction.RightGrayInput.preservesColimits line 785

    Source documentation

    Cocontinuity follows from the published right internal-hom adjunction.

    theorem preservesColimits : Limits.PreservesColimitsOfSize.{0, 0} G.cylinder := by
…
  53. def OAI.Thomason.Construction.RightGrayInput.prism line 790

    Source documentation

    The constructed chain prism transported through the published comparison.

    noncomputable def prism {m n : ℕ} {A : Set (Fin (m + 1))} (hA : IsLowerSet A)
    (f g : Fin (m + 1) →o Fin (n + 1)) (hfg : ∀ i, f i ≤ g i)
    (hagree : ∀ i ∈ A, f i = g i) (hconstant : ∀ x ∉ A, ∀ y ∉ A, g x = g y) :
    G.cylinder.obj (h.object m) ⟶ h.object n :=
…
  54. theorem OAI.Thomason.Construction.RightGrayInput.prism_endpoint line 798

    Source documentation

    The comparison preserves the two endpoint functors of the new prism.

    theorem prism_endpoint {m n : ℕ} {A : Set (Fin (m + 1))} (hA : IsLowerSet A)
    (f g : Fin (m + 1) →o Fin (n + 1)) (hfg : ∀ i, f i ≤ g i)
    (hagree : ∀ i ∈ A, f i = g i) (hconstant : ∀ x ∉ A, ∀ y ∉ A, g x = g y)
    (a : Bool) :
    (G.endpoint a).app (h.object m) ≫ G.prism hA f g hfg hagree hconstant =
      h.map (if a then g else f) := by
…
  55. theorem OAI.Thomason.Construction.RightGrayInput.prism_stationary line 823

    Source documentation

    Stationarity of the complete strict chain prism passes to the right Gray cylinder along the published natural comparison.

    theorem prism_stationary {l m n : ℕ} {A : Set (Fin (m + 1))} (hA : IsLowerSet A)
    (f g : Fin (m + 1) →o Fin (n + 1)) (hfg : ∀ i, f i ≤ g i)
    (hagree : ∀ i ∈ A, f i = g i) (hconstant : ∀ x ∉ A, ∀ y ∉ A, g x = g y)
    (a : Fin (l + 1) →o Fin (m + 1)) (ha : ∀ i, a i ∈ A) :
    G.cylinder.map (h.map a) ≫ G.prism hA f g hfg hagree hconstant =
      G.projection.app (h.object l) ≫ h.map (f.comp a) := by
…
  56. theorem OAI.Thomason.Construction.RightGrayInput.cylinder_hom_ext line 888

    Source documentation

    Equality on all simplex cylinders is equality on the colimit cylinder.

    theorem cylinder_hom_ext {Y : StrictOmegaCategory.{0}}
    {P Q : G.cylinder.obj c.pt ⟶ Y}
    (he : ∀ j, G.cylinder.map (c.ι.app j) ≫ P = G.cylinder.map (c.ι.app j) ≫ Q) : P = Q := by
…
  57. theorem OAI.Thomason.Construction.RightGrayInput.assemble_cylinder line 895

    Source documentation

    Compatible local strict cylinders assemble to a unique whole cylinder.

    theorem assemble_cylinder {Y : StrictOmegaCategory.{0}}
    (P : ∀ j, G.cylinder.obj (D.obj j) ⟶ Y)
    (hP : ∀ {i j} (a : i ⟶ j), G.cylinder.map (D.map a) ≫ P j = P i) :
    ∃! Q : G.cylinder.obj c.pt ⟶ Y,
      ∀ j, G.cylinder.map (c.ι.app j) ≫ Q = P j := by
…
  58. theorem OAI.Thomason.Construction.RightGrayInput.assembled_endpoint line 911

    Source documentation

    The endpoint of an assembled cylinder is the map prescribed on every piece of the colimit.

    theorem assembled_endpoint {Y : StrictOmegaCategory.{0}}
    (P : G.cylinder.obj c.pt ⟶ Y) (F : c.pt ⟶ Y) (a : Bool)
    (hF : ∀ j, (G.endpoint a).app (D.obj j) ≫ G.cylinder.map (c.ι.app j) ≫ P =
      c.ι.app j ≫ F) :
    (G.endpoint a).app c.pt ≫ P = F := by
…
  59. theorem OAI.Thomason.Construction.RightGrayInput.assembled_stationary line 929

    Source documentation

    To prove stationarity on a subcategory presented as a colimit, it suffices to prove the factorization on the whole cylinder of every piece.

    theorem assembled_stationary {X Y : StrictOmegaCategory.{0}}
    (a : c.pt ⟶ X) (v : c.pt ⟶ Y) (P : G.cylinder.obj X ⟶ Y)
    (hs : ∀ j, G.cylinder.map (c.ι.app j ≫ a) ≫ P =
      G.projection.app (D.obj j) ≫ (c.ι.app j ≫ v)) :
    G.cylinder.map a ≫ P = G.projection.app c.pt ≫ v := by
…