SubdivisionWeakLifting.lean`

51 declarations, 0 contain sorry, 0 declared as axioms

Extension preserves the deletion/closed-star cover

A map from the nerve of a poset with a greatest vertex into a simplex subcomplex either avoids its greatest allowed vertex, or lies in that vertex's closed star. Appending the greatest source vertex supplies the face witnessing the second alternative.

def OAI.Thomason.Construction.appendGreatestSimplex line 35
theorem OAI.Thomason.Construction.appendGreatestSimplex_castSucc line 51
theorem OAI.Thomason.Construction.appendGreatestSimplex_last line 58
theorem OAI.Thomason.Construction.simplex_in_containing_face line 64
theorem OAI.Thomason.Construction.nerve_map_factors_deletion_or_star line 77
theorem OAI.Thomason.Construction.extension_deletion_star_cover line 141
def OAI.Thomason.Construction.containedSubcomplexIso line 191
theorem OAI.Thomason.Construction.canonicalExtension_anodyne_of_cover_inside line 202
theorem OAI.Thomason.Construction.canonicalExtension_simplexSubcomplex_aux line 216
theorem OAI.Thomason.Construction.canonicalExtension_simplexSubcomplex_anodyne line 255
Source documentation
Every subcomplex of a standard simplex has an anodyne canonical extension, including its entire original boundary.
```
theorem canonicalExtension_simplexSubcomplex_anodyne {n : ℕ}
    (A : (Δ[n] : SSet.{0}).Subcomplex) :
    SSet.anodyneExtensions (canonicalExtension.app A.toSSet) :=
…
```
theorem OAI.Thomason.Construction.canonicalExtension_boundary_anodyne line 261
theorem OAI.Thomason.Construction.relativeCanonicalExtension_boundary_anodyne line 265
def OAI.Thomason.Construction.subdivisionUnitHomotopy line 294
Source documentation
The mate of the double-last-vertex homotopy compares the canonical extension on Sd K with the adjunction unit on K.
```
def subdivisionUnitHomotopy (K : SSet.{0}) :
    SSet.Homotopy (lastVertex.app K ≫ SSet.sdExAdjunction.unit.app K)
      (canonicalExtension.app (SSet.sd.obj K)) := by
…
```

theorem OAI.Thomason.Construction.exists_subdivision_descent line 310

Source documentation

If the canonical extension of the subdivided parameter is anodyne, every map from that subdivision into a Kan complex descends up to an actual simplicial homotopy.

theorem exists_subdivision_descent (K X : SSet.{0}) [SSet.KanComplex X]
    (hK : SSet.anodyneExtensions (canonicalExtension.app (SSet.sd.obj K)))
    (f : SSet.sd.obj K ⟶ X) :
    ∃ g : K ⟶ X, Nonempty (SSet.Homotopy
      (lastVertex.app K ≫ g) f) := by
…

theorem OAI.Thomason.Construction.exists_standard_subdivision_descent line 327

Source documentation

This descent is already unconditional for every standard simplex.

theorem exists_standard_subdivision_descent (n : ℕ) (X : SSet.{0}) [SSet.KanComplex X]
    (f : SSet.sd.obj (SSet.stdSimplex.obj (.mk n)) ⟶ X) :
    ∃ g : SSet.stdSimplex.obj (.mk n) ⟶ X, Nonempty (SSet.Homotopy
      (lastVertex.app (SSet.stdSimplex.obj (.mk n)) ≫ g) f) :=
…

theorem OAI.Thomason.Construction.finitePoset_nerve_simplex_embedding line 356
theorem OAI.Thomason.Construction.canonicalExtension_subdivision_of_simplex_mono line 377
theorem OAI.Thomason.Construction.canonicalExtension_subdivision_finitePoset_anodyne line 384
theorem OAI.Thomason.Construction.exists_finitePoset_subdivision_descent line 396
theorem OAI.Thomason.Construction.exists_subcomplex_subdivision_descent line 402
def OAI.Thomason.Construction.SubdivisionBarycentric.subdivisionHomeomorphOfMono line 430
def OAI.Thomason.Construction.SubdivisionBarycentric.finitePosetSubdivisionHomeomorph line 440
Source documentation
For every finite poset, including the empty one, subdivision retains the actual realization space homeomorphically.
```
def finitePosetSubdivisionHomeomorph (P : Type) [PartialOrder P] [Finite P] :
    SSet.toTop.obj (SSet.sd.obj (nerve P)) ≃ₜ SSet.toTop.obj (nerve P) := by
…
```
theorem OAI.Thomason.Construction.subdivision_descent_weak_iff line 477

theorem OAI.Thomason.Construction.exists_finitePoset_weak_descent line 491

Source documentation

Finite-poset descent preserves and reflects the actual topological weak-equivalence predicate, with a simplicial comparison homotopy.

theorem exists_finitePoset_weak_descent (P : Type) [PartialOrder P] [Finite P]
    (X : SSet.{0}) [SSet.KanComplex X] (f : SSet.sd.obj (nerve P) ⟶ X) :
    ∃ g : nerve P ⟶ X, Nonempty (SSet.Homotopy (lastVertex.app (nerve P) ≫ g) f) ∧
      (realizationWeakEquivalences g ↔ realizationWeakEquivalences f) := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.subdivision_unit_extension_lastVertex line 520

theorem OAI.Thomason.Construction.exists_subdivision_descent_over_kan line 527

Source documentation

A map on a subdivided parameter descends over the same base map. The two anodyne premises hold for the finite poset parameters used below.

theorem exists_subdivision_descent_over_kan {K E B : SSet.{0}}
    [SSet.KanComplex B] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (hK : SSet.anodyneExtensions (canonicalExtension.app K))
    (hSd : SSet.anodyneExtensions (canonicalExtension.app (SSet.sd.obj K)))
    (a : SSet.sd.obj K ⟶ E) (b : K ⟶ B)
    (hab : a ≫ p = lastVertex.app K ≫ b) :
    ∃ g : K ⟶ E, g ≫ p = b ∧
      Nonempty (SSet.Homotopy (lastVertex.app K ≫ g) a) := by
…

theorem OAI.Thomason.Construction.exists_finitePoset_subdivision_descent_over_kan line 563

Source documentation

Concrete relative descent for every finite poset, with no additional published input.

theorem exists_finitePoset_subdivision_descent_over_kan
    (P : Type) [PartialOrder P] [Finite P] {E B : SSet.{0}}
    [SSet.KanComplex B] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (a : SSet.sd.obj (nerve P) ⟶ E) (b : nerve P ⟶ B)
    (hab : a ≫ p = lastVertex.app (nerve P) ≫ b) :
    ∃ g : nerve P ⟶ E, g ≫ p = b ∧
      Nonempty (SSet.Homotopy (lastVertex.app (nerve P) ≫ g) a) :=
…

def OAI.Thomason.Construction.NerveSubdivisionMap.faceEmbedding line 595
theorem OAI.Thomason.Construction.NerveSubdivisionMap.faceEmbedding_range line 605
theorem OAI.Thomason.Construction.NerveSubdivisionMap.map_surjective line 617
Source documentation
Every simplex of the chain nerve lifts through one actual standard subdivision simplex.
```
theorem map_surjective (P : Type) [PartialOrder P] (d : SimplexCategoryᵒᵖ) :
    Function.Surjective ((map P).app d) := by
…
```
Mentions: OAI.Thomason.Construction.NerveSubdivisionMap.map
theorem OAI.Thomason.Construction.NerveSubdivisionMap.map_epi line 654
theorem OAI.Thomason.Construction.NerveSubdivisionMap.map_mono line 660
Source documentation
A finite linear extension reduces monicity to the standard simplex.
```
theorem map_mono (P : Type) [PartialOrder P] [Finite P] : Mono (map P) := by
…
```
Mentions: OAI.Thomason.Construction.NerveSubdivisionMap.map
def OAI.Thomason.Construction.NerveSubdivisionMap.iso line 714
def OAI.Thomason.Construction.iteratedChainPoset line 745
instance OAI.Thomason.Construction.iteratedChainPoset_finite line 749
def OAI.Thomason.Construction.iteratedSubdivisionNerveIso line 757
theorem OAI.Thomason.Construction.iteratedSubdivision_canonical_anodyne line 766
Source documentation
Every iterated finite parameter has the exact canonical-extension lifting property, rather than just a realization weak equivalence.
```
theorem iteratedSubdivision_canonical_anodyne (P : PartOrd.{0}) [Finite P] (r : ℕ) :
    SSet.anodyneExtensions (canonicalExtension.app ((iteratedSubdivision r).obj (nerve P))) :=
…
```
Mentions: OAI.Thomason.Construction.iteratedSubdivision
def OAI.Thomason.Construction.iteratedLastVertex line 771
theorem OAI.Thomason.Construction.iteratedLastVertex_weak line 775

theorem OAI.Thomason.Construction.exists_iteratedSubdivision_step_descent line 784

Source documentation

A map out of the next actual subdivision descends into the same Kan target with an actual simplicial comparison and unchanged weak test.

theorem exists_iteratedSubdivision_step_descent (P : PartOrd.{0}) [Finite P]
    (r : ℕ) (X : SSet.{0}) [SSet.KanComplex X]
    (f : (iteratedSubdivision (r+1)).obj (nerve P) ⟶ X) :
    ∃ g : (iteratedSubdivision r).obj (nerve P) ⟶ X,
      Nonempty (SSet.Homotopy (lastVertex.app ((iteratedSubdivision r).obj (nerve P)) ≫ g) f) ∧
        (realizationWeakEquivalences g ↔ realizationWeakEquivalences f) := by
…

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

def OAI.Thomason.Construction.ChainCardBound line 815
theorem OAI.Thomason.Construction.chainCardBound_chains line 818
theorem OAI.Thomason.Construction.iteratedChainPoset_cardBound line 843
theorem OAI.Thomason.Construction.simplex_dimension_le_chainCardBound line 849
theorem OAI.Thomason.Construction.iteratedChainPoset_dimension_le line 868
Source documentation
Every finite starting poset gives one bound valid at every stage.
```
theorem iteratedChainPoset_dimension_le (P : PartOrd.{0}) [Fintype P]
    (r m : ℕ) (s : Fin (m+1) ⥤ iteratedChainPoset P r) (hs : StrictMono s.obj) :
    m ≤ Fintype.card P := by
…
```
Mentions: OAI.Thomason.Construction.iteratedChainPoset
theorem OAI.Thomason.Construction.subdivision_weak_mono line 895
Source documentation
Weak monomorphisms remain weak monomorphisms under actual subdivision.
```
theorem subdivision_weak_mono {K L : SSet.{0}} (f : K ⟶ L) [Mono f]
    (hf : realizationWeakEquivalences f) :
    Mono (SSet.sd.map f) ∧ realizationWeakEquivalences (SSet.sd.map f) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.subdivision_weak_mono_deformation line 902

Source documentation

Subdividing a weak mono retains an exact stationary deformation on its entire realized image.

theorem subdivision_weak_mono_deformation {K L : SSet.{0}} (f : K ⟶ L) [Mono f]
    (hf : realizationWeakEquivalences f) :
    ∃ r : SSet.toTop.obj (SSet.sd.obj L) ⟶ SSet.toTop.obj (SSet.sd.obj K),
      SSet.toTop.map (SSet.sd.map f) ≫ r = 𝟙 _ ∧
      Nonempty ((r ≫ SSet.toTop.map (SSet.sd.map f)).hom.HomotopyRel
        (ContinuousMap.id _) (Set.range (SSet.toTop.map (SSet.sd.map f)).hom)) := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.extension_boundary_weak line 913
Source documentation
Extension preserves boundary lifting and consequently its actual weak equivalence, without requiring the open general acyclic-Kan implication.
```
theorem extension_boundary_weak {K L : SSet.{0}} (p : K ⟶ L) (hp : I.rlp p) :
    I.rlp (SSet.ex.map p) ∧ realizationWeakEquivalences (SSet.ex.map p) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.extension_twice_boundary_weak line 919
Source documentation
The same precise consequence for the double extension in the Thomason fibration functor.
```
theorem extension_twice_boundary_weak {K L : SSet.{0}} (p : K ⟶ L) (hp : I.rlp p) :
    I.rlp ((SSet.ex ⋙ SSet.ex).map p) ∧
      realizationWeakEquivalences ((SSet.ex ⋙ SSet.ex).map p) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.extension_twice_singular_acyclic line 926

Source documentation

The proved singular acyclic case remains a boundary-lifting weak map after the actual double extension.

theorem extension_twice_singular_acyclic {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) :
    I.rlp ((SSet.ex ⋙ SSet.ex).map (TopCat.toSSet.map p)) ∧
      realizationWeakEquivalences ((SSet.ex ⋙ SSet.ex).map (TopCat.toSSet.map p)) :=
…

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

theorem OAI.Thomason.Construction.street_subdivision_twice_weak_iff line 935
Source documentation
Double subdivision detects exactly the implemented omega-Street weak equivalences. No Gray or Kan–Quillen assumption appears.
```
theorem street_subdivision_twice_weak_iff (h : NormalizedSimplexIdentities)
    {C D : StrictOmegaCategory} (f : C ⟶ D) :
    realizationWeakEquivalences ((SSet.sd ⋙ SSet.sd).map (h.streetNerve.map f)) ↔
      h.streetWeakEquivalences f :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictOmegaCategory, OAI.Thomason.Construction.realizationWeakEquivalences