FiniteSingularRelativeLifting.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

The subdivision-homotopy reduction for the canonical extension

An explicit homotopy between the two last-vertex maps on double subdivision implies the full canonical-extension weak-equivalence theorem through the adjunction identities and the two-out-of-six argument.

def OAI.Thomason.Construction.subdivisionAdjunctHomotopy line 33

Source documentation

The mates of a simplicial homotopy are simplicially homotopic.

def subdivisionAdjunctHomotopy {A B : SSet.{0}} {f g : SSet.sd.obj A ⟶ B}
    (H : SSet.Homotopy f g) :
    SSet.Homotopy (SSet.sdExAdjunction.homEquiv A B f)
      (SSet.sdExAdjunction.homEquiv A B g) where
…

def OAI.Thomason.Construction.postcomposeSimplicialHomotopy line 55
theorem OAI.Thomason.Construction.canonicalExtension_adjunct line 71
theorem OAI.Thomason.Construction.canonicalExtension_counit line 81

def OAI.Thomason.Construction.canonicalExtensionCounitHomotopy line 89

Source documentation

A double-subdivision homotopy gives the precise counit composite needed by the weak-equivalence argument.

def canonicalExtensionCounitHomotopy (X : SSet.{0})
    (H : SSet.Homotopy (SSet.sd.map (lastVertex.app (SSet.ex.obj X)))
      (lastVertex.app (SSet.sd.obj (SSet.ex.obj X)))) :
    SSet.Homotopy (lastVertex.app (SSet.ex.obj X))
      (SSet.sdExAdjunction.counit.app X ≫ canonicalExtension.app X) := by
…

theorem OAI.Thomason.Construction.canonicalExtension_weak_of_subdivision_homotopy line 120
Source documentation
Once the explicit subdivision homotopy has been constructed, the general canonical-extension theorem follows without an approximation assumption or a Kan--Quillen model structure.
```
theorem canonicalExtension_weak_of_subdivision_homotopy
    (H : ∀ K : SSet.{0}, SSet.Homotopy (SSet.sd.map (lastVertex.app K))
      (lastVertex.app (SSet.sd.obj K))) (X : SSet.{0}) :
    realizationWeakEquivalences (canonicalExtension.app X) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.finite_nonemptyFiniteChains line 152
theorem OAI.Thomason.Construction.subdivision_standard_finite line 159
Source documentation
Subdividing a standard simplex still has only finitely many nondegenerate simplices, not merely finite sets in each degree.
```
theorem subdivision_standard_finite (n : SimplexCategory) :
    (SSet.sd.obj (SSet.stdSimplex.{0}.obj n)).Finite := by
…
```
def OAI.Thomason.Construction.nondegenerateSimplexFamily line 166
def OAI.Thomason.Construction.nondegenerateSimplexCover line 168
theorem OAI.Thomason.Construction.nondegenerateSimplexCover_epi line 174
Source documentation
The finite-dimensional generators cover every simplex, including the original degenerate simplices.
```
theorem nondegenerateSimplexCover_epi (K : SSet.{0}) : Epi (nondegenerateSimplexCover K) := by
…
```
Mentions: OAI.Thomason.Construction.nondegenerateSimplexCover
theorem OAI.Thomason.Construction.subdivision_finite line 191
Source documentation
Actual subdivision preserves finite simplicial sets.
```
theorem subdivision_finite (K : SSet.{0}) [K.Finite] : (SSet.sd.obj K).Finite := by
…
```
theorem OAI.Thomason.Construction.subdivision_twice_finite line 202
Source documentation
The double subdivision used in the Thomason left adjoint also preserves finite carrier data.
```
theorem subdivision_twice_finite (K : SSet.{0}) [K.Finite] :
    ((SSet.sd ⋙ SSet.sd).obj K).Finite := by
…
```

theorem OAI.Thomason.Construction.finite_map_extension_factors line 230

Source documentation

A finite simplicial family in Ex K comes from Ex A for an actual finite subcomplex A of K. The factorization is an equality of maps.

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

theorem OAI.Thomason.Construction.compact_map_extension_factors line 247

Source documentation

Every compact family of points of |Ex K| is supported over the extension of one finite subcomplex of K.

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

def OAI.Thomason.Construction.subdividedSimplexCover line 281
theorem OAI.Thomason.Construction.subdividedSimplexCover_epi line 286
theorem OAI.Thomason.Construction.subdividedSimplexCover_ι line 291

theorem OAI.Thomason.Construction.subdivision_simplex_finite_support line 302

Source documentation

Every simplex of a subdivision is already in the subdivided image of a single finite simplex carrier of the original simplicial set.

theorem subdivision_simplex_finite_support (K : SSet.{0})
    (d : SimplexCategoryᵒᵖ) (x : (SSet.sd.obj K).obj d) :
    ∃ A : K.Subcomplex, SSet.Finite A.toSSet ∧
      x ∈ (SSet.Subcomplex.range (SSet.sd.map A.ι)).obj d := by
…

theorem OAI.Thomason.Construction.finite_map_subdivision_factors line 330

Source documentation

A map with finite source into Sd K factors through Sd A for an actual finite subcomplex A of K. The factorization is exactly simplicial.

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

theorem OAI.Thomason.Construction.finite_simplicial_maps line 385
Source documentation
A simplicial map is determined by its values on the finitely many nondegenerate source simplices.
```
theorem finite_simplicial_maps (X Y : SSet.{0}) [X.Finite] [Y.Finite] : Finite (X ⟶ Y) := by
…
```

theorem OAI.Thomason.Construction.finite_boundary_lifting_stage line 421

Source documentation

When boundary lifting has been proved for a map, all lifting problems of bounded dimension between two finite supports have solutions inside one finite enlargement of the source. All simplices remain in the original map. The hypothesis is used for the already proved singular cases.

theorem finite_boundary_lifting_stage {E B : SSet.{0}} (p : E ⟶ B) (hp : I.rlp p)
    (S : E.Subcomplex) [S.toSSet.Finite] (T : B.Subcomplex) [T.toSSet.Finite] (d : ℕ) :
    ∃ (U : E.Subcomplex) (_ : SSet.Finite U.toSSet) (hSU : S ≤ U),
      U ≤ S ⊔ T.preimage p ∧ ∀ (n : ℕ) (_ : n ≤ d)
        (a : (SSet.boundary n : SSet.{0}) ⟶ S.toSSet)
        (b : (Δ[n] : SSet.{0}) ⟶ T.toSSet)
        (_ : a ≫ S.ι ≫ p = (SSet.boundary n).ι ≫ b ≫ T.ι),
        ∃ l : (Δ[n] : SSet.{0}) ⟶ U.toSSet,
          (SSet.boundary n).ι ≫ l = a ≫ SSet.Subcomplex.homOfLE hSU ∧
          l ≫ U.ι ≫ p = b ≫ T.ι := by
…

theorem OAI.Thomason.Construction.finite_map_iSup_factors line 505

Source documentation

Every map from a finite simplicial set into an increasing union is already an exact simplicial map into one stage.

theorem finite_map_iSup_factors {A E : SSet.{0}} [A.Finite]
    (U : ℕ → E.Subcomplex) (hU : Monotone U) (f : A ⟶ (iSup U).toSSet) :
    ∃ (n : ℕ) (g : A ⟶ (U n).toSSet),
      g ≫ (U n).ι = f ≫ (iSup U).ι := by
…

structure OAI.Thomason.Construction.BoundarySupport line 548
instance OAI.Thomason.Construction.(instance at line 553) line 553
structure OAI.Thomason.Construction.BoundaryEnlargement line 556
def OAI.Thomason.Construction.boundaryEnlarge line 568
def OAI.Thomason.Construction.boundarySupportChain line 575
theorem OAI.Thomason.Construction.boundarySupportChain_mono line 579

theorem OAI.Thomason.Construction.exists_finite_exhausted_boundary_subfibration line 589

Source documentation

Every finite subcomplex over a finite base support lies in a genuine boundary-lifting subfibration of the original map, exhausted by an increasing sequence of finite subcomplexes. No new simplices outside the original map are added.

theorem exists_finite_exhausted_boundary_subfibration {E B : SSet.{0}} (p : E ⟶ B)
    (hp : I.rlp p) (T : B.Subcomplex) [T.toSSet.Finite]
    (S : E.Subcomplex) [S.toSSet.Finite] (hS : S ≤ T.preimage p) :
    ∃ (U : E.Subcomplex) (q : U.toSSet ⟶ T.toSSet),
      S ≤ U ∧ U ≤ T.preimage p ∧ q ≫ T.ι = U.ι ≫ p ∧
      I.rlp q ∧ realizationWeakEquivalences q ∧
      ∃ c : ℕ → E.Subcomplex, Monotone c ∧
        (∀ n, SSet.Finite (c n).toSSet) ∧ c 0 = S ∧ iSup c = U := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.finite_kan_horn_stage line 668

Source documentation

From finite source and base supports, a single finite enlargement contains every Kan horn filler needed up to the specified dimension. The new simplices are actual simplices of the original total space.

theorem finite_kan_horn_stage {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (S : E.Subcomplex) [S.toSSet.Finite]
    (T : B.Subcomplex) [T.toSSet.Finite] (d : ℕ) :
    ∃ (U : E.Subcomplex) (_ : SSet.Finite U.toSSet) (hSU : S ≤ U),
      U ≤ S ⊔ T.preimage p ∧ ∀ (n : ℕ) (_ : n ≤ d) (i : Fin (n+2))
        (a : (Λ[n+1, i] : SSet.{0}) ⟶ S.toSSet)
        (b : (Δ[n+1] : SSet.{0}) ⟶ T.toSSet)
        (_ : a ≫ S.ι ≫ p = Λ[n+1, i].ι ≫ b ≫ T.ι),
        ∃ l : (Δ[n+1] : SSet.{0}) ⟶ U.toSSet,
          Λ[n+1, i].ι ≫ l = a ≫ SSet.Subcomplex.homOfLE hSU ∧
          l ≫ U.ι ≫ p = b ≫ T.ι := by
…

structure OAI.Thomason.Construction.KanSupport line 754
instance OAI.Thomason.Construction.(instance at line 759) line 759
structure OAI.Thomason.Construction.KanEnlargement line 762
def OAI.Thomason.Construction.kanEnlarge line 774
def OAI.Thomason.Construction.kanSupportChain line 781
theorem OAI.Thomason.Construction.kanSupportChain_mono line 785

theorem OAI.Thomason.Construction.exists_finite_exhausted_kan_subfibration line 795

Source documentation

Every finite subcomplex over a finite base support lies in a genuine Kan subfibration of the original map, exhausted by an increasing sequence of finite subcomplexes. No new simplices outside the original map are added.

theorem exists_finite_exhausted_kan_subfibration {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (T : B.Subcomplex) [T.toSSet.Finite]
    (S : E.Subcomplex) [S.toSSet.Finite] (hS : S ≤ T.preimage p) :
    ∃ (U : E.Subcomplex) (q : U.toSSet ⟶ T.toSSet),
      S ≤ U ∧ U ≤ T.preimage p ∧ q ≫ T.ι = U.ι ≫ p ∧
      HomotopicalAlgebra.Fibration q ∧
      ∃ c : ℕ → E.Subcomplex, Monotone c ∧
        (∀ n, SSet.Finite (c n).toSSet) ∧ c 0 = S ∧ iSup c = U := by
…

theorem OAI.Thomason.Construction.compact_homotopyFiber_kan_support line 876

Source documentation

Compact homotopy-fibre data for a Kan fibration lie in an actual Kan subfibration over a finite base. Its total space is an increasing union of finite subcomplexes of the original total space. The entire family retains its original point and path coordinates.

theorem compact_homotopyFiber_kan_support {K : Type} [TopologicalSpace K] [CompactSpace K]
    {E B : SSet.{0}} (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (b : B.obj (.op (.mk 0)))
    (f : C(K, continuousHomotopyFiber (SSet.toTop.map p) (RealizationPrism.vertexPoint B b))) :
    ∃ (A : B.Subcomplex) (_ : SSet.Finite A.toSSet) (U : E.Subcomplex)
      (u : U.toSSet ⟶ A.toSSet) (_ : HomotopicalAlgebra.Fibration u)
      (bA : A.toSSet.obj (.op (.mk 0))),
      u ≫ A.ι = U.ι ≫ p ∧ bA.val = b ∧
      (∃ c : ℕ → E.Subcomplex, Monotone c ∧
        (∀ n, SSet.Finite (c n).toSSet) ∧ iSup c = U) ∧
      ∃ g : C(K, continuousHomotopyFiber (SSet.toTop.map u)
          (RealizationPrism.vertexPoint A.toSSet bA)),
…

Mentions: OAI.Thomason.Construction.continuousHomotopyFiber, OAI.Thomason.Construction.RealizationPrism.vertexPoint

theorem OAI.Thomason.Construction.finite_singular_boundary_hull line 942

Source documentation

Finite singular data over a finite base support is contained in an actual boundary-lifting subfibration, exhausted by finite subcomplexes. The boundary-lifting hypothesis is discharged here by the proved singular acyclic theorem; no general simplicial acyclic implication is assumed.

theorem finite_singular_boundary_hull {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom)
    (T : (TopCat.toSSet.obj Y).Subcomplex) [T.toSSet.Finite]
    (S : (TopCat.toSSet.obj X).Subcomplex) [S.toSSet.Finite]
    (hS : S ≤ T.preimage (TopCat.toSSet.map p)) :
    ∃ (U : (TopCat.toSSet.obj X).Subcomplex) (q : U.toSSet ⟶ T.toSSet),
      S ≤ U ∧ U ≤ T.preimage (TopCat.toSSet.map p) ∧
      q ≫ T.ι = U.ι ≫ TopCat.toSSet.map p ∧
      I.rlp q ∧ realizationWeakEquivalences q ∧
      ∃ c : ℕ → (TopCat.toSSet.obj X).Subcomplex, Monotone c ∧
        (∀ n, SSet.Finite (c n).toSSet) ∧ c 0 = S ∧ iSup c = U :=
…

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

theorem OAI.Thomason.Construction.finite_singular_acyclic_relative_lift line 978

Source documentation

A finite relative problem for an actual acyclic singular fibration has an exact simplicial solution inside a finite-exhausted acyclic subfibration over one finite base. Both original maps and the entire lifting square are retained exactly.

theorem finite_singular_acyclic_relative_lift {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom)
    {A K : SSet.{0}} [K.Finite] (i : A ⟶ K) [Mono i]
    (a : A ⟶ TopCat.toSSet.obj X) (b : K ⟶ TopCat.toSSet.obj Y)
    (h : a ≫ TopCat.toSSet.map p = i ≫ b) :
    ∃ (T : (TopCat.toSSet.obj Y).Subcomplex) (_ : SSet.Finite T.toSSet)
      (U : (TopCat.toSSet.obj X).Subcomplex) (q : U.toSSet ⟶ T.toSSet),
      I.rlp q ∧ realizationWeakEquivalences q ∧
      ∃ (aU : A ⟶ U.toSSet) (bT : K ⟶ T.toSSet) (l : K ⟶ U.toSSet),
        q ≫ T.ι = U.ι ≫ TopCat.toSSet.map p ∧ aU ≫ U.ι = a ∧ bT ≫ T.ι = b ∧
        i ≫ l = aU ∧ l ≫ q = bT ∧
…

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