OAI/CategoryTheory/Thomason/Simplicial/LastVertexWeakEquivalence.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thomason.Construction.lastVertex_initial_weak line 31
2. theorem OAI.Thomason.Construction.lastVertex_face_weak line 40

   Source documentation

   The original last-vertex component is weak on any individual face.

   theorem lastVertex_face_weak {n : ℕ} (S : Finset (Fin (n+1))) :
       realizationWeakEquivalences (lastVertex.app (SSet.stdSimplex.face S : SSet.{0})) := by
   …

   Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

3. theorem OAI.Thomason.Construction.lastVertex_union_weak line 57

   Source documentation

   Actual last-vertex comparison is compatible with geometric gluing.

   theorem lastVertex_union_weak {n : ℕ} (A B : (Δ[n] : SSet.{0}).Subcomplex)
       (hi : Mono (subdivisionInclusion (A ⊓ B)))
       (hI : realizationWeakEquivalences (lastVertex.app ((A ⊓ B).toSSet)))
       (hA : realizationWeakEquivalences (lastVertex.app (A : SSet)))
       (hB : realizationWeakEquivalences (lastVertex.app (B : SSet))) :
       realizationWeakEquivalences (lastVertex.app ((A ⊔ B).toSSet)) := by
   …

   Mentions: OAI.Thomason.Construction.subdivisionInclusion, OAI.Thomason.Construction.realizationWeakEquivalences

4. theorem OAI.Thomason.Construction.lastVertex_faceUnion_weak_aux line 73
5. theorem OAI.Thomason.Construction.lastVertex_faceUnion_weak line 108

   Source documentation

   No last-vertex or Kan–Quillen hypothesis: this uses the explicit chain contractions and the proved weak-equivalence gluing theorem.

   theorem lastVertex_faceUnion_weak {n : ℕ} (F : Finset (Finset (Fin (n+1)))) :
       realizationWeakEquivalences (lastVertex.app (faceUnion F : SSet)) :=
   …

   Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.faceUnion

6. theorem OAI.Thomason.Construction.NonsingularLastVertex.proper_subset_card_lt line 136
7. theorem OAI.Thomason.Construction.NonsingularLastVertex.restrictedMap_weak_finite line 150

   Source documentation

   The actual comparison on any finite lower set of nondegenerate faces is a realization weak equivalence.

   theorem restrictedMap_weak_finite (S : Set X.N) (hS : IsLowerSet S) [Finite S] :
       realizationWeakEquivalences (restrictedMap S) := by
   …

   Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.NonsingularLastVertex.restrictedMap

8. theorem OAI.Thomason.Construction.NonsingularLastVertex.univ_nerveMap_isIso line 207
9. theorem OAI.Thomason.Construction.NonsingularLastVertex.map_weak line 227

   Source documentation

   Every finite nonsingular simplicial set has its actual finite face poset as a weakly equivalent simplicial model.

   theorem map_weak (X : SSet.{0}) [X.Nonsingular] [X.Finite] :
       realizationWeakEquivalences (map X) := by
   …

   Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.NonsingularLastVertex.map

10. def OAI.Thomason.Construction.boundaryFaces line 260
11. theorem OAI.Thomason.Construction.faceUnion_boundaryFaces line 263
12. theorem OAI.Thomason.Construction.subdivision_boundary_mono line 272

    Source documentation

    No identifications are introduced in subdividing the entire boundary.

    theorem subdivision_boundary_mono (n : ℕ) :
        Mono (SSet.sd.map (SSet.boundary.{0} n).ι) := by
    …

13. theorem OAI.Thomason.Construction.subdivision_boundary_range line 282

    Source documentation

    Exact finite-chain image of the subdivided whole boundary.

    theorem subdivision_boundary_range (n : ℕ) :
        SSet.Subcomplex.range (subdivisionInclusion (SSet.boundary.{0} n)) =
          subdividedFaceUnion (boundaryFaces n) := by
    …

    Mentions: OAI.Thomason.Construction.subdivisionInclusion, OAI.Thomason.Construction.subdividedFaceUnion, OAI.Thomason.Construction.boundaryFaces

14. theorem OAI.Thomason.Construction.lastVertex_boundary_weak line 290

    Source documentation

    The last-vertex map on every boundary is an actual realization weak equivalence, derived by finite face gluing.

    theorem lastVertex_boundary_weak (n : ℕ) :
        realizationWeakEquivalences (lastVertex.app (SSet.boundary.{0} n : SSet)) := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

15. theorem OAI.Thomason.Construction.extension_boundary_rlp line 316

    Source documentation

    Extension preserves the algebraic boundary right lifting class.

    theorem extension_boundary_rlp {X Y : SSet.{0}} (p : X ⟶ Y) (hp : I.rlp p) :
        I.rlp (SSet.ex.map p) := by
    …

16. theorem OAI.Thomason.Construction.subdivision_map_mono line 327

    Source documentation

    The actual left-Kan-extension subdivision functor preserves every simplicial monomorphism, with no semantic model-category assumption.

    theorem subdivision_map_mono {X Y : SSet.{0}} (f : X ⟶ Y) [Mono f] :
        Mono (SSet.sd.map f) := by
    …

17. theorem OAI.Thomason.Construction.lastVertex_coproduct_weak line 355

    Source documentation

    Last vertex commutes with arbitrary simultaneous cell families.

    theorem lastVertex_coproduct_weak {α : Type} (K : α → SSet.{0})
        (hK : ∀ a, realizationWeakEquivalences (lastVertex.app (K a))) :
        realizationWeakEquivalences (lastVertex.app (∐ K)) := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

18. theorem OAI.Thomason.Construction.lastVertex_skeletonOfEmpty_weak line 371

    Source documentation

    Every finite-dimensional stage of the actual relative skeletal filtration has a weak last-vertex component. No finiteness of the cell set is required.

    theorem lastVertex_skeletonOfEmpty_weak (K : SSet.{0}) (n : ℕ) :
        realizationWeakEquivalences (lastVertex.app
          ((SSet.skeletonOfMono (⊥ : K.Subcomplex).ι n).toSSet)) := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

19. def OAI.Thomason.Construction.subcomplexExhaustionCocone line 413
20. def OAI.Thomason.Construction.subcomplexExhaustionIsColimit line 417
21. def OAI.Thomason.Construction.subdivisionExhaustion line 423
22. theorem OAI.Thomason.Construction.subdivisionExhaustion_monotone line 427
23. theorem OAI.Thomason.Construction.iSup_subdivisionExhaustion line 438
24. def OAI.Thomason.Construction.subdivisionRangeIso line 449
25. theorem OAI.Thomason.Construction.subdivisionRangeIso_hom_ι line 459
26. def OAI.Thomason.Construction.lastVertexExhaustionMap line 464

    Source documentation

    The last-vertex map restricted to each actual subdivision image stage.

    def lastVertexExhaustionMap (n : ℕ) :
        (subdivisionExhaustion A n).toSSet ⟶ (A n).toSSet :=
    …

    Mentions: OAI.Thomason.Construction.subdivisionExhaustion

27. theorem OAI.Thomason.Construction.lastVertexExhaustionMap_fac line 468
28. theorem OAI.Thomason.Construction.lastVertex_weak_of_exhaustion line 481

    Source documentation

    Stagewise last-vertex weak equivalences pass to the exhausted simplicial set, using exact compact factorization of cubes and their based homotopies.

    theorem lastVertex_weak_of_exhaustion (hc : iSup A = ⊤)
        (hw : ∀ n, realizationWeakEquivalences (lastVertex.app (A n).toSSet)) :
        realizationWeakEquivalences (lastVertex.app K) := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

29. theorem OAI.Thomason.Construction.FaceSimplexResolution.augmentation_initial_weak line 514
30. theorem OAI.Thomason.Construction.FaceSimplexResolution.augmentation_face_weak line 522
31. theorem OAI.Thomason.Construction.FaceSimplexResolution.augmentation_union_weak line 538
32. theorem OAI.Thomason.Construction.FaceSimplexResolution.augmentation_faceUnion_weak_aux line 549
33. theorem OAI.Thomason.Construction.FaceSimplexResolution.augmentation_boundary_weak line 577
34. theorem OAI.Thomason.Construction.FaceSimplexResolution.augmentation_coproduct_weak line 582
35. theorem OAI.Thomason.Construction.FaceSimplexResolution.augmentation_skeleton_weak line 595
36. def OAI.Thomason.Construction.FaceSimplexResolution.exhaustion line 617
37. theorem OAI.Thomason.Construction.FaceSimplexResolution.exhaustion_monotone line 621
38. theorem OAI.Thomason.Construction.FaceSimplexResolution.iSup_exhaustion line 632
39. def OAI.Thomason.Construction.FaceSimplexResolution.rangeIso line 641
40. theorem OAI.Thomason.Construction.FaceSimplexResolution.rangeIso_hom_ι line 649
41. def OAI.Thomason.Construction.FaceSimplexResolution.exhaustionMap line 652
42. theorem OAI.Thomason.Construction.FaceSimplexResolution.exhaustionMap_fac line 655
43. theorem OAI.Thomason.Construction.FaceSimplexResolution.augmentation_weak_of_exhaustion line 665
44. theorem OAI.Thomason.Construction.FaceSimplexResolution.augmentation_weak line 677

    Source documentation

    An unconditional comparison for every small simplicial set, including arbitrary singular simplicial sets.

    theorem augmentation_weak (K : SSet.{0}) :
        realizationWeakEquivalences (augmentation K) := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.FaceSimplexResolution.augmentation

45. theorem OAI.Thomason.Construction.FaceSimplexResolution.finite_relative_resolved_lift line 705
46. theorem OAI.Thomason.Construction.NonsingularLastVertex.faceMap_injective line 747
47. instance OAI.Thomason.Construction.NonsingularLastVertex.faceMap_nerve_mono line 764
48. theorem OAI.Thomason.Construction.NonsingularLastVertex.relative_facePoset_lift line 777

    Source documentation

    Lifting through the finite face-poset comparison makes the boundary an exact order map. Only the projection to the old target is homotopic.

    theorem relative_facePoset_lift {A B K : SSet.{0}}
        [A.Nonsingular] [B.Nonsingular] [K.Nonsingular] [K.Finite]
        (i : A ⟶ B) [Mono i] (a : A ⟶ K) (ha : PreservesNondegenerate a)
        (b : SSet.toTop.obj B ⟶ SSet.toTop.obj K)
        (h : SSet.toTop.map i ≫ b = SSet.toTop.map a) :
        ∃ c : SSet.toTop.obj (nerve B.N) ⟶ SSet.toTop.obj (nerve K.N),
          SSet.toTop.map (nerveMap (faceMap i (preservesNondegenerate_of_mono i)).monotone.functor)
            ≫ c = SSet.toTop.map (nerveMap (faceMap a ha).monotone.functor) ∧
          Nonempty ((c ≫ SSet.toTop.map (map K)).hom.HomotopyRel
            (SSet.toTop.map (map B) ≫ b).hom
            (Set.range (SSet.toTop.map
              (nerveMap (faceMap i (preservesNondegenerate_of_mono i)).monotone.functor)).hom)) := by
    …

    Mentions: OAI.Thomason.Construction.NonsingularLastVertex.PreservesNondegenerate, OAI.Thomason.Construction.NonsingularLastVertex.faceMap, OAI.Thomason.Construction.NonsingularLastVertex.preservesNondegenerate_of_mono, OAI.Thomason.Construction.NonsingularLastVertex.map

49. theorem OAI.Thomason.Construction.FaceSimplexResolution.finite_relative_order_lift line 812

    Source documentation

    An arbitrary original boundary map admits a continuous relative extension into a finite poset nerve after the two specified face-poset comparisons. The equation back in the original target is literal.

    theorem finite_relative_order_lift {A B X : SSet.{0}}
        [A.Nonsingular] [B.Nonsingular] [B.Finite]
        (i : nerve A.N ⟶ B) [Mono i] (a : A ⟶ X)
        (b : SSet.toTop.obj B ⟶ SSet.toTop.obj X)
        (h : SSet.toTop.map (NonsingularLastVertex.map A ≫ a) = SSet.toTop.map i ≫ b) :
        ∃ (S : (functor.obj X).Subcomplex) (_ : SSet.Finite S.toSSet)
          (a' : nerve A.N ⟶ S.toSSet)
          (ha' : NonsingularLastVertex.PreservesNondegenerate a')
          (c : SSet.toTop.obj (nerve B.N) ⟶ SSet.toTop.obj (nerve S.toSSet.N)),
          a' ≫ S.ι = resolvedMap a ∧
          SSet.toTop.map (nerveMap (NonsingularLastVertex.faceMap i
            (NonsingularLastVertex.preservesNondegenerate_of_mono i)).monotone.functor) ≫ c =
    …

    Mentions: OAI.Thomason.Construction.NonsingularLastVertex.map, OAI.Thomason.Construction.NonsingularLastVertex.PreservesNondegenerate, OAI.Thomason.Construction.FaceSimplexResolution.resolvedMap, OAI.Thomason.Construction.NonsingularLastVertex.faceMap, OAI.Thomason.Construction.NonsingularLastVertex.preservesNondegenerate_of_mono

50. theorem OAI.Thomason.Construction.FaceSimplexResolution.finite_relative_order_lift_with_comparison line 857
51. def OAI.Thomason.Construction.FiniteSimplicialExhaustion.support line 938
52. instance OAI.Thomason.Construction.FiniteSimplicialExhaustion.support_finite line 941
53. theorem OAI.Thomason.Construction.FiniteSimplicialExhaustion.support_monotone line 946
54. theorem OAI.Thomason.Construction.FiniteSimplicialExhaustion.iSup_support line 952
55. abbrev OAI.Thomason.Construction.FiniteSimplicialExhaustion.diagram line 962
56. def OAI.Thomason.Construction.FiniteSimplicialExhaustion.cocone line 965
57. def OAI.Thomason.Construction.FiniteSimplicialExhaustion.isColimit line 969
58. theorem OAI.Thomason.Construction.lastVertex_weak line 995

    Source documentation

    Last vertex on the actual left-Kan-extension subdivision is an actual geometric-realization weak equivalence for every small simplicial set.

    theorem lastVertex_weak (K : SSet.{0}) :
        realizationWeakEquivalences (lastVertex.app K) := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

59. theorem OAI.Thomason.Construction.subdivision_weak_iff line 1003

    Source documentation

    Subdivision preserves and reflects the actual weak-equivalence class.

    theorem subdivision_weak_iff {K L : SSet.{0}} (f : K ⟶ L) :
        realizationWeakEquivalences (SSet.sd.map f) ↔ realizationWeakEquivalences f :=
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

60. theorem OAI.Thomason.Construction.subdivision_twice_weak_iff line 1009

    Source documentation

    The same compatibility for the double subdivision in the Thomason adjunction.

    theorem subdivision_twice_weak_iff {K L : SSet.{0}} (f : K ⟶ L) :
        realizationWeakEquivalences ((SSet.sd ⋙ SSet.sd).map f) ↔
          realizationWeakEquivalences f :=
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

61. theorem OAI.Thomason.Construction.nerve_subdivision_weak_equivalences_eq line 1016

    Source documentation

    Applied to an actual nerve, double subdivision detects precisely the original weak equivalences.

    theorem nerve_subdivision_weak_equivalences_eq {C : Type*} [Category* C]
        (N : C ⥤ SSet.{0}) :
        realizationWeakEquivalences.inverseImage (N ⋙ SSet.sd ⋙ SSet.sd) =
          realizationWeakEquivalences.inverseImage N := by
    …