OAI/CategoryTheory/Thomason/Simplicial/RealizationCellClosure.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Nondegenerate barycentric coordinates of a realization point

  1. abbrev OAI.Thomason.Construction.RealizationPrism.NondegenerateCoordinates line 24

    Source documentation

    A nondegenerate simplex with its barycentric coordinates.

    abbrev NondegenerateCoordinates (K : SSet.{0}) :=
…
  2. def OAI.Thomason.Construction.RealizationPrism.normalizeSimplex line 28

    Source documentation

    Remove degeneracies from a simplex and push forward its barycentric coordinates.

    def normalizeSimplex (K : SSet.{0}) {n : ℕ} (s : K.obj (.op (.mk n)))
    (x : StdSimplex ℝ (Fin (n+1))) : NondegenerateCoordinates K :=
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.NondegenerateCoordinates

  3. theorem OAI.Thomason.Construction.RealizationPrism.normalizeSimplex_of_representation line 33

    Source documentation

    Any nondegenerate epimorphic presentation computes the same normalization.

    theorem normalizeSimplex_of_representation (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) (x : StdSimplex ℝ (Fin (n+1)))
    (c : K.N) (f : SimplexCategory.mk n ⟶ .mk c.dim) [Epi f]
    (h : K.map f.op c.simplex = s) :
    normalizeSimplex K s x = ⟨c, StdSimplex.map f.toOrderHom x⟩ := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.normalizeSimplex

  4. theorem OAI.Thomason.Construction.RealizationPrism.normalizeSimplex_epi line 51

    Source documentation

    Removing degeneracies commutes with an epimorphic simplex operator.

    theorem normalizeSimplex_epi (K : SSet.{0}) {m n : ℕ}
    (f : SimplexCategory.mk m ⟶ .mk n) [Epi f]
    (s : K.obj (.op (.mk n))) (x : StdSimplex ℝ (Fin (m+1))) :
    normalizeSimplex K (K.map f.op s) x =
      normalizeSimplex K s (StdSimplex.map f.toOrderHom x) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.normalizeSimplex

  5. def OAI.Thomason.Construction.RealizationPrism.normalizeSupported line 69

    Source documentation

    First discard zero coordinates, then remove degeneracies from the supported simplex.

    def normalizeSupported (K : SSet.{0}) {n : ℕ} (s : K.obj (.op (.mk n)))
    (x : StdSimplex ℝ (Fin (n+1))) : NondegenerateCoordinates K :=
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.NondegenerateCoordinates

  6. theorem OAI.Thomason.Construction.RealizationPrism.normalizeSupported_naturality line 76

    Source documentation

    The supported nondegenerate coordinates are invariant under all simplex operators.

    theorem normalizeSupported_naturality (K : SSet.{0}) {m n : ℕ}
    (f : SimplexCategory.mk m ⟶ .mk n) (s : K.obj (.op (.mk n)))
    (x : StdSimplex ℝ (Fin (m+1))) :
    normalizeSupported K (K.map f.op s) x =
      normalizeSupported K s (StdSimplex.map f.toOrderHom x) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.normalizeSupported

  7. def OAI.Thomason.Construction.RealizationPrism.normalizationCocone line 106

    Source documentation

    Nondegenerate coordinates form a cocone of sets over all realization simplices.

    def normalizationCocone (K : SSet.{0}) : Cocone (diagram K ⋙ forget TopCat) where
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.diagram

  8. def OAI.Thomason.Construction.RealizationPrism.normalization line 121

    Source documentation

    The nondegenerate coordinates of an actual realization point.

    def normalization (K : SSet.{0}) : SSet.toTop.obj K → NondegenerateCoordinates K :=
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.NondegenerateCoordinates

  9. theorem OAI.Thomason.Construction.RealizationPrism.normalization_leg line 124
  10. def OAI.Thomason.Construction.RealizationPrism.denormalize line 148

    Source documentation

    Evaluate a nondegenerate simplex with specified barycentric coordinates.

    def denormalize (K : SSet.{0}) (p : NondegenerateCoordinates K) : SSet.toTop.obj K :=
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.NondegenerateCoordinates

  11. theorem OAI.Thomason.Construction.RealizationPrism.denormalize_normalizeSimplex line 151
  12. theorem OAI.Thomason.Construction.RealizationPrism.denormalize_normalizeSupported line 160
  13. theorem OAI.Thomason.Construction.RealizationPrism.normalization_simplexPoint line 170
  14. theorem OAI.Thomason.Construction.RealizationPrism.denormalize_normalization line 180

    Source documentation

    The intrinsic normal coordinates reconstruct every actual realization point.

    theorem denormalize_normalization (K : SSet.{0}) (x : SSet.toTop.obj K) :
    denormalize K (normalization K x) = x := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.denormalize, OAI.Thomason.Construction.RealizationPrism.normalization

  15. theorem OAI.Thomason.Construction.RealizationPrism.normalization_injective line 186

    Source documentation

    Distinct realization points have distinct intrinsic nondegenerate coordinates.

    theorem normalization_injective (K : SSet.{0}) : Function.Injective (normalization K) :=
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.normalization

  16. theorem OAI.Thomason.Construction.RealizationPrism.normalizeSupported_of_full_support line 191

    Source documentation

    With no zero coordinates the support normalization agrees with degeneracy normalization.

    theorem normalizeSupported_of_full_support (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) (x : StdSimplex ℝ (Fin (n+1)))
    (hx : ∀ i, x.weights i ≠ 0) :
    normalizeSupported K s x = normalizeSimplex K s x := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.normalizeSupported, OAI.Thomason.Construction.RealizationPrism.normalizeSimplex

  17. theorem OAI.Thomason.Construction.RealizationPrism.normalization_nondegenerate_interior line 208

    Source documentation

    Interior points of a nondegenerate simplex have precisely that simplex's coordinates.

    theorem normalization_nondegenerate_interior (K : SSet.{0}) (s : K.N)
    (x : StdSimplex ℝ (Fin (s.dim+1))) (hx : ∀ i, x.weights i ≠ 0) :
    normalization K (simplexPoint K s.simplex x) = ⟨s, x⟩ := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.normalization, OAI.Thomason.Construction.RealizationPrism.simplexPoint

  18. theorem OAI.Thomason.Construction.RealizationPrism.normalizeSimplex_continuous line 234

    Source documentation

    Degeneracy normalization on a fixed simplex is continuous into the disjoint union.

    theorem normalizeSimplex_continuous (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) : Continuous (normalizeSimplex K s) :=
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.normalizeSimplex

  19. theorem OAI.Thomason.Construction.RealizationPrism.nondegenerateCoordinates_t2Space line 238
  20. theorem OAI.Thomason.Construction.RealizationPrism.simplexPoint_fiber_eq line 245

    Source documentation

    A point fibre on a parameter simplex is a finite union of compact affine images.

    theorem simplexPoint_fiber_eq (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) (z : SSet.toTop.obj K) :
    (simplexPoint K s) ⁻¹' {z} =
      ⋃ i : FaceIndex n, (StdSimplex.map i.2.toOrderHom) ''
        ((normalizeSimplex K (K.map i.2.op s)) ⁻¹' {normalization K z}) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint, OAI.Thomason.Construction.RealizationPrism.FaceIndex, OAI.Thomason.Construction.RealizationPrism.normalizeSimplex, OAI.Thomason.Construction.RealizationPrism.normalization

  21. theorem OAI.Thomason.Construction.RealizationPrism.simplexPoint_fiber_isClosed line 271

    Source documentation

    Individual point fibres are closed on every barycentric parameter simplex.

    theorem simplexPoint_fiber_isClosed (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) (z : SSet.toTop.obj K) :
    IsClosed ((simplexPoint K s) ⁻¹' {z}) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint

  22. theorem OAI.Thomason.Construction.RealizationPrism.realization_t1Space line 284

    Source documentation

    Every actual geometric realization is a T₁ space.

    theorem realization_t1Space (K : SSet.{0}) : T1Space (SSet.toTop.obj K) where
…
  23. theorem OAI.Thomason.Construction.RealizationPrism.simplexCarrier_range_finite line 319

    Source documentation

    Only finitely many supported simplex carriers occur in one parameter simplex.

    theorem simplexCarrier_range_finite (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) : Set.Finite (Set.range (simplexCarrier K s)) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.simplexCarrier

  24. theorem OAI.Thomason.Construction.RealizationPrism.isClosed_of_carrier_injOn line 331

    Source documentation

    A set containing at most one point in each carrier is closed.

    theorem isClosed_of_carrier_injOn (K : SSet.{0}) (S : Set (SSet.toTop.obj K))
    (hS : Set.InjOn (carrier K) S) : IsClosed S := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.carrier

  25. theorem OAI.Thomason.Construction.RealizationPrism.isDiscrete_of_carrier_injOn line 351

    Source documentation

    Such a set is also discrete, since each of its subsets has the same carrier property.

    theorem isDiscrete_of_carrier_injOn (K : SSet.{0}) (S : Set (SSet.toTop.obj K))
    (hS : Set.InjOn (carrier K) S) : IsDiscrete S := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.carrier

  26. theorem OAI.Thomason.Construction.RealizationPrism.compact_carriers_finite line 358

    Source documentation

    Every compact subset of realization meets only finitely many supported simplex carriers.

    theorem compact_carriers_finite (K : SSet.{0}) (C : Set (SSet.toTop.obj K))
    (hC : IsCompact C) : Set.Finite (carrier K '' C) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.carrier

  27. theorem OAI.Thomason.Construction.RealizationPrism.carrier_finite line 395

    Source documentation

    Every intrinsic carrier is generated by one simplex, hence is a finite simplicial set.

    theorem carrier_finite (K : SSet.{0}) (x : SSet.toTop.obj K) :
    SSet.Finite (carrier K x : SSet) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.carrier

  28. def OAI.Thomason.Construction.RealizationPrism.compactSubcomplex line 403

    Source documentation

    The finite subcomplex generated by all carriers met by a compact subset.

    def compactSubcomplex (K : SSet.{0}) (C : Set (SSet.toTop.obj K)) : K.Subcomplex :=
…
  29. theorem OAI.Thomason.Construction.RealizationPrism.compactSubcomplex_finite line 406
  30. theorem OAI.Thomason.Construction.RealizationPrism.compactSubcomplex_contains line 414

    Source documentation

    The compact subset lies in the realization of its finite carrier subcomplex.

    theorem compactSubcomplex_contains (K : SSet.{0}) (C : Set (SSet.toTop.obj K)) :
    C ⊆ Set.range (SSet.toTop.map (compactSubcomplex K C).ι).hom := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.compactSubcomplex

  31. theorem OAI.Thomason.Construction.RealizationPrism.compact_map_factors line 422

    Source documentation

    Every continuous map from a compact space into realization factors continuously through the realization of a finite simplicial subcomplex.

    theorem compact_map_factors {X : Type} [TopologicalSpace X] [CompactSpace X]
    (K : SSet.{0}) (f : C(X, SSet.toTop.obj K)) :
    ∃ (A : K.Subcomplex), SSet.Finite (A : SSet) ∧
      ∃ g : C(X, SSet.toTop.obj (A : SSet)), (SSet.toTop.map A.ι).hom.comp g = f := by
…
  32. theorem OAI.Thomason.Construction.RealizationPrism.based_cube_factors line 459

    Source documentation

    Every positive-dimensional based cube in realization factors through a finite subcomplex, with its entire boundary still constant at a lifted basepoint.

    theorem based_cube_factors (K : SSet.{0}) {x : SSet.toTop.obj K} (n : ℕ)
    (p : GenLoop (Fin (n+1)) (SSet.toTop.obj K) x) :
    ∃ (A : K.Subcomplex), SSet.Finite (A : SSet) ∧
      ∃ (a : SSet.toTop.obj (A : SSet)), (SSet.toTop.map A.ι).hom a = x ∧
        ∃ q : GenLoop (Fin (n+1)) (SSet.toTop.obj (A : SSet)) a,
          ∀ t, (SSet.toTop.map A.ι).hom (q t) = p t := by
…
  33. theorem OAI.Thomason.Construction.RealizationPrism.based_homotopy_factors line 479

    Source documentation

    A relative homotopy of based cubes has a single finite-subcomplex factorization, including both endpoint cubes and the fixed boundary.

    theorem based_homotopy_factors (K : SSet.{0}) {x : SSet.toTop.obj K} (n : ℕ)
    {p q : GenLoop (Fin (n+1)) (SSet.toTop.obj K) x}
    (H : p.val.HomotopyRel q.val (Cube.boundary (Fin (n+1)))) :
    ∃ (A : K.Subcomplex), SSet.Finite (A : SSet) ∧
      ∃ (a : SSet.toTop.obj (A : SSet)), (SSet.toTop.map A.ι).hom a = x ∧
        ∃ (p' q' : GenLoop (Fin (n+1)) (SSet.toTop.obj (A : SSet)) a)
          (H' : p'.val.HomotopyRel q'.val (Cube.boundary (Fin (n+1)))),
          (∀ t, (SSet.toTop.map A.ι).hom (p' t) = p t) ∧
          (∀ t, (SSet.toTop.map A.ι).hom (q' t) = q t) ∧
          (∀ z, (SSet.toTop.map A.ι).hom (H' z) = H z) := by
…
  34. theorem OAI.Thomason.Construction.RealizationPrism.compact_square_factors line 536

    Source documentation

    A continuous compact lifting problem over a realized simplicial map factors through one map between finite simplicial subcomplexes. The lifted square still commutes exactly, including any prescribed boundary values.

    theorem compact_square_factors {P Q : Type}
    [TopologicalSpace P] [CompactSpace P] [TopologicalSpace Q] [CompactSpace Q]
    {K L : SSet.{0}} (f : K ⟶ L)
    (u : C(P, Q)) (a : C(P, SSet.toTop.obj K)) (b : C(Q, SSet.toTop.obj L))
    (h : (SSet.toTop.map f).hom.comp a = b.comp u) :
    ∃ (A : K.Subcomplex) (B : L.Subcomplex),
      SSet.Finite (A : SSet) ∧ SSet.Finite (B : SSet) ∧
      ∃ (g : (A : SSet) ⟶ (B : SSet))
        (a' : C(P, SSet.toTop.obj (A : SSet)))
        (b' : C(Q, SSet.toTop.obj (B : SSet))),
        g ≫ B.ι = A.ι ≫ f ∧
        (SSet.toTop.map A.ι).hom.comp a' = a ∧
…
  35. def OAI.Thomason.Construction.RealizationPrism.supportFaceIndex line 611
  36. def OAI.Thomason.Construction.RealizationPrism.matchingFacePairs line 616

    Source documentation

    Pairs of face points whose nondegenerate coordinate descriptions agree.

    def matchingFacePairs (K : SSet.{0}) {n m : ℕ}
    (s : K.obj (.op (.mk n))) (t : K.obj (.op (.mk m)))
    (B : Set (StdSimplex ℝ (Fin (n+1)))) (i : FaceIndex n) (j : FaceIndex m) :
    Set (StdSimplex ℝ (Fin (i.1.val+1)) × StdSimplex ℝ (Fin (j.1.val+1))) :=
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.FaceIndex

  37. theorem OAI.Thomason.Construction.RealizationPrism.matchingFacePairs_isClosed line 623
  38. theorem OAI.Thomason.Construction.RealizationPrism.simplexPoint_preimage_image line 633

    Source documentation

    Equality of points from two parameter simplices is detected by finitely many face pairs.

    theorem simplexPoint_preimage_image (K : SSet.{0}) {n m : ℕ}
    (s : K.obj (.op (.mk n))) (t : K.obj (.op (.mk m)))
    (B : Set (StdSimplex ℝ (Fin (n+1)))) :
    (simplexPoint K t) ⁻¹' ((simplexPoint K s) '' B) =
      ⋃ ij : FaceIndex n × FaceIndex m,
        (fun p => StdSimplex.map ij.2.2.toOrderHom p.2) ''
          matchingFacePairs K s t B ij.1 ij.2 := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint, OAI.Thomason.Construction.RealizationPrism.FaceIndex, OAI.Thomason.Construction.RealizationPrism.matchingFacePairs

  39. theorem OAI.Thomason.Construction.RealizationPrism.simplexPoint_isClosedMap line 661

    Source documentation

    Each continuous simplex parameter map into realization is closed.

    theorem simplexPoint_isClosedMap (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) : IsClosedMap (simplexPoint K s) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint

  40. theorem OAI.Thomason.Construction.RealizationPrism.nondegenerateProjection_isClosedMap line 708
  41. theorem OAI.Thomason.Construction.RealizationPrism.nondegenerateProjection_isQuotientMap line 728

    Source documentation

    A finite realization has its actual quotient topology from its finitely many nondegenerate simplex parameter spaces.

    theorem nondegenerateProjection_isQuotientMap (K : SSet.{0}) [K.Finite] :
    IsQuotientMap (nondegenerateProjection K) :=
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.nondegenerateProjection

  42. theorem OAI.Thomason.Construction.RealizationPrism.finite_realization_t2Space line 735

    Source documentation

    Finite simplicial realizations are Hausdorff; no ambient separation assumption on arbitrary realizations is used.

    theorem finite_realization_t2Space (K : SSet.{0}) [K.Finite] :
    T2Space (SSet.toTop.obj K) := by
…
  43. def OAI.Thomason.Construction.RealizationPrism.monogenousPoint line 787

    Source documentation

    The parameter map onto the entire subcomplex generated by one simplex.

    def monogenousPoint (K : SSet.{0}) {n : ℕ} (s : K.obj (.op (.mk n))) :
    C(StdSimplex ℝ (Fin (n+1)), SSet.toTop.obj (SSet.Subcomplex.ofSimplex s : SSet)) :=
…
  44. theorem OAI.Thomason.Construction.RealizationPrism.monogenousPoint_surjective line 792

    Source documentation

    This map covers every point, including all degenerate representations.

    theorem monogenousPoint_surjective (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) : Function.Surjective (monogenousPoint K s) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.monogenousPoint

  45. theorem OAI.Thomason.Construction.RealizationPrism.monogenousPoint_isQuotientMap line 807

    Source documentation

    The realization of a simplex-generated subcomplex is its closed topological quotient.

    theorem monogenousPoint_isQuotientMap (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) : IsQuotientMap (monogenousPoint K s) :=
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.monogenousPoint

  46. theorem OAI.Thomason.Construction.RealizationPrism.monogenousPoint_inclusion line 813

    Source documentation

    The original simplex parameter map factors through that quotient and the closed inclusion.

    theorem monogenousPoint_inclusion (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) :
    (SSet.toTop.map (SSet.Subcomplex.ofSimplex s).ι).hom.comp (monogenousPoint K s) =
      simplexPoint K s := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.monogenousPoint, OAI.Thomason.Construction.RealizationPrism.simplexPoint

  47. def OAI.Thomason.Construction.RealizationPrism.fullSupport line 839

    Source documentation

    The barycentric interior, expressed by its nonzero coordinates.

    def fullSupport (n : ℕ) : Set (StdSimplex ℝ (Fin (n+1))) :=
…
  48. theorem OAI.Thomason.Construction.RealizationPrism.fullSupport_isOpen line 842
  49. theorem OAI.Thomason.Construction.RealizationPrism.normalization_dim_le_supportLen line 853
  50. theorem OAI.Thomason.Construction.RealizationPrism.fullSupport_of_supportLen_ge line 859
  51. theorem OAI.Thomason.Construction.RealizationPrism.interior_simplexPoint_fiber line 872

    Source documentation

    A point of a nondegenerate simplex interior has no other representative in that simplex, including on its boundary.

    theorem interior_simplexPoint_fiber (K : SSet.{0}) (s : K.N)
    (x y : StdSimplex ℝ (Fin (s.dim+1))) (hx : x ∈ fullSupport s.dim)
    (hxy : simplexPoint K s.simplex y = simplexPoint K s.simplex x) : y = x := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.fullSupport, OAI.Thomason.Construction.RealizationPrism.simplexPoint

  52. theorem OAI.Thomason.Construction.RealizationPrism.interior_preimage_image line 886

    Source documentation

    The nondegenerate interior is saturated under the simplex quotient.

    theorem interior_preimage_image (K : SSet.{0}) (s : K.N) :
    (simplexPoint K s.simplex) ⁻¹' ((simplexPoint K s.simplex) '' fullSupport s.dim) =
      fullSupport s.dim := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint, OAI.Thomason.Construction.RealizationPrism.fullSupport

  53. theorem OAI.Thomason.Construction.RealizationPrism.closedMap_restrictPreimage line 914

    Source documentation

    A closed map remains closed on the preimage of any target subspace.

    theorem closedMap_restrictPreimage {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} (hf : IsClosedMap f) (S : Set Y) : IsClosedMap (S.restrictPreimage f) := by
…
  54. def OAI.Thomason.Construction.RealizationPrism.cellInteriorHomeomorph line 930

    Source documentation

    The open barycentric simplex is homeomorphic to the corresponding nondegenerate cell in the actual realization.

    def cellInteriorHomeomorph (K : SSet.{0}) (s : K.N) :
    fullSupport s.dim ≃ₜ (simplexPoint K s.simplex '' fullSupport s.dim) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.fullSupport, OAI.Thomason.Construction.RealizationPrism.simplexPoint

  55. theorem OAI.Thomason.Construction.RealizationPrism.fullSupport_dense line 972

    Source documentation

    Every barycentric point is approached by points with all coordinates nonzero, by moving it towards the barycenter.

    theorem fullSupport_dense (n : ℕ) : Dense (fullSupport n) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.fullSupport

  56. theorem OAI.Thomason.Construction.RealizationPrism.closure_cellInterior line 1000

    Source documentation

    The closed characteristic simplex is the closure of its open cell. The statement is valid even when some boundary faces are identified.

    theorem closure_cellInterior (K : SSet.{0}) (s : K.N) :
    closure (simplexPoint K s.simplex '' fullSupport s.dim) =
      Set.range (simplexPoint K s.simplex) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint, OAI.Thomason.Construction.RealizationPrism.fullSupport