OAI/CategoryTheory/Thomason/Gray/GrayChainGlobeRestriction.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Exact intersection of the realized cylinder pieces

The two globe pieces have retractions which collapse the opposite piece to the common face. These identities make their intersection square a pullback after every functor, in particular after the concrete right-chain cylinder and realization. Generation of the full realized cylinder is a separate question.

  1. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.pullback_of_piece_retractions line 29
  2. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.functor_commonFace_isPullback line 58

    Source documentation

    The common-face square is an absolute pullback, by its explicit piece retractions. This theorem does not assert preservation of a colimit.

    theorem functor_commonFace_isPullback
    {D : Type*} [Category D] (F : StrictOmegaCategory.{0} ⥤ D)
    (n m k : ℕ) (hkn : k ≤ n) (hkm : k ≤ m) :
    IsPullback (F.map (Globe.faceMap true k n)) (F.map (Globe.faceMap false k m))
      (F.map (left n m k)) (F.map (right n m k)) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.left, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.right

  3. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.model_commonFace_isPullback line 79

    Source documentation

    In the actual realized chain cylinder, the two globe pieces intersect in exactly their common realized face-cylinder.

    theorem model_commonFace_isPullback (n m k : ℕ) (hkn : k ≤ n) (hkm : k ≤ m) :
    IsPullback (GrayChainExtension.model.map (Globe.faceMap true k n))
      (GrayChainExtension.model.map (Globe.faceMap false k m))
      (GrayChainExtension.model.map (left n m k))
      (GrayChainExtension.model.map (right n m k)) :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.left, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.right

  4. abbrev OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.model line 107
  5. abbrev OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.source line 109
  6. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.piece line 112
  7. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.targetPiece line 115
  8. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.comparison line 119
  9. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.piece_comparison line 123
  10. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.globeIso line 129
  11. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.basisComparison line 133
  12. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.piece_basisComparison line 137
  13. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.map_retract line 143
  14. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.same_piece_injective line 152

    Source documentation

    Cells from one original piece are distinguished by the comparison.

    theorem same_piece_injective (n k : ℕ) (hkn : k ≤ n) (s : Bool)
    (x y : model.obj (Globe.category n))
    (he : (targetPiece n k s).toFun x = (targetPiece n k s).toFun y) : x = y := by
…

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

  15. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.cross_piece_eq line 163

    Source documentation

    Equality of a left and a right original piece cell is already forced by the common-face relation in the source pushout.

    theorem cross_piece_eq (n k : ℕ) (hkn : k ≤ n)
    (x y : model.obj (Globe.category n))
    (he : (targetPiece n k false).toFun x = (targetPiece n k true).toFun y) :
    (piece n k false).toFun x = (piece n k true).toFun y := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.targetPiece, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.piece

  16. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.piece_eq_of_comparison line 200
  17. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.atom_in_side_bounded line 228
  18. abbrev OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.atomBasis line 257
  19. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.representativeSide line 259
  20. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.representativeCell line 262
  21. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.representative_spec line 266
  22. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.atomLift line 274

    Source documentation

    The chosen atom lift lies in an original globe-cylinder piece.

    def atomLift {n k : ℕ} (hkn : k < n) (a : (atomBasis hkn).AtomIndex) : source n k :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.atomBasis, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.source

  23. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.atomLift_dimension line 278
  24. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.atomLift_image line 283
  25. theorem OAI.Thomason.Construction.PastingGlobeBasis.embed_lower line 311
  26. theorem OAI.Thomason.Construction.PastingGlobeBasis.inclusion_basisAtom line 324
  27. def OAI.Thomason.Construction.PastingGlobeCylinderBasis.pieceBasisMap line 348
  28. theorem OAI.Thomason.Construction.PastingGlobeCylinderBasis.sideMap_atom line 353
  29. theorem OAI.Thomason.Construction.GridGlobeBasis.embed_lower line 387
  30. theorem OAI.Thomason.Construction.GridGlobeBasis.inclusion_atom line 404
  31. def OAI.Thomason.Construction.GridGlobeBasis.rowCylinderIndex line 422
  32. theorem OAI.Thomason.Construction.GridGlobeBasis.rowCylinder_atom line 428
  33. theorem OAI.Thomason.Construction.GridGlobeBasis.cylinderAtom_in_row line 449
  34. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.piece_eq_of_basisComparison line 494
  35. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.piece_atom_image line 510
  36. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.piece_atom_eq_lift line 524

    Source documentation

    Every original piece atom is the corresponding canonical atom lift.

    theorem piece_atom_eq_lift {n k p : ℕ} (hkn : k < n) (s : Bool)
    (b : (DirectedGlobeComplex.cylinderOrderedAtomBasis n).Index p) :
    (piece n k s).toFun ((globeIso n).inv.toFun
      ((DirectedGlobeComplex.cylinderOrderedAtomBasis n).atom p b)) =
    atomLift hkn ⟨p, PastingGlobeCylinderBasis.pieceBasisMap hkn s b⟩ := by
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.cylinderOrderedAtomBasis, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.piece, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.globeIso, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.atomLift, OAI.Thomason.Construction.PastingGlobeCylinderBasis.pieceBasisMap

  37. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.piece_cell_generated line 534
  38. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.generated line 566

    Source documentation

    The actual source pushout is composition-generated by the bounded chosen lifts of the explicit pasted-cylinder atoms.

    theorem generated {n k : ℕ} (hkn : k < n) (x : source n k) :
    Nonempty (CompositionExpression (source n k) (atomLift hkn) x) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.source, OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.atomLift

  39. def OAI.Thomason.Construction.NormalizedSimplexIdentities.chainCosimplicial line 598

    Source documentation

    The normalized directed simplex complexes, including degenerate maps.

    def chainCosimplicial (h : NormalizedSimplexIdentities) :
    SimplexCategory ⥤ DirectedComplex.{0} where
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

  40. def OAI.Thomason.Construction.NormalizedSimplexIdentities.chainCylinderRealizationIso line 614

    Source documentation

    The chain-cylinder cosimplicial object has precisely the earlier literal strict objects and maps.

    def chainCylinderRealizationIso (h : NormalizedSimplexIdentities) :
    h.chainCosimplicial ⋙ rightCylinderFunctor ⋙ realizationFunctor ≅
      h.cylinderCosimplicial :=
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

  41. def OAI.Thomason.Construction.SimplexAtomsInput.abelianizationCosimplicialIso line 627

    Source documentation

    The inverse presentation of normalized chains commutes with all simplex operators, including those which collapse a basis element to zero.

    def abelianizationCosimplicialIso :
    h.cosimplicial ⋙ StrictOmegaCategory.Abelianization.functor ≅
      h.chainCosimplicial :=
…

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

  42. def OAI.Thomason.Construction.SimplexAtomsInput.chainModelComparison line 650

    Source documentation

    The actual chain-cylinder comparison, natural in the simplex.

    def chainModelComparison :
    h.cylinderCosimplicial ≅
      h.cosimplicial ⋙ StrictOmegaCategory.GrayChainExtension.model :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.model

  43. theorem OAI.Thomason.Construction.SimplexAtomsInput.unit_eq_realized_inverse line 661

    Source documentation

    On an oriental the actual abelianization unit is the realization of the inverse normalized-chain presentation.

    theorem unit_eq_realized_inverse (m : ℕ) :
    StrictOmegaCategory.Abelianization.unit (h.object m) =
      (a.fromSimplexChains m).realization := by
…

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

  44. theorem OAI.Thomason.Construction.SimplexAtomsInput.chainModelComparison_endpoint line 673

    Source documentation

    The comparison preserves the two concrete interval endpoints.

    theorem chainModelComparison_endpoint (side : Bool) (m : SimplexCategory) :
    (h.cylinderEndpoint side).app m ≫ a.chainModelComparison.hom.app m =
      (StrictOmegaCategory.GrayChainExtension.modelEndpoint side).app
        (h.object m.len) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.modelEndpoint

  45. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.truncated_iff_source_collapse line 722

    Source documentation

    Source collapse alone detects truncation; target collapse follows from the same-level globular identity.

    theorem truncated_iff_source_collapse (C : StrictOmegaCategory.{0}) (n : ℕ) :
    C.IsTruncated n ↔ ∀ (m : ℕ) (f : category m ⟶ C),
      collapse false n m ≫ f = f := by
…

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

  46. theorem OAI.Thomason.Construction.internalHom_truncated_iff_cylinder_source_globes line 743

    Source documentation

    The right adjoint is truncated when all source collapses of its left adjoint's actual globe cylinders are invisible in the target.

    theorem internalHom_truncated_iff_cylinder_source_globes
    {F R : StrictOmegaCategory.{0} ⥤ StrictOmegaCategory.{0}} (adj : F ⊣ R)
    (Y : StrictOmegaCategory.{0}) (n : ℕ) :
    (R.obj Y).IsTruncated n ↔
      ∀ (m : ℕ) (f : F.obj (StrictOmegaCategory.Globe.category m) ⟶ Y),
        F.map (StrictOmegaCategory.Globe.collapse false n m) ≫ f = f := by
…

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

  47. theorem OAI.Thomason.Construction.DirectedGlobeComplex.chainMap_sourceCollapse line 781

    Source documentation

    The chain map presenting source collapse is the map of the source table.

    theorem chainMap_sourceCollapse {m n : ℕ} (hnm : n < m) :
    chainMap (StrictOmegaCategory.Globe.collapse false n m) =
      cellMap m ((topCell m).face false n) := by
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.chainMap, OAI.Thomason.Construction.StrictOmegaCategory.Globe.collapse, OAI.Thomason.Construction.DirectedGlobeComplex.cellMap, OAI.Thomason.Construction.DirectedGlobeComplex.topCell

  48. theorem OAI.Thomason.Construction.DirectedGlobeComplex.chainMap_sourceCollapse_agree_below line 800

    Source documentation

    Below the collapsed source dimension every chain is unchanged.

    theorem chainMap_sourceCollapse_agree_below {m n : ℕ} (hnm : n < m) :
    ∀ k, k < n → (chainMap (StrictOmegaCategory.Globe.collapse false n m)).app k =
      (Hom.id (complex m)).app k := by
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.chainMap, OAI.Thomason.Construction.StrictOmegaCategory.Globe.collapse, OAI.Thomason.Construction.DirectedGlobeComplex.complex

  49. theorem OAI.Thomason.Construction.DirectedGlobeComplex.chainMap_sourceCollapse_positive_bridge line 826

    Source documentation

    The discrepancy at dimension n is an explicit positive boundary.

    theorem chainMap_sourceCollapse_positive_bridge {m n : ℕ} (hnm : n < m) :
    ∀ v : (complex m).group n, v ∈ (complex m).positive n →
      ∃ z : (complex m).group (n+1), z ∈ (complex m).positive (n+1) ∧
        (complex m).differential n z = (Hom.id (complex m)).app n v -
          (chainMap (StrictOmegaCategory.Globe.collapse false n m)).app n v := by
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex, OAI.Thomason.Construction.DirectedGlobeComplex.positive, OAI.Thomason.Construction.DirectedGlobeComplex.differential, OAI.Thomason.Construction.DirectedGlobeComplex.chainMap, OAI.Thomason.Construction.StrictOmegaCategory.Globe.collapse

  50. theorem OAI.Thomason.Construction.DirectedGlobeComplex.rightGlobeCylinder_sourceCollapse line 870

    Source documentation

    Every map from the actual right-cylinder globe to an n-truncated target kills source collapse in dimension n.

    theorem rightGlobeCylinder_sourceCollapse {Y : StrictOmegaCategory.{0}}
    {m n : ℕ} (hY : Y.IsTruncated n)
    (H : rightGlobeCylinder.obj ⟨m⟩ ⟶ Y) :
    rightGlobeCylinder.map (StrictOmegaCategory.Globe.collapse false n m) ≫ H = H := by
…

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

  51. theorem OAI.Thomason.Construction.internalHom_truncated_of_rightGlobeComparison line 904

    Source documentation

    A literal comparison on all free globe cylinders suffices to derive truncation of the right adjoint. No claim about arbitrary cells of a tensor product is needed.

    theorem internalHom_truncated_of_rightGlobeComparison
    {F R : StrictOmegaCategory.{0} ⥤ StrictOmegaCategory.{0}} (adj : F ⊣ R)
    (e : StrictOmegaCategory.Globe.inclusion ⋙ F ≅
      DirectedGlobeComplex.rightGlobeCylinder)
    {Y : StrictOmegaCategory.{0}} {n : ℕ} (hY : Y.IsTruncated n) :
    (R.obj Y).IsTruncated n := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.inclusion, OAI.Thomason.Construction.DirectedGlobeComplex.rightGlobeCylinder

  52. theorem OAI.Thomason.Construction.grayTruncationInput_of_rightGlobeComparison line 935

    Source documentation

    A natural comparison with the concrete free-globe cylinders gives preservation of finite truncations by the right internal hom.

    theorem grayTruncationInput_of_rightGlobeComparison
    {h : NormalizedSimplexIdentities} (G : RightGrayInput h)
    (e : StrictOmegaCategory.Globe.inclusion ⋙ G.cylinder ≅
      DirectedGlobeComplex.rightGlobeCylinder) : GrayTruncationInput G :=
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.StrictOmegaCategory.Globe.inclusion, OAI.Thomason.Construction.DirectedGlobeComplex.rightGlobeCylinder, OAI.Thomason.Construction.GrayTruncationInput

  53. def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.globeModelIso line 962

    Source documentation

    Restriction of the global extension to globes agrees naturally with its original chain model.

    def globeModelIso : Globe.inclusion ⋙ cylinder ≅ Globe.inclusion ⋙ model :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.inclusion, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cylinder, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.model

  54. def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.globeRestrictionIso line 971

    Source documentation

    The extended cylinder has the concrete signed right-cylinder values and maps on the actual finite globes.

    def globeRestrictionIso : Globe.inclusion ⋙ cylinder ≅
    DirectedGlobeComplex.rightGlobeCylinder :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.inclusion, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cylinder, OAI.Thomason.Construction.DirectedGlobeComplex.rightGlobeCylinder

  55. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.rightAdjoint_truncated line 978

    Source documentation

    Every right adjoint of the actual extension preserves truncation. Adjointness itself is a separate construction; the truncation proof uses only the now-established concrete globe restriction.

    theorem rightAdjoint_truncated {R : StrictOmegaCategory.{0} ⥤ StrictOmegaCategory.{0}}
    (adj : cylinder ⊣ R) {Y : StrictOmegaCategory.{0}} {n : ℕ}
    (hY : Y.IsTruncated n) : (R.obj Y).IsTruncated n :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cylinder, OAI.Thomason.Construction.StrictOmegaCategory.IsTruncated

  56. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.truncationInput line 985

    Source documentation

    A natural isomorphism of cylinder functors transports preservation of finite truncations by their right adjoints.

    theorem truncationInput {h : NormalizedSimplexIdentities} (G : RightGrayInput h)
    (e : G.cylinder ≅ cylinder) : GrayTruncationInput G :=
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cylinder, OAI.Thomason.Construction.GrayTruncationInput