OAI/CategoryTheory/Thomason/Simplicial/InfiniteExtensionBaseChange.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thomason.Construction.canonicalExtension_isIso_of_initial line 31
2. theorem OAI.Thomason.Construction.canonicalExtension_subdividedFace_anodyne line 38
3. def OAI.Thomason.Construction.extendedSubdividedFace line 60
4. theorem OAI.Thomason.Construction.extendedSubdividedFace_inter line 64
5. def OAI.Thomason.Construction.extendedFaceUnion line 71
6. theorem OAI.Thomason.Construction.original_to_extendedFaceUnion_anodyne line 75
7. theorem OAI.Thomason.Construction.extendedFaceUnion_anodyne line 103

   Source documentation

   The finite union comparison has the left lifting property against every Kan fibration, preserving all extended faces and the original subdivided simplex exactly.

   theorem extendedFaceUnion_anodyne {n : ℕ} (F : Finset (Finset (Fin (n+1)))) :
       SSet.anodyneExtensions (extendedFaceUnion F).ι := by
   …

   Mentions: OAI.Thomason.Construction.extendedFaceUnion

8. def OAI.Thomason.Construction.fullSubposetComplexIso line 142
9. theorem OAI.Thomason.Construction.nerve_map_factors_of_sieve_cover line 149

   Source documentation

   A map from a nerve with a greatest vertex factors through one of any two covering sieves.

   theorem nerve_map_factors_of_sieve_cover {P Q : Type} [PartialOrder P] [PartialOrder Q]
       (v : Q) (hv : ∀ q, q ≤ v) (A B : Set P)
       (hA : IsLowerSet A) (hB : IsLowerSet B) (hcover : ∀ p, p ∈ A ∨ p ∈ B)
       (f : nerve Q ⟶ nerve P) :
       (∃ g : nerve Q ⟶ (fullSubposetComplex A).toSSet,
         g ≫ (fullSubposetComplex A).ι = f) ∨
       (∃ g : nerve Q ⟶ (fullSubposetComplex B).toSSet,
         g ≫ (fullSubposetComplex B).ι = f) := by
   …

   Mentions: OAI.Thomason.Construction.fullSubposetComplex

10. theorem OAI.Thomason.Construction.extension_sieve_simplex_cover line 175

    Source documentation

    Every extension simplex of a poset nerve lies in the extension of one of two covering full sieves.

    theorem extension_sieve_simplex_cover {P : Type} [PartialOrder P]
        (A B : Set P) (hA : IsLowerSet A) (hB : IsLowerSet B)
        (hcover : ∀ p, p ∈ A ∨ p ∈ B) (d : SimplexCategoryᵒᵖ)
        (s : (SSet.ex.obj (nerve P)).obj d) :
        s ∈ (extensionImage (fullSubposetComplex A)).obj d ∨
          s ∈ (extensionImage (fullSubposetComplex B)).obj d := by
    …

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

11. theorem OAI.Thomason.Construction.extension_sieve_cover line 203
12. theorem OAI.Thomason.Construction.canonicalExtension_anodyne_of_extended_cover line 236

    Source documentation

    Binary gluing for canonical extensions, provided the actual extended subobjects cover the extended target.

    theorem canonicalExtension_anodyne_of_extended_cover {X : SSet.{0}}
        (A B : X.Subcomplex)
        (hcover : extensionImage A ⊔ extensionImage B = ⊤)
        (hA : SSet.anodyneExtensions (canonicalExtension.app A.toSSet))
        (hB : SSet.anodyneExtensions (canonicalExtension.app B.toSSet))
        (hAB : SSet.anodyneExtensions (canonicalExtension.app (A ⊓ B).toSSet)) :
        SSet.anodyneExtensions (canonicalExtension.app X) := by
    …

    Mentions: OAI.Thomason.Construction.extensionImage

13. theorem OAI.Thomason.Construction.canonicalExtension_anodyne_of_sieve_cover line 284
14. theorem OAI.Thomason.Construction.canonicalExtension_finitePoset_aux line 300
15. theorem OAI.Thomason.Construction.canonicalExtension_finitePoset_anodyne line 343

    Source documentation

    The canonical extension of the nerve of any finite poset is anodyne. No contractibility of the poset is required.

    theorem canonicalExtension_finitePoset_anodyne (P : Type) [PartialOrder P] [Finite P] :
        SSet.anodyneExtensions (canonicalExtension.app (nerve P)) := by
    …

16. def OAI.Thomason.Construction.faceFamilyVertices line 370
17. theorem OAI.Thomason.Construction.subdividedFaceUnion_eq_full line 374
18. def OAI.Thomason.Construction.faceUnionSubdivisionIso line 393
19. theorem OAI.Thomason.Construction.canonicalExtension_subdivision_faceUnion_anodyne line 401
20. def OAI.Thomason.Construction.subcomplexFaceFamily line 408
21. theorem OAI.Thomason.Construction.faceUnion_subcomplexFaceFamily line 413
22. theorem OAI.Thomason.Construction.canonicalExtension_subdivision_subcomplex_anodyne line 436
23. theorem OAI.Thomason.Construction.canonicalExtension_subdivision_boundary_anodyne line 444

    Source documentation

    The entire subdivided boundary has an anodyne canonical extension; this includes extensions whose simplices span several original faces.

    theorem canonicalExtension_subdivision_boundary_anodyne (n : ℕ) :
        SSet.anodyneExtensions
          (canonicalExtension.app (SSet.sd.obj (SSet.boundary.{0} n).toSSet)) :=
    …

24. theorem OAI.Thomason.Construction.relativeCanonicalExtension_subdivision_boundary_anodyne line 451

    Source documentation

    Exact relative lifting with the whole extended subdivided boundary and the original subdivided simplex prescribed.

    theorem relativeCanonicalExtension_subdivision_boundary_anodyne (n : ℕ) :
        SSet.anodyneExtensions
          (relativeCanonicalExtension (SSet.sd.map (SSet.boundary.{0} n).ι)) := by
    …

    Mentions: OAI.Thomason.Construction.relativeCanonicalExtension

25. def OAI.Thomason.Construction.SubdivisionBarycentric.faceUnionCoordinates line 481
26. theorem OAI.Thomason.Construction.SubdivisionBarycentric.faceUnionCoordinates_isClosedEmbedding line 486
27. theorem OAI.Thomason.Construction.SubdivisionBarycentric.faceUnionCoordinates_range line 491
28. def OAI.Thomason.Construction.SubdivisionBarycentric.faceUnionCoordinatesHomeomorph line 507
29. def OAI.Thomason.Construction.SubdivisionBarycentric.faceUnionSubdivisionRangeIso line 513
30. theorem OAI.Thomason.Construction.SubdivisionBarycentric.faceUnionSubdivisionRangeIso_inclusion line 519
31. def OAI.Thomason.Construction.SubdivisionBarycentric.faceUnionSubdivisionHomeomorph line 525
32. def OAI.Thomason.Construction.SubdivisionBarycentric.subcomplexSubdivisionHomeomorph line 533

    Source documentation

    The actual realization of the subdivision of any simplex subcomplex is homeomorphic to the original realization.

    def subcomplexSubdivisionHomeomorph {n : ℕ} (A : (Δ[n] : SSet.{0}).Subcomplex) :
        SSet.toTop.obj (SSet.sd.obj A.toSSet) ≃ₜ SSet.toTop.obj A.toSSet :=
    …

33. theorem OAI.Thomason.Construction.SubdivisionBarycentric.faceUnionSubdivisionHomeomorph_inclusion line 543

    Source documentation

    The face-union homeomorphism is the restriction of the barycentric simplex map along the original inclusion.

    theorem faceUnionSubdivisionHomeomorph_inclusion {n : ℕ}
        (F : Finset (Finset (Fin (n+1))))
        (z : SSet.toTop.obj (SSet.sd.obj (faceUnion F).toSSet)) :
        (SSet.toTop.map (faceUnion F).ι).hom (faceUnionSubdivisionHomeomorph F z) =
          standardSubdivisionHomeomorph n
            ((SSet.toTop.map (SSet.sd.map (faceUnion F).ι)).hom z) := by
    …

    Mentions: OAI.Thomason.Construction.faceUnion, OAI.Thomason.Construction.SubdivisionBarycentric.faceUnionSubdivisionHomeomorph, OAI.Thomason.Construction.SubdivisionBarycentric.standardSubdivisionHomeomorph

34. def OAI.Thomason.Construction.closedVertexStar line 593
35. theorem OAI.Thomason.Construction.closedVertexStar_le line 601
36. theorem OAI.Thomason.Construction.face_le_closedVertexStar line 606
37. def OAI.Thomason.Construction.closedVertexStarVertex line 613
38. def OAI.Thomason.Construction.closedVertexStarContraction line 621
39. theorem OAI.Thomason.Construction.canonicalExtension_closedVertexStar_anodyne line 680
40. theorem OAI.Thomason.Construction.extension_horn_filler line 718

    Source documentation

    The exact two-subdivision retraction gives a filler for every horn in Ex X after the specified canonical map to Ex (Ex X).

    theorem extension_horn_filler (X : SSet.{0}) (n : ℕ) (k : Fin (n+2))
        (a : (SSet.horn.{0} (n+1) k : SSet) ⟶ SSet.ex.obj X) :
        ∃ b : (Δ[n+1] : SSet.{0}) ⟶ SSet.ex.obj (SSet.ex.obj X),
          (SSet.horn.{0} (n+1) k).ι ≫ b = a ≫ canonicalExtension.app (SSet.ex.obj X) := by
    …

41. theorem OAI.Thomason.Construction.extension_twice_horn_filler line 757

    Source documentation

    A horn in an arbitrary simplicial set fills after its two canonical extension maps; no fibrancy of the starting simplicial set is required.

    theorem extension_twice_horn_filler (X : SSet.{0}) (n : ℕ) (k : Fin (n+2))
        (a : (SSet.horn.{0} (n+1) k : SSet) ⟶ X) :
        ∃ b : (Δ[n+1] : SSet.{0}) ⟶ SSet.ex.obj (SSet.ex.obj X),
          (SSet.horn.{0} (n+1) k).ι ≫ b =
            a ≫ canonicalExtension.app X ≫ canonicalExtension.app (SSet.ex.obj X) :=
    …

42. theorem OAI.Thomason.Construction.InfiniteExtension.horn_lifting line 785

    Source documentation

    A finite horn lies in a stage and fills after two further extensions. The colimit compatibility retains the prescribed horn exactly.

    theorem horn_lifting (X : SSet.{0}) (n : ℕ) (k : Fin (n+2)) :
        HasLiftingProperty (SSet.horn (n+1) k).ι (terminal.from (obj X)) := by
    …

    Mentions: OAI.Thomason.Construction.InfiniteExtension.obj

43. instance OAI.Thomason.Construction.InfiniteExtension.kan line 797

    Source documentation

    No fibrancy assumption is needed on the input.

    instance kan (X : SSet.{0}) : SSet.KanComplex (obj X) := by
    …

    Mentions: OAI.Thomason.Construction.InfiniteExtension.obj

44. def OAI.Thomason.Construction.InfiniteExtension.pullbackUnit line 827

    Source documentation

    The original pullback maps weakly to the pullback of its constructed Kan replacements, with no properness hypothesis.

    def pullbackUnit {E B C : SSet.{0}} (p : E ⟶ B) (g : C ⟶ B) :
        pullback p g ⟶ pullback (map p) (map g) :=
    …

    Mentions: OAI.Thomason.Construction.InfiniteExtension.map

45. theorem OAI.Thomason.Construction.InfiniteExtension.pullbackUnit_fst line 831
46. theorem OAI.Thomason.Construction.InfiniteExtension.pullbackUnit_snd line 840
47. theorem OAI.Thomason.Construction.InfiniteExtension.pullbackUnit_weak line 849
48. theorem OAI.Thomason.Construction.InfiniteExtension.pullback_fst_weak_iff line 857

    Source documentation

    The exact base-change projection is weak if and only if the projection between the actual Kan replacements is weak. This is a compatibility statement, not an assumption of properness.

    theorem pullback_fst_weak_iff {E B C : SSet.{0}} (p : E ⟶ B) (g : C ⟶ B) :
        realizationWeakEquivalences (pullback.fst p g) ↔
          realizationWeakEquivalences (pullback.fst (map p) (map g)) := by
    …

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

49. theorem OAI.Thomason.Construction.InfiniteExtension.pullback_snd_weak_iff line 873

    Source documentation

    The second projection has the same exact compatibility.

    theorem pullback_snd_weak_iff {E B C : SSet.{0}} (p : E ⟶ B) (g : C ⟶ B) :
        realizationWeakEquivalences (pullback.snd p g) ↔
          realizationWeakEquivalences (pullback.snd (map p) (map g)) := by
    …

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