OAI/CategoryTheory/Thomason/Simplicial/FaceSimplexLift.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thomason.Construction.discreteCoproductCocone line 36

   Source documentation

   The chosen coproduct also presents a discrete diagram not syntactically written as Discrete.functor.

   def discreteCoproductCocone : Cocone F where
   …

2. def OAI.Thomason.Construction.discreteCoproductIsColimit line 41

   Source documentation

   Its universal property follows directly from the coproduct universal property.

   def discreteCoproductIsColimit : IsColimit (discreteCoproductCocone F) where
   …

   Mentions: OAI.Thomason.Construction.discreteCoproductCocone

3. def OAI.Thomason.Construction.discreteCoproductIso line 50

   Source documentation

   Comparison from the chosen coproduct to any colimit of the same diagram.

   def discreteCoproductIso {c : Cocone F} (hc : IsColimit c) :
       (∐ fun a => F.obj ⟨a⟩) ≅ c.pt :=
   …

4. theorem OAI.Thomason.Construction.discreteCoproductIso_fac line 55
5. def OAI.Thomason.Construction.chainMaximum line 84

   Source documentation

   The greatest vertex of a finite nonempty chain in a linear order.

   noncomputable def chainMaximum {X : Type*} [LinearOrder X]
       (A : NonemptyFiniteChains X) : X := A.finset.max' A.nonempty

6. theorem OAI.Thomason.Construction.chainMaximum_monotone line 87
7. theorem OAI.Thomason.Construction.chainMaximum_eq_chainGreatest line 95

   Source documentation

   The finite maximum agrees with the greatest element of the chain.

   theorem chainMaximum_eq_chainGreatest {X : Type*} [LinearOrder X]
       (A : NonemptyFiniteChains X) :
       chainMaximum A = Thomason.Subdivision.chainGreatest A := by
   …

   Mentions: OAI.Thomason.Construction.chainMaximum, OAI.Thomason.Subdivision.chainGreatest

8. def OAI.Thomason.Construction.chainMaximumHom line 105

   Source documentation

   Greatest vertex as an order-preserving map.

   noncomputable def chainMaximumHom {X : Type*} [LinearOrder X] :
       NonemptyFiniteChains X →o X :=
   …

9. theorem OAI.Thomason.Construction.chainMaximum_map line 110

   Source documentation

   Monotone maps commute with the greatest-vertex operation.

   theorem chainMaximum_map {X Y : Type*} [LinearOrder X] [LinearOrder Y]
       (f : X →o Y) (A : NonemptyFiniteChains X) :
       chainMaximum (A.map f) = f (chainMaximum A) := by
   …

   Mentions: OAI.Thomason.Construction.chainMaximum

10. def OAI.Thomason.Construction.simplexChainMaximum line 124

    Source documentation

    Greatest vertex as a natural transformation on the finite ordered sets indexing simplicial sets.

    noncomputable def simplexChainMaximum :
        (SimplexCategory.toPartOrd.{u} ⋙ PartOrd.nonemptyFiniteChainsFunctor) ⟶
          SimplexCategory.toPartOrd.{u} where
    …

11. theorem OAI.Thomason.Construction.simplexChainMaximum_eq line 137

    Source documentation

    The simplex maximum is the restriction of the greatest-chain transformation.

    theorem simplexChainMaximum_eq :
        simplexChainMaximum.{u} = Functor.whiskerLeft SimplexCategory.toPartOrd
          Thomason.Subdivision.chainLastNat := by
    …

    Mentions: OAI.Thomason.Subdivision.chainLastNat

12. def OAI.Thomason.Construction.simplexNerveIso line 147

    Source documentation

    The standard cosimplicial simplex is the nerve of its ordered vertex set.

    def simplexNerveIso :
        SSet.stdSimplex.{u} ≅ SimplexCategory.toPartOrd.{u} ⋙ PartOrd.nerveFunctor :=
    …

13. def OAI.Thomason.Construction.simplexLastVertex line 155

    Source documentation

    The last-vertex map on the subdivisions of the standard simplices.

    noncomputable def simplexLastVertex : SimplexCategory.sd.{u} ⟶ SSet.stdSimplex.{u} :=
    …

14. theorem OAI.Thomason.Construction.simplexLastVertex_eq line 159

    Source documentation

    The simplex comparison agrees with the greatest-chain construction.

    theorem simplexLastVertex_eq :
        simplexLastVertex.{u} = Thomason.Subdivision.simplexLastVertex := by
    …

    Mentions: OAI.Thomason.Subdivision.simplexLastVertex

15. def OAI.Thomason.Construction.lastVertex line 166

    Source documentation

    The last-vertex map Sd K ⟶ K, defined for every simplicial set.

    noncomputable def lastVertex : SSet.sd.{u} ⟶ 𝟭 SSet.{u} :=
    …

16. theorem OAI.Thomason.Construction.lastVertex_eq line 170

    Source documentation

    Both greatest-vertex constructions extend to the same subdivision map.

    theorem lastVertex_eq : lastVertex.{u} = Thomason.Subdivision.lastVertex := by
    …

    Mentions: OAI.Thomason.Subdivision.lastVertex

17. theorem OAI.Thomason.Construction.lastVertex_on_standard_simplex line 175

    Source documentation

    On a standard simplex the last-vertex map is induced by greatest vertex.

    theorem lastVertex_on_standard_simplex (n : SimplexCategory) :
        SSet.stdSimplex.sdIso.inv.app n ≫ lastVertex.app (SSet.stdSimplex.obj n) =
          simplexLastVertex.app n :=
    …

18. def OAI.Thomason.Construction.FaceSimplexResolution.restriction line 201
19. abbrev OAI.Thomason.Construction.FaceSimplexResolution.Face line 205
20. def OAI.Thomason.Construction.FaceSimplexResolution.projection line 207
21. def OAI.Thomason.Construction.FaceSimplexResolution.functor line 210
22. def OAI.Thomason.Construction.FaceSimplexResolution.cell line 213
23. theorem OAI.Thomason.Construction.FaceSimplexResolution.cell_map line 215
24. instance OAI.Thomason.Construction.FaceSimplexResolution.(instance at line 218) line 218
25. def OAI.Thomason.Construction.FaceSimplexResolution.vertex line 223
26. theorem OAI.Thomason.Construction.FaceSimplexResolution.vertex_monotone line 229
27. def OAI.Thomason.Construction.FaceSimplexResolution.ordinal line 244
28. def OAI.Thomason.Construction.FaceSimplexResolution.simplex line 249
29. theorem OAI.Thomason.Construction.FaceSimplexResolution.ordinal_naturality line 253
30. theorem OAI.Thomason.Construction.FaceSimplexResolution.simplex_naturality line 269
31. def OAI.Thomason.Construction.FaceSimplexResolution.augmentation line 278
32. theorem OAI.Thomason.Construction.FaceSimplexResolution.augmentation_naturality line 286

    Source documentation

    The augmentation has the original simplicial set as its natural codomain.

    theorem augmentation_naturality {X Y : SSet.{0}} (f : X ⟶ Y) :
        functor.map f ≫ augmentation Y = augmentation X ≫ f := by
    …

    Mentions: OAI.Thomason.Construction.FaceSimplexResolution.augmentation

33. def OAI.Thomason.Construction.FaceSimplexResolution.augmentationNatTrans line 296
34. def OAI.Thomason.Construction.FaceSimplexResolution.semiProjection line 322
35. instance OAI.Thomason.Construction.FaceSimplexResolution.(instance at line 325) line 325
36. abbrev OAI.Thomason.Construction.FaceSimplexResolution.Shape line 331
37. def OAI.Thomason.Construction.FaceSimplexResolution.ofShape line 333
38. theorem OAI.Thomason.Construction.FaceSimplexResolution.ofShape_projection line 359
39. theorem OAI.Thomason.Construction.FaceSimplexResolution.ofShape_cell line 362
40. theorem OAI.Thomason.Construction.FaceSimplexResolution.ofShape_reconstruct line 370
41. def OAI.Thomason.Construction.FaceSimplexResolution.shapeEquiv line 390

    Source documentation

    In each degree the resolution is a disjoint union of evaluations of X.

    def shapeEquiv (X : SSet.{0}) (n : ℕ) :
        (functor.obj X) _⦋n⦌ ≃
          Σ s : Shape n, X.obj (.op (SemiSimplexCategory.toSimplexCategory.obj
            (s.obj (Fin.last n)))) where
    …

    Mentions: OAI.Thomason.Construction.FaceSimplexResolution.Shape

42. theorem OAI.Thomason.Construction.FaceSimplexResolution.shapeEquiv_naturality line 403

    Source documentation

    The shape is unchanged by a map of simplicial sets; only the final simplex is mapped.

    theorem shapeEquiv_naturality {X Y : SSet.{0}} (f : X ⟶ Y) (n : ℕ)
        (s : (functor.obj X) _⦋n⦌) :
        shapeEquiv Y n ((functor.map f).app _ s) =
          ⟨(shapeEquiv X n s).1, f.app _ (shapeEquiv X n s).2⟩ := rfl

    Mentions: OAI.Thomason.Construction.FaceSimplexResolution.shapeEquiv

43. theorem OAI.Thomason.Construction.FaceSimplexResolution.ofShape_naturality line 408
44. instance OAI.Thomason.Construction.FaceSimplexResolution.map_mono line 417
45. abbrev OAI.Thomason.Construction.FaceSimplexResolution.shapeEvaluation line 456
46. instance OAI.Thomason.Construction.FaceSimplexResolution.(instance at line 460) line 460
47. def OAI.Thomason.Construction.FaceSimplexResolution.shapeDiagram line 464
48. instance OAI.Thomason.Construction.FaceSimplexResolution.(instance at line 468) line 468
49. def OAI.Thomason.Construction.FaceSimplexResolution.degreeCoproductIso line 474
50. instance OAI.Thomason.Construction.FaceSimplexResolution.(instance at line 504) line 504
51. def OAI.Thomason.Construction.FaceSimplexResolution.dimension line 530
52. theorem OAI.Thomason.Construction.FaceSimplexResolution.dimension_le line 532
53. theorem OAI.Thomason.Construction.FaceSimplexResolution.simplex_mono_eqToHom line 535
54. theorem OAI.Thomason.Construction.FaceSimplexResolution.face_eq_of_dimension_eq line 540
55. theorem OAI.Thomason.Construction.FaceSimplexResolution.face_endomorphism_eq_id line 557
56. theorem OAI.Thomason.Construction.FaceSimplexResolution.face_map_eqToHom line 565
57. def OAI.Thomason.Construction.FaceSimplexResolution.repeatDeletion line 570
58. theorem OAI.Thomason.Construction.FaceSimplexResolution.repeatDeletion_apply line 573
59. theorem OAI.Thomason.Construction.FaceSimplexResolution.le_repeatDeletion line 583
60. theorem OAI.Thomason.Construction.FaceSimplexResolution.degenerate_of_dimension_eq line 594

    Source documentation

    Equal consecutive dimensions give the actual simplicial degeneracy, including all arrows of the flag.

    theorem degenerate_of_dimension_eq {X : SSet.{0}} {n : ℕ}
        (s : (nerve (Face X)) _⦋n+1⦌) (i : Fin (n+1))
        (h : dimension (s.obj i.castSucc) = dimension (s.obj i.succ)) :
        s ∈ (nerve (Face X)).degenerate (n+1) := by
    …

    Mentions: OAI.Thomason.Construction.FaceSimplexResolution.Face, OAI.Thomason.Construction.FaceSimplexResolution.dimension

61. theorem OAI.Thomason.Construction.FaceSimplexResolution.nondegenerate_dimension_strictMono line 628
62. instance OAI.Thomason.Construction.FaceSimplexResolution.(instance at line 643) line 643
63. def OAI.Thomason.Construction.fullSubposetComplex line 681

    Source documentation

    The full subcomplex of the ordinary nerve on a set of vertices.

    def fullSubposetComplex (A : Set E) : (nerve E).Subcomplex where
    …

64. theorem OAI.Thomason.Construction.mem_fullSubposetComplex line 686
65. def OAI.Thomason.Construction.fullSubposetInclusion line 691

    Source documentation

    The ordinary functor including the full induced subposet.

    def fullSubposetInclusion (A : Set E) : A ⥤ E :=
    …

66. def OAI.Thomason.Construction.liftSimplexToSubposet line 695

    Source documentation

    Every simplex whose vertices lie in A lifts to the nerve of A.

    def liftSimplexToSubposet (A : Set E) {Δ : SimplexCategoryᵒᵖ}
        (s : (nerve E).obj Δ) (hs : ∀ i, s.obj i ∈ A) : (nerve A).obj Δ where
    …

67. theorem OAI.Thomason.Construction.nerveMap_liftSimplexToSubposet line 701
68. theorem OAI.Thomason.Construction.fullSubposetComplex_eq_range line 708

    Source documentation

    The vertex-defined subcomplex is the actual image of the nerve of the full induced subposet.

    theorem fullSubposetComplex_eq_range (A : Set E) :
        fullSubposetComplex A = SSet.Subcomplex.range (nerveMap (fullSubposetInclusion A)) := by
    …

    Mentions: OAI.Thomason.Construction.fullSubposetComplex, OAI.Thomason.Construction.fullSubposetInclusion

69. theorem OAI.Thomason.Construction.fullSubposetComplex_inter line 718

    Source documentation

    The intersection of full subposet nerves is the nerve of the intersection.

    theorem fullSubposetComplex_inter (A B : Set E) :
        fullSubposetComplex (A ∩ B) = fullSubposetComplex A ⊓ fullSubposetComplex B := by
    …

    Mentions: OAI.Thomason.Construction.fullSubposetComplex

70. theorem OAI.Thomason.Construction.fullSubposetComplex_isPushout line 729

    Source documentation

    A cover of the ordinary nerve by full subcomplexes is an ordinary pushout along the common full subcomplex.

    theorem fullSubposetComplex_isPushout (A B : Set E)
        (hcover : fullSubposetComplex A ⊔ fullSubposetComplex B = ⊤) :
        IsPushout
          (SSet.Subcomplex.homOfLE (show fullSubposetComplex (A ∩ B) ≤
            fullSubposetComplex A from fun _ _ h i => (h i).1))
          (SSet.Subcomplex.homOfLE (show fullSubposetComplex (A ∩ B) ≤
            fullSubposetComplex B from fun _ _ h i => (h i).2))
          (fullSubposetComplex A).ι (fullSubposetComplex B).ι := by
    …

    Mentions: OAI.Thomason.Construction.fullSubposetComplex

71. theorem OAI.Thomason.Construction.vertex_mem_of_last_mem line 745

    Source documentation

    A sieve containing the final vertex contains every vertex of a simplex.

    theorem vertex_mem_of_last_mem {A : Set E} (hA : IsLowerSet A)
        {Δ : SimplexCategoryᵒᵖ} (s : (nerve E).obj Δ)
        (hlast : s.obj (Fin.last Δ.unop.len) ∈ A)
        (i : Fin (Δ.unop.len + 1)) : s.obj i ∈ A :=
    …

72. theorem OAI.Thomason.Construction.mem_fullSubposetComplex_iff_last line 752

    Source documentation

    Membership in a full sieve nerve is detected at the final vertex.

    theorem mem_fullSubposetComplex_iff_last {A : Set E} (hA : IsLowerSet A)
        {Δ : SimplexCategoryᵒᵖ} (s : (nerve E).obj Δ) :
        s ∈ (fullSubposetComplex A).obj Δ ↔ s.obj (Fin.last Δ.unop.len) ∈ A :=
    …

    Mentions: OAI.Thomason.Construction.fullSubposetComplex

73. theorem OAI.Thomason.Construction.simplex_mem_of_sieve_cover line 758

    Source documentation

    Two sieves covering the vertices cover every simplex of the ordinary nerve.

    theorem simplex_mem_of_sieve_cover {A B : Set E}
        (hA : IsLowerSet A) (hB : IsLowerSet B) (hcover : ∀ e, e ∈ A ∨ e ∈ B)
        {Δ : SimplexCategoryᵒᵖ} (s : (nerve E).obj Δ) :
        s ∈ (fullSubposetComplex A).obj Δ ∨ s ∈ (fullSubposetComplex B).obj Δ :=
    …

    Mentions: OAI.Thomason.Construction.fullSubposetComplex

74. theorem OAI.Thomason.Construction.sieve_nerve_cover line 766

    Source documentation

    The actual ordinary nerve is the union of the nerves of two covering sieves.

    theorem sieve_nerve_cover {A B : Set E}
        (hA : IsLowerSet A) (hB : IsLowerSet B) (hcover : ∀ e, e ∈ A ∨ e ∈ B) :
        fullSubposetComplex A ⊔ fullSubposetComplex B = ⊤ := by
    …

    Mentions: OAI.Thomason.Construction.fullSubposetComplex

75. theorem OAI.Thomason.Construction.sieve_nerve_isPushout line 775

    Source documentation

    The two covering sieve nerves and their intersection form an actual pushout square in simplicial sets.

    theorem sieve_nerve_isPushout {A B : Set E}
        (hA : IsLowerSet A) (hB : IsLowerSet B) (hcover : ∀ e, e ∈ A ∨ e ∈ B) :
        IsPushout
          (SSet.Subcomplex.homOfLE (show fullSubposetComplex (A ∩ B) ≤
            fullSubposetComplex A from fun _ _ h i => (h i).1))
          (SSet.Subcomplex.homOfLE (show fullSubposetComplex (A ∩ B) ≤
            fullSubposetComplex B from fun _ _ h i => (h i).2))
          (fullSubposetComplex A).ι (fullSubposetComplex B).ι :=
    …

    Mentions: OAI.Thomason.Construction.fullSubposetComplex

76. theorem OAI.Thomason.Construction.vertex_mem_of_first_mem line 786

    Source documentation

    A cosieve containing the initial vertex contains every simplex vertex.

    theorem vertex_mem_of_first_mem {A : Set E} (hA : IsUpperSet A)
        {Δ : SimplexCategoryᵒᵖ} (s : (nerve E).obj Δ)
        (hfirst : s.obj 0 ∈ A) (i : Fin (Δ.unop.len + 1)) : s.obj i ∈ A :=
    …

77. theorem OAI.Thomason.Construction.mem_fullSubposetComplex_iff_first line 792

    Source documentation

    Membership in a full cosieve nerve is detected at the initial vertex.

    theorem mem_fullSubposetComplex_iff_first {A : Set E} (hA : IsUpperSet A)
        {Δ : SimplexCategoryᵒᵖ} (s : (nerve E).obj Δ) :
        s ∈ (fullSubposetComplex A).obj Δ ↔ s.obj 0 ∈ A :=
    …

    Mentions: OAI.Thomason.Construction.fullSubposetComplex

78. theorem OAI.Thomason.Construction.cosieve_nerve_cover line 798

    Source documentation

    Two cosieves covering the vertices cover the actual ordinary nerve.

    theorem cosieve_nerve_cover {A B : Set E}
        (hA : IsUpperSet A) (hB : IsUpperSet B) (hcover : ∀ e, e ∈ A ∨ e ∈ B) :
        fullSubposetComplex A ⊔ fullSubposetComplex B = ⊤ := by
    …

    Mentions: OAI.Thomason.Construction.fullSubposetComplex

79. def OAI.Thomason.Construction.NonsingularLastVertex.vertex line 829

    Source documentation

    Read a face's last vertex inside the greatest face of a flag.

    def vertex {n : SimplexCategory} (s : (nerve X.N).obj (.op n))
        (i : Fin (n.len+1)) : Fin ((s.obj (Fin.last n.len)).dim+1) :=
    …

80. theorem OAI.Thomason.Construction.NonsingularLastVertex.vertex_monotone line 834
81. def OAI.Thomason.Construction.NonsingularLastVertex.ordinal line 847
82. def OAI.Thomason.Construction.NonsingularLastVertex.simplex line 851
83. theorem OAI.Thomason.Construction.NonsingularLastVertex.ordinal_naturality line 855

    Source documentation

    Restricting a flag changes its greatest face by the unique face map.

    theorem ordinal_naturality {m n : SimplexCategory} (a : m ⟶ n)
        (s : (nerve X.N).obj (.op n)) :
        a ≫ ordinal s = ordinal ((nerve X.N).map a.op s) ≫
          SSet.N.monoOfLE (s.monotone (Fin.le_last (a.toOrderHom (Fin.last m.len)))) := by
    …

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

84. theorem OAI.Thomason.Construction.NonsingularLastVertex.simplex_naturality line 872
85. def OAI.Thomason.Construction.NonsingularLastVertex.map line 883

    Source documentation

    Actual face-poset last vertex, with codomain the original simplicial set.

    def map (X : SSet.{0}) [X.Nonsingular] : nerve X.N ⟶ X where
    …

86. theorem OAI.Thomason.Construction.NonsingularLastVertex.simplex_carrier line 891

    Source documentation

    Every output simplex remains inside the greatest input face.

    theorem simplex_carrier {n : SimplexCategory} (s : (nerve X.N).obj (.op n)) :
        SSet.Subcomplex.ofSimplex (simplex s) ≤ (s.obj (Fin.last n.len)).subcomplex :=
    …

    Mentions: OAI.Thomason.Construction.NonsingularLastVertex.simplex

87. def OAI.Thomason.Construction.FaceSimplexResolution.simplexObject line 917
88. def OAI.Thomason.Construction.FaceSimplexResolution.simplexMorphism line 920
89. theorem OAI.Thomason.Construction.FaceSimplexResolution.simplexMorphism_projection line 933
90. def OAI.Thomason.Construction.FaceSimplexResolution.nondegenerateFaceFunctor line 939
91. def OAI.Thomason.Construction.FaceSimplexResolution.nondegenerateLift line 957
92. theorem OAI.Thomason.Construction.FaceSimplexResolution.nondegenerateLift_ordinal line 960
93. theorem OAI.Thomason.Construction.FaceSimplexResolution.nondegenerateLift_augmentation line 972

    Source documentation

    The diagram commutes as simplicial maps into the original source.

    theorem nondegenerateLift_augmentation (X : SSet.{0}) [X.Nonsingular] :
        nondegenerateLift X ≫ augmentation X = NonsingularLastVertex.map X := by
    …

    Mentions: OAI.Thomason.Construction.FaceSimplexResolution.nondegenerateLift, OAI.Thomason.Construction.FaceSimplexResolution.augmentation, OAI.Thomason.Construction.NonsingularLastVertex.map

94. def OAI.Thomason.Construction.FaceSimplexResolution.resolvedMap line 985

    Source documentation

    A map out of a nonsingular source has a specified map into the resolution after passing to its nondegenerate face poset.

    def resolvedMap {A X : SSet.{0}} [A.Nonsingular] (a : A ⟶ X) :
        nerve A.N ⟶ functor.obj X := nondegenerateLift A ≫ functor.map a
    …

    Mentions: OAI.Thomason.Construction.FaceSimplexResolution.nondegenerateLift

95. theorem OAI.Thomason.Construction.FaceSimplexResolution.resolvedMap_augmentation line 989