SimplexCubeRetract.lean`

57 declarations, 0 contain sorry, 0 declared as axioms

Weak equivalences on compatible simplicial exhaustions

theorem OAI.Thomason.Construction.RealizationPrism.exhaustion_map_naturality line 29
Source documentation
Compatibility with the ambient map determines every transition square.
```
theorem exhaustion_map_naturality {m n : ℕ} (hmn : m ≤ n) :
    SSet.Subcomplex.homOfLE (hA hmn) ≫ g n =
      g m ≫ SSet.Subcomplex.homOfLE (hB hmn) := by
…
```
theorem OAI.Thomason.Construction.RealizationPrism.exhaustion_map_components_surjective line 44
Source documentation
Component surjectivity passes from all stages to their exhausted target.
```
theorem exhaustion_map_components_surjective (hcoverB : iSup B = ⊤)
    (hW : ∀ n, realizationWeakEquivalences (g n)) :
    Function.Surjective (HomotopyMaps.componentsMap (SSet.toTop.map f).hom) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.RealizationPrism.exhaustion_map_components_injective line 74
Source documentation
Component equality in the target is already witnessed in a common finite stage, where the stage weak equivalence reflects it.
```
theorem exhaustion_map_components_injective
    (hcoverA : iSup A = ⊤) (hcoverB : iSup B = ⊤)
    (hW : ∀ n, realizationWeakEquivalences (g n)) :
    Function.Injective (HomotopyMaps.componentsMap (SSet.toTop.map f).hom) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.RealizationPrism.exhaustion_map_groupMap_injective_stage line 130
Source documentation
Positive homotopy injectivity at a basepoint in a specified stage. Only the two representatives and their target homotopy are enlarged.
```
theorem exhaustion_map_groupMap_injective_stage
    (hcoverA : iSup A = ⊤) (hcoverB : iSup B = ⊤)
    (hW : ∀ n, realizationWeakEquivalences (g n))
    (m : ℕ) (x : SSet.toTop.obj (A m : SSet)) (d : ℕ) :
    Function.Injective (HomotopyMaps.groupMap (SSet.toTop.map f).hom (d+1)
      ((SSet.toTop.map (A m).ι).hom x)) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.HomotopyMaps.groupMap
theorem OAI.Thomason.Construction.RealizationPrism.exhaustion_map_groupMap_surjective_stage line 223
Source documentation
Every target sphere has a preimage in some finite stage, with the original source basepoint retained exactly.
```
theorem exhaustion_map_groupMap_surjective_stage
    (hcoverB : iSup B = ⊤) (hW : ∀ n, realizationWeakEquivalences (g n))
    (m : ℕ) (x : SSet.toTop.obj (A m : SSet)) (d : ℕ) :
    Function.Surjective (HomotopyMaps.groupMap (SSet.toTop.map f).hom (d+1)
      ((SSet.toTop.map (A m).ι).hom x)) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.HomotopyMaps.groupMap
theorem OAI.Thomason.Construction.RealizationPrism.exhaustion_map_weak line 283
Source documentation
A compatible map of exhaustive increasing simplicial subcomplexes is an actual weak equivalence whenever every stage map is one. No model structure, singular comparison, or gluing theorem is assumed.
```
theorem exhaustion_map_weak (hcoverA : iSup A = ⊤) (hcoverB : iSup B = ⊤)
    (hW : ∀ n, realizationWeakEquivalences (g n)) :
    realizationWeakEquivalences f := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
def OAI.Thomason.Construction.RealizedCube.obj line 316
Source documentation
Only finite powers of the simplicial interval are needed for homotopy groups.
```
def obj (n : ℕ) : SSet.{0} :=
…
```
def OAI.Thomason.Construction.RealizedCube.coordinates line 322
Source documentation
Continuous coordinates on the realization of a finite simplicial cube.
```
def coordinates (n : ℕ) : C(SSet.toTop.obj (obj n), Fin n → unitInterval) :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
def OAI.Thomason.Construction.RealizedCube.sectionMap line 339
Source documentation
Iterated realization prisms give a continuous section of the cube coordinates.
```
def sectionMap (n : ℕ) : C((Fin n → unitInterval), SSet.toTop.obj (obj n)) :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.coordinates_section line 348
Source documentation
The section has exactly the specified coordinates, in every dimension.
```
theorem coordinates_section (n : ℕ) (p : Fin n → unitInterval) :
    coordinates n (sectionMap n p) = p := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.coordinates, OAI.Thomason.Construction.RealizedCube.sectionMap
def OAI.Thomason.Construction.RealizedCube.singularMap line 362
Source documentation
A continuous cube has an exact lift through singular evaluation after finite triangulation.
```
def singularMap {X : TopCat.{0}} (n : ℕ) (p : C((Fin n → unitInterval), X)) :
    obj n ⟶ TopCat.toSSet.obj X :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.singularMap_evaluation line 367
Source documentation
Evaluation of the realized triangulated lift recovers the original continuous cube.
```
theorem singularMap_evaluation {X : TopCat.{0}} (n : ℕ)
    (p : C((Fin n → unitInterval), X)) (t : Fin n → unitInterval) :
    (sSetTopAdj.counit.app X).hom
      ((SSet.toTop.map (singularMap n p)).hom (sectionMap n t)) = p t := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.singularMap, OAI.Thomason.Construction.RealizedCube.sectionMap
def OAI.Thomason.Construction.RealizedCube.endpoint line 396
def OAI.Thomason.Construction.RealizedCube.face line 399
Source documentation
The coordinate face of a finite simplicial cube.
```
def face (n : ℕ) (i : Fin (n+1)) (e : Bool) : obj n ⟶ obj (n+1) :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.face_zero line 405
theorem OAI.Thomason.Construction.RealizedCube.face_succ line 408
theorem OAI.Thomason.Construction.RealizedCube.coordinates_comparison line 411
theorem OAI.Thomason.Construction.RealizedCube.face_zero_apply line 421

theorem OAI.Thomason.Construction.RealizedCube.coordinates_whisker line 430

Source documentation

The two projections of a mapped prism are its mapped base and unchanged time.

theorem coordinates_whisker {K : SSet.{0}} (n : ℕ) (f : K ⟶ obj n)
    (x : SSet.toTop.obj (K ⊗ Δ[1])) :
    coordinates (n+1) ((SSet.toTop.map (f ▷ Δ[1])).hom x) =
      Fin.cons
        (PrismBarycentric.realizationTime.hom ((SSet.toTop.map (snd K Δ[1])).hom x))
        (coordinates n ((SSet.toTop.map f).hom ((SSet.toTop.map (fst K Δ[1])).hom x))) := by
…

Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.RealizedCube.coordinates

theorem OAI.Thomason.Construction.RealizedCube.coordinates_face line 454
Source documentation
Every realized simplicial face has the expected cubical coordinates.
```
theorem coordinates_face (n : ℕ) (i : Fin (n+1)) (e : Bool)
    (x : SSet.toTop.obj (obj n)) :
    coordinates (n+1) ((SSet.toTop.map (face n i e)).hom x) =
      Fin.insertNth i (endpoint e) (coordinates n x) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.RealizedCube.coordinates, OAI.Thomason.Construction.RealizedCube.face, OAI.Thomason.Construction.RealizedCube.endpoint
theorem OAI.Thomason.Construction.RealizedCube.section_face line 474
Source documentation
The chosen section sends every topological face into the corresponding simplicial face.
```
theorem section_face (n : ℕ) (i : Fin (n+1)) (e : Bool) (p : Fin n → unitInterval) :
    sectionMap (n+1) (Fin.insertNth i (endpoint e) p) =
      (SSet.toTop.map (face n i e)).hom (sectionMap n p) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.sectionMap, OAI.Thomason.Construction.RealizedCube.endpoint, OAI.Thomason.Construction.RealizedCube.face
def OAI.Thomason.Construction.RealizedCube.boundary line 517
Source documentation
All coordinate faces of the (n+1)-dimensional simplicial cube.
```
def boundary (n : ℕ) : (obj (n+1)).Subcomplex :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.range_boundary_inclusion line 520
theorem OAI.Thomason.Construction.RealizedCube.coordinates_boundary line 530
Source documentation
The coordinates of every point of the realized boundary lie on a topological coordinate face.
```
theorem coordinates_boundary (n : ℕ)
    (x : SSet.toTop.obj (boundary n : SSet.{0})) :
    coordinates (n+1) ((SSet.toTop.map (boundary n).ι).hom x) ∈
      Cube.boundary (Fin (n+1)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.boundary, OAI.Thomason.Construction.RealizedCube.coordinates
theorem OAI.Thomason.Construction.RealizedCube.section_mem_boundary line 546
Source documentation
The cubical section preserves the entire boundary as a subspace.
```
theorem section_mem_boundary (n : ℕ) (x : Fin (n+1) → unitInterval)
    (hx : x ∈ Cube.boundary (Fin (n+1))) :
    sectionMap (n+1) x ∈ Set.range (SSet.toTop.map (boundary n).ι).hom := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.sectionMap, OAI.Thomason.Construction.RealizedCube.boundary
def OAI.Thomason.Construction.RealizedCube.boundaryCoordinates line 561
def OAI.Thomason.Construction.RealizedCube.boundarySection line 570
Source documentation
The ordinary boundary section, with values in the actual realized simplicial boundary.
```
def boundarySection (n : ℕ) :
    C(Cube.boundary (Fin (n+1)), SSet.toTop.obj (boundary n : SSet.{0})) :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.boundary
theorem OAI.Thomason.Construction.RealizedCube.boundarySection_inclusion line 579
theorem OAI.Thomason.Construction.RealizedCube.boundaryCoordinates_section line 585
def OAI.Thomason.Construction.RealizedCube.boundaryInclusion line 591
def OAI.Thomason.Construction.RealizedCube.boundaryArrowRetract line 597
Source documentation
A retract in the actual topological arrow category, preserving both boundaries and ambient cubes.
```
def boundaryArrowRetract (n : ℕ) :
    RetractArrow (boundaryInclusion n) (SSet.toTop.map (boundary n).ι) where
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.boundaryInclusion, OAI.Thomason.Construction.RealizedCube.boundary
theorem OAI.Thomason.Construction.RealizedCube.boundary_lifting_of_barycentric line 619
Source documentation
Barycentric boundary lifting implies ordinary cubical boundary lifting, without a singular comparison or a Kan--Quillen model structure.
```
theorem boundary_lifting_of_barycentric {X Y : TopCat.{0}} (p : X ⟶ Y)
    (hp : ∀ n, HasLiftingProperty (RealizationPrism.boundaryInclusion n) p) (n : ℕ) :
    HasLiftingProperty (boundaryInclusion n) p := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion, OAI.Thomason.Construction.RealizedCube.boundaryInclusion
theorem OAI.Thomason.Construction.CubeBoundaryValues.isClosed_boundary line 641
def OAI.Thomason.Construction.CubeBoundaryValues.region line 652
theorem OAI.Thomason.Construction.CubeBoundaryValues.region_closed line 657
theorem OAI.Thomason.Construction.CubeBoundaryValues.region_cover line 663
def OAI.Thomason.Construction.CubeBoundaryValues.chart line 676
theorem OAI.Thomason.Construction.CubeBoundaryValues.chart_overlap line 681
def OAI.Thomason.Construction.CubeBoundaryValues.map line 694
Source documentation
The boundary map with p at time zero, q at time one, and value x on every lateral face.
```
def map (p q : GenLoop (Fin n) X x) : C(Cube.boundary (Fin (n+1)), X) where
…
```
theorem OAI.Thomason.Construction.CubeBoundaryValues.map_zero line 708
theorem OAI.Thomason.Construction.CubeBoundaryValues.map_one line 713
theorem OAI.Thomason.Construction.CubeBoundaryValues.map_lateral line 718
def OAI.Thomason.Construction.CubicalLifting.homotopyCube line 744
theorem OAI.Thomason.Construction.CubicalLifting.homotopyBoundarySquare line 748
structure OAI.Thomason.Construction.CubicalLifting.HomotopyLift line 770
def OAI.Thomason.Construction.CubicalLifting.liftHomotopy line 776
Source documentation
The full homotopy lifts with both endpoints and all boundary values prescribed; this is stronger than lifting an unbased path.
```
def liftHomotopy (hf : ∀ m, HasLiftingProperty (RealizedCube.boundaryInclusion m) f) :
    HomotopyLift f p q H := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.boundaryInclusion, OAI.Thomason.Construction.CubicalLifting.HomotopyLift
def OAI.Thomason.Construction.SieveSimplex.whole line 819
Source documentation
Every cell of a simplex in the sieve belongs to its full zero fibre.
```
noncomputable def whole {m : ℕ} (s : Fin (m+1) →o A) :
    h.object m ⟶ labelFiber (label A hA ((subposetInclusion A).comp s) h) 0 where
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.label, OAI.Thomason.Construction.subposetInclusion
theorem OAI.Thomason.Construction.SieveSimplex.whole_cut_clamp line 830
Source documentation
The clamped vertex map of a simplex already in the sieve is unchanged.
```
theorem whole_cut_clamp {m : ℕ} (s : Fin (m+1) →o A)
    (c : Cut A ((subposetInclusion A).comp s)) : c.clamp = s := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.Cut, OAI.Thomason.Construction.subposetInclusion
theorem OAI.Thomason.Construction.SieveSimplex.whole_back line 838
Source documentation
On an entire sieve simplex, the clamping inverse is its original colimit leg.
```
theorem whole_back {m : ℕ} (s : Fin (m+1) →o A) :
    whole A hA h s ≫ back A hA h ((subposetInclusion A).comp s) = h.posetLeg s := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.whole, OAI.Thomason.Construction.SieveSimplex.back, OAI.Thomason.Construction.subposetInclusion
def OAI.Thomason.Construction.cubeSimplexRank line 865
Source documentation
Count the interval coordinates of a cube simplex, pointwise along its ordinal parameter. This is monotone in that parameter.
```
def cubeSimplexRank (n : ℕ) : {d : SimplexCategoryᵒᵖ} →
    (RealizedCube.obj n).obj d → (Fin (d.unop.len + 1) →o Fin (n+1)) :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj

theorem OAI.Thomason.Construction.cubeSimplexRank_naturality line 882

Source documentation

Counting commutes exactly with every ordinal face and degeneracy.

theorem cubeSimplexRank_naturality (n : ℕ) {d e : SimplexCategoryᵒᵖ} (f : d ⟶ e)
    (x : (RealizedCube.obj n).obj d) (j : Fin (e.unop.len+1)) :
    cubeSimplexRank n ((RealizedCube.obj n).map f x) j =
      cubeSimplexRank n x (f.unop.toOrderHom j) := by
…

Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.cubeSimplexRank

def OAI.Thomason.Construction.cubeToSimplex line 897
Source documentation
The actual simplicial map from the cube to the simplex counting its ordered interval coordinates.
```
def cubeToSimplex (n : ℕ) : RealizedCube.obj n ⟶ (Δ[n] : SSet.{0}) where
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
def OAI.Thomason.Construction.simplexCubeClamp line 909
Source documentation
Truncate the last vertex of a standard simplex to its preceding one.
```
def simplexCubeClamp (n : ℕ) : ⦋n+1⦌ ⟶ ⦋n⦌ :=
…
```
def OAI.Thomason.Construction.simplexCubeLast line 918
Source documentation
The final Boolean coordinate records exactly the final simplex vertex.
```
def simplexCubeLast (n : ℕ) : ⦋n+1⦌ ⟶ ⦋1⦌ :=
…
```
def OAI.Thomason.Construction.simplexToCube line 937
Source documentation
Embed the ordered simplex as the chain of cube vertices with increasing numbers of final coordinates.
```
def simplexToCube (n : ℕ) : (Δ[n] : SSet.{0}) ⟶ RealizedCube.obj n :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.cubeSimplexRank_simplexToCube line 945
Source documentation
Counting the embedded coordinates recovers every ordinal coordinate, including degenerate simplices.
```
theorem cubeSimplexRank_simplexToCube (n : ℕ) {d : SimplexCategoryᵒᵖ}
    (x : (Δ[n] : SSet.{0}).obj d) (j : Fin (d.unop.len+1)) :
    cubeSimplexRank n ((simplexToCube n).app d x) j =
      (SSet.stdSimplex.objEquiv x).toOrderHom j := by
…
```
Mentions: OAI.Thomason.Construction.cubeSimplexRank, OAI.Thomason.Construction.simplexToCube
theorem OAI.Thomason.Construction.simplexToCube_cubeToSimplex line 972
Source documentation
The standard simplex is a genuine simplicial retract of the cube of the same dimension. No geometric approximation is involved.
```
theorem simplexToCube_cubeToSimplex (n : ℕ) :
    simplexToCube n ≫ cubeToSimplex n = 𝟙 (Δ[n] : SSet.{0}) := by
…
```
Mentions: OAI.Thomason.Construction.simplexToCube, OAI.Thomason.Construction.cubeToSimplex