OAI/CategoryTheory/Thomason/Gray/PastingGlobeCylinderRetractions.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Right cylinders preserve the actual pasted-globe chain pushouts

The explicit path-complex hom-set correspondence constructs the descended positive chain map. The subsequent realization gluing is a separate claim; no preservation of pushouts by realization is assumed here.

  1. abbrev OAI.Thomason.Construction.DirectedComplex.RightPath.rawApp line 25
  2. theorem OAI.Thomason.Construction.DirectedComplex.RightPath.rawApp_differential line 29
  3. def OAI.Thomason.Construction.DirectedComplex.RightPath.firstApp line 35
  4. def OAI.Thomason.Construction.DirectedComplex.RightPath.secondApp line 40
  5. def OAI.Thomason.Construction.DirectedComplex.RightPath.shiftedFrom line 45
  6. def OAI.Thomason.Construction.DirectedComplex.RightPath.first line 50
  7. def OAI.Thomason.Construction.DirectedComplex.RightPath.second line 58
  8. theorem OAI.Thomason.Construction.DirectedComplex.RightPath.shiftedFrom_positive line 71
  9. theorem OAI.Thomason.Construction.DirectedComplex.RightPath.shiftedFrom_differential_zero line 76
  10. theorem OAI.Thomason.Construction.DirectedComplex.RightPath.shiftedFrom_differential_succ line 80
  11. def OAI.Thomason.Construction.DirectedComplex.RightPath.uncurryApp line 91
  12. def OAI.Thomason.Construction.DirectedComplex.RightPath.uncurry line 104

    Source documentation

    Uncurrying preserves positivity, augmentation, and the signed differential.

    def uncurry (f : Hom K (complex L)) : Hom (rightCylinder K) L where
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.RightPath.complex, OAI.Thomason.Construction.DirectedComplex.rightCylinder

  13. theorem OAI.Thomason.Construction.DirectedComplex.RightPath.uncurry_curry line 137
  14. theorem OAI.Thomason.Construction.DirectedComplex.RightPath.curry_uncurry line 147
  15. def OAI.Thomason.Construction.DirectedComplex.RightPath.homEquiv line 178

    Source documentation

    The actual hom-set correspondence for the right interval chain tensor.

    def homEquiv : Hom (rightCylinder K) L ≃ Hom K (complex L) where
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.RightPath.complex

  16. theorem OAI.Thomason.Construction.DirectedComplex.RightPath.curry_naturality line 184
  17. theorem OAI.Thomason.Construction.DirectedComplex.RightPath.uncurry_naturality line 215
  18. theorem OAI.Thomason.Construction.DirectedComplex.RightPath.rightCylinder_isPushout line 224

    Source documentation

    The positive path-complex correspondence gives an actual chain pushout of right cylinders, with the prescribed four maps.

    theorem rightCylinder_isPushout {A B C P : DirectedComplex.{0}}
    {i : A ⟶ B} {j : A ⟶ C} {l : B ⟶ P} {r : C ⟶ P}
    (hP : IsPushout i j l r) :
    IsPushout (C := DirectedComplex.{0}) (RightCylinder.map i) (RightCylinder.map j)
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.RightCylinder.map

  19. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.rightCylinder_abelianization_isPushout line 274

    Source documentation

    The actual positive chain presentation of the pasted-globe cylinder is a pushout of the two globe-cylinder chain presentations.

    theorem rightCylinder_abelianization_isPushout (n m k : ℕ) :
    IsPushout (C := DirectedComplex.{0})
…
  20. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.zeroEquiv line 301
  21. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.succEquiv line 309
  22. instance OAI.Thomason.Construction.PastingGlobeCylinderBasis.finiteBasis line 322
  23. instance OAI.Thomason.Construction.PastingGlobeCylinderBasis.fintypeBasis line 327
  24. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficientHom line 330

    Source documentation

    Every literal coefficient is an additive map.

    def coefficientHom {n k p : ℕ} (hkn : k < n) (b : Basis n k p) :
    (Cylinder hkn).group p →+ ℤ where
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder

  25. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.toFinsupp line 349

    Source documentation

    The finitely supported coordinate function of an actual cylinder chain.

    def toFinsupp {n k p : ℕ} (hkn : k < n) (x : (Cylinder hkn).group p) :
    Basis n k p →₀ ℤ :=
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis

  26. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.toFinsupp_apply line 353
  27. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.fromFinsupp line 358

    Source documentation

    Reassemble a chain from its finite basis coefficients.

    def fromFinsupp {n k p : ℕ} (hkn : k < n) :
    (Basis n k p →₀ ℤ) →ₗ[ℤ] (Cylinder hkn).group p :=
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder

  28. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.fromFinsupp_single line 362
  29. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient_fromFinsupp line 367

    Source documentation

    Reassembly recovers each coefficient exactly.

    theorem coefficient_fromFinsupp {n k p : ℕ} (hkn : k < n)
    (b : Basis n k p) (u : Basis n k p →₀ ℤ) :
    coefficient hkn b (fromFinsupp hkn u) = u b := by
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.fromFinsupp

  30. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.coordinateEquiv line 385

    Source documentation

    Literal free coordinates on every degree of the actual right cylinder.

    def coordinateEquiv {n k p : ℕ} (hkn : k < n) :
    (Cylinder hkn).group p ≃+ (Basis n k p →₀ ℤ) where
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis

  31. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.coordinateEquiv_positive_iff line 401

    Source documentation

    The coordinate equivalence identifies the actual positive cone.

    theorem coordinateEquiv_positive_iff {n k p : ℕ} (hkn : k < n)
    (x : (Cylinder hkn).group p) :
    x ∈ (Cylinder hkn).positive p ↔ ∀ b, 0 ≤ coordinateEquiv hkn x b :=
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coordinateEquiv

  32. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.augmentation_vector line 407

    Source documentation

    Every degree-zero basis vector has augmentation one.

    theorem augmentation_vector {n k : ℕ} (hkn : k < n) (b : Basis n k 0) :
    (Cylinder hkn).augmentation (vector hkn b) = 1 := by
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector

  33. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.augmentation_fromFinsupp line 419

    Source documentation

    Augmentation is the sum of all degree-zero coordinates.

    theorem augmentation_fromFinsupp {n k : ℕ} (hkn : k < n) (u : Basis n k 0 →₀ ℤ) :
    (Cylinder hkn).augmentation (fromFinsupp hkn u) =
      Finsupp.linearCombination ℤ (fun _ : Basis n k 0 => (1 : ℤ)) u := by
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.fromFinsupp

  34. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.augmentation_coordinate line 430

    Source documentation

    The exact augmentation formula in free coordinates.

    theorem augmentation_coordinate {n k : ℕ} (hkn : k < n) (x : (Cylinder hkn).group 0) :
    (Cylinder hkn).augmentation x =
      (coordinateEquiv hkn x).sum (fun _ z => z) := by
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coordinateEquiv

  35. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient_differential_fromFinsupp line 464
  36. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.differential_coefficient_sum line 479

    Source documentation

    Every boundary coefficient is the finite sum of its basis incidences.

    theorem differential_coefficient_sum {n k p : ℕ} (hkn : k < n)
    (x : (Cylinder hkn).group (p+1)) (c : Basis n k p) :
    coefficient hkn c ((Cylinder hkn).differential p x) =
      ∑ b ∈ (coordinateEquiv hkn x).support,
        coordinateEquiv hkn x b *
          coefficient hkn c ((Cylinder hkn).differential p (vector hkn b)) := by
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coordinateEquiv, OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector

  37. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.negative_boundary_witness line 495

    Source documentation

    A negative coefficient has an actual negative incidence in its support.

    theorem negative_boundary_witness {n k p : ℕ} (hkn : k < n)
    (x : (Cylinder hkn).group (p+1)) (hx : x ∈ (Cylinder hkn).positive (p+1))
    (c : Basis n k p) (hc : coefficient hkn c ((Cylinder hkn).differential p x) < 0) :
    ∃ b ∈ (coordinateEquiv hkn x).support,
      coefficient hkn c ((Cylinder hkn).differential p (vector hkn b)) < 0 := by
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coordinateEquiv, OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector

  38. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.positive_boundary_witness line 513

    Source documentation

    A positive coefficient has an actual positive incidence in its support.

    theorem positive_boundary_witness {n k p : ℕ} (hkn : k < n)
    (x : (Cylinder hkn).group (p+1)) (hx : x ∈ (Cylinder hkn).positive (p+1))
    (c : Basis n k p) (hc : 0 < coefficient hkn c ((Cylinder hkn).differential p x)) :
    ∃ b ∈ (coordinateEquiv hkn x).support,
      0 < coefficient hkn c ((Cylinder hkn).differential p (vector hkn b)) := by
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coordinateEquiv, OAI.Thomason.Construction.PastingGlobeCylinderBasis.vector

  39. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom_side_bounds line 531

    Source documentation

    Weak side-height bounds, including the top degree.

    theorem atom_side_bounds {n k p : ℕ} (hkn : k < n) (b : Basis n k p)
    (a : Bool) (q : ℕ) (hqp : q ≤ p) (c : Basis n k q)
    (hc : coefficient hkn c ((atom hkn b).table a q) ≠ 0) :
    if a then height b ≤ height c else height c ≤ height b := by
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom, OAI.Thomason.Construction.PastingGlobeCylinderBasis.height

  40. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom_side_height line 572

    Source documentation

    Below the top degree the side-height bounds are strict.

    theorem atom_side_height {n k p q : ℕ} (hkn : k < n) (b : Basis n k p)
    (a : Bool) (hqp : q < p) (c : Basis n k q)
    (hc : coefficient hkn c ((atom hkn b).table a q) ≠ 0) :
    if a then height b < height c else height c < height b := by
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom, OAI.Thomason.Construction.PastingGlobeCylinderBasis.height

  41. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.ordered_atoms_disjoint line 602

    Source documentation

    Increasingly ordered actual atoms have disjoint lower signed supports.

    theorem ordered_atoms_disjoint {n k p q r : ℕ} (hkn : k < n)
    (b : Basis n k p) (c : Basis n k q) (hrp : r < p) (hrq : r < q)
    (hbc : height b ≤ height c) (e : Basis n k r) :
    coefficient hkn e ((atom hkn b).table false r) = 0 ∨
      coefficient hkn e ((atom hkn c).table true r) = 0 := by
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.height, OAI.Thomason.Construction.PastingGlobeCylinderBasis.coefficient, OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom

  42. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.orderedAtomBasis line 638

    Source documentation

    The concrete ordered atom data of two equal globes pasted along a face.

    def orderedAtomBasis {n k : ℕ} (hkn : k < n) : OrderedAtomBasis (Cylinder hkn) where
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder

  43. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.generated line 655

    Source documentation

    Endpoint atoms and mixed prism atoms composition-generate this cylinder.

    theorem generated {n k : ℕ} (hkn : k < n) (P : Cell (Cylinder hkn) → Prop)
    (hatom : ∀ p (b : Basis n k p), P (atom hkn b))
    (hcomp : ∀ r x y hxy, P x → P y → P (Cell.comp x y r hxy)) :
    ∀ X, P X :=
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom

  44. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.hom_ext line 662

    Source documentation

    Strict maps out of the cylinder are determined by its explicit atoms.

    theorem hom_ext {n k : ℕ} (hkn : k < n) {D : StrictOmegaCategory}
    (F G : (Cylinder hkn).realization ⟶ D)
    (he : ∀ p (b : Basis n k p), F.toFun (atom hkn b) = G.toFun (atom hkn b)) :
    F = G :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom

  45. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.sideMap line 690

    Source documentation

    Each original globe gives its actual positive-table cylinder inclusion.

    def sideMap {n k : ℕ} (hkn : k < n) (s : Bool) :
    (rightCylinder (DirectedGlobeComplex.complex n)).realization ⟶
      (Cylinder hkn).realization :=
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder

  46. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.endpoint_cell_naturality line 695
  47. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom_in_side line 704

    Source documentation

    Every literal atom is in the image of a globe-cylinder inclusion.

    theorem atom_in_side {n k p : ℕ} (hkn : k < n) (b : Basis n k p) :
    ∃ (s : Bool) (x : Cell (rightCylinder (DirectedGlobeComplex.complex n))),
      (sideMap hkn s).toFun x = atom hkn b := by
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.Basis, OAI.Thomason.Construction.DirectedGlobeComplex.complex, OAI.Thomason.Construction.PastingGlobeCylinderBasis.sideMap, OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom

  48. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.sideMap_joint_epi line 718

    Source documentation

    Agreement on both cylinder pieces forces equality on their target.

    theorem sideMap_joint_epi {n k : ℕ} (hkn : k < n) {D : StrictOmegaCategory}
    (F G : (Cylinder hkn).realization ⟶ D)
    (he : ∀ s, sideMap hkn s ≫ F = sideMap hkn s ≫ G) : F = G := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder, OAI.Thomason.Construction.PastingGlobeCylinderBasis.sideMap

  49. abbrev OAI.Thomason.Construction.PastingGlobeCylinderBasis.pasted line 750
  50. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.piece line 752
  51. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.abelianization_piece line 757

    Source documentation

    The chain comparison respects either specified globe inclusion.

    theorem abelianization_piece {n k : ℕ} (hkn : k < n) (s : Bool) :
    StrictOmegaCategory.Abelianization.functor.map (piece (n := n) (k := k) s) ≫
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.piece

  52. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.modelIso line 788

    Source documentation

    Literal positive-table comparison for the full pasted-globe cylinder.

    def modelIso {n k : ℕ} (hkn : k < n) :
    GrayChainExtension.model.obj (pasted n k) ≅ (Cylinder hkn).realization :=
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.pasted, OAI.Thomason.Construction.PastingGlobeCylinderBasis.Cylinder

  53. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.globeModelIso line 793
  54. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.model_piece line 800

    Source documentation

    The full-cylinder isomorphism is compatible with each piece.

    theorem model_piece {n k : ℕ} (hkn : k < n) (s : Bool) :
    GrayChainExtension.model.map (piece (n := n) (k := k) s) ≫ (modelIso hkn).hom =
…

    Mentions: OAI.Thomason.Construction.PastingGlobeCylinderBasis.piece, OAI.Thomason.Construction.PastingGlobeCylinderBasis.modelIso

  55. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.model_joint_epi line 812

    Source documentation

    Actual model-cylinder maps are determined by their restrictions to the two actual globe cylinders.

    theorem model_joint_epi {n k : ℕ} (hkn : k < n) {D : StrictOmegaCategory}
    (F G : GrayChainExtension.model.obj (pasted n k) ⟶ D)
    (hl : GrayChainExtension.model.map (StrictOmegaCategory.PastingGlobe.left n n k) ≫ F =
      GrayChainExtension.model.map (StrictOmegaCategory.PastingGlobe.left n n k) ≫ G)
    (hr : GrayChainExtension.model.map (StrictOmegaCategory.PastingGlobe.right n n k) ≫ F =
      GrayChainExtension.model.map (StrictOmegaCategory.PastingGlobe.right n n k) ≫ G) : F = G := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory, OAI.Thomason.Construction.PastingGlobeCylinderBasis.pasted, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.left, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.right

  56. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.collapseTo line 856

    Source documentation

    Collapse a higher globe to the universal cell of a lower globe.

    def collapseTo (n k : ℕ) (hkn : k ≤ n) : Globe.category n ⟶ Globe.category k :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category

  57. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.collapseTo_top line 860
  58. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.retractLeft line 864

    Source documentation

    Retract the left half, collapsing the right half to the shared target face.

    def retractLeft (n m k : ℕ) (hkm : k ≤ m) : category n m k ⟶ Globe.category n :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category

  59. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.retractRight line 872

    Source documentation

    Retract the right half, collapsing the left half to the shared source face.

    def retractRight (n m k : ℕ) (hkn : k ≤ n) : category n m k ⟶ Globe.category m :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category

  60. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.retractCommon line 880

    Source documentation

    The common projection remembers the entire shared k-globe.

    def retractCommon (n m k : ℕ) (hkn : k ≤ n) (hkm : k ≤ m) :
    category n m k ⟶ Globe.category k :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category

  61. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.left_retractLeft line 888
  62. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.right_retractRight line 893
  63. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.right_retractLeft line 898
  64. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.left_retractRight line 904
  65. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.left_retractCommon line 910
  66. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.right_retractCommon line 915
  67. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.collapseTo_face line 920
  68. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.retractLeft_common line 930

    Source documentation

    The two retractions have exactly the same projection to their common face.

    theorem retractLeft_common (n m k : ℕ) (hkn : k ≤ n) (hkm : k ≤ m) :
    retractLeft n m k hkm ≫ collapseTo n k hkn = retractCommon n m k hkn hkm := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.retractLeft, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.collapseTo, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.retractCommon

  69. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.retractRight_common line 937
  70. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.model_left_retractLeft line 945

    Source documentation

    Both piece-cylinder maps are split monos for the actual chain model.

    theorem model_left_retractLeft (n m k : ℕ) (hkm : k ≤ m) :
    GrayChainExtension.model.map (left n m k) ≫
      GrayChainExtension.model.map (retractLeft n m k hkm) = 𝟙 _ := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.left, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.retractLeft

  71. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.model_right_retractRight line 950
  72. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.model_common line 957

    Source documentation

    The table projections of the two cylinder halves retain precisely the same common-cylinder value.

    theorem model_common (n m k : ℕ) (hkn : k ≤ n) (hkm : k ≤ m) :
    GrayChainExtension.model.map (retractLeft n m k hkm) ≫
      GrayChainExtension.model.map (collapseTo n k hkn) =
    GrayChainExtension.model.map (retractRight n m k hkn) ≫
      GrayChainExtension.model.map (collapseTo m k hkm) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.retractLeft, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.collapseTo, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.retractRight