OAI/CategoryTheory/Thomason/Simplicial/SimplicialSpanFactorization.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

The interval specialization of the Alexander--Whitney diagonal

Only the last two cuts of the classical diagonal survive after mapping the right factor to the normalized interval complex. We give this map explicitly. Its chain identity and naturality are the precise specialization of Goerss--Jardine, IV.2, Remark 2.5, retained as published inputs in this phase. Positivity, the right counit and both endpoints are proved from the formula.

  1. def OAI.Thomason.Construction.SimplexComplex.awEnd line 32

    Source documentation

    The last vertex of a basis simplex decides its endpoint summand.

    noncomputable def awEnd {m : ℕ} (θ : Fin (m + 1) →o Fin 2) (a : Fin 2) (p : ℕ) :
    Chains m p →ₗ[ℤ] Chains m p :=
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains

  2. def OAI.Thomason.Construction.SimplexComplex.awEdge line 39

    Source documentation

    The penultimate cut contributes an edge precisely when its interval vertices are 0 and 1.

    noncomputable def awEdge {m : ℕ} (θ : Fin (m + 1) →o Fin 2) (p : ℕ) :
    Chains m (p + 1) →ₗ[ℤ] Chains m p :=
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains

  3. def OAI.Thomason.Construction.SimplexComplex.awApp line 45
  4. theorem OAI.Thomason.Construction.SimplexComplex.awEnd_single line 53
  5. theorem OAI.Thomason.Construction.SimplexComplex.awEdge_single line 62
  6. theorem OAI.Thomason.Construction.SimplexComplex.awEnd_positive line 71
  7. theorem OAI.Thomason.Construction.SimplexComplex.awEdge_positive line 82
  8. theorem OAI.Thomason.Construction.SimplexComplex.awEnd_sum line 94
  9. theorem OAI.Thomason.Construction.SimplexComplex.awEnd_const line 110
  10. theorem OAI.Thomason.Construction.SimplexComplex.awEdge_const line 120
  11. structure OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput line 131

    Source documentation

    Only the classical chain identity and its ordinal naturality are left as hypotheses. All objects and maps here have their explicit formulas.

    structure AlexanderWhitneyInput (h : NormalizedSimplexIdentities) : Prop where
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

  12. def OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput.chainMap line 145

    Source documentation

    The positive augmented chain map obtained from the explicit AW formula.

    noncomputable def chainMap {m : ℕ} (θ : Fin (m + 1) →o Fin 2) :
    Hom (directedComplex m (h.squared m)) (rightCylinder (directedComplex m (h.squared m))) where
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.directedComplex

  13. theorem OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput.projection_chainMap line 157
  14. theorem OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput.chainMap_const line 162
  15. theorem OAI.Thomason.Construction.SimplexComplex.deleteVertex_last_castSucc line 189

    Source documentation

    Deleting a vertex other than the last preserves the last vertex.

    theorem deleteVertex_last_castSucc {m p : ℕ} (s : Basis m (p + 1)) (i : Fin (p + 1)) :
    deleteVertex s i.castSucc (Fin.last p) = s (Fin.last (p + 1)) := by
…

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

  16. theorem OAI.Thomason.Construction.SimplexComplex.deleteVertex_last_last line 196

    Source documentation

    Deleting the last vertex exposes the penultimate vertex.

    theorem deleteVertex_last_last {m p : ℕ} (s : Basis m (p + 1)) :
    deleteVertex s (Fin.last (p + 1)) (Fin.last p) = s (Fin.last p).castSucc := by
…

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

  17. theorem OAI.Thomason.Construction.SimplexComplex.awEnd_boundary_expansion line 202

    Source documentation

    Boundary projection is determined by the two final vertex labels.

    theorem awEnd_boundary_expansion {m p : ℕ} (θ : Fin (m + 1) →o Fin 2)
    (a : Fin 2) (s : Basis m (p + 1)) :
    awEnd θ a p (differentialBasis m p s) =
      (∑ i : Fin (p + 1), if θ (s (Fin.last (p + 1))) = a then
        Finsupp.single (deleteVertex s i.castSucc) ((-1 : ℤ) ^ i.val) else 0) +
      (if θ (s (Fin.last p).castSucc) = a then
        Finsupp.single (deleteVertex s (Fin.last (p + 1))) ((-1 : ℤ) ^ (p + 1)) else 0) := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.awEnd, OAI.Thomason.Construction.SimplexComplex.differentialBasis, OAI.Thomason.Construction.SimplexComplex.deleteVertex

  18. theorem OAI.Thomason.Construction.SimplexComplex.awEnd_one_differential_basis line 215

    Source documentation

    The final endpoint's boundary defect is the signed interval-edge term.

    theorem awEnd_one_differential_basis {m p : ℕ} (θ : Fin (m + 1) →o Fin 2)
    (s : Basis m (p + 1)) :
    awEnd θ 1 p (differentialBasis m p s) =
      differential m p (awEnd θ 1 (p + 1) (Finsupp.single s 1)) +
        ((-1 : ℤ) ^ p) • awEdge θ p (Finsupp.single s 1) := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.awEnd, OAI.Thomason.Construction.SimplexComplex.differentialBasis, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.awEdge

  19. theorem OAI.Thomason.Construction.SimplexComplex.awEnd_one_differential line 241

    Source documentation

    The endpoint defect formula extends to all normalized chains by linearity.

    theorem awEnd_one_differential {m p : ℕ} (θ : Fin (m + 1) →o Fin 2)
    (x : Chains m (p + 1)) :
    awEnd θ 1 p (differential m p x) =
      differential m p (awEnd θ 1 (p + 1) x) + ((-1 : ℤ) ^ p) • awEdge θ p x := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.awEnd, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.awEdge

  20. theorem OAI.Thomason.Construction.SimplexComplex.awEnd_zero_differential line 256

    Source documentation

    The initial endpoint has the opposite boundary defect.

    theorem awEnd_zero_differential {m p : ℕ} (θ : Fin (m + 1) →o Fin 2)
    (x : Chains m (p + 1)) :
    awEnd θ 0 p (differential m p x) =
      differential m p (awEnd θ 0 (p + 1) x) - ((-1 : ℤ) ^ p) • awEdge θ p x := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.awEnd, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.awEdge

  21. theorem OAI.Thomason.Construction.SimplexComplex.awEdge_differential line 274

    Source documentation

    The interval-edge operator commutes with the normalized differential.

    theorem awEdge_differential {m p : ℕ} (θ : Fin (m + 1) →o Fin 2)
    (x : Chains m (p + 2)) :
    awEdge θ p (differential m (p + 1) x) =
      differential m p (awEdge θ (p + 1) x) := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.awEdge, OAI.Thomason.Construction.SimplexComplex.differential

  22. theorem OAI.Thomason.Construction.SimplexComplex.awApp_differential line 298

    Source documentation

    The explicit AW interval formula is a chain map, without a published input.

    theorem awApp_differential (h : NormalizedSimplexIdentities) {m : ℕ}
    (θ : Fin (m + 1) →o Fin 2) (p : ℕ) (x : Chains m (p + 1)) :
    awApp h θ p (differential m p x) =
      (rightCylinder (directedComplex m (h.squared m))).differential p
        (awApp h θ (p + 1) x) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.awApp, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.directedComplex

  23. theorem OAI.Thomason.Construction.SimplexComplex.awEnd_mapBasis line 332

    Source documentation

    The final label of a normalized image is the label of its final vertex.

    theorem awEnd_mapBasis {l m p : ℕ} (a : Fin (l + 1) →o Fin (m + 1))
    (θ : Fin (m + 1) →o Fin 2) (e : Fin 2) (s : Basis l p) :
    awEnd θ e p (mapBasis a p s) =
      if θ (a (s (Fin.last p))) = e then mapBasis a p s else 0 := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.awEnd, OAI.Thomason.Construction.SimplexComplex.mapBasis

  24. theorem OAI.Thomason.Construction.SimplexComplex.awEnd_naturality line 343

    Source documentation

    Endpoint projection commutes with every normalized ordinal map.

    theorem awEnd_naturality {l m p : ℕ} (a : Fin (l + 1) →o Fin (m + 1))
    (θ : Fin (m + 1) →o Fin 2) (e : Fin 2) (x : Chains l p) :
    mapChains a p (awEnd (θ.comp a) e p x) = awEnd θ e p (mapChains a p x) := by
…

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

  25. theorem OAI.Thomason.Construction.SimplexComplex.strictMono_of_prefix line 356

    Source documentation

    A strict prefix and a strict last step give a strict full vertex map.

    theorem strictMono_of_prefix {p m : ℕ} (g : Fin (p + 2) → Fin (m + 1))
    (hp : StrictMono (fun i : Fin (p + 1) => g i.castSucc))
    (hl : g (Fin.last p).castSucc < g (Fin.last (p + 1))) : StrictMono g := by
…
  26. theorem OAI.Thomason.Construction.SimplexComplex.mapBasis_prefix_vanish line 366

    Source documentation

    Crossing the interval prevents a final-vertex collapse from being the only collapse.

    theorem mapBasis_prefix_vanish {l m p : ℕ} (a : Fin (l + 1) →o Fin (m + 1))
    (θ : Fin (m + 1) →o Fin 2) (s : Basis l (p + 1))
    (ha : ¬StrictMono (fun i => a (s i)))
    (hc : θ (a (s (Fin.last p).castSucc)) = 0 ∧
      θ (a (s (Fin.last (p + 1)))) = 1) :
    mapBasis a p (deleteVertex s (Fin.last (p + 1))) = 0 := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.mapBasis, OAI.Thomason.Construction.SimplexComplex.deleteVertex

  27. theorem OAI.Thomason.Construction.SimplexComplex.awEdge_mapBasis line 390

    Source documentation

    The edge component commutes with ordinal maps on each source simplex.

    theorem awEdge_mapBasis {l m p : ℕ} (a : Fin (l + 1) →o Fin (m + 1))
    (θ : Fin (m + 1) →o Fin 2) (s : Basis l (p + 1)) :
    mapChains a p (awEdge (θ.comp a) p (Finsupp.single s 1)) =
      awEdge θ p (mapBasis a (p + 1) s) := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.mapChains, OAI.Thomason.Construction.SimplexComplex.awEdge, OAI.Thomason.Construction.SimplexComplex.mapBasis

  28. theorem OAI.Thomason.Construction.SimplexComplex.awEdge_naturality line 414

    Source documentation

    Edge projection commutes with every normalized ordinal map.

    theorem awEdge_naturality {l m p : ℕ} (a : Fin (l + 1) →o Fin (m + 1))
    (θ : Fin (m + 1) →o Fin 2) (x : Chains l (p + 1)) :
    mapChains a p (awEdge (θ.comp a) p x) = awEdge θ p (mapChains a (p + 1) x) := by
…

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

  29. theorem OAI.Thomason.Construction.SimplexComplex.awApp_naturality line 426

    Source documentation

    The concrete interval diagonal is natural, without a published input.

    theorem awApp_naturality (h : NormalizedSimplexIdentities) {l m : ℕ}
    (a : Fin (l + 1) →o Fin (m + 1)) (θ : Fin (m + 1) →o Fin 2)
    (p : ℕ) (x : Chains l p) :
    (RightCylinder.map (directedMap (h.squared l) (h.squared m) a (h.naturality a))).app p
      (awApp h (θ.comp a) p x) = awApp h θ p (mapChains a p x) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.directedMap, OAI.Thomason.Construction.SimplexComplex.awApp, OAI.Thomason.Construction.SimplexComplex.mapChains

  30. theorem OAI.Thomason.Construction.SimplexComplex.alexanderWhitneyInput line 438

    Source documentation

    Both classical identities for the explicit interval diagonal are proved.

    theorem alexanderWhitneyInput (h : NormalizedSimplexIdentities) : AlexanderWhitneyInput h where
…

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

  31. def OAI.Thomason.Construction.SimplexComplex.coneInclusion line 462

    Source documentation

    Include the old vertices before a new final vertex.

    def coneInclusion (m : ℕ) : Fin (m + 1) →o Fin (m + 2) :=
…
  32. def OAI.Thomason.Construction.SimplexComplex.coneVertex line 466

    Source documentation

    The constant map to the new final vertex.

    def coneVertex (m : ℕ) : Fin (m + 1) →o Fin (m + 2) :=
…
  33. theorem OAI.Thomason.Construction.SimplexComplex.cone_le line 469
  34. def OAI.Thomason.Construction.SimplexComplex.coneChainMap line 473

    Source documentation

    The concrete positive prism from the old simplex to the new vertex.

    noncomputable def coneChainMap (h : NormalizedSimplexIdentities) (m : ℕ) :
    Hom (rightCylinder (directedComplex m (h.squared m)))
      (directedComplex (m + 1) (h.squared (m + 1))) :=
…

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

  35. def OAI.Thomason.Construction.SimplexComplex.coneCell line 481

    Source documentation

    Cone a cell by applying the positive prism to its explicit interval table.

    noncomputable def coneCell (h : NormalizedSimplexIdentities) {m : ℕ} (x : h.object m) :
    h.object (m + 1) :=
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

  36. theorem OAI.Thomason.Construction.SimplexComplex.coneChainMap_succ_app line 486

    Source documentation

    Evaluation of the cone map in a fixed positive degree.

    theorem coneChainMap_succ_app (h : NormalizedSimplexIdentities) (m p : ℕ)
    (z : (rightCylinder (directedComplex m (h.squared m))).group (p + 1)) :
    (coneChainMap h m).app (p + 1) z =
      mapChains (coneInclusion m) (p + 1) z.1 +
      mapChains (coneVertex m) (p + 1) z.2.1 +
      prism (coneInclusion m) (coneVertex m) (cone_le m) p z.2.2 := rfl

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.directedComplex, OAI.Thomason.Construction.SimplexComplex.coneChainMap, OAI.Thomason.Construction.SimplexComplex.mapChains, OAI.Thomason.Construction.SimplexComplex.coneInclusion, OAI.Thomason.Construction.SimplexComplex.coneVertex, OAI.Thomason.Construction.SimplexComplex.prism, OAI.Thomason.Construction.SimplexComplex.cone_le

  37. theorem OAI.Thomason.Construction.SimplexComplex.coneCell_table line 494

    Source documentation

    Evaluation of the cone table, retaining explicit directed-complex types.

    theorem coneCell_table (h : NormalizedSimplexIdentities) {m : ℕ}
    (x : h.object m) (a : Bool) (n : ℕ) :
    (coneCell h x).table a n = (coneChainMap h m).app n
      (RightCylinder.intervalCellTable (K := directedComplex m (h.squared m)) x a n) := rfl

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

  38. theorem OAI.Thomason.Construction.SimplexComplex.coneCell_top line 500

    Source documentation

    The upper chain of the coned cell is the cone of its old upper chain.

    theorem coneCell_top (h : NormalizedSimplexIdentities) {m : ℕ}
    (x : h.object m) (a : Bool) :
    (coneCell h x).table a (m + 1) =
      prism (coneInclusion m) (coneVertex m) (cone_le m) m (x.table a m) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.coneCell, OAI.Thomason.Construction.SimplexComplex.prism, OAI.Thomason.Construction.SimplexComplex.coneInclusion, OAI.Thomason.Construction.SimplexComplex.coneVertex, OAI.Thomason.Construction.SimplexComplex.cone_le

  39. theorem OAI.Thomason.Construction.SimplexComplex.prismBasis_cone_top line 512

    Source documentation

    The prism on a top simplex appends exactly the new final vertex.

    theorem prismBasis_cone_top (m : ℕ) :
    prismBasis (coneInclusion m) (coneVertex m) (cone_le m) m (topBasis m) =
      Finsupp.single (topBasis (m + 1)) 1 := by
…

    Mentions: OAI.Thomason.Construction.SimplexComplex.prismBasis, OAI.Thomason.Construction.SimplexComplex.coneInclusion, OAI.Thomason.Construction.SimplexComplex.coneVertex, OAI.Thomason.Construction.SimplexComplex.cone_le, OAI.Thomason.Construction.SimplexComplex.topBasis

  40. theorem OAI.Thomason.Construction.SimplexComplex.coneCell_source line 531

    Source documentation

    The source of the cone is the inclusion of the old source.

    theorem coneCell_source (h : NormalizedSimplexIdentities) {m : ℕ} (x : h.object m) :
    (h.object (m + 1)).source 0 (coneCell h x) =
      (h.map (coneInclusion m)).toFun ((h.object m).source 0 x) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.coneCell, OAI.Thomason.Construction.SimplexComplex.coneInclusion

  41. theorem OAI.Thomason.Construction.SimplexComplex.coneCell_target line 551

    Source documentation

    The target of the cone is the constant image of the old target.

    theorem coneCell_target (h : NormalizedSimplexIdentities) {m : ℕ} (x : h.object m) :
    (h.object (m + 1)).target 0 (coneCell h x) =
      (h.map (coneVertex m)).toFun ((h.object m).target 0 x) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.coneCell, OAI.Thomason.Construction.SimplexComplex.coneVertex

  42. def OAI.Thomason.Construction.SimplexComplex.principalCell line 571

    Source documentation

    The principal cell, built recursively rather than postulated.

    noncomputable def principalCell (h : NormalizedSimplexIdentities) : (m : ℕ) → h.object m
  | 0 => vertex h 0
  | m + 1 => coneCell h (principalCell h m)

/-- The constructed cell contains exactly the principal top simplex. -/

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.vertex, OAI.Thomason.Construction.SimplexComplex.coneCell, OAI.Thomason.Construction.SimplexComplex.top

  43. theorem OAI.Thomason.Construction.SimplexComplex.principalCell_top line 576

    Source documentation

    The constructed cell contains exactly the principal top simplex.

    theorem principalCell_top (h : NormalizedSimplexIdentities) (m : ℕ) (a : Bool) :
    (principalCell h m).table a m = Finsupp.single (topBasis m) 1 := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.principalCell, OAI.Thomason.Construction.SimplexComplex.topBasis

  44. theorem OAI.Thomason.Construction.SimplexComplex.principalCell_source line 590

    Source documentation

    The initial vertex of the constructed principal cell is zero.

    theorem principalCell_source (h : NormalizedSimplexIdentities) (m : ℕ) :
    (h.object m).source 0 (principalCell h m) = vertex h 0 := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.principalCell, OAI.Thomason.Construction.SimplexComplex.vertex

  45. theorem OAI.Thomason.Construction.SimplexComplex.principalCell_target line 599

    Source documentation

    The final vertex of the constructed principal cell is the last vertex.

    theorem principalCell_target (h : NormalizedSimplexIdentities) (m : ℕ) :
    (h.object m).target 0 (principalCell h m) = vertex h (Fin.last m) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.principalCell, OAI.Thomason.Construction.SimplexComplex.vertex

  46. theorem OAI.Thomason.Construction.SimplexComplex.positive_middle_of_disjoint line 625

    Source documentation

    Two expressions for a middle chain prove its positivity coefficientwise.

    theorem positive_middle_of_disjoint {m p : ℕ} (x y ap am bp bm : Chains m p)
    (hx : x ∈ positive m p) (hy : y ∈ positive m p)
    (hap : ap ∈ positive m p) (hbm : bm ∈ positive m p)
    (he : x + ap - am = y + bm - bp)
    (hd : ∀ b, am b = 0 ∨ bp b = 0) :
    x + ap - am ∈ positive m p := by
…

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

  47. theorem OAI.Thomason.Construction.SimplexComplex.split_of_disjoint_boundaries line 641

    Source documentation

    Ordered, disjoint r-boundaries produce an actual strict binary composite.

    theorem split_of_disjoint_boundaries (h : NormalizedSimplexIdentities) {m : ℕ}
    (X A B : h.object m) (r : ℕ)
    (he : ∀ n, r < n → ∀ side, X.table side n = A.table side n + B.table side n)
    (hd : ∀ b, A.table false r b = 0 ∨ B.table true r b = 0) :
    ∃ (Y Z : h.object m) (hyz : (h.object m).target r Y = (h.object m).source r Z),
      (h.object m).comp r Y Z hyz = X ∧
      (∀ n, r < n → ∀ side, Y.table side n = A.table side n) ∧
      (∀ n, r < n → ∀ side, Z.table side n = B.table side n) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

  48. theorem OAI.Thomason.Construction.SimplexComplex.split_of_disjoint_positiveTables line 661

    Source documentation

    The same splitting allows either upper summand to be a finite sum of atoms: its augmentation need not be one.

    theorem split_of_disjoint_positiveTables (h : NormalizedSimplexIdentities) {m : ℕ}
    (X : h.object m)
    (A B : Cell.PositiveTable (directedComplex m (h.squared m))) (r : ℕ)
    (he : ∀ n, r < n → ∀ side, X.table side n = A.table side n + B.table side n)
    (hd : ∀ b, A.table false r b = 0 ∨ B.table true r b = 0) :
    ∃ (Y Z : h.object m) (hyz : (h.object m).target r Y = (h.object m).source r Z),
      (h.object m).comp r Y Z hyz = X ∧
      (∀ n, r < n → ∀ side, Y.table side n = A.table side n) ∧
      (∀ n, r < n → ∀ side, Z.table side n = B.table side n) := by
…

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

  49. instance OAI.Thomason.Construction.boundarySmallObjectCardinal line 701

    Source documentation

    Finite boundaries permit the ordinary countable small-object argument.

    instance boundarySmallObjectCardinal :
    I.{0}.IsCardinalForSmallObjectArgument Cardinal.aleph0.{0} where
…
  50. instance OAI.Thomason.Construction.boundarySmallObjectArgument line 710
  51. theorem OAI.Thomason.Construction.boundary_left_class line 714

    Source documentation

    The left boundary lifting class is exactly the monomorphisms.

    theorem boundary_left_class : I.{0}.rlp.llp = monomorphisms SSet.{0} := by
…
  52. theorem OAI.Thomason.Construction.boundary_weakFactorizationSystem line 725

    Source documentation

    Actual boundary factorization, independent of the weak-equivalence definition.

    theorem boundary_weakFactorizationSystem :
    IsWeakFactorizationSystem (monomorphisms SSet.{0}) I.rlp := by
…
  53. theorem OAI.Thomason.Construction.horn_weakFactorizationSystem line 732

    Source documentation

    Actual horn factorization, independent of the weak-equivalence definition.

    theorem horn_weakFactorizationSystem :
    IsWeakFactorizationSystem SSet.anodyneExtensions.{0} J.rlp := by
…
  54. theorem OAI.Thomason.Construction.kanQuillenInput_of_semantic_classes line 739

    Source documentation

    Only the semantic identifications remain when supplying the classical Kan–Quillen input: both factorization constructions are already proved.

    theorem kanQuillenInput_of_semantic_classes
    (h2 : realizationWeakEquivalences.{0}.HasTwoOutOfThreeProperty)
    (hb : I.rlp = J.rlp ⊓ realizationWeakEquivalences.{0})
    (hh : SSet.anodyneExtensions.{0} = monomorphisms SSet.{0} ⊓ realizationWeakEquivalences) :
    KanQuillenPublishedInput.{0} where
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  55. structure OAI.Thomason.Construction.SimplicialSpan.Diagram line 764
  56. structure OAI.Thomason.Construction.SimplicialSpan.Hom line 771
  57. def OAI.Thomason.Construction.SimplicialSpan.Hom.id line 780
  58. def OAI.Thomason.Construction.SimplicialSpan.Hom.comp line 787
  59. instance OAI.Thomason.Construction.SimplicialSpan.(instance at line 796) line 796
  60. theorem OAI.Thomason.Construction.SimplicialSpan.comp_a line 804
  61. theorem OAI.Thomason.Construction.SimplicialSpan.comp_b line 806
  62. theorem OAI.Thomason.Construction.SimplicialSpan.comp_c line 808
  63. abbrev OAI.Thomason.Construction.SimplicialSpan.pushout line 811
  64. def OAI.Thomason.Construction.SimplicialSpan.pushoutMap line 813
  65. theorem OAI.Thomason.Construction.SimplicialSpan.inl_pushoutMap line 819
  66. theorem OAI.Thomason.Construction.SimplicialSpan.inr_pushoutMap line 823
  67. def OAI.Thomason.Construction.SimplicialSpan.pushoutFunctor line 827
  68. theorem OAI.Thomason.Construction.SimplicialSpan.pushoutMap_fac line 838

    Source documentation

    The comparison is the supplied fourth map of the actual pushout squares.

    theorem pushoutMap_fac {X Y : Diagram} {P Q : SSet.{0}}
    {b : X.B ⟶ P} {c : X.C ⟶ P} {b' : Y.B ⟶ Q} {c' : Y.C ⟶ Q}
    (hp : IsPushout X.left X.right b c) (hq : IsPushout Y.left Y.right b' c')
    (f : X ⟶ Y) (g : P ⟶ Q) (hb : b ≫ g = f.b ≫ b') (hc : c ≫ g = f.c ≫ c') :
    hp.isoPushout.hom ≫ pushoutMap f ≫ hq.isoPushout.inv = g := by
…

    Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram, OAI.Thomason.Construction.SimplicialSpan.pushoutMap

  69. def OAI.Thomason.Construction.SimplicialSpan.relativeB line 859

    Source documentation

    The relative map at the covariant end of a span.

    noncomputable def relativeB {X Y : Diagram} (f : X ⟶ Y) :
    Limits.pushout X.left f.a ⟶ Y.B := Limits.pushout.desc f.b Y.left f.left_w

    Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram

  70. theorem OAI.Thomason.Construction.SimplicialSpan.inl_relativeB line 862
  71. theorem OAI.Thomason.Construction.SimplicialSpan.inr_relativeB line 866
  72. structure OAI.Thomason.Construction.SimplicialSpan.Prefix line 870
  73. def OAI.Thomason.Construction.SimplicialSpan.factorPrefix line 888

    Source documentation

    Factor first at C and then at the matching object over C.

    noncomputable def factorPrefix {X Y : Diagram} (f : X ⟶ Y) (kq : KanQuillenPublishedInput.{0}) :
    Prefix f := by
…

    Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram, OAI.Thomason.Construction.SimplicialSpan.Prefix

  74. structure OAI.Thomason.Construction.SimplicialSpan.Cofibration line 925

    Source documentation

    The specialized cofibration conditions for this span orientation.

    structure Cofibration {X Y : Diagram} (f : X ⟶ Y) : Prop where
…

    Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram

  75. structure OAI.Thomason.Construction.SimplicialSpan.Factorization line 930
  76. def OAI.Thomason.Construction.SimplicialSpan.factorization line 942

    Source documentation

    The final factorization at B is relative to the already constructed A. No diagram model structure or gluing theorem is assumed.

    noncomputable def factorization {X Y : Diagram} (f : X ⟶ Y)
    (kq : KanQuillenPublishedInput.{0}) : Factorization f := by
…

    Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram, OAI.Thomason.Construction.SimplicialSpan.Factorization