OAI/CategoryTheory/Thomason/Simplicial/CanonicalExtensionImageLattice.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thomason.Construction.InfiniteExtension.extension_boundary_rlp line 34

   Source documentation

   Extension preserves the already defined 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
   …

2. theorem OAI.Thomason.Construction.InfiniteExtension.stageMap_boundary_rlp line 42
3. theorem OAI.Thomason.Construction.InfiniteExtension.map_finite_lifting line 50

   Source documentation

   Every lifting square with finite source and target occurs in one common stage of the two extension towers.

   theorem map_finite_lifting {A B X Y : SSet.{0}} [A.Finite] [B.Finite]
       (i : A ⟶ B) (p : X ⟶ Y)
       (hp : ∀ m, HasLiftingProperty i (stageMap p m)) :
       HasLiftingProperty i (map p) := by
   …

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

4. theorem OAI.Thomason.Construction.InfiniteExtension.map_boundary_rlp line 84

   Source documentation

   The extension colimit preserves the boundary right lifting class.

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

   Mentions: OAI.Thomason.Construction.InfiniteExtension.map

5. def OAI.Thomason.Construction.InfiniteExtension.relativeUnit line 114

   Source documentation

   This relative comparison retains both the original target and the entire replacement of its prescribed subcomplex.

   def relativeUnit {A B : SSet.{0}} (i : A ⟶ B) :
       pushout i (unit A) ⟶ obj B :=
   …

   Mentions: OAI.Thomason.Construction.InfiniteExtension.unit, OAI.Thomason.Construction.InfiniteExtension.obj

6. theorem OAI.Thomason.Construction.InfiniteExtension.relativeUnit_inl line 118
7. theorem OAI.Thomason.Construction.InfiniteExtension.relativeUnit_inr line 122
8. instance OAI.Thomason.Construction.InfiniteExtension.relativeUnit_mono line 126
9. theorem OAI.Thomason.Construction.InfiniteExtension.relativeUnit_weak line 142

   Source documentation

   The exact relative comparison is an actual realization weak equivalence. No recognition of acyclic monomorphisms as anodyne maps is used.

   theorem relativeUnit_weak {A B : SSet.{0}} (i : A ⟶ B) [Mono i] :
       realizationWeakEquivalences (relativeUnit i) := by
   …

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

10. theorem OAI.Thomason.Construction.InfiniteExtension.finite_stage_map_factors line 174

    Source documentation

    The finite carrier can be chosen in the original source, through any specified finite number of extensions.

    theorem finite_stage_map_factors {T X : SSet.{0}} [T.Finite]
        (n : ℕ) (f : T ⟶ stage X n) :
        ∃ A : X.Subcomplex, SSet.Finite A.toSSet ∧
          ∃ g : T ⟶ stage A.toSSet n, g ≫ stageMap A.ι n = f := by
    …

    Mentions: OAI.Thomason.Construction.InfiniteExtension.stage, OAI.Thomason.Construction.InfiniteExtension.stageMap

11. theorem OAI.Thomason.Construction.InfiniteExtension.finite_original_map_factors line 193

    Source documentation

    Every finite family in the colimit is induced from the colimit over one finite subcomplex of the original object.

    theorem finite_original_map_factors {T X : SSet.{0}} [T.Finite]
        (f : T ⟶ obj X) :
        ∃ A : X.Subcomplex, SSet.Finite A.toSSet ∧
          ∃ g : T ⟶ obj A.toSSet, g ≫ map A.ι = f := by
    …

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

12. theorem OAI.Thomason.Construction.InfiniteExtension.compact_original_map_factors line 204

    Source documentation

    Compact continuous families also have a finite original carrier. The factorization is an exact equality of continuous maps.

    theorem compact_original_map_factors {Z : Type} [TopologicalSpace Z] [CompactSpace Z]
        (X : SSet.{0}) (f : C(Z, SSet.toTop.obj (obj X))) :
        ∃ A : X.Subcomplex, SSet.Finite A.toSSet ∧
          ∃ g : C(Z, SSet.toTop.obj (obj A.toSSet)),
            (SSet.toTop.map (map A.ι)).hom.comp g = f := by
    …

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

13. theorem OAI.Thomason.Construction.InfiniteExtension.finite_relative_original_map_factors line 237

    Source documentation

    A finite family with boundary in the original object factors over one finite original subcomplex, retaining that complete boundary exactly.

    theorem finite_relative_original_map_factors {A K X : SSet.{0}} [K.Finite]
        (i : A ⟶ K) [Mono i] (a : A ⟶ X) (f : K ⟶ obj X)
        (hf : i ≫ f = a ≫ unit X) :
        ∃ S : X.Subcomplex, SSet.Finite S.toSSet ∧
          ∃ (aS : A ⟶ S.toSSet) (g : K ⟶ obj S.toSSet),
            aS ≫ S.ι = a ∧ g ≫ map S.ι = f ∧ i ≫ g = aS ≫ unit S.toSSet := by
    …

    Mentions: OAI.Thomason.Construction.InfiniteExtension.obj, OAI.Thomason.Construction.InfiniteExtension.unit, OAI.Thomason.Construction.InfiniteExtension.map

14. theorem OAI.Thomason.Construction.relativeCanonicalExtension_weak line 302

    Source documentation

    The original target and the extension of its entire prescribed subcomplex together include weakly into the extended target.

    theorem relativeCanonicalExtension_weak {A B : SSet.{0}} (i : A ⟶ B) [Mono i] :
        realizationWeakEquivalences (relativeCanonicalExtension i) := by
    …

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

15. theorem OAI.Thomason.Construction.relativeCanonicalExtension_weak_mono line 317

    Source documentation

    The relative comparison is both an actual subcomplex inclusion and an actual realization weak equivalence.

    theorem relativeCanonicalExtension_weak_mono {A B : SSet.{0}} (i : A ⟶ B) [Mono i] :
        (MorphismProperty.monomorphisms SSet.{0} ⊓ realizationWeakEquivalences)
          (relativeCanonicalExtension i) :=
    …

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

16. theorem OAI.Thomason.Construction.RealizationPrism.standard_face_carrier_iff line 343
17. theorem OAI.Thomason.Construction.RealizationPrism.standard_face_point_iff line 368
18. theorem OAI.Thomason.Construction.RealizationPrism.standard_faceUnion_point_iff line 381
19. def OAI.Thomason.Construction.SubdivisionBarycentric.lastVertexCoordinates line 430
20. theorem OAI.Thomason.Construction.SubdivisionBarycentric.subdividedFace_lastVertex line 435
21. theorem OAI.Thomason.Construction.SubdivisionBarycentric.lastVertexCoordinates_face line 445
22. theorem OAI.Thomason.Construction.SubdivisionBarycentric.lastVertexCoordinates_zero line 470

    Source documentation

    A zero barycentric coordinate stays zero under the last-vertex map.

    theorem lastVertexCoordinates_zero {n : ℕ} (z : SSet.toTop.obj (nerve (Faces n)))
        (i : Fin (n+1)) (hi : (point n z).weights i = 0) :
        (lastVertexCoordinates n z).weights i = 0 := by
    …

    Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.SubdivisionBarycentric.lastVertexCoordinates

23. def OAI.Thomason.Construction.SubdivisionBarycentric.lastVertexHomotopy line 500
24. theorem OAI.Thomason.Construction.SubdivisionBarycentric.lastVertexHomotopy_zero line 522

    Source documentation

    The homotopy never introduces a new positive coordinate.

    theorem lastVertexHomotopy_zero {n : ℕ} (z : SSet.toTop.obj (nerve (Faces n)))
        (t : unitInterval) (i : Fin (n+1)) (hi : (point n z).weights i = 0) :
        (lastVertexHomotopy n (t, z)).weights i = 0 := by
    …

    Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.SubdivisionBarycentric.lastVertexHomotopy

25. theorem OAI.Thomason.Construction.SubdivisionBarycentric.lastVertexHomotopy_face line 530

    Source documentation

    In particular the same complete face is retained at every time.

    theorem lastVertexHomotopy_face {n : ℕ} (S : Finset (Fin (n+1)))
        (z : SSet.toTop.obj (nerve (Faces n))) (t : unitInterval)
        (hz : ∀ i ∉ S, (point n z).weights i = 0) :
        ∀ i ∉ S, (lastVertexHomotopy n (t, z)).weights i = 0 :=
    …

    Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.SubdivisionBarycentric.lastVertexHomotopy

26. theorem OAI.Thomason.Construction.SubdivisionBarycentric.lastVertexHomotopy_faceUnion line 536
27. def OAI.Thomason.Construction.equalRangeIso line 560
28. theorem OAI.Thomason.Construction.equalRangeIso_fac line 569
29. def OAI.Thomason.Construction.subdivisionFaceIso line 584
30. def OAI.Thomason.Construction.originalMaximum line 589
31. def OAI.Thomason.Construction.originalMaximumNerve line 593
32. def OAI.Thomason.Construction.originalSimplexIso line 598
33. def OAI.Thomason.Construction.originalLastVertex line 602
34. def OAI.Thomason.Construction.hornIntoFaces line 606
35. instance OAI.Thomason.Construction.hornIntoFaces_mono line 610
36. def OAI.Thomason.Construction.hornFaceInclusion line 615
37. instance OAI.Thomason.Construction.hornFaceInclusion_mono line 620
38. def OAI.Thomason.Construction.hornSubdivisionIso line 623
39. theorem OAI.Thomason.Construction.hornSubdivisionIso_fac line 628
40. theorem OAI.Thomason.Construction.subdivision_lastVertex_standard_chain line 633
41. def OAI.Thomason.Construction.rawHornRetraction line 671
42. theorem OAI.Thomason.Construction.old_chain_retraction line 678
43. theorem OAI.Thomason.Construction.rawHornRetraction_fac line 696
44. def OAI.Thomason.Construction.subdivisionHornRetraction line 754

    Source documentation

    After two subdivisions, a simplex retracts into the once-subdivided horn with restriction exactly Sd(lastVertex_horn). This is the finite-stage extension identity used to fill horns in the extension tower.

    def subdivisionHornRetraction (n : ℕ) (k : Fin (n+2)) :
        SSet.sd.obj (SSet.sd.obj (SSet.stdSimplex.obj ⦋n+1⦌)) ⟶
          SSet.sd.obj (SSet.horn.{0} (n+1) k) :=
    …

45. theorem OAI.Thomason.Construction.subdivisionHornRetraction_fac line 759
46. theorem OAI.Thomason.Construction.canonicalExtension_anodyne_of_iso line 786

    Source documentation

    Transport the canonical-extension anodyne property through an actual simplicial isomorphism.

    theorem canonicalExtension_anodyne_of_iso {X Y : SSet.{0}} (e : X ≅ Y)
        (hY : SSet.anodyneExtensions (canonicalExtension.app Y)) :
        SSet.anodyneExtensions (canonicalExtension.app X) := by
    …

47. theorem OAI.Thomason.Construction.canonicalExtension_anodyne_nerve_greatest line 802

    Source documentation

    A greatest vertex supplies the concrete simplicial contraction used for the face-poset nerve.

    theorem canonicalExtension_anodyne_nerve_greatest {P : Type} [PartialOrder P]
        (v : P) (hv : ∀ x, x ≤ v) :
        SSet.anodyneExtensions (canonicalExtension.app (nerve P)) := by
    …

48. def OAI.Thomason.Construction.simplexTopFace line 821
49. theorem OAI.Thomason.Construction.canonicalExtension_subdivision_standard_anodyne line 828

    Source documentation

    The once-subdivided simplex also admits exact Kan lifting across its canonical extension; its full face is the contracting greatest vertex.

    theorem canonicalExtension_subdivision_standard_anodyne (n : ℕ) :
        SSet.anodyneExtensions (canonicalExtension.app (SSet.sd.obj (Δ[n] : SSet.{0}))) := by
    …

50. theorem OAI.Thomason.Construction.canonicalExtension_anodyne_of_homotopy_span line 836

    Source documentation

    The second orientation of a two-step contraction, used for the face-poset model of a subdivided horn.

    theorem canonicalExtension_anodyne_of_homotopy_span (X : SSet.{0})
        (f : X ⟶ (Δ[0] : SSet.{0})) (g : (Δ[0] : SSet.{0}) ⟶ X) (u : X ⟶ X)
        (H : SSet.Homotopy (f ≫ g) u) (G : SSet.Homotopy (𝟙 X) u) :
        SSet.anodyneExtensions (canonicalExtension.app X) := by
    …

51. theorem OAI.Thomason.Construction.canonicalExtension_hornFaceNerve_anodyne line 865

    Source documentation

    On the horn face poset the maps id ≤ addVertex ≥ constant give the needed two-step contraction.

    theorem canonicalExtension_hornFaceNerve_anodyne (n : ℕ) (k : Fin (n+2)) :
        SSet.anodyneExtensions
          (canonicalExtension.app (nerve (SubdivisionHornFaces.HornFaces n k))) := by
    …

    Mentions: OAI.Thomason.Construction.SubdivisionHornFaces.HornFaces

52. theorem OAI.Thomason.Construction.canonicalExtension_subdivision_horn_anodyne line 893

    Source documentation

    The actual subdivided horn inherits its anodyne canonical extension through the constructed face-poset isomorphism.

    theorem canonicalExtension_subdivision_horn_anodyne (n : ℕ) (k : Fin (n+2)) :
        SSet.anodyneExtensions
          (canonicalExtension.app (SSet.sd.obj (Λ[n+1, k] : SSet.{0}))) :=
    …

53. theorem OAI.Thomason.Construction.relativeCanonicalExtension_subdivision_standard_anodyne line 901

    Source documentation

    The original subdivided simplex and the extended subdivided face can both remain fixed in the relative lifting problem.

    theorem relativeCanonicalExtension_subdivision_standard_anodyne {m n : ℕ}
        (i : (Δ[m] : SSet.{0}) ⟶ (Δ[n] : SSet.{0})) [Mono i] :
        SSet.anodyneExtensions (relativeCanonicalExtension (SSet.sd.map i)) := by
    …

    Mentions: OAI.Thomason.Construction.relativeCanonicalExtension

54. theorem OAI.Thomason.Construction.relativeCanonicalExtension_subdivision_horn_anodyne line 911

    Source documentation

    Exact relative Kan lifting for a subdivided generating horn, with both the original subdivided simplex and the whole extended horn fixed.

    theorem relativeCanonicalExtension_subdivision_horn_anodyne (n : ℕ) (k : Fin (n+2)) :
        SSet.anodyneExtensions (relativeCanonicalExtension (SSet.sd.map
          (Λ[n+1, k].ι : (Λ[n+1, k] : SSet.{0}) ⟶ (Δ[n+1] : SSet.{0})))) := by
    …

    Mentions: OAI.Thomason.Construction.relativeCanonicalExtension

55. theorem OAI.Thomason.Construction.subcomplex_inf_isPullback line 941
56. theorem OAI.Thomason.Construction.range_comp_eq_inf_of_isPullback line 957
57. theorem OAI.Thomason.Construction.anodyne_range_inclusion line 974
58. def OAI.Thomason.Construction.extensionImage line 987
59. def OAI.Thomason.Construction.originalImage line 990
60. theorem OAI.Thomason.Construction.extensionImage_inf line 993
61. theorem OAI.Thomason.Construction.originalImage_inter_extensionImage line 1002
62. theorem OAI.Thomason.Construction.originalImage_inter_extensionImage_anodyne line 1009