OAI/CategoryTheory/Thomason/Strict/OrientalFiniteCells.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Extracting chains from actual oriental-valued simplices

The normalized-chain presentation identifies strict maps from an oriental to a directed realization with positive augmented chain maps. This uses the atom-generation premise.

  1. def OAI.Thomason.Construction.SimplexAtomsInput.chainOfSimplex line 33

    Source documentation

    The positive chain map represented by an actual Street simplex.

    def chainOfSimplex {K : DirectedComplex.{0}} {m : ℕ}
    (F : h.object m ⟶ K.realization) :
    (directedComplex m (h.squared m)) ⟶ K :=
…
  2. theorem OAI.Thomason.Construction.SimplexAtomsInput.chainOfSimplex_realization line 39

    Source documentation

    Realizing this extracted chain map recovers the entire strict functor.

    theorem chainOfSimplex_realization {K : DirectedComplex.{0}} {m : ℕ}
    (F : h.object m ⟶ K.realization) :
    (a.chainOfSimplex F).realization = F := by
…
  3. theorem OAI.Thomason.Construction.SimplexAtomsInput.chainOfSimplex_precomp line 48

    Source documentation

    Extraction respects precomposition by every simplex operator.

    theorem chainOfSimplex_precomp {K : DirectedComplex.{0}} {l m : ℕ}
    (f : Fin (l+1) →o Fin (m+1)) (F : h.object m ⟶ K.realization) :
    a.chainOfSimplex (h.map f ≫ F) = Hom.comp
      (directedMap (h.squared l) (h.squared m) f (h.naturality f))
        (a.chainOfSimplex F) := by
…
  4. theorem OAI.Thomason.Construction.SimplexAtomsInput.chainOfSimplex_postcomp line 76

    Source documentation

    Extraction respects postcomposition by positive chain maps.

    theorem chainOfSimplex_postcomp {K L : DirectedComplex.{0}} {m : ℕ}
    (F : h.object m ⟶ K.realization) (g : K ⟶ L) :
    a.chainOfSimplex (F ≫ g.realization) = a.chainOfSimplex F ≫ g := by
…
  5. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.weakEquivalence_of_fullStreet_cover line 118

    Source documentation

    The local-to-global weak-equivalence bridge for an actual full cover.

    theorem weakEquivalence_of_fullStreet_cover
    (g : PublishedSimplicialGluingInput) (kq : KanQuillenPublishedInput.{0})
    {X C : StrictOmegaCategory.{0}} (S T : Set C)
    (hc : h.fullStreetSubcomplex C S ⊔ h.fullStreetSubcomplex C T = ⊤)
    (f : X ⟶ C) (fS : X ⟶ C.fullOn S) (fT : X ⟶ C.fullOn T)
    (fI : X ⟶ C.fullOn (S ∩ T))
    (hS : fS ≫ C.fullInclusion S = f) (hT : fT ≫ C.fullInclusion T = f)
    (hI : fI ≫ C.fullInclusion (S ∩ T) = f)
    (wS : h.streetWeakEquivalences fS) (wT : h.streetWeakEquivalences fT)
    (wI : h.streetWeakEquivalences fI) : h.streetWeakEquivalences f := by
…

    Mentions: OAI.Thomason.Construction.PublishedSimplicialGluingInput

  6. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.weakEquivalence_of_sieveStreet_cover line 172

    Source documentation

    In particular the hypotheses on the cover can be checked on objects using the original binary labels of two full sieves.

    theorem weakEquivalence_of_sieveStreet_cover
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {X C : StrictOmegaCategory.{0}} (p q : C ⟶ StrictPoset.category (Fin 2))
    (hc : ∀ x : Objects C, p.toFun x.val = StrictPoset.identity 0 ∨
      q.toFun x.val = StrictPoset.identity 0)
    (f : X ⟶ C) (fS : X ⟶ labelFiber p 0) (fT : X ⟶ labelFiber q 0)
    (fI : X ⟶ C.fullOn
      ({x | p.toFun x = StrictPoset.identity 0} ∩ {x | q.toFun x = StrictPoset.identity 0}))
    (hS : fS ≫ labelFiberInclusion p 0 = f) (hT : fT ≫ labelFiberInclusion q 0 = f)
    (hI : fI ≫ C.fullInclusion _ = f)
    (wS : h.streetWeakEquivalences fS) (wT : h.streetWeakEquivalences fT)
…

    Mentions: OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictPoset.identity

  7. instance OAI.Thomason.Construction.StrictOmegaCategory.globeCoyoneda_preservesFilteredColimits line 206
  8. instance OAI.Thomason.Construction.StrictOmegaCategory.globe_finitelyPresentable line 210
  9. instance OAI.Thomason.Construction.StrictOmegaCategory.locallyFinitelyPresentable line 213
  10. instance OAI.Thomason.Construction.StrictOmegaCategory.locallyPresentable line 220
  11. theorem OAI.Thomason.Construction.StrictOmegaCategory.finite_cells_dimension_bound line 242
  12. theorem OAI.Thomason.Construction.StrictOmegaCategory.comp_self_of_dimensionLE line 250
  13. theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.finite_representatives line 260
  14. theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.finite_equations line 269
  15. theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.finite_hom_descends line 280

    Source documentation

    A finite strict functor into the constructed colimit descends exactly.

    theorem finite_hom_descends (C : StrictOmegaCategory.{0}) [Finite C]
    (f : C ⟶ category F) :
    ∃ (j : J) (g : C ⟶ F.obj j), g ≫ leg F j = f := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.category, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.leg

  16. def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.finiteHomIsColimit line 365
  17. instance OAI.Thomason.Construction.StrictOmegaCategory.finiteCellsCoyoneda_preservesFilteredColimitsOfShape line 383
  18. instance OAI.Thomason.Construction.StrictOmegaCategory.finiteCellsCoyoneda_preservesFilteredColimits line 389
  19. instance OAI.Thomason.Construction.StrictOmegaCategory.finiteCells_finitelyPresentable line 394
  20. theorem OAI.Thomason.Construction.SimplexComplex.alternating_nonneg line 419
  21. def OAI.Thomason.Construction.SimplexComplex.vertexWeight line 440
  22. def OAI.Thomason.Construction.SimplexComplex.chainWeight line 442
  23. def OAI.Thomason.Construction.SimplexComplex.chainMass line 445
  24. theorem OAI.Thomason.Construction.SimplexComplex.chainWeight_single line 448
  25. theorem OAI.Thomason.Construction.SimplexComplex.chainMass_single line 452
  26. theorem OAI.Thomason.Construction.SimplexComplex.vertexWeight_nonneg line 456
  27. theorem OAI.Thomason.Construction.SimplexComplex.vertexWeight_le line 459
  28. theorem OAI.Thomason.Construction.SimplexComplex.vertexWeight_delete line 468
  29. theorem OAI.Thomason.Construction.SimplexComplex.boundary_weight_positive line 475
  30. theorem OAI.Thomason.Construction.SimplexComplex.chainWeight_nonneg line 504
  31. theorem OAI.Thomason.Construction.SimplexComplex.chainMass_nonneg line 510
  32. theorem OAI.Thomason.Construction.SimplexComplex.coefficient_le_mass line 516
  33. theorem OAI.Thomason.Construction.SimplexComplex.chainWeight_le_mass line 525
  34. theorem OAI.Thomason.Construction.SimplexComplex.chainMass_le_boundaryWeight line 535
  35. def OAI.Thomason.Construction.SimplexComplex.tableMassBound line 549
  36. theorem OAI.Thomason.Construction.SimplexComplex.cell_mass_le line 553
  37. theorem OAI.Thomason.Construction.SimplexComplex.cell_coefficient_bounds line 573
  38. def OAI.Thomason.Construction.SimplexComplex.finiteCellCode line 578
  39. theorem OAI.Thomason.Construction.SimplexComplex.finiteCellCode_injective line 585
  40. instance OAI.Thomason.Construction.SimplexComplex.oriental_finite line 601
  41. instance OAI.Thomason.Construction.SimplexComplex.oriental_finitelyPresentable line 604