KanRealizedEdgeComposition.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Simplicial edge components and actual realization components

def OAI.Thomason.Construction.RealizationPrism.initialVertexEdgeOperator line 24
def OAI.Thomason.Construction.RealizationPrism.initialVertexEdge line 32
def OAI.Thomason.Construction.RealizationPrism.simplexComponent line 53
theorem OAI.Thomason.Construction.RealizationPrism.simplexComponent_vertex line 56
theorem OAI.Thomason.Construction.RealizationPrism.simplexComponent_map line 61
def OAI.Thomason.Construction.RealizationPrism.simplicialComponentsSpace line 69
Source documentation
Edge components carry the discrete topology for this comparison.
```
def simplicialComponentsSpace (K : SSet.{0}) : TopCat.{0} :=
…
```
instance OAI.Thomason.Construction.RealizationPrism.(instance at line 72) line 72
def OAI.Thomason.Construction.RealizationPrism.simplicialComponentsCocone line 74
def OAI.Thomason.Construction.RealizationPrism.realizationComponent line 90
theorem OAI.Thomason.Construction.RealizationPrism.realizationComponent_simplex line 94
theorem OAI.Thomason.Construction.RealizationPrism.realizationComponent_vertex line 105
theorem OAI.Thomason.Construction.RealizationPrism.realizationComponent_path line 121
Source documentation
A continuous path in the actual realization cannot change its simplicial edge component. This direction does not require a Kan condition.
```
theorem realizationComponent_path {K : SSet.{0}} {x y : SSet.toTop.obj K}
    (p : Path x y) : realizationComponent K x = realizationComponent K y := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.realizationComponent
theorem OAI.Thomason.Construction.RealizationPrism.edge_zigzag_of_realization_path line 128
Source documentation
Actual paths between vertices yield finite zigzags of simplicial edges.
```
theorem edge_zigzag_of_realization_path {K : SSet.{0}}
    {v w : K.obj (.op (.mk 0))} (p : Path (vertexPoint K v) (vertexPoint K w)) :
    Relation.EqvGen SSet.π₀Rel v w := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint
theorem OAI.Thomason.Construction.RealizationPrism.point_joined_vertex line 139
Source documentation
Every point is joined to an actual simplicial vertex, before any subdivision or fibrancy replacement.
```
theorem point_joined_vertex (K : SSet.{0}) (x : SSet.toTop.obj K) :
    ∃ v : K.obj (.op (.mk 0)), Joined x (vertexPoint K v) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint
theorem OAI.Thomason.Construction.RealizationPrism.simplicial_components_surjective_of_realization line 154
Source documentation
Surjectivity on actual path components gives surjectivity on simplicial edge components. No Kan hypothesis is used in this compatibility bridge.
```
theorem simplicial_components_surjective_of_realization {K L : SSet.{0}}
    (f : K ⟶ L)
    (hf : Function.Surjective (HomotopyMaps.componentsMap (SSet.toTop.map f).hom)) :
    Function.Surjective (SSet.mapπ₀ f) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.RealizationPrism.vertexPoint_simplexVertex line 172
Source documentation
The geometric vertex of any simplex is the geometric point of its corresponding zero-dimensional face.
```
theorem vertexPoint_simplexVertex (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) (i : Fin (n+1)) :
    vertexPoint K (simplexVertex K s i) = simplexPoint K s (StdSimplex.single i) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint, OAI.Thomason.Construction.RealizationPrism.simplexVertex, OAI.Thomason.Construction.RealizationPrism.simplexPoint
theorem OAI.Thomason.Construction.RealizationPrism.edge_joined line 181
Source documentation
Every simplicial edge gives an actual path with exactly its prescribed vertices as endpoints.
```
theorem edge_joined {K : SSet.{0}} {v w : K.obj (.op (.mk 0))}
    (e : SSet.Edge v w) : Joined (vertexPoint K v) (vertexPoint K w) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint
def OAI.Thomason.Construction.RealizationPrism.vertexComponents line 209
Source documentation
Simplicial edge components map to actual path components.
```
def vertexComponents (K : SSet.{0}) : SSet.π₀ K → ZerothHomotopy (SSet.toTop.obj K) :=
…
```
def OAI.Thomason.Construction.RealizationPrism.realizationComponents line 214
Source documentation
The map to discrete edge components descends through actual paths.
```
def realizationComponents (K : SSet.{0}) : ZerothHomotopy (SSet.toTop.obj K) → SSet.π₀ K :=
…
```
def OAI.Thomason.Construction.RealizationPrism.realizationComponentsEquiv line 219
Source documentation
Actual path components of geometric realization are exactly the simplicial edge components, without a Kan or model-category hypothesis.
```
def realizationComponentsEquiv (K : SSet.{0}) :
    ZerothHomotopy (SSet.toTop.obj K) ≃ SSet.π₀ K where
…
```
theorem OAI.Thomason.Construction.RealizationPrism.vertexComponents_naturality line 235
theorem OAI.Thomason.Construction.RealizationPrism.components_bijective_iff line 245
Source documentation
The component part of the actual weak-equivalence interface is the usual simplicial component test.
```
theorem components_bijective_iff {K L : SSet.{0}} (f : K ⟶ L) :
    Function.Bijective (HomotopyMaps.componentsMap (SSet.toTop.map f).hom) ↔
      Function.Bijective (SSet.mapπ₀ f) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap

theorem OAI.Thomason.Construction.kan_fibration_lift_edge_face line 281

Source documentation

Lift a one-simplex of the base from either prescribed endpoint.

theorem kan_fibration_lift_edge_face {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] (j : Fin 2) (x : X _⦋0⦌)
    (b : Δ[1] ⟶ Y) (hb : SSet.const x ≫ p = SSet.stdSimplex.δ j ≫ b) :
    ∃ a : Δ[1] ⟶ X, SSet.stdSimplex.δ j ≫ a = SSet.const x ∧ a ≫ p = b := by
…

theorem OAI.Thomason.Construction.kan_fibration_edge_image_iff line 298

Source documentation

The image on vertices of a Kan fibration is closed in both directions along every edge of the base.

theorem kan_fibration_edge_image_iff {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] {y₀ y₁ : Y _⦋0⦌} (e : SSet.Edge y₀ y₁) :
    (∃ x : X _⦋0⦌, p.app _ x = y₀) ↔ (∃ x : X _⦋0⦌, p.app _ x = y₁) := by
…

theorem OAI.Thomason.Construction.kan_fibration_zigzag_image_iff line 324

Source documentation

A vertex image is a union of entire simplicial edge components.

theorem kan_fibration_zigzag_image_iff {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] {y₀ y₁ : Y _⦋0⦌}
    (h : Relation.EqvGen SSet.π₀Rel y₀ y₁) :
    (∃ x : X _⦋0⦌, p.app _ x = y₀) ↔ (∃ x : X _⦋0⦌, p.app _ x = y₁) := by
…

theorem OAI.Thomason.Construction.kan_fibration_vertices_surjective line 336
Source documentation
A Kan fibration surjective on actual realization components is strictly surjective on vertices. This is the general, non-singular degree-zero case.
```
theorem kan_fibration_vertices_surjective {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p]
    (hp : Function.Surjective (HomotopyMaps.componentsMap (SSet.toTop.map p).hom)) :
    Function.Surjective (p.app (.op (.mk 0))) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.acyclic_kan_boundary_zero line 349
Source documentation
An actual realization-weak Kan fibration has the required degree-zero boundary lifting property, without assuming the higher-dimensional input.
```
theorem acyclic_kan_boundary_zero {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] (hp : realizationWeakEquivalences p) :
    HasLiftingProperty (SSet.boundary 0).ι p := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.kan_lift_edge_composition line 384

Source documentation

Two composable edges lift a prescribed base triangle, retaining both outer edges and the exact middle face over the base.

theorem kan_lift_edge_composition {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] {x y z : X _⦋0⦌}
    (u : SSet.Edge x y) (v : SSet.Edge y z) (s : Y _⦋2⦌)
    (h₂ : Y.δ 2 s = p.app _ u.edge) (h₀ : Y.δ 0 s = p.app _ v.edge) :
    ∃ w : SSet.Edge x z, Nonempty (SSet.Edge.CompStruct u v w) ∧
      p.app _ w.edge = Y.δ 1 s := by
…

theorem OAI.Thomason.Construction.kan_compose_edges_over line 436

Source documentation

The long edge of a lifted triangle lies over its prescribed base edge.

theorem kan_compose_edges_over {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] {x y z : X _⦋0⦌}
    (u : SSet.Edge x y) (v : SSet.Edge y z) (s : Y _⦋2⦌)
    (h₂ : Y.δ 2 s = p.app _ u.edge) (h₀ : Y.δ 0 s = p.app _ v.edge) :
    ∃ w : SSet.Edge x z, p.app _ w.edge = Y.δ 1 s := by
…

theorem OAI.Thomason.Construction.kan_compose_edges_triangle line 445

Source documentation

Composable edges in a Kan complex have a composition triangle.

theorem kan_compose_edges_triangle {X : SSet.{0}} [SSet.KanComplex X]
    {x y z : X _⦋0⦌} (u : SSet.Edge x y) (v : SSet.Edge y z) :
    ∃ w : SSet.Edge x z, Nonempty (SSet.Edge.CompStruct u v w) := by
…

theorem OAI.Thomason.Construction.kan_compose_edges line 455

Source documentation

Composable edges in a Kan complex can be represented by one edge.

theorem kan_compose_edges {X : SSet.{0}} [SSet.KanComplex X]
    {x y z : X _⦋0⦌} (u : SSet.Edge x y) (v : SSet.Edge y z) :
    Nonempty (SSet.Edge x z) := by
…

theorem OAI.Thomason.Construction.kan_right_inverse_edge line 462

Source documentation

An edge in a Kan complex has an edge in the opposite direction.

theorem kan_right_inverse_edge {X : SSet.{0}} [SSet.KanComplex X]
    {x y : X _⦋0⦌} (e : SSet.Edge x y) :
    ∃ e' : SSet.Edge y x, Nonempty (SSet.Edge.CompStruct e e' (SSet.Edge.id x)) := by
…

theorem OAI.Thomason.Construction.kan_reverse_edge line 498
Source documentation
An edge in a Kan complex has an edge in the opposite direction.
```
theorem kan_reverse_edge {X : SSet.{0}} [SSet.KanComplex X]
    {x y : X _⦋0⦌} (e : SSet.Edge x y) : Nonempty (SSet.Edge y x) := by
…
```

theorem OAI.Thomason.Construction.kan_edge_of_zigzag line 504

Source documentation

Finite edge zigzags compress to a single directed edge in a Kan complex.

theorem kan_edge_of_zigzag {X : SSet.{0}} [SSet.KanComplex X]
    {x y : X _⦋0⦌} (h : Relation.EqvGen SSet.π₀Rel x y) : Nonempty (SSet.Edge x y) := by
…

theorem OAI.Thomason.Construction.kan_edge_of_realization_path line 515
Source documentation
Every continuous path between realized vertices of a Kan complex gives an exact simplicial edge with those endpoints.
```
theorem kan_edge_of_realization_path {X : SSet.{0}} [SSet.KanComplex X]
    {x y : X _⦋0⦌}
    (h : Path (RealizationPrism.vertexPoint X x) (RealizationPrism.vertexPoint X y)) :
    Nonempty (SSet.Edge x y) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint

theorem OAI.Thomason.Construction.boundary_one_lifting_of_edges line 540

Source documentation

Exact lifting of all edges with both endpoints prescribed is the one-dimensional boundary lifting property, with the complete boundary map.

theorem boundary_one_lifting_of_edges {X Y : SSet.{0}} (p : X ⟶ Y)
    (h : ∀ (x y : X _⦋0⦌) (b : SSet.Edge (p.app _ x) (p.app _ y)),
      ∃ e : SSet.Edge x y, e.map p = b) :
    HasLiftingProperty (SSet.boundary 1).ι p := by
…

theorem OAI.Thomason.Construction.kan_lift_edge_of_fiber_components line 588

Source documentation

A Kan edge lift can have its final endpoint corrected inside a connected literal vertex fibre. The base edge remains exactly the prescribed edge.

theorem kan_lift_edge_of_fiber_components {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] (x y : X _⦋0⦌)
    (b : SSet.Edge (p.app _ x) (p.app _ y))
    (hc : Function.Injective (HomotopyMaps.componentsMap
      (ContinuousMap.const (SSet.toTop.obj (simplicialPointFiber p (p.app _ y)).toSSet) ()))) :
    ∃ e : SSet.Edge x y, e.map p = b := by
…

Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap, OAI.Thomason.Construction.simplicialPointFiber

def OAI.Thomason.Construction.initialSimplexVertex line 656
def OAI.Thomason.Construction.simplexInitialContraction line 660
Source documentation
The ordered simplex contracts simplicially to its initial vertex.
```
def simplexInitialContraction (n : ℕ) :
    SSet.Homotopy (SSet.const (initialSimplexVertex n)) (𝟙 (Δ[n] : SSet.{0})) where
…
```
Mentions: OAI.Thomason.Construction.initialSimplexVertex
theorem OAI.Thomason.Construction.kan_fibration_simplex_lift line 704
Source documentation
A whole simplex of the base lifts from any chosen point over its initial vertex. This needs only the Kan fibration condition.
```
theorem kan_fibration_simplex_lift {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, a ≫ p = b := by
…
```
Mentions: OAI.Thomason.Construction.initialSimplexVertex
theorem OAI.Thomason.Construction.kan_fibration_degree_surjective line 719
Source documentation
Surjectivity on the actual realization components makes a Kan fibration surjective in every simplicial degree.
```
theorem kan_fibration_degree_surjective {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p]
    (hp : Function.Surjective (HomotopyMaps.componentsMap (SSet.toTop.map p).hom)) (n : ℕ) :
    Function.Surjective (p.app (.op (.mk n))) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.acyclic_kan_epi line 732
Source documentation
In particular, an actual weak Kan fibration is a simplicial epimorphism.
```
theorem acyclic_kan_epi {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] (hp : realizationWeakEquivalences p) : Epi p := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.RealizationPrism.edge_initial_vertex line 756
theorem OAI.Thomason.Construction.RealizationPrism.edge_final_vertex line 768
def OAI.Thomason.Construction.RealizationPrism.edgePath line 781
Source documentation
The actual linear path inside the geometric one-simplex of an edge.
```
def edgePath {X : SSet.{0}} {x y : X _⦋0⦌} (e : SSet.Edge x y) :
    Path (vertexPoint X x) (vertexPoint X y) where
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint
theorem OAI.Thomason.Construction.RealizationPrism.edgePath_map line 792
Source documentation
Every map of simplicial sets preserves canonical edge paths exactly, including their parametrization, after the stated endpoint identifications.
```
theorem edgePath_map {X Y : SSet.{0}} (f : X ⟶ Y) {x y : X _⦋0⦌}
    (e : SSet.Edge x y) :
    ((edgePath e).map (SSet.toTop.map f).hom.continuous).cast
      (map_vertexPoint f x).symm (map_vertexPoint f y).symm = edgePath (e.map f) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.edgePath, OAI.Thomason.Construction.RealizationPrism.map_vertexPoint
theorem OAI.Thomason.Construction.RealizationPrism.edgePath_id line 802
Source documentation
A degenerate identity edge gives the constant path, not just its homotopy class.
```
theorem edgePath_id {X : SSet.{0}} (x : X _⦋0⦌) :
    edgePath (SSet.Edge.id x) = Path.refl (vertexPoint X x) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.edgePath, OAI.Thomason.Construction.RealizationPrism.vertexPoint
theorem OAI.Thomason.Construction.RealizationPrism.edgePath_comp_homotopic line 830
Source documentation
The two sides and the long edge of a simplicial triangle represent the same actual path-homotopy class, with both endpoints fixed.
```
theorem edgePath_comp_homotopic {X : SSet.{0}} {x y z : X _⦋0⦌}
    {u : SSet.Edge x y} {v : SSet.Edge y z} {w : SSet.Edge x z}
    (s : SSet.Edge.CompStruct u v w) :
    ((edgePath u).trans (edgePath v)).Homotopic (edgePath w) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.edgePath
def OAI.Thomason.Construction.RealizationPrism.homotopyCategoryToFundamentalGroupoid line 882
Source documentation
A simplicial edge is sent to its actual linear path class. The triangle relation holds by the explicit barycentric relative homotopy.
```
def homotopyCategoryToFundamentalGroupoid (X : SSet.{0}) :
    X.HomotopyCategory ⥤ FundamentalGroupoid (SSet.toTop.obj X) :=
…
```
theorem OAI.Thomason.Construction.RealizationPrism.homotopyCategoryToFundamentalGroupoid_obj line 892
theorem OAI.Thomason.Construction.RealizationPrism.homotopyCategoryToFundamentalGroupoid_map line 897
theorem OAI.Thomason.Construction.RealizationPrism.edgePath_homotopic_of_homMk_eq line 905
Source documentation
Equality of simplicial edge classes implies an actual relative path homotopy after realization, without any Kan or fibrancy hypothesis.
```
theorem edgePath_homotopic_of_homMk_eq {X : SSet.{0}} {x y : X _⦋0⦌}
    {u v : SSet.Edge x y} (h : SSet.HomotopyCategory.homMk u = SSet.HomotopyCategory.homMk v) :
    (edgePath u).Homotopic (edgePath v) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.edgePath

theorem OAI.Thomason.Construction.kan_homMk_surjective line 932

Source documentation

Every homotopy-category morphism of a Kan complex is represented by a single edge, retaining the homotopy-category class under composition.

theorem kan_homMk_surjective {X : SSet.{0}} [SSet.KanComplex X] (x y : X _⦋0⦌) :
    Function.Surjective (SSet.HomotopyCategory.homMk :
      SSet.Edge x y → (SSet.HomotopyCategory.mk x ⟶ SSet.HomotopyCategory.mk y)) := by
…

theorem OAI.Thomason.Construction.kan_homMk_isIso line 948

Source documentation

A Kan edge becomes an isomorphism with a represented inverse.

theorem kan_homMk_isIso {X : SSet.{0}} [SSet.KanComplex X]
    {x y : X _⦋0⦌} (e : SSet.Edge x y) : IsIso (SSet.HomotopyCategory.homMk e) := by
…

theorem OAI.Thomason.Construction.kan_homotopyCategory_isIso line 966
Source documentation
In a Kan complex, every homotopy-category morphism is invertible.
```
theorem kan_homotopyCategory_isIso {X : SSet.{0}} [SSet.KanComplex X]
    {x y : X.HomotopyCategory} (f : x ⟶ y) : IsIso f := by
…
```

theorem OAI.Thomason.Construction.kan_compose_realized_edges_over line 993

Source documentation

Exact composition over a prescribed base triangle preserves the whole realized relative path class of the two lifted edges.

theorem kan_compose_realized_edges_over {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] {x y z : X _⦋0⦌}
    (u : SSet.Edge x y) (v : SSet.Edge y z) (s : Y _⦋2⦌)
    (h₂ : Y.δ 2 s = p.app _ u.edge) (h₀ : Y.δ 0 s = p.app _ v.edge) :
    ∃ w : SSet.Edge x z, p.app _ w.edge = Y.δ 1 s ∧
      ((RealizationPrism.edgePath u).trans (RealizationPrism.edgePath v)).Homotopic
        (RealizationPrism.edgePath w) := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.edgePath

theorem OAI.Thomason.Construction.kan_realized_right_inverse line 1005
Source documentation
The reverse edge furnished by an outer Kan horn is an inverse on actual path-homotopy classes, not merely an edge with reversed endpoints.
```
theorem kan_realized_right_inverse {X : SSet.{0}} [SSet.KanComplex X]
    {x y : X _⦋0⦌} (e : SSet.Edge x y) :
    ∃ v : SSet.Edge y x,
      ((RealizationPrism.edgePath e).trans (RealizationPrism.edgePath v)).Homotopic
        (Path.refl (RealizationPrism.vertexPoint X x)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.edgePath, OAI.Thomason.Construction.RealizationPrism.vertexPoint
theorem OAI.Thomason.Construction.kan_realized_morphism_edge line 1016
Source documentation
Every realized image of a Kan homotopy-category morphism has a single edge representative in exactly the same actual path-homotopy class.
```
theorem kan_realized_morphism_edge {X : SSet.{0}} [SSet.KanComplex X]
    (x y : X _⦋0⦌) (f : SSet.HomotopyCategory.mk x ⟶ SSet.HomotopyCategory.mk y) :
    ∃ e : SSet.Edge x y,
      (RealizationPrism.homotopyCategoryToFundamentalGroupoid X).map f =
        Path.Homotopic.Quotient.mk (RealizationPrism.edgePath e) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.homotopyCategoryToFundamentalGroupoid, OAI.Thomason.Construction.RealizationPrism.edgePath