SingularCounitSurjectivity.lean`

56 declarations, 0 contain sorry, 0 declared as axioms

Cellular closure of actual realization deformations

def OAI.Thomason.Construction.realizationDeformations line 30
Source documentation
Maps whose actual realizations admit a stationary deformation retraction.
```
def realizationDeformations : MorphismProperty SSet.{0} :=
…
```
theorem OAI.Thomason.Construction.realizationDeformations_weak line 33
theorem OAI.Thomason.Construction.realizationDeformations_coproducts line 39
Source documentation
Realized stationary deformations are closed under arbitrary small coproducts.
```
theorem realizationDeformations_coproducts :
    coproducts.{0} realizationDeformations ≤ realizationDeformations := by
…
```
Mentions: OAI.Thomason.Construction.realizationDeformations
theorem OAI.Thomason.Construction.realizationDeformations_pushouts line 61
Source documentation
Realized stationary deformations extend over every simplicial pushout.
```
theorem realizationDeformations_pushouts :
    realizationDeformations.pushouts ≤ realizationDeformations := by
…
```
Mentions: OAI.Thomason.Construction.realizationDeformations
def OAI.Thomason.Construction.realizedSequenceData line 68
Source documentation
A countable simplicial sequence of realized deformations has a realized stationary deformation on its actual colimit inclusion.
```
def realizedSequenceData {F : ℕ ⥤ SSet.{0}} {c : Cocone F} (hc : IsColimit c)
    (d : ∀ n, TopologicalDeformation.Data
      (SSet.toTop.map (F.map (homOfLE (Nat.le_succ n))))) :
    TopologicalDeformation.Data (SSet.toTop.map (c.ι.app 0)) :=
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data
theorem OAI.Thomason.Construction.realizationDeformations_countable line 75
Source documentation
The precise countable closure used by the horn small-object argument.
```
theorem realizationDeformations_countable :
    realizationDeformations.transfiniteCompositionsOfShape ℕ ≤ realizationDeformations := by
…
```
Mentions: OAI.Thomason.Construction.realizationDeformations
theorem OAI.Thomason.Construction.horn_generators_deformations line 112
Source documentation
Every generating horn has a stationary deformation after realization.
```
theorem horn_generators_deformations : J.{0} ≤ realizationDeformations := by
…
```
Mentions: OAI.Thomason.Construction.realizationDeformations
theorem OAI.Thomason.Construction.horn_cell_stages_deformations line 119
Source documentation
All stages in the countable horn construction admit actual deformations.
```
theorem horn_cell_stages_deformations :
    (coproducts.{0} J.{0}).pushouts ≤ realizationDeformations :=
…
```
Mentions: OAI.Thomason.Construction.realizationDeformations
theorem OAI.Thomason.Construction.horn_cell_complexes_weak line 126
Source documentation
Every countable horn-cell complex is weak for actual geometric realization.
```
theorem horn_cell_complexes_weak :
    (coproducts.{0} J.{0}).pushouts.transfiniteCompositionsOfShape ℕ ≤
      realizationWeakEquivalences :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.anodyne_realization_weak line 133
Source documentation
The semantic half of the anodyne characterization, proved without any KQ input.
```
theorem anodyne_realization_weak : SSet.anodyneExtensions.{0} ≤ realizationWeakEquivalences := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.anodyne_mono_realization_weak line 140
Source documentation
Anodyne extensions satisfy both parts of the intended trivial-cofibration class.
```
theorem anodyne_mono_realization_weak :
    SSet.anodyneExtensions.{0} ≤ monomorphisms SSet.{0} ⊓ realizationWeakEquivalences := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
instance OAI.Thomason.Construction.(instance at line 163) line 163
theorem OAI.Thomason.Construction.anodyne_realization_deformations line 167
Source documentation
The complete cellular construction gives a deformation, including the final arrow retract.
```
theorem anodyne_realization_deformations : SSet.anodyneExtensions.{0} ≤ realizationDeformations := by
…
```
Mentions: OAI.Thomason.Construction.realizationDeformations
def OAI.Thomason.Construction.anodyneRealizationData line 174
Source documentation
A chosen actual stationary deformation for any anodyne extension.
```
def anodyneRealizationData {A B : SSet.{0}} (f : A ⟶ B) (hf : SSet.anodyneExtensions f) :
    TopologicalDeformation.Data (SSet.toTop.map f) :=
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data

def OAI.Thomason.Construction.singularAnodyneExtension line 179

Source documentation

Every singular map on an anodyne subobject extends by the constructed retraction.

def singularAnodyneExtension {A B : SSet.{0}} (f : A ⟶ B)
    (hf : SSet.anodyneExtensions f) (X : TopCat.{0}) (a : A ⟶ TopCat.toSSet.obj X) :
    B ⟶ TopCat.toSSet.obj X :=
…

theorem OAI.Thomason.Construction.singularAnodyneExtension_fac line 186
theorem OAI.Thomason.Construction.singular_realized_anodyne_weak line 194
Source documentation
Singularization preserves the weak status of these actual geometric inclusions.
```
theorem singular_realized_anodyne_weak {A B : SSet.{0}} (f : A ⟶ B)
    (hf : SSet.anodyneExtensions f) :
    realizationWeakEquivalences (TopCat.toSSet.map (SSet.toTop.map f)) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.kan_fiber_deformation_reverse line 220

Source documentation

Lift a reverse contraction of the base to a stationary deformation onto the actual point fibre. The stationarity premise is the exact cylinder equality on that fibre, not a weak-equivalence or lifting assumption.

theorem kan_fiber_deformation_reverse {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (b : B _⦋0⦌)
    (H : SSet.Homotopy (SSet.const b) (𝟙 B))
    (hs : ((simplicialPointFiber p b).ι ≫ p) ▷ Δ[1] ≫ H.h =
      fst (simplicialPointFiber p b).toSSet Δ[1] ≫ (simplicialPointFiber p b).ι ≫ p) :
    ∃ r : E ⟶ (simplicialPointFiber p b).toSSet,
      (simplicialPointFiber p b).ι ≫ r = 𝟙 _ ∧
      ∃ T : SSet.Homotopy (r ≫ (simplicialPointFiber p b).ι) (𝟙 E),
        (simplicialPointFiber p b).ι ▷ Δ[1] ≫ T.h =
          fst (simplicialPointFiber p b).toSSet Δ[1] ≫ (simplicialPointFiber p b).ι ∧
        T.h ≫ p = p ▷ Δ[1] ≫ H.h := by
…

Mentions: OAI.Thomason.Construction.simplicialPointFiber

theorem OAI.Thomason.Construction.simplicial_retraction_weak_of_zigzag line 309
Source documentation
Two simplicial homotopies through a common map suffice for an actual homotopy inverse after realization.
```
theorem simplicial_retraction_weak_of_zigzag {A E : SSet.{0}}
    (i : A ⟶ E) (r : E ⟶ A) (f : E ⟶ E) (hir : i ≫ r = 𝟙 A)
    (H₀ : SSet.Homotopy f (𝟙 E)) (H₁ : SSet.Homotopy f (r ≫ i)) :
    realizationWeakEquivalences i := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.kan_fiber_weak_of_zigzag line 335
Source documentation
A stationary zigzag from the identity of the base to a constant lifts relative to the entire point fibre. This includes contractions to interior vertices, for which no single directed simplicial homotopy exists.
```
theorem kan_fiber_weak_of_zigzag {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (b : B _⦋0⦌) (D : B ⟶ B)
    (H₀ : SSet.Homotopy D (𝟙 B)) (H₁ : SSet.Homotopy D (SSet.const b))
    (hs₀ : ∀ K : SSet.{0}, (SSet.const (X := K) b) ▷ Δ[1] ≫ H₀.h =
…
```

theorem OAI.Thomason.Construction.singular_unit_anodyne_iff line 458

Source documentation

The genuine singular-unit weak test is invariant under anodyne extension.

theorem singular_unit_anodyne_iff {A B : SSet.{0}} (f : A ⟶ B)
    (hf : SSet.anodyneExtensions f) :
    realizationWeakEquivalences (sSetTopAdj.unit.app A) ↔
      realizationWeakEquivalences (sSetTopAdj.unit.app B) := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

def OAI.Thomason.Construction.kanReplacementFactorization line 477
Source documentation
The actual horn factorization of the map to the terminal simplicial set.
```
def kanReplacementFactorization (K : SSet.{0}) :
    MapFactorizationData SSet.anodyneExtensions J.rlp (terminal.from K) := by
…
```
theorem OAI.Thomason.Construction.kanReplacement_kan line 483
Source documentation
The object produced by that factorization is Kan.
```
theorem kanReplacement_kan (K : SSet.{0}) :
    SSet.KanComplex (kanReplacementFactorization K).Z := by
…
```
Mentions: OAI.Thomason.Construction.kanReplacementFactorization
theorem OAI.Thomason.Construction.singular_unit_kan_replacement_iff line 494
Source documentation
The singular-unit comparison on any simplicial set is exactly its test on the constructed Kan replacement.
```
theorem singular_unit_kan_replacement_iff (K : SSet.{0}) :
    realizationWeakEquivalences (sSetTopAdj.unit.app K) ↔
      realizationWeakEquivalences (sSetTopAdj.unit.app (kanReplacementFactorization K).Z) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.kanReplacementFactorization

theorem OAI.Thomason.Construction.singular_unit_weak_of_kan_cases line 500

Source documentation

It suffices to prove the unit weak theorem on actual Kan complexes.

theorem singular_unit_weak_of_kan_cases
    (h : ∀ K : SSet.{0}, SSet.KanComplex K →
      realizationWeakEquivalences (sSetTopAdj.unit.app K)) (K : SSet.{0}) :
    realizationWeakEquivalences (sSetTopAdj.unit.app K) :=
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

def OAI.Thomason.Construction.singularVertex line 524
Source documentation
A point of a space gives the corresponding vertex in its singular realization.
```
def singularVertex (X : TopCat.{0}) (x : X) : SSet.toTop.obj (TopCat.toSSet.obj X) :=
…
```
theorem OAI.Thomason.Construction.singularVertex_map_counit line 529
Source documentation
Adjunction identifies a constant singular vertex with the actual constant map.
```
theorem singularVertex_map_counit (X : TopCat.{0}) (x : X) :
    SSet.toTop.map (SSet.const (X := (Δ[0] : SSet.{0}))
…
```
theorem OAI.Thomason.Construction.counit_singularVertex line 540
Source documentation
Evaluation sends the canonical singular vertex back to its original point.
```
theorem counit_singularVertex (X : TopCat.{0}) (x : X) :
    (sSetTopAdj.counit.app X).hom (singularVertex X x) = x :=
…
```
Mentions: OAI.Thomason.Construction.singularVertex
theorem OAI.Thomason.Construction.singular_counit_surjective line 545
Source documentation
The actual evaluation counit is surjective, before taking components.
```
theorem singular_counit_surjective (X : TopCat.{0}) :
    Function.Surjective (sSetTopAdj.counit.app X).hom :=
…
```
theorem OAI.Thomason.Construction.singular_counit_components_surjective line 550
Source documentation
In particular the actual counit is surjective on path components.
```
theorem singular_counit_components_surjective (X : TopCat.{0}) :
    Function.Surjective (HomotopyMaps.componentsMap (sSetTopAdj.counit.app X).hom) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.CubicalLifting.groupMap_injective line 580
Source documentation
All based homotopy groups, including degree zero, are injective under the cubical boundary lifting hypothesis.
```
theorem groupMap_injective (n : ℕ) (x : X) :
    Function.Injective (HomotopyMaps.groupMap f.hom n x) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap
def OAI.Thomason.Construction.CubicalLifting.liftLoop line 592
Source documentation
A positive-dimensional based loop lifts with every boundary value fixed.
```
def liftLoop {x : X} (n : ℕ) (p : GenLoop (Fin (n+1)) Y (f.hom x)) :
    GenLoop (Fin (n+1)) X x := by
…
```
theorem OAI.Thomason.Construction.CubicalLifting.liftLoop_comp line 606
theorem OAI.Thomason.Construction.CubicalLifting.groupMap_surjective line 618
theorem OAI.Thomason.Construction.CubicalLifting.componentsMap_injective line 629
theorem OAI.Thomason.Construction.CubicalLifting.surjective_of_barycentric line 658
Source documentation
Barycentric boundary lifting also forces surjectivity on actual points. Only the singular adjunction and its explicit evaluation map are used.
```
theorem surjective_of_barycentric
    (hp : ∀ n, HasLiftingProperty (RealizationPrism.boundaryInclusion n) f) :
    Function.Surjective f.hom := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion
theorem OAI.Thomason.Construction.CubicalLifting.weak_of_barycentric line 677
Source documentation
The elementary topological lifting test gives the actual bijections on components and on every positive homotopy group, independently of the remaining singular comparison and Kan--Quillen hypotheses.
```
theorem weak_of_barycentric
    (hp : ∀ n, HasLiftingProperty (RealizationPrism.boundaryInclusion n) f) :
    IsWeakHomotopyEquivalence f.hom := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion, OAI.Thomason.Construction.IsWeakHomotopyEquivalence
theorem OAI.Thomason.Construction.singularVertex_naturality line 707
Source documentation
The canonical point of the singular realization is natural on continuous maps.
```
theorem singularVertex_naturality {X Y : TopCat.{0}} (f : X ⟶ Y) (x : X) :
    (SSet.toTop.map (TopCat.toSSet.map f)).hom (singularVertex X x) =
      singularVertex Y (f.hom x) := by
…
```
Mentions: OAI.Thomason.Construction.singularVertex
def OAI.Thomason.Construction.singularVertexPath line 720
Source documentation
Every actual path gives a path between the corresponding singular vertices.
```
def singularVertexPath {X : TopCat.{0}} {x y : X} (p : Path x y) :
    Path (singularVertex X x) (singularVertex X y) := by
…
```
Mentions: OAI.Thomason.Construction.singularVertex

theorem OAI.Thomason.Construction.singular_zero_simplex_eq_vertex line 739

Source documentation

A singular zero-simplex is exactly the canonical vertex of its evaluated point.

theorem singular_zero_simplex_eq_vertex (X : TopCat.{0})
    (a : (Δ[0] : SSet.{0}) ⟶ TopCat.toSSet.obj X)
    (z : SSet.toTop.obj (Δ[0] : SSet.{0})) :
    (SSet.toTop.map a).hom z =
      singularVertex X ((sSetTopAdj.counit.app X).hom ((SSet.toTop.map a).hom z)) := by
…

Mentions: OAI.Thomason.Construction.singularVertex

theorem OAI.Thomason.Construction.singular_point_joined_vertex line 772
Source documentation
Every point of the singular realization is connected to the vertex of its evaluation.
```
theorem singular_point_joined_vertex (X : TopCat.{0})
    (x : SSet.toTop.obj (TopCat.toSSet.obj X)) :
    Joined x (singularVertex X ((sSetTopAdj.counit.app X).hom x)) := by
…
```
Mentions: OAI.Thomason.Construction.singularVertex
theorem OAI.Thomason.Construction.singular_counit_components_bijective line 799
Source documentation
The path-component part of the genuine singular counit weak-equivalence test.
```
theorem singular_counit_components_bijective (X : TopCat.{0}) :
    Function.Bijective (HomotopyMaps.componentsMap (sSetTopAdj.counit.app X).hom) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.singular_map_components_bijective_iff line 832
Source documentation
Singular realization induces the same bijectivity test on path components as the original continuous map, using the proved counit component isomorphisms.
```
theorem singular_map_components_bijective_iff {X Y : TopCat.{0}} (p : X ⟶ Y) :
    Function.Bijective (HomotopyMaps.componentsMap
      (SSet.toTop.map (TopCat.toSSet.map p)).hom) ↔
      Function.Bijective (HomotopyMaps.componentsMap p.hom) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.singular_acyclic_surjective line 847
Source documentation
The zero-dimensional part of an actual singular weak equivalence suffices for strict point surjectivity when the singular map is also Kan.
```
theorem singular_acyclic_surjective {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) :
    Function.Surjective p.hom :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.singular_boundary_zero_lifting_of_surjective line 856
Source documentation
For a surjective continuous map, singularization lifts the degree-zero boundary. This proves the zero-dimensional lifting statement explicitly.
```
theorem singular_boundary_zero_lifting_of_surjective {X Y : TopCat.{0}}
    (p : X ⟶ Y) (hp : Function.Surjective p.hom) :
    HasLiftingProperty (SSet.boundary 0).ι (TopCat.toSSet.map p) := by
…
```
theorem OAI.Thomason.Construction.singular_acyclic_boundary_zero line 882
Source documentation
The first case of the published acyclic Kan lifting implication is proved for actual singular maps, with no comparison-W assumption.
```
theorem singular_acyclic_boundary_zero {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) :
    HasLiftingProperty (SSet.boundary 0).ι (TopCat.toSSet.map p) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.singular_adjoint_const line 906

Source documentation

The adjoint of a constant topological map is the corresponding constant singular map.

theorem singular_adjoint_const (K : SSet.{0}) (X : TopCat.{0}) (x : X) :
    sSetTopAdj.homEquiv K X (TopCat.const x) =
      SSet.const (TopCat.toSSetObj₀Equiv.symm x) := by
…

theorem OAI.Thomason.Construction.realized_singular_const line 912

Source documentation

Realization of a constant singular map has its value at the canonical vertex.

theorem realized_singular_const (K : SSet.{0}) (X : TopCat.{0}) (x : X)
    (p : SSet.toTop.obj K) :
    (SSet.toTop.map (SSet.const (X := K) (TopCat.toSSetObj₀Equiv.symm x))).hom p =
…

theorem OAI.Thomason.Construction.RealizedCube.singularMap_face line 929
Source documentation
Each boundary face of a based cube becomes the constant singular simplex.
```
theorem singularMap_face {X : TopCat.{0}} {x : X} (n : ℕ)
    (p : GenLoop (Fin (n+1)) X x) (i : Fin (n+1)) (e : Bool) :
    face n i e ≫ singularMap (n+1) p.val =
      SSet.const (TopCat.toSSetObj₀Equiv.symm x) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.face, OAI.Thomason.Construction.RealizedCube.singularMap
theorem OAI.Thomason.Construction.RealizedCube.singularMap_boundary line 952
Source documentation
The realized lift of a based cube is constant on its entire topological boundary.
```
theorem singularMap_boundary {X : TopCat.{0}} {x : X} (n : ℕ)
    (p : GenLoop (Fin (n+1)) X x) (t : Fin (n+1) → unitInterval)
    (ht : t ∈ Cube.boundary (Fin (n+1))) :
    (SSet.toTop.map (singularMap (n+1) p.val)).hom (sectionMap (n+1) t) =
      singularVertex X x := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.singularMap, OAI.Thomason.Construction.RealizedCube.sectionMap, OAI.Thomason.Construction.singularVertex
def OAI.Thomason.Construction.RealizedCube.liftLoop line 971
Source documentation
Every based topological cube has a based lift through singular realization.
```
def liftLoop {X : TopCat.{0}} {x : X} (n : ℕ) (p : GenLoop (Fin (n+1)) X x) :
    GenLoop (Fin (n+1)) (SSet.toTop.obj (TopCat.toSSet.obj X)) (singularVertex X x) :=
…
```
Mentions: OAI.Thomason.Construction.singularVertex
theorem OAI.Thomason.Construction.RealizedCube.liftLoop_evaluation line 977
Source documentation
The lift evaluates to the original loop pointwise.
```
theorem liftLoop_evaluation {X : TopCat.{0}} {x : X} (n : ℕ)
    (p : GenLoop (Fin (n+1)) X x) (t : Fin (n+1) → unitInterval) :
    (sSetTopAdj.counit.app X).hom (liftLoop n p t) = p t :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.liftLoop
theorem OAI.Thomason.Construction.basedGroupMap_surjective_iff line 998
theorem OAI.Thomason.Construction.singular_counit_basedGroupMap_surjective line 1007
Source documentation
The based singular counit is surjective on every positive homotopy group.
```
theorem singular_counit_basedGroupMap_surjective (X : TopCat.{0}) (x : X) (n : ℕ) :
    Function.Surjective (HomotopyMaps.basedGroupMap (sSetTopAdj.counit.app X).hom
      (counit_singularVertex X x) (n+1)) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.basedGroupMap, OAI.Thomason.Construction.counit_singularVertex
theorem OAI.Thomason.Construction.singular_counit_groupMap_surjective_vertex line 1020
Source documentation
The same surjectivity in the exact, untransported weak-equivalence convention.
```
theorem singular_counit_groupMap_surjective_vertex (X : TopCat.{0}) (x : X) (n : ℕ) :
    Function.Surjective (HomotopyMaps.groupMap (sSetTopAdj.counit.app X).hom
      (n+1) (singularVertex X x)) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap, OAI.Thomason.Construction.singularVertex
theorem OAI.Thomason.Construction.singular_counit_groupMap_surjective line 1028
Source documentation
The actual singular counit is surjective on every positive homotopy group, including basepoints that are not singular vertices.
```
theorem singular_counit_groupMap_surjective (X : TopCat.{0})
    (x : SSet.toTop.obj (TopCat.toSSet.obj X)) (n : ℕ) :
    Function.Surjective (HomotopyMaps.groupMap (sSetTopAdj.counit.app X).hom (n+1) x) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap