KanFiberComponentTransport.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

Naturality of the realized homotopy-category comparison

theorem OAI.Thomason.Construction.RealizationPrism.edgePath_class_naturality line 24

Source documentation

Naturality on an edge includes the actual equalities of its realized endpoints; no basepoint transport is left implicit.

theorem edgePath_class_naturality {X Y : SSet.{0}} (f : X ⟶ Y)
    {x y : X _⦋0⦌} (e : SSet.Edge x y) :
    eqToHom (congrArg FundamentalGroupoid.mk (map_vertexPoint f x).symm) ≫
      (FundamentalGroupoid.map (SSet.toTop.map f).hom).map
        (Path.Homotopic.Quotient.mk (edgePath e)) ≫
      eqToHom (congrArg FundamentalGroupoid.mk (map_vertexPoint f y)) =
        Path.Homotopic.Quotient.mk (edgePath (e.map f)) := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.map_vertexPoint, OAI.Thomason.Construction.RealizationPrism.edgePath

def OAI.Thomason.Construction.RealizationPrism.homotopyCategoryToFundamentalGroupoid_naturality line 40
Source documentation
The comparison with the actual fundamental groupoid is natural in simplicial maps, with the canonical endpoint identifications.
```
def homotopyCategoryToFundamentalGroupoid_naturality {X Y : SSet.{0}} (f : X ⟶ Y) :
    SSet.mapHomotopyCategory f ⋙ homotopyCategoryToFundamentalGroupoid Y ≅
      homotopyCategoryToFundamentalGroupoid X ⋙
        FundamentalGroupoid.map (SSet.toTop.map f).hom :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.homotopyCategoryToFundamentalGroupoid
theorem OAI.Thomason.Construction.zeroFaceSection_naturality line 87

theorem OAI.Thomason.Construction.initial_point_lifting_of_vertices line 96

Source documentation

Vertex-surjectivity is lifting against the initial map into the point.

theorem initial_point_lifting_of_vertices {X Y : SSet.{0}} (p : X ⟶ Y)
    (hp : Function.Surjective (p.app (.op (.mk 0)))) :
    HasLiftingProperty (initial.to (Δ[0] : SSet.{0})) p := by
…

theorem OAI.Thomason.Construction.lifting_of_relativeMapping_components line 109
Source documentation
Exact lifting of i follows from actual component-surjectivity of its relative mapping-space fibration. Its Kan property is supplied by the proved pushout-product theorem, independently of Kan–Quillen weak factorization.
```
theorem lifting_of_relativeMapping_components {A B X Y : SSet.{0}}
    (i : A ⟶ B) [Mono i] (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p]
    (q : MonoidalClosed.internalHom.PullbackObjObj i p)
    (hq : Function.Surjective (HomotopyMaps.componentsMap (SSet.toTop.map q.π).hom)) :
    HasLiftingProperty i p := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap
def OAI.Thomason.Construction.finalSimplexVertex line 158
def OAI.Thomason.Construction.simplexFinalContraction line 162
Source documentation
The explicit monotone contraction from a simplex to its final vertex.
```
def simplexFinalContraction (n : ℕ) :
    SSet.Homotopy (𝟙 (Δ[n] : SSet.{0})) (SSet.const (finalSimplexVertex n)) where
…
```
Mentions: OAI.Thomason.Construction.finalSimplexVertex
theorem OAI.Thomason.Construction.simplexFinalContraction_stationary line 206
Source documentation
Every constant family at the final vertex is fixed throughout the contraction, with an arbitrary simplicial parameter.
```
theorem simplexFinalContraction_stationary (n : ℕ) (K : SSet.{0}) :
    (SSet.const (X := K) (finalSimplexVertex n)) ▷ Δ[1] ≫
…
```
Mentions: OAI.Thomason.Construction.finalSimplexVertex

theorem OAI.Thomason.Construction.kan_simplex_fiber_deformation line 225

Source documentation

A Kan fibration over a simplex has an actual stationary simplicial retraction onto its final-vertex fibre. This is the local fibre comparison needed before passing through a base's simplices.

theorem kan_simplex_fiber_deformation {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p] :
    ∃ r : E ⟶ (simplicialPointFiber p (finalSimplexVertex n)).toSSet,
      (simplicialPointFiber p (finalSimplexVertex n)).ι ≫ r = 𝟙 _ ∧
      ∃ T : SSet.Homotopy (𝟙 E) (r ≫ (simplicialPointFiber p (finalSimplexVertex n)).ι),
        (simplicialPointFiber p (finalSimplexVertex n)).ι ▷ Δ[1] ≫ T.h =
          fst (simplicialPointFiber p (finalSimplexVertex n)).toSSet Δ[1] ≫
            (simplicialPointFiber p (finalSimplexVertex n)).ι ∧
        T.h ≫ p = p ▷ Δ[1] ≫ (simplexFinalContraction n).h := by
…

Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.finalSimplexVertex, OAI.Thomason.Construction.simplexFinalContraction

theorem OAI.Thomason.Construction.kan_simplex_fiber_weak line 240
Source documentation
Inclusion of the literal final-vertex fibre is an actual realization weak equivalence. The base simplex itself need not be a Kan complex.
```
theorem kan_simplex_fiber_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p] :
    realizationWeakEquivalences (simplicialPointFiber p (finalSimplexVertex n)).ι := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.finalSimplexVertex

theorem OAI.Thomason.Construction.horn_supported line 265

Source documentation

Changing simplex vertices only to the distinguished horn vertex stays inside the horn, since an omitted different vertex is still omitted.

theorem horn_supported {n : ℕ} (i : Fin (n+2)) {m : SimplexCategoryᵒᵖ}
    (s : (Λ[n+1, i] : SSet.{0}).obj m)
    (f : Fin (m.unop.len+1) →o Fin (n+2))
    (hf : ∀ k, f k = (SSet.stdSimplex.objEquiv s.val).toOrderHom k ∨ f k = i) :
    SSet.stdSimplex.objMk f ∈ (Λ[n+1, i] : (Δ[n+1] : SSet.{0}).Subcomplex).obj m := by
…

def OAI.Thomason.Construction.hornVertex line 283
Source documentation
The distinguished vertex belongs to its horn in every positive dimension.
```
def hornVertex (n : ℕ) (i : Fin (n+2)) : (Λ[n+1, i] : SSet.{0}) _⦋0⦌ :=
…
```
def OAI.Thomason.Construction.hornClamp line 291
def OAI.Thomason.Construction.hornClampToId line 309
Source documentation
The clamp is below the identity, with no change of an omitted vertex.
```
def hornClampToId (n : ℕ) (i : Fin (n+2)) :
    SSet.Homotopy (hornClamp n i) (𝟙 (Λ[n+1, i] : SSet.{0})) where
…
```
Mentions: OAI.Thomason.Construction.hornClamp
def OAI.Thomason.Construction.hornClampToVertex line 361
Source documentation
The same clamp is below the constant distinguished vertex.
```
def hornClampToVertex (n : ℕ) (i : Fin (n+2)) :
    SSet.Homotopy (hornClamp n i) (SSet.const (hornVertex n i)) where
…
```
Mentions: OAI.Thomason.Construction.hornClamp, OAI.Thomason.Construction.hornVertex
theorem OAI.Thomason.Construction.hornClampToId_stationary line 412
theorem OAI.Thomason.Construction.hornClampToVertex_stationary line 427
def OAI.Thomason.Construction.initialVertexInclusion line 460
theorem OAI.Thomason.Construction.initialVertexInclusion_mono line 463
theorem OAI.Thomason.Construction.simplexInitialContraction_stationary line 476
Source documentation
The explicit simplex contraction fixes the initial vertex in every simplicial degree and at every cylinder time.
```
theorem simplexInitialContraction_stationary (n : ℕ) :
    initialVertexInclusion n ▷ Δ[1] ≫ (simplexInitialContraction n).h =
      fst (Δ[0] : SSet.{0}) Δ[1] ≫ initialVertexInclusion n := by
…
```
Mentions: OAI.Thomason.Construction.initialVertexInclusion, OAI.Thomason.Construction.simplexInitialContraction
theorem OAI.Thomason.Construction.initialVertexInclusion_anodyne line 492
Source documentation
The actual vertex inclusion is anodyne without using the Kan–Quillen weak-equivalence characterization of anodyne maps.
```
theorem initialVertexInclusion_anodyne (n : ℕ) :
    SSet.anodyneExtensions (initialVertexInclusion n) := by
…
```
Mentions: OAI.Thomason.Construction.initialVertexInclusion
theorem OAI.Thomason.Construction.kan_fibration_simplex_lift_vertex line 516
Source documentation
A simplex lift can preserve the originally specified initial vertex exactly, in addition to commuting with the fibration.
```
theorem kan_fibration_simplex_lift_vertex {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] (n : ℕ) (b : Δ[n] ⟶ Y) (x : X _⦋0⦌)
    (hx : p.app _ x = b.app _ (initialSimplexVertex n)) :
    ∃ a : Δ[n] ⟶ X, initialVertexInclusion n ≫ a = SSet.const x ∧ a ≫ p = b := by
…
```
Mentions: OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.initialVertexInclusion

theorem OAI.Thomason.Construction.kan_lift_of_boundary_homotopy line 550

Source documentation

A boundary homotopy over a fixed base map corrects any preliminary simplicial lift to an exact lift. This works for every monomorphism.

theorem kan_lift_of_boundary_homotopy {A K E B : SSet.{0}}
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (d : K ⟶ E) (b : K ⟶ B) (hd : d ≫ p = b) (a : A ⟶ E)
    (H : SSet.Homotopy (i ≫ d) a)
    (hH : H.h ≫ p = fst A Δ[1] ≫ i ≫ b) :
    ∃ l : K ⟶ E, i ≫ l = a ∧ l ≫ p = b := by
…

theorem OAI.Thomason.Construction.kan_extension_of_nullhomotopy line 576

Source documentation

A simplicial nullhomotopy extends across any monomorphic inclusion into a Kan complex. The extension keeps the given map exactly.

theorem kan_extension_of_nullhomotopy {A K X : SSet.{0}} [SSet.KanComplex X]
    (i : A ⟶ K) [Mono i] (a : A ⟶ X) (x : X _⦋0⦌)
    (H : SSet.Homotopy (SSet.const x) a) :
    ∃ l : K ⟶ X, i ≫ l = a := by
…

def OAI.Thomason.Construction.boundaryNullhomotopyOfExtension line 589
Source documentation
Any extension over a standard simplex supplies an explicit simplicial nullhomotopy, by the actual initial-vertex contraction.
```
def boundaryNullhomotopyOfExtension {X : SSet.{0}} (n : ℕ)
    (a : (SSet.boundary n : SSet.{0}) ⟶ X) (d : (Δ[n] : SSet.{0}) ⟶ X)
    (hd : (SSet.boundary n).ι ≫ d = a) :
    SSet.Homotopy (SSet.const (d.app _ (initialSimplexVertex n))) a where
…
```
Mentions: OAI.Thomason.Construction.initialSimplexVertex
theorem OAI.Thomason.Construction.kan_boundary_extension_iff_nullhomotopy line 626
Source documentation
In every dimension, the exact boundary extension problem in a Kan complex is equivalent to an actual simplicial nullhomotopy. This is a reduction, not an assumption about continuous nullhomotopies.
```
theorem kan_boundary_extension_iff_nullhomotopy {X : SSet.{0}} [SSet.KanComplex X]
    (n : ℕ) (a : (SSet.boundary n : SSet.{0}) ⟶ X) :
    (∃ l : (Δ[n] : SSet.{0}) ⟶ X, (SSet.boundary n).ι ≫ l = a) ↔
      ∃ x : X _⦋0⦌, Nonempty (SSet.Homotopy (SSet.const x) a) := by
…
```

theorem OAI.Thomason.Construction.kan_pullback_snd_fibration line 654

Source documentation

Horn lifting is stable under actual simplicial pullback.

theorem kan_pullback_snd_fibration {E B C : SSet.{0}} (p : E ⟶ B) (g : C ⟶ B)
    [HomotopicalAlgebra.Fibration p] :
    HomotopicalAlgebra.Fibration (pullback.snd p g) := by
…

def OAI.Thomason.Construction.pointFiberToPullback line 663
Source documentation
The original point fibre maps canonically into every pullback containing that point.
```
def pointFiberToPullback {E B C : SSet.{0}} (p : E ⟶ B) (g : C ⟶ B)
    (c : C.obj (.op (.mk 0))) :
    (simplicialPointFiber p (g.app _ c)).toSSet ⟶ pullback p g :=
…
```
Mentions: OAI.Thomason.Construction.simplicialPointFiber
theorem OAI.Thomason.Construction.pointFiberToPullback_fst line 670
theorem OAI.Thomason.Construction.pointFiberToPullback_snd line 676

def OAI.Thomason.Construction.simplicialPointFiberBaseChangeIso line 683

Source documentation

Fibres of the actual simplicial pullback identify exactly with the original point fibres.

def simplicialPointFiberBaseChangeIso {E B C : SSet.{0}} (p : E ⟶ B) (g : C ⟶ B)
    (c : C.obj (.op (.mk 0))) :
    (simplicialPointFiber p (g.app _ c)).toSSet ≅
      (simplicialPointFiber (pullback.snd p g) c).toSSet where
…

Mentions: OAI.Thomason.Construction.simplicialPointFiber

theorem OAI.Thomason.Construction.simplicialPointFiberBaseChangeIso_hom_ι line 706
theorem OAI.Thomason.Construction.kan_simplex_baseChange_fiber_weak line 714
Source documentation
In a Kan fibration, the canonical map from the fibre over the final vertex of any base simplex into that simplex pullback is an actual W. This local result does not assume right properness or acyclic Kan lifting.
```
theorem kan_simplex_baseChange_fiber_weak {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (n : ℕ) (g : SSet.stdSimplex.obj (.mk n) ⟶ B) :
    realizationWeakEquivalences (pointFiberToPullback p g (finalSimplexVertex n)) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.pointFiberToPullback, OAI.Thomason.Construction.finalSimplexVertex
theorem OAI.Thomason.Construction.simplexInitialContraction_const line 740
theorem OAI.Thomason.Construction.kan_simplex_initialFiber_anodyne line 757
Source documentation
The initial fibre inclusion is even anodyne, by the reverse lifted stationary simplex contraction.
```
theorem kan_simplex_initialFiber_anodyne {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p] :
    SSet.anodyneExtensions (simplicialPointFiber p (initialSimplexVertex n)).ι := by
…
```
Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex
theorem OAI.Thomason.Construction.kan_simplex_initialFiber_weak line 769
theorem OAI.Thomason.Construction.kan_simplex_baseChange_initialFiber_weak line 774
theorem OAI.Thomason.Construction.kan_simplex_baseChange_weak_of_final line 784
Source documentation
A restriction preserving the final vertex induces a weak equivalence on the total pullback of any Kan fibration over a simplex.
```
theorem kan_simplex_baseChange_weak_of_final {E : SSet.{0}} (n m : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (g : (Δ[m] : SSet.{0}) ⟶ Δ[n])
    (hg : g.app _ (finalSimplexVertex m) = finalSimplexVertex n) :
    realizationWeakEquivalences (pullback.fst p g) := by
…
```
Mentions: OAI.Thomason.Construction.finalSimplexVertex, OAI.Thomason.Construction.realizationWeakEquivalences
def OAI.Thomason.Construction.finalVertexEdgeOperator line 795
Source documentation
The ordinal edge from any vertex to the final one.
```
def finalVertexEdgeOperator {n : ℕ} (j : Fin (n+1)) : ⦋1⦌ ⟶ ⦋n⦌ :=
…
```
theorem OAI.Thomason.Construction.finalVertexEdgeOperator_final line 803
theorem OAI.Thomason.Construction.finalVertexEdgeOperator_initial line 813
theorem OAI.Thomason.Construction.kan_simplex_vertexFiber_weak line 825
Source documentation
Every vertex fibre, not only an endpoint fibre, includes weakly in the total space of a Kan fibration over a standard simplex.
```
theorem kan_simplex_vertexFiber_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (j : Fin (n+1)) :
    realizationWeakEquivalences
      (simplicialPointFiber p (SSet.stdSimplex.objEquiv.symm (RealizationPrism.vertexOperator j))).ι := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.RealizationPrism.vertexOperator
theorem OAI.Thomason.Construction.standard_vertex_eq line 840
Source documentation
A vertex of a standard simplex is exactly one of its ordinal vertices.
```
theorem standard_vertex_eq (n : ℕ) (v : (Δ[n] : SSet.{0}) _⦋0⦌) :
    v = SSet.stdSimplex.objEquiv.symm
      (RealizationPrism.vertexOperator ((SSet.stdSimplex.objEquiv v).toOrderHom 0)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexOperator
theorem OAI.Thomason.Construction.kan_simplex_anyFiber_weak line 851
theorem OAI.Thomason.Construction.kan_simplex_baseChange_weak line 861
Source documentation
Every map of standard simplices induces an actual weak equivalence on pullback total spaces of a Kan fibration over the target simplex. This is proved from the endpoint deformations, without global acyclic Kan lifting.
```
theorem kan_simplex_baseChange_weak {E : SSet.{0}} (n m : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (g : (Δ[m] : SSet.{0}) ⟶ Δ[n]) :
    realizationWeakEquivalences (pullback.fst p g) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.kan_fiber_weak_iff_of_edge line 891
Source documentation
In a Kan fibration, whether a vertex fibre includes by an actual weak equivalence is unchanged along a simplicial edge. This uses the proved simplex fibre theorem, rather than a global homotopy-fibre assumption.
```
theorem kan_fiber_weak_iff_of_edge {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] {x y : B _⦋0⦌} (e : SSet.Edge x y) :
    realizationWeakEquivalences (simplicialPointFiber p x).ι ↔
      realizationWeakEquivalences (simplicialPointFiber p y).ι := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.simplicialPointFiber

theorem OAI.Thomason.Construction.kan_fiber_weak_iff_of_zigzag line 933

Source documentation

The same exact test is constant on an entire simplicial edge component.

theorem kan_fiber_weak_iff_of_zigzag {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] {x y : B _⦋0⦌}
    (h : Relation.EqvGen SSet.π₀Rel x y) :
    realizationWeakEquivalences (simplicialPointFiber p x).ι ↔
      realizationWeakEquivalences (simplicialPointFiber p y).ι := by
…

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

theorem OAI.Thomason.Construction.kan_fiber_weak_iff_of_realization_path line 947
Source documentation
Actual continuous paths between realized vertices transport the fibre weak-equivalence test. No simplicial approximation of the path is assumed: the already proved component comparison supplies the finite edge zigzag.
```
theorem kan_fiber_weak_iff_of_realization_path {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] {x y : B _⦋0⦌}
    (h : Path (RealizationPrism.vertexPoint B x) (RealizationPrism.vertexPoint B y)) :
    realizationWeakEquivalences (simplicialPointFiber p x).ι ↔
      realizationWeakEquivalences (simplicialPointFiber p y).ι :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.simplicialPointFiber