FinitePosetCoordinates.lean`

67 declarations, 0 contain sorry, 0 declared as axioms

Relative homotopies lift through finite singular cubes

def OAI.Thomason.Construction.RealizedCube.homotopyCube line 24
Source documentation
Regard the homotopy parameter as the first coordinate of one larger cube.
```
def homotopyCube {X : TopCat.{0}} {n : ℕ} {p q : C((Fin n → unitInterval), X)}
    (H : p.Homotopy q) : C((Fin (n+1) → unitInterval), X) :=
…
```
theorem OAI.Thomason.Construction.RealizedCube.homotopyCube_zero line 28
theorem OAI.Thomason.Construction.RealizedCube.homotopyCube_one line 34
theorem OAI.Thomason.Construction.RealizedCube.homotopyCube_side line 40

def OAI.Thomason.Construction.RealizedCube.liftLoopHomotopy line 64

Source documentation

The cubical lift preserves a homotopy relative to the entire boundary.

def liftLoopHomotopy {X : TopCat.{0}} {x : X} {n : ℕ}
    {p q : GenLoop (Fin (n+1)) X x}
    (H : p.val.HomotopyRel q.val (Cube.boundary (Fin (n+1)))) :
    (liftLoop n p).val.HomotopyRel (liftLoop n q).val (Cube.boundary (Fin (n+1))) where
…

Mentions: OAI.Thomason.Construction.RealizedCube.liftLoop

theorem OAI.Thomason.Construction.RealizedCube.liftLoop_homotopic line 98
Source documentation
The based cube construction is well-defined on homotopy classes.
```
theorem liftLoop_homotopic {X : TopCat.{0}} {x : X} {n : ℕ}
    {p q : GenLoop (Fin (n+1)) X x} (h : GenLoop.Homotopic p q) :
    GenLoop.Homotopic (liftLoop n p) (liftLoop n q) :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.liftLoop
def OAI.Thomason.Construction.RealizedCube.liftGroup line 120
Source documentation
Cubical singular lifting descends through actual relative homotopies.
```
def liftGroup (X : TopCat.{0}) (x : X) (n : ℕ) :
    HomotopyGroup.Pi (n+1) X x →
      HomotopyGroup.Pi (n+1) (SSet.toTop.obj (TopCat.toSSet.obj X)) (singularVertex X x) :=
…
```
Mentions: OAI.Thomason.Construction.singularVertex
theorem OAI.Thomason.Construction.RealizedCube.counit_liftGroup line 126
Source documentation
Evaluation is a left inverse to this section on the actual homotopy quotient.
```
theorem counit_liftGroup (X : TopCat.{0}) (x : X) (n : ℕ)
    (p : HomotopyGroup.Pi (n+1) X x) :
    HomotopyMaps.basedGroupMap (sSetTopAdj.counit.app X).hom
      (counit_singularVertex X x) (n+1) (liftGroup X x n p) = p := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.basedGroupMap, OAI.Thomason.Construction.counit_singularVertex, OAI.Thomason.Construction.RealizedCube.liftGroup
theorem OAI.Thomason.Construction.RealizedCube.liftGroup_injective line 137
theorem OAI.Thomason.Construction.RealizedCube.singularMap_naturality line 142
Source documentation
Singular cubical maps commute with postcomposition by continuous maps.
```
theorem singularMap_naturality {X Y : TopCat.{0}} (f : X ⟶ Y) (n : ℕ)
    (p : C((Fin n → unitInterval), X)) :
    singularMap n (f.hom.comp p) = singularMap n p ≫ TopCat.toSSet.map f := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.singularMap

theorem OAI.Thomason.Construction.RealizedCube.liftMap_naturality line 148

Source documentation

The continuous cubical lifting operation is natural in its target space.

theorem liftMap_naturality {X Y : TopCat.{0}} (f : X ⟶ Y) (n : ℕ)
    (p : C((Fin n → unitInterval), X)) (t : Fin n → unitInterval) :
    (SSet.toTop.map (TopCat.toSSet.map f)).hom (liftMap n p t) =
      liftMap n (f.hom.comp p) t := by
…

Mentions: OAI.Thomason.Construction.RealizedCube.liftMap

theorem OAI.Thomason.Construction.RealizedCube.liftGroup_naturality line 157
Source documentation
The section on positive homotopy groups is natural in all continuous maps.
```
theorem liftGroup_naturality {X Y : TopCat.{0}} (f : X ⟶ Y) (x : X) (n : ℕ)
    (p : HomotopyGroup.Pi (n+1) X x) :
    HomotopyMaps.basedGroupMap (SSet.toTop.map (TopCat.toSSet.map f)).hom
      (singularVertex_naturality f x) (n+1) (liftGroup X x n p) =
      liftGroup Y (f.hom x) n (HomotopyMaps.groupMap f.hom (n+1) x p) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.basedGroupMap, OAI.Thomason.Construction.singularVertex_naturality, OAI.Thomason.Construction.RealizedCube.liftGroup, OAI.Thomason.Construction.HomotopyMaps.groupMap

theorem OAI.Thomason.Construction.singular_unit_continuous_left_inverse line 186

Source documentation

The adjunction triangle is an actual continuous left inverse to the realized unit.

theorem singular_unit_continuous_left_inverse (K : SSet.{0}) :
    (sSetTopAdj.counit.app (SSet.toTop.obj K)).hom.comp
      (SSet.toTop.map (sSetTopAdj.unit.app K)).hom = ContinuousMap.id _ :=
…

theorem OAI.Thomason.Construction.singular_unit_groupMap_injective line 192
Source documentation
The realized unit is injective on every positive homotopy group.
```
theorem singular_unit_groupMap_injective (K : SSet.{0})
    (x : SSet.toTop.obj K) (n : ℕ) :
    Function.Injective (HomotopyMaps.groupMap
      (SSet.toTop.map (sSetTopAdj.unit.app K)).hom (n+1) x) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap
theorem OAI.Thomason.Construction.singular_unit_components_bijective line 211
Source documentation
The realized unit is already bijective on path components.
```
theorem singular_unit_components_bijective (K : SSet.{0}) :
    Function.Bijective (HomotopyMaps.componentsMap
      (SSet.toTop.map (sSetTopAdj.unit.app K)).hom) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.singular_unit_weak_iff_groupMap_surjective line 221
Source documentation
Only surjectivity in positive degrees remains in the unit weak-equivalence test.
```
theorem singular_unit_weak_iff_groupMap_surjective (K : SSet.{0}) :
    realizationWeakEquivalences (sSetTopAdj.unit.app K) ↔
      ∀ (n : ℕ) (x : SSet.toTop.obj K), Function.Surjective (HomotopyMaps.groupMap
        (SSet.toTop.map (sSetTopAdj.unit.app K)).hom (n+1) x) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.HomotopyMaps.groupMap

theorem OAI.Thomason.Construction.singular_counit_weak_iff_groupMap_injective line 233

Source documentation

Dually, only positive-degree injectivity remains for the singular counit.

theorem singular_counit_weak_iff_groupMap_injective (X : TopCat.{0}) :
    topologicalWeakEquivalences (sSetTopAdj.counit.app X) ↔
      ∀ (n : ℕ) (x : SSet.toTop.obj (TopCat.toSSet.obj X)),
        Function.Injective (HomotopyMaps.groupMap (sSetTopAdj.counit.app X).hom (n+1) x) := by
…

Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.HomotopyMaps.groupMap

theorem OAI.Thomason.Construction.RealizedCube.realization_contractible line 262
Source documentation
The actual realization of each finite simplicial cube is contractible.
```
theorem realization_contractible (n : ℕ) : ContractibleSpace (SSet.toTop.obj (obj n)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.singular_unit_weak line 274
Source documentation
Every finite cubical local model satisfies the genuine singular-unit weak test.
```
theorem singular_unit_weak (n : ℕ) :
    realizationWeakEquivalences (sSetTopAdj.unit.app (obj n)) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.singular_counit_weak line 280
Source documentation
The actual evaluation counit is weak on each realized finite cubical local model.
```
theorem singular_counit_weak (n : ℕ) :
    topologicalWeakEquivalences (sSetTopAdj.counit.app (SSet.toTop.obj (obj n))) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.RealizedCube.obj

theorem OAI.Thomason.Construction.singular_counit_group_naturality line 307

Source documentation

Evaluation commutes with the actual based group maps at singular vertices.

theorem singular_counit_group_naturality {X Y : TopCat.{0}} (p : X ⟶ Y)
    (x : X) (n : ℕ)
    (a : HomotopyGroup.Pi (n+1) (SSet.toTop.obj (TopCat.toSSet.obj X))
      (singularVertex X x)) :
    HomotopyMaps.groupMap p.hom (n+1) x
      (HomotopyMaps.basedGroupMap (sSetTopAdj.counit.app X).hom
        (counit_singularVertex X x) (n+1) a) =
    HomotopyMaps.basedGroupMap (sSetTopAdj.counit.app Y).hom
      (counit_singularVertex Y (p.hom x)) (n+1)
      (HomotopyMaps.basedGroupMap (SSet.toTop.map (TopCat.toSSet.map p)).hom
        (singularVertex_naturality p x) (n+1) a) := by
…

Mentions: OAI.Thomason.Construction.singularVertex, OAI.Thomason.Construction.HomotopyMaps.groupMap, OAI.Thomason.Construction.HomotopyMaps.basedGroupMap, OAI.Thomason.Construction.counit_singularVertex, OAI.Thomason.Construction.singularVertex_naturality

theorem OAI.Thomason.Construction.singular_groupMap_bijective_reflects line 327
Source documentation
Bijectivity on a positive homotopy group is reflected by singular realization, through the natural section and evaluation retraction.
```
theorem singular_groupMap_bijective_reflects {X Y : TopCat.{0}} (p : X ⟶ Y)
    (x : X) (n : ℕ)
    (hp : Function.Bijective
      (HomotopyMaps.basedGroupMap (SSet.toTop.map (TopCat.toSSet.map p)).hom
        (singularVertex_naturality p x) (n+1))) :
    Function.Bijective (HomotopyMaps.groupMap p.hom (n+1) x) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.basedGroupMap, OAI.Thomason.Construction.singularVertex_naturality, OAI.Thomason.Construction.HomotopyMaps.groupMap
theorem OAI.Thomason.Construction.singular_realization_reflects_weak line 346
Source documentation
The actual realization weak-equivalence test on the singular map implies that the original continuous map is a weak homotopy equivalence.
```
theorem singular_realization_reflects_weak {X Y : TopCat.{0}} (p : X ⟶ Y)
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) :
    IsWeakHomotopyEquivalence p.hom := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.IsWeakHomotopyEquivalence
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.comp_of_le line 368
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.comp_congr line 372
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.left_unit line 378
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.right_unit line 390
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.assoc line 401
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.face_comp line 434
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.interchange line 464
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.category line 506
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.isTruncated line 520
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.projection line 524
Source documentation
The quotient projection from the bounded representative category.
```
noncomputable def projection (C : StrictOmegaCategory.{0}) (n : ℕ) :
    (C.bounded n).Hom (category C n) where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Hom, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.category
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unitCell line 544
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unitCell_face line 546
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unitCell_comp line 570
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unit line 596
Source documentation
Kill all cells above n by their source, imposing the necessary n-cell relation.
```
noncomputable def unit (C : StrictOmegaCategory.{0}) (n : ℕ) : C ⟶ category C n where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unit_surjective line 602
Source documentation
Every quotient cell is represented by an original cell of dimension at most n.
```
theorem unit_surjective (C : StrictOmegaCategory.{0}) (n : ℕ) :
    Function.Surjective (unit C n).toFun := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unit
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.descendCell line 625
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.descendCell_mk line 628
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.descend line 631
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unit_descend line 656
Source documentation
The descended functor agrees with the given functor on every original cell.
```
theorem unit_descend (hD : D.IsTruncated n) (f : C ⟶ D) :
    unit C n ≫ descend hD f = f := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unit, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.descend
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unit_hom_ext line 664
Source documentation
Uniqueness is cellwise surjectivity of the explicit quotient unit.
```
theorem unit_hom_ext {g g' : category C n ⟶ D}
    (h : unit C n ≫ g = unit C n ≫ g') : g = g' := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.category, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unit
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.descend_unique line 671
theorem OAI.Thomason.Construction.RealizationPrism.map_mem_vertexStar_iff line 692
Source documentation
A target vertex has positive mass precisely when some source vertex over it has positive mass. Repeated vertices are allowed.
```
theorem map_mem_vertexStar_iff {K L : SSet.{0}} (f : K ⟶ L)
    (x : SSet.toTop.obj K) (w : L.obj (.op (.mk 0))) :
    (SSet.toTop.map f).hom x ∈ vertexStar L w ↔
      ∃ v, f.app (.op (.mk 0)) v = w ∧ x ∈ vertexStar K v := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexStar

theorem OAI.Thomason.Construction.RealizationPrism.vertexStar_transfer line 710

Source documentation

A relation between maps on vertices transports positive vertex support for every point of the actual realization.

theorem vertexStar_transfer {K L M : SSet.{0}} (f : K ⟶ L) (g : K ⟶ M)
    (v : L.obj (.op (.mk 0))) (w : M.obj (.op (.mk 0)))
    (h : ∀ u, f.app (.op (.mk 0)) u = v → g.app (.op (.mk 0)) u = w)
    (x : SSet.toTop.obj K) (hx : (SSet.toTop.map f).hom x ∈ vertexStar L v) :
    (SSet.toTop.map g).hom x ∈ vertexStar M w := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.vertexStar

instance OAI.Thomason.Construction.fullSubposetInclusion_nerve_mono line 737
def OAI.Thomason.Construction.fullSubposetIso line 748
theorem OAI.Thomason.Construction.fullSubposetIso_hom_ι line 752
def OAI.Thomason.Construction.fullSubposetCarrierHomeomorph line 757
theorem OAI.Thomason.Construction.fullSubposetCarrierHomeomorph_inclusion line 764
theorem OAI.Thomason.Construction.fullSubposet_realization_isClosedEmbedding line 773
Source documentation
Full induced subposets realize as actual closed embeddings.
```
theorem fullSubposet_realization_isClosedEmbedding (A : Set P) :
    IsClosedEmbedding (SSet.toTop.map (nerveMap (fullSubposetInclusion A))).hom := by
…
```
Mentions: OAI.Thomason.Construction.fullSubposetInclusion
def OAI.Thomason.Construction.PosetGeometry.vertex line 803
theorem OAI.Thomason.Construction.PosetGeometry.simplexVertex_obj line 806
theorem OAI.Thomason.Construction.PosetGeometry.vertex_injective line 809
def OAI.Thomason.Construction.PosetGeometry.comparable line 813
theorem OAI.Thomason.Construction.PosetGeometry.vertexStar_carrier line 817
Source documentation
Every positive-support vertex in a simplex containing v is comparable with v; passing to the intrinsic interior removes zero-weight vertices.
```
theorem vertexStar_carrier (v : P) (x : SSet.toTop.obj (nerve P))
    (hx : x ∈ vertexStar (nerve P) (vertex v)) :
    carrier (nerve P) x ≤ fullSubposetComplex (comparable v) := by
…
```
Mentions: OAI.Thomason.Construction.PosetGeometry.vertex, OAI.Thomason.Construction.fullSubposetComplex, OAI.Thomason.Construction.PosetGeometry.comparable
def OAI.Thomason.Construction.PosetGeometry.coordinates line 858
Source documentation
Combine the zero-simplex coordinates using the corresponding poset elements.
```
def coordinates : C(SSet.toTop.obj (nerve P), StdSimplex ℝ P) :=
…
```
theorem OAI.Thomason.Construction.PosetGeometry.coordinates_simplexPoint line 862
theorem OAI.Thomason.Construction.PosetGeometry.coordinates_support_interior line 875
Source documentation
For an interior point, positive barycentric support is exactly the set of vertices of its intrinsic simplex.
```
theorem coordinates_support_interior {n : ℕ} (s : (nerve P).obj (.op (.mk n)))
    (p : StdSimplex ℝ (Fin (n+1))) (hp : p ∈ fullSupport n) (v : P) :
    v ∈ (coordinates P (simplexPoint (nerve P) s p)).weights.support ↔
      v ∈ Set.range s.obj := by
…
```
Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates

theorem OAI.Thomason.Construction.PosetGeometry.interior_eq_of_coordinates_eq line 892

Source documentation

Equal coordinates of nondegenerate interior points give equal actual realization points, including all possible face identifications.

theorem interior_eq_of_coordinates_eq (s t : (nerve P).N)
    (p : StdSimplex ℝ (Fin (s.dim+1))) (q : StdSimplex ℝ (Fin (t.dim+1)))
    (hp : p ∈ fullSupport s.dim) (hq : q ∈ fullSupport t.dim)
    (he : coordinates P (simplexPoint (nerve P) s.simplex p) =
      coordinates P (simplexPoint (nerve P) t.simplex q)) :
    simplexPoint (nerve P) s.simplex p = simplexPoint (nerve P) t.simplex q := by
…

Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates

theorem OAI.Thomason.Construction.PosetGeometry.coordinates_injective line 918
Source documentation
Barycentric vertex coordinates distinguish every point of the actual realization of a poset nerve, without a finiteness assumption.
```
theorem coordinates_injective : Function.Injective (coordinates P) := by
…
```
Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates
def OAI.Thomason.Construction.PosetGeometry.vertexSet line 950
Source documentation
A nondegenerate poset simplex is determined by its finite vertex set.
```
def vertexSet (s : (nerve P).N) : Finset P := by
…
```
theorem OAI.Thomason.Construction.PosetGeometry.vertexSet_injective line 954
theorem OAI.Thomason.Construction.PosetGeometry.nerve_finite line 967
Source documentation
Finitely many vertices in a poset give finitely many nondegenerate nerve simplices, rather than merely degreewise finiteness.
```
theorem nerve_finite [Finite P] : (nerve P).Finite where
…
```
theorem OAI.Thomason.Construction.PosetGeometry.coordinates_isClosedEmbedding line 971
Source documentation
For finite posets the coordinate injection is a closed embedding.
```
theorem coordinates_isClosedEmbedding [Finite P] : IsClosedEmbedding (coordinates P) := by
…
```
Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates
def OAI.Thomason.Construction.PosetGeometry.coordinatesHomeomorph line 979
Source documentation
The actual finite-poset realization is homeomorphic to its barycentric image.
```
def coordinatesHomeomorph [Finite P] :
    SSet.toTop.obj (nerve P) ≃ₜ Set.range (coordinates P) :=
…
```
Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates