PastingGlobeChains.lean`

81 declarations, 0 contain sorry, 0 declared as axioms

Extending the actual globe-and-pasting presentation

The proved cellwise presentation is dense. Consequently a cocontinuous functor and its natural transformations are recovered from these small parameters. The extension below is a genuine small colimit, with its restriction and universal comparison maps explicitly retained.

instance OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.(instance at line 28) line 28
instance OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.(instance at line 31) line 31
instance OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.(instance at line 34) line 34
def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.presentationIso line 40
Source documentation
The original strict category is recovered by the small presentation.
```
def presentationIso : inclusion.leftKanExtension inclusion ≅ 𝟭 StrictOmegaCategory.{0} :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion
def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.extend line 44
Source documentation
Extend actual data on the finite parameters by its small colimit.
```
def extend (F : Shape ⥤ StrictOmegaCategory.{0}) :
    StrictOmegaCategory.{0} ⥤ StrictOmegaCategory.{0} :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape
def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.restrictionIso line 50
Source documentation
Every parameter is recovered, since the parameter inclusion is full and faithful. This statement assumes no global preservation by the extension.
```
def restrictionIso (F : Shape ⥤ StrictOmegaCategory.{0}) :
    F ≅ inclusion ⋙ extend F := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.extend
def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.extensionObjIso line 58
Source documentation
The extension is computed on the actual category of parameters over C.
```
def extensionObjIso (F : Shape ⥤ StrictOmegaCategory.{0}) (C : StrictOmegaCategory.{0}) :
    (extend F).obj C ≅ colimit (CostructuredArrow.proj inclusion C ⋙ F) :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.extend, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion
def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.compare line 63
Source documentation
The explicit global comparison determined by a parameter-level map.
```
def compare (F : Shape ⥤ StrictOmegaCategory.{0})
    (T : StrictOmegaCategory.{0} ⥤ StrictOmegaCategory.{0}) (a : F ⟶ inclusion ⋙ T) :
    extend F ⟶ T :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.extend
theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.restriction_compare line 69
theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.compare_ext line 77
Source documentation
Global maps from the extension are determined by their finite-parameter values.
```
theorem compare_ext (F : Shape ⥤ StrictOmegaCategory.{0})
    {T : StrictOmegaCategory.{0} ⥤ StrictOmegaCategory.{0}}
    {a b : extend F ⟶ T}
    (he : (restrictionIso F).hom ≫ whiskerLeft inclusion a =
      (restrictionIso F).hom ≫ whiskerLeft inclusion b) : a = b :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.extend, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.restrictionIso, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion
def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.globes line 101
Source documentation
Keep the globe objects and all of their strict maps in the dense presentation.
```
def globes : Globe.Shapes ⥤ Shape where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.Shapes, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape
def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.globesInclusionIso line 106
Source documentation
The restricted inclusion is exactly the original globe inclusion.
```
def globesInclusionIso : globes ⋙ inclusion ≅ Globe.inclusion :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.globes, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion, OAI.Thomason.Construction.StrictOmegaCategory.Globe.inclusion
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.model line 134
Source documentation
The chain-cylinder model before extension from the finite parameters.
```
def model : StrictOmegaCategory.{0} ⥤ StrictOmegaCategory.{0} :=
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.modelEndpoint line 138
Source documentation
The actual endpoint into the chain model, using the constructed unit.
```
def modelEndpoint (a : Bool) : 𝟭 StrictOmegaCategory.{0} ⟶ model where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.model
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameters line 167
Source documentation
The concrete diagram being extended.
```
def parameters : GlobePasting.Shape ⥤ StrictOmegaCategory.{0} :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cylinder line 171
Source documentation
Small-colimit extension of the explicit cylinders.
```
def cylinder : StrictOmegaCategory.{0} ⥤ StrictOmegaCategory.{0} :=
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameterIso line 175
Source documentation
Exact agreement with the actual chain model on every chosen parameter.
```
def parameterIso : parameters ≅ GlobePasting.inclusion ⋙ cylinder :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameters, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cylinder
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.comparison line 179
Source documentation
The canonical comparison to the chain model on arbitrary strict categories.
```
def comparison : cylinder ⟶ model :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cylinder, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.model
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameter_comparison line 183
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpoint line 188
Source documentation
Density extends the literal endpoint maps to every strict category.
```
def endpoint (a : Bool) : 𝟭 StrictOmegaCategory.{0} ⟶ cylinder :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cylinder
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpoint_parameters line 193
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpoint_comparison line 201
Source documentation
The globally defined endpoints agree with the original chain endpoints under the canonical comparison.
```
theorem endpoint_comparison (a : Bool) : endpoint a ≫ comparison = modelEndpoint a := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpoint, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.comparison, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.modelEndpoint
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.comparison_parameter_isIso line 224
Source documentation
Restricting the global comparison to the generating parameters is an isomorphism, although no global isomorphism is asserted.
```
theorem comparison_parameter_isIso (i : GlobePasting.Shape) :
    IsIso (comparison.app (GlobePasting.object i)) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.object
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.presentationDiagram line 259
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.presentationIso line 263
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.presentationCocone line 267
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.presentationIsColimit line 277
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.presentation_leg line 297
Source documentation
The colimit leg is the actual parameter comparison followed by the extended cylinder of the corresponding strict map.
```
theorem presentation_leg (C : StrictOmegaCategory.{0})
    (j : CostructuredArrow GlobePasting.inclusion C) :
    (presentationCocone C).ι.app j = parameterIso.hom.app j.left ≫ cylinder.map j.hom := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.presentationCocone
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.presentation_leg_map line 303
Source documentation
Naturality of parameter legs in the category being presented.
```
theorem presentation_leg_map {C D : StrictOmegaCategory.{0}} (f : C ⟶ D)
    (j : CostructuredArrow GlobePasting.inclusion C) :
    (presentationCocone C).ι.app j ≫ cylinder.map f =
      (presentationCocone D).ι.app (CostructuredArrow.mk (Y := j.left) (j.hom ≫ f)) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.presentationCocone
def OAI.Thomason.Construction.PastingGlobeBasis.top line 334
Source documentation
The canonical positive top cell of either half.
```
def top {n k : ℕ} (hkn : k < n) (s : Bool) : (complex n k hkn).realization :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.complex
theorem OAI.Thomason.Construction.PastingGlobeBasis.top_dimension line 338
Source documentation
Both top cells have dimension at most n.
```
theorem top_dimension {n k : ℕ} (hkn : k < n) (s : Bool) :
    (complex n k hkn).realization.DimensionLE n (top hkn s) :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.complex, OAI.Thomason.Construction.PastingGlobeBasis.top
theorem OAI.Thomason.Construction.PastingGlobeBasis.top_matching line 343
Source documentation
The two top cells share their specified target and source k-faces.
```
theorem top_matching {n k : ℕ} (hkn : k < n) :
    (top hkn false).face true k = (top hkn true).face false k := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.top, OAI.Thomason.Construction.PastingGlobeBasis.face
def OAI.Thomason.Construction.PastingGlobeBasis.fromPasting line 364
Source documentation
The actual strict map from the pasted globes to its ordered chain model.
```
def fromPasting {n k : ℕ} (hkn : k < n) :
    StrictOmegaCategory.PastingGlobe.category n n k ⟶ (complex n k hkn).realization :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.PastingGlobeBasis.complex
def OAI.Thomason.Construction.PastingGlobeBasis.abelianizationToBasis line 370
Source documentation
Evaluating strict abelianization on the actual ordered chain model.
```
def abelianizationToBasis {n k : ℕ} (hkn : k < n) :
    Hom (StrictOmegaCategory.Abelianization.complex
      (StrictOmegaCategory.PastingGlobe.category n n k)) (complex n k hkn) :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.PastingGlobeBasis.complex
theorem OAI.Thomason.Construction.PastingGlobeBasis.unit_matching line 377
Source documentation
The unit of strict abelianization carries the two pasted cells to matching positive tables.
```
theorem unit_matching {n k : ℕ} :
    (StrictOmegaCategory.Abelianization.unitCell _
      (StrictOmegaCategory.PastingGlobe.leftCell n n k)).face true k =
    (StrictOmegaCategory.Abelianization.unitCell _
      (StrictOmegaCategory.PastingGlobe.rightCell n n k)).face false k := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unitCell, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.leftCell, OAI.Thomason.Construction.PastingGlobeBasis.face, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.rightCell
def OAI.Thomason.Construction.PastingGlobeBasis.basisToAbelianization line 388
Source documentation
Read the unit's actual cell tables on each basis.
```
def basisToAbelianization {n k : ℕ} (hkn : k < n) :
    Hom (complex n k hkn) (StrictOmegaCategory.Abelianization.complex
      (StrictOmegaCategory.PastingGlobe.category n n k)) :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.complex, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category

theorem OAI.Thomason.Construction.PastingGlobeBasis.desc_top line 398

Source documentation

The universal map evaluates the canonical top cell on either side.

theorem desc_top {n k : ℕ} {L : DirectedComplex.{0}} (hkn : k < n)
    (x y : Cell L) (hxy : x.face true k = y.face false k) (s : Bool)
    (hb : L.realization.DimensionLE n (if s then y else x)) :
    (desc hkn x y hxy).realization.toFun (top hkn s) = if s then y else x := by
…

Mentions: OAI.Thomason.Construction.PastingGlobeBasis.desc, OAI.Thomason.Construction.PastingGlobeBasis.top

theorem OAI.Thomason.Construction.PastingGlobeBasis.abelianizationToBasis_unit line 407
Source documentation
Evaluation of the abelianization unit is the strict comparison itself.
```
theorem abelianizationToBasis_unit {n k : ℕ} (hkn : k < n)
    (x : StrictOmegaCategory.PastingGlobe.category n n k) :
    (abelianizationToBasis hkn).realization.toFun
      (StrictOmegaCategory.Abelianization.unitCell _ x) = (fromPasting hkn).toFun x := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.PastingGlobeBasis.abelianizationToBasis, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.unitCell, OAI.Thomason.Construction.PastingGlobeBasis.fromPasting
theorem OAI.Thomason.Construction.PastingGlobeBasis.basisToAbelianization_top line 414
theorem OAI.Thomason.Construction.PastingGlobeBasis.abelianizationToBasis_inverse line 428
Source documentation
The two maps are inverse on strict abelianization, by the actual universal property of the pasted pair.
```
theorem abelianizationToBasis_inverse {n k : ℕ} (hkn : k < n) :
    Hom.comp (abelianizationToBasis hkn) (basisToAbelianization hkn) = Hom.id _ := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.abelianizationToBasis, OAI.Thomason.Construction.PastingGlobeBasis.basisToAbelianization
theorem OAI.Thomason.Construction.PastingGlobeBasis.basisToAbelianization_inverse line 455
Source documentation
The two maps are inverse on the explicit chain basis.
```
theorem basisToAbelianization_inverse {n k : ℕ} (hkn : k < n) :
    Hom.comp (basisToAbelianization hkn) (abelianizationToBasis hkn) = Hom.id _ := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.basisToAbelianization, OAI.Thomason.Construction.PastingGlobeBasis.abelianizationToBasis
def OAI.Thomason.Construction.PastingGlobeBasis.abelianizationIso line 472
Source documentation
The ordered finite complex is the actual abelianization of the pasted pair, with its specified two globe inclusions.
```
def abelianizationIso {n k : ℕ} (hkn : k < n) :
    StrictOmegaCategory.Abelianization.complex
      (StrictOmegaCategory.PastingGlobe.category n n k) ≅ complex n k hkn where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.PastingGlobeBasis.complex
theorem OAI.Thomason.Construction.PastingGlobeBasis.embed_self line 502
Source documentation
Canonical representatives are unchanged by their chosen globe inclusion.
```
theorem embed_self {n k p : ℕ} (hkn : k < n) (b : Basis n k p) :
    embed hkn b.val.1 ⟨b.val.2, b.property.1⟩ = b := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.embed
def OAI.Thomason.Construction.PastingGlobeBasis.atom line 517
Source documentation
The atom is the appropriate face of the corresponding globe's top cell.
```
def atom {n k p : ℕ} (hkn : k < n) (b : Basis n k p) : Cell (complex n k hkn) :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.complex
theorem OAI.Thomason.Construction.PastingGlobeBasis.atom_top line 522
Source documentation
Its top chain is exactly the chosen basis, on both sides.
```
theorem atom_top {n k p : ℕ} (hkn : k < n) (b : Basis n k p) (a : Bool) :
    (atom hkn b).table a p = Finsupp.single b 1 := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.atom
theorem OAI.Thomason.Construction.PastingGlobeBasis.atom_dimension line 532
Source documentation
Every atom is bounded by its basis degree.
```
theorem atom_dimension {n k p : ℕ} (hkn : k < n) (b : Basis n k p) :
    (complex n k hkn).realization.DimensionLE p (atom hkn b) :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.complex, OAI.Thomason.Construction.PastingGlobeBasis.atom
theorem OAI.Thomason.Construction.PastingGlobeBasis.atom_above line 539
Source documentation
All chains strictly above the basis degree vanish.
```
theorem atom_above {n k p q : ℕ} (hkn : k < n) (b : Basis n k p)
    (hpq : p < q) (a : Bool) : (atom hkn b).table a q = 0 :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.atom
theorem OAI.Thomason.Construction.PastingGlobeBasis.atom_below line 544
Source documentation
Every lower row is the corresponding singleton face of that globe.
```
theorem atom_below {n k p q : ℕ} (hkn : k < n) (b : Basis n k p)
    (hqp : q < p) (a : Bool) :
    (atom hkn b).table a q = Finsupp.single
      (embed hkn b.val.1 ⟨a, Or.inl (hqp.trans_le (degree_le b))⟩) 1 := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.atom, OAI.Thomason.Construction.PastingGlobeBasis.embed, OAI.Thomason.Construction.PastingGlobeBasis.degree_le
theorem OAI.Thomason.Construction.PastingGlobeBasis.embed_polarities_ne line 556
Source documentation
Source and target representatives below the top dimension are distinct.
```
theorem embed_polarities_ne {n k q : ℕ} (hkn : k < n) (s : Bool) (hqn : q < n) :
    embed hkn s (⟨false, Or.inl hqn⟩ : DirectedGlobeComplex.Basis n q) ≠
      embed hkn s (⟨true, Or.inl hqn⟩ : DirectedGlobeComplex.Basis n q) := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.embed, OAI.Thomason.Construction.DirectedGlobeComplex.Basis
theorem OAI.Thomason.Construction.PastingGlobeBasis.atom_lower_disjoint line 569
Source documentation
The two lower atom rows have disjoint basis supports.
```
theorem atom_lower_disjoint {n k p q : ℕ} (hkn : k < n) (b : Basis n k p)
    (hqp : q < p) (c : Basis n k q) :
    DFunLike.coe (F := Chains n k q) ((atom hkn b).table false q) c = 0 ∨
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.Chains, OAI.Thomason.Construction.PastingGlobeBasis.atom
def OAI.Thomason.Construction.PastingGlobeBasis.mixedAtom line 588
Source documentation
The mixed tensor generator is the top chain of the explicit prism atom.
```
def mixedAtom {n k p : ℕ} (hkn : k < n) (b : Basis n k p) :
    Cell (rightCylinder (complex n k hkn)) := RightCylinder.prism (atom hkn b)
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.complex, OAI.Thomason.Construction.PastingGlobeBasis.atom
theorem OAI.Thomason.Construction.PastingGlobeBasis.mixedAtom_top line 591
theorem OAI.Thomason.Construction.PastingGlobeBasis.mixedAtom_dimension line 596
def OAI.Thomason.Construction.PastingGlobeBasis.endpointAtom line 601
Source documentation
Endpoint tensor generators are also actual bounded positive cells.
```
def endpointAtom {n k p : ℕ} (hkn : k < n) (s : Bool) (b : Basis n k p) :
    Cell (rightCylinder (complex n k hkn)) :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.complex
theorem OAI.Thomason.Construction.PastingGlobeBasis.endpointAtom_top line 605
theorem OAI.Thomason.Construction.PastingGlobeBasis.endpointAtom_dimension line 612
def OAI.Thomason.Construction.GridGlobeBasis.embedApp line 633
theorem OAI.Thomason.Construction.GridGlobeBasis.embedApp_single line 637
theorem OAI.Thomason.Construction.GridGlobeBasis.embedApp_differential line 642
theorem OAI.Thomason.Construction.GridGlobeBasis.embedApp_augmentation line 654
theorem OAI.Thomason.Construction.GridGlobeBasis.embedApp_positive line 662
def OAI.Thomason.Construction.GridGlobeBasis.inclusion line 676
def OAI.Thomason.Construction.GridGlobeBasis.value line 700
theorem OAI.Thomason.Construction.GridGlobeBasis.value_embed line 703
def OAI.Thomason.Construction.GridGlobeBasis.descApp line 726
theorem OAI.Thomason.Construction.GridGlobeBasis.descApp_single line 730
theorem OAI.Thomason.Construction.GridGlobeBasis.descApp_embedApp line 734
theorem OAI.Thomason.Construction.GridGlobeBasis.descApp_differential line 745
theorem OAI.Thomason.Construction.GridGlobeBasis.descApp_augmentation line 764
theorem OAI.Thomason.Construction.GridGlobeBasis.descApp_positive line 771
def OAI.Thomason.Construction.GridGlobeBasis.desc line 782
theorem OAI.Thomason.Construction.GridGlobeBasis.inclusion_desc line 792
theorem OAI.Thomason.Construction.GridGlobeBasis.hom_ext line 802
theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.abelianization_isPushout line 849
Source documentation
Lambda sends the universal composable pair to a pushout of actual positive chain maps.
```
theorem abelianization_isPushout (n m k : ℕ) :
    IsPushout (C := DirectedComplex.{0}) (Abelianization.map (Globe.faceMap true k n))
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.map, OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap
def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.leftBounded line 857
def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.rightBounded line 861
theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.composite_generator line 866
Source documentation
The chain of the universal composite is exactly the sum of its factors.
```
theorem composite_generator (n m k : ℕ) (hk : k < max n m) :
    Abelianization.generator (category n m k) (max n m)
      ⟨composite n m k, composite_dimension n m k hk⟩ =
    Abelianization.generator (category n m k) (max n m) (leftBounded n m k) +
      Abelianization.generator (category n m k) (max n m) (rightBounded n m k) :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.generator, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.composite, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.composite_dimension, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.leftBounded, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.rightBounded
theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.compositionMap_generator line 875
Source documentation
The chain map of the strict composition parameter has the prescribed sum.
```
theorem compositionMap_generator (n m k : ℕ) (hk : k < max n m) :
    (Abelianization.map (compositionMap n m k hk)).app (max n m)
      (Abelianization.generator (Globe.category (max n m)) (max n m)
        ⟨Globe.Cell.top, Globe.category_truncated (max n m) Globe.Cell.top⟩) =
    Abelianization.generator (category n m k) (max n m) (leftBounded n m k) +
      Abelianization.generator (category n m k) (max n m) (rightBounded n m k) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.map, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.compositionMap, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.generator, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category_truncated, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.leftBounded, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.rightBounded
def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.cylinderComposition line 885
Source documentation
The concrete signed chain prism of the universal composition map.
```
def cylinderComposition (n m k : ℕ) (hk : k < max n m) :
    DirectedComplex.Hom
      (rightCylinder (Abelianization.complex (Globe.category (max n m))))
      (rightCylinder (Abelianization.complex (category n m k))) :=
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.cylinderComposition_endpoint line 892
Source documentation
At either endpoint the prism realizes the actual universal composite.
```
theorem cylinderComposition_endpoint (n m k : ℕ) (hk : k < max n m)
    (a : Bool) (j : ℕ)
    (x : (Abelianization.complex (Globe.category (max n m))).group j) :
    (cylinderComposition n m k hk).app j
      ((RightCylinder.endpoint _ a).app j x) =
    (RightCylinder.endpoint _ a).app j
      ((Abelianization.map (compositionMap n m k hk)).app j x) :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.cylinderComposition, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.map, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.compositionMap
theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.cylinderComposition_shifted line 902
Source documentation
The shifted top component of the right prism retains the sum relation.
```
theorem cylinderComposition_shifted (n m k : ℕ) (hk : k < max n m) :
    (cylinderComposition n m k hk).app (max n m + 1)
      (0, 0, Abelianization.generator (Globe.category (max n m)) (max n m)
        ⟨Globe.Cell.top, Globe.category_truncated (max n m) Globe.Cell.top⟩) =
    (0, 0,
      Abelianization.generator (category n m k) (max n m) (leftBounded n m k) +
        Abelianization.generator (category n m k) (max n m) (rightBounded n m k)) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.cylinderComposition, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.generator, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category_truncated, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.leftBounded, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.rightBounded