RealizationTopology.lean`

74 declarations, 0 contain sorry, 0 declared as axioms

Barycentric retraction onto the geometric horn

Subtract the smallest non-cone coordinate from every such coordinate and move the removed mass to the cone vertex. This continuous retraction fixes the entire horn pointwise, as needed for relative horn attachments.

def OAI.Thomason.Construction.HornBarycentric.others line 31
Source documentation
The vertices other than the horn's cone vertex.
```
def others {n : ℕ} (i : Fin (n+2)) : Finset (Fin (n+2)) := Finset.univ.erase i
```
theorem OAI.Thomason.Construction.HornBarycentric.others_nonempty line 33
def OAI.Thomason.Construction.HornBarycentric.mass line 38
Source documentation
The smallest coordinate away from the cone vertex.
```
def mass {n : ℕ} (i : Fin (n+2)) (x : StdSimplex ℝ (Fin (n+2))) : ℝ :=
…
```
theorem OAI.Thomason.Construction.HornBarycentric.mass_nonneg line 41
theorem OAI.Thomason.Construction.HornBarycentric.mass_le line 44
theorem OAI.Thomason.Construction.HornBarycentric.mass_attained line 48
theorem OAI.Thomason.Construction.HornBarycentric.continuous_mass line 53
def OAI.Thomason.Construction.HornBarycentric.shiftedWeights line 58
Source documentation
Coordinates after shifting a nonnegative amount of mass to the cone vertex.
```
def shiftedWeights {n : ℕ} (i : Fin (n+2)) (x : StdSimplex ℝ (Fin (n+2))) (a : ℝ) :
    Fin (n+2) →₀ ℝ :=
…
```
def OAI.Thomason.Construction.HornBarycentric.shift line 65
Source documentation
Every shift up to the minimum coordinate remains a barycentric point.
```
def shift {n : ℕ} (i : Fin (n+2)) (x : StdSimplex ℝ (Fin (n+2)))
    (a : ℝ) (ha : 0 ≤ a) (hb : a ≤ mass i x) : StdSimplex ℝ (Fin (n+2)) where
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.mass
def OAI.Thomason.Construction.HornBarycentric.horn line 91
Source documentation
The geometric horn is the union of all faces except the opposite face.
```
def horn {n : ℕ} (i : Fin (n+2)) : Set (StdSimplex ℝ (Fin (n+2))) :=
…
```
theorem OAI.Thomason.Construction.HornBarycentric.shift_mass_mem line 95
Source documentation
Subtracting the minimum lands in the geometric horn.
```
theorem shift_mass_mem {n : ℕ} (i : Fin (n+2)) (x : StdSimplex ℝ (Fin (n+2))) :
    shift i x (mass i x) (mass_nonneg i x) le_rfl ∈ horn i := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.shift, OAI.Thomason.Construction.HornBarycentric.mass, OAI.Thomason.Construction.HornBarycentric.mass_nonneg, OAI.Thomason.Construction.HornBarycentric.horn
theorem OAI.Thomason.Construction.HornBarycentric.mass_eq_zero line 103
Source documentation
On the geometric horn the minimum coordinate is zero.
```
theorem mass_eq_zero {n : ℕ} (i : Fin (n+2)) {x : StdSimplex ℝ (Fin (n+2))}
    (hx : x ∈ horn i) : mass i x = 0 := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.horn, OAI.Thomason.Construction.HornBarycentric.mass
theorem OAI.Thomason.Construction.HornBarycentric.shift_zero line 109
def OAI.Thomason.Construction.HornBarycentric.retraction line 118
Source documentation
The actual continuous retraction to the geometric horn.
```
def retraction {n : ℕ} (i : Fin (n+2)) : C(StdSimplex ℝ (Fin (n+2)), horn i) where
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.horn
theorem OAI.Thomason.Construction.HornBarycentric.retraction_fixed line 133
Source documentation
The retraction fixes the whole horn, including every overlap of faces.
```
theorem retraction_fixed {n : ℕ} (i : Fin (n+2)) (x : horn i) :
    (retraction i x.val).val = x.val := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.horn, OAI.Thomason.Construction.HornBarycentric.retraction
def OAI.Thomason.Construction.HornBarycentric.deformation line 144
Source documentation
Shift only the fraction of mass specified by the interval coordinate.
```
def deformation {n : ℕ} (i : Fin (n+2)) :
    C(StdSimplex ℝ (Fin (n+2)) × unitInterval, StdSimplex ℝ (Fin (n+2))) where
…
```
theorem OAI.Thomason.Construction.HornBarycentric.deformation_zero line 165
theorem OAI.Thomason.Construction.HornBarycentric.deformation_one line 175
theorem OAI.Thomason.Construction.HornBarycentric.deformation_fixed line 186
Source documentation
The entire deformation is stationary on the geometric horn.
```
theorem deformation_fixed {n : ℕ} (i : Fin (n+2)) (x : horn i) (t : unitInterval) :
    deformation i (x.val, t) = x.val := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.horn, OAI.Thomason.Construction.HornBarycentric.deformation
def OAI.Thomason.Construction.HornBarycentric.deletion line 218
Source documentation
A monotone deletion map, with an arbitrary choice only at the deleted vertex.
```
def deletion {n : ℕ} (j : Fin (n+2)) : Fin (n+2) →o Fin (n+1) :=
…
```
theorem OAI.Thomason.Construction.HornBarycentric.insertion_deletion line 223
Source documentation
Reinserting the deleted coordinate is the identity away from it.
```
theorem insertion_deletion {n : ℕ} (j k : Fin (n+2)) (hk : k ≠ j) :
    j.succAbove (deletion j k) = k := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.deletion
theorem OAI.Thomason.Construction.HornBarycentric.deletion_insertion line 234
theorem OAI.Thomason.Construction.HornBarycentric.simplex_map_injective line 240
Source documentation
Injective vertex maps remain injective on barycentric points.
```
theorem simplex_map_injective {α β : Type*} {f : α → β} (hf : Function.Injective f) :
    Function.Injective (StdSimplex.map (R := ℝ) f) := by
…
```
theorem OAI.Thomason.Construction.HornBarycentric.face_recover line 247
Source documentation
Inserting after deleting a zero coordinate recovers the original point.
```
theorem face_recover {n : ℕ} (j : Fin (n+2))
    (x : StdSimplex ℝ (Fin (n+2))) (hx : x.weights j = 0) :
    StdSimplex.map j.succAbove (StdSimplex.map (deletion j) x) = x := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.deletion
theorem OAI.Thomason.Construction.HornBarycentric.face_delete_insert line 263
Source documentation
Deletion is the inverse on the entire face chart.
```
theorem face_delete_insert {n : ℕ} (j : Fin (n+2))
    (x : StdSimplex ℝ (Fin (n+1))) :
    StdSimplex.map (deletion j) (StdSimplex.map j.succAbove x) = x := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.deletion
theorem OAI.Thomason.Construction.HornBarycentric.support_nonempty line 292
def OAI.Thomason.Construction.HornBarycentric.supportLen line 300
theorem OAI.Thomason.Construction.HornBarycentric.support_card line 302
def OAI.Thomason.Construction.HornBarycentric.supportMap line 309
Source documentation
The increasing enumeration of the nonzero coordinates.
```
def supportMap {n : ℕ} (x : StdSimplex ℝ (Fin (n+1))) :
    Fin (supportLen x+1) ↪o Fin (n+1) := x.weights.support.orderEmbOfFin (support_card x)
```
Mentions: OAI.Thomason.Construction.HornBarycentric.supportLen, OAI.Thomason.Construction.HornBarycentric.support_card
theorem OAI.Thomason.Construction.HornBarycentric.supportMap_mem line 312
theorem OAI.Thomason.Construction.HornBarycentric.supportMap_ne line 316
def OAI.Thomason.Construction.HornBarycentric.supportCoordinates line 323
Source documentation
Coordinates on the ordered support.
```
def supportCoordinates {n : ℕ} (x : StdSimplex ℝ (Fin (n+1))) :
    StdSimplex ℝ (Fin (supportLen x+1)) := StdSimplex.map (Function.invFun (supportMap x)) x
```
Mentions: OAI.Thomason.Construction.HornBarycentric.supportLen, OAI.Thomason.Construction.HornBarycentric.supportMap
theorem OAI.Thomason.Construction.HornBarycentric.support_recover line 327
Source documentation
Reinsert the support coordinates to recover the original point.
```
theorem support_recover {n : ℕ} (x : StdSimplex ℝ (Fin (n+1))) :
    StdSimplex.map (supportMap x) (supportCoordinates x) = x := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.supportMap, OAI.Thomason.Construction.HornBarycentric.supportCoordinates
theorem OAI.Thomason.Construction.HornBarycentric.support_delete line 345
Source documentation
A face chart receives exactly the support coordinates via its face map.
```
theorem support_delete {n : ℕ} (x : StdSimplex ℝ (Fin (n+2))) (j : Fin (n+2)) :
    StdSimplex.map ((deletion j).comp (supportMap x).toOrderHom) (supportCoordinates x) =
      StdSimplex.map (deletion j) x := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.deletion, OAI.Thomason.Construction.HornBarycentric.supportMap, OAI.Thomason.Construction.HornBarycentric.supportCoordinates
theorem OAI.Thomason.Construction.HornBarycentric.supportMap_range line 367
theorem OAI.Thomason.Construction.HornBarycentric.support_map line 371
theorem OAI.Thomason.Construction.HornBarycentric.map_supportMap_mem line 376
def OAI.Thomason.Construction.HornBarycentric.supportOrdinal line 383
Source documentation
Restriction of an ordinal map to the ordered supports of a barycentric point and its image.
```
def supportOrdinal {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (x : StdSimplex ℝ (Fin (m+1))) :
    Fin (supportLen x+1) →o Fin (supportLen (StdSimplex.map f x)+1) where
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.supportLen
theorem OAI.Thomason.Construction.HornBarycentric.supportOrdinal_commutes line 401
Source documentation
The support square commutes even when the original operator is degenerate.
```
theorem supportOrdinal_commutes {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (x : StdSimplex ℝ (Fin (m+1))) (k : Fin (supportLen x+1)) :
    supportMap (StdSimplex.map f x) (supportOrdinal f x k) = f (supportMap x k) := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.supportLen, OAI.Thomason.Construction.HornBarycentric.supportMap, OAI.Thomason.Construction.HornBarycentric.supportOrdinal
theorem OAI.Thomason.Construction.HornBarycentric.supportOrdinal_surjective line 410
Source documentation
Every supported target vertex comes from a supported source vertex.
```
theorem supportOrdinal_surjective {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (x : StdSimplex ℝ (Fin (m+1))) : Function.Surjective (supportOrdinal f x) := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.supportOrdinal
theorem OAI.Thomason.Construction.HornBarycentric.supportCoordinates_naturality line 424
Source documentation
Coordinates on the ordered support commute with the induced support operator.
```
theorem supportCoordinates_naturality {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (x : StdSimplex ℝ (Fin (m+1))) :
    StdSimplex.map (supportOrdinal f x) (supportCoordinates x) =
      supportCoordinates (StdSimplex.map f x) := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.supportOrdinal, OAI.Thomason.Construction.HornBarycentric.supportCoordinates
abbrev OAI.Thomason.Construction.HornBarycentric.faceIndex line 456
Source documentation
An actual codimension-one simplex of the horn.
```
abbrev faceIndex {n : ℕ} (i j : Fin (n+2)) (hj : j ≠ i) :
    CostructuredArrow SSet.stdSimplex (Λ[n+1, i] : SSet.{0}) :=
…
```
def OAI.Thomason.Construction.HornBarycentric.supportHom line 461
Source documentation
The simplex on the ordered support of a point of the geometric horn.
```
def supportHom {n : ℕ} (i : Fin (n+2)) (x : horn i) :
    (Δ[supportLen x.val] : SSet.{0}) ⟶ Λ[n+1, i] :=
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.horn, OAI.Thomason.Construction.HornBarycentric.supportLen
abbrev OAI.Thomason.Construction.HornBarycentric.supportIndex line 473
def OAI.Thomason.Construction.HornBarycentric.supportToFace line 478
Source documentation
Support inclusion factors through every zero-coordinate face.
```
def supportToFace {n : ℕ} (i j : Fin (n+2)) (hj : j ≠ i)
    (x : horn i) (hx : x.val.weights j = 0) : supportIndex i x ⟶ faceIndex i j hj :=
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.horn, OAI.Thomason.Construction.HornBarycentric.supportIndex, OAI.Thomason.Construction.HornBarycentric.faceIndex
def OAI.Thomason.Construction.HornBarycentric.faceValue line 496
Source documentation
The local chart on a chosen zero coordinate, with values in the actual realization.
```
def faceValue {n : ℕ} (i j : Fin (n+2)) (hj : j ≠ i)
    (x : StdSimplex ℝ (Fin (n+2))) : SSet.toTop.obj (Λ[n+1, i] : SSet.{0}) :=
…
```
theorem OAI.Thomason.Construction.HornBarycentric.faceValue_support line 502
Source documentation
All face charts take the canonical support value wherever they apply.
```
theorem faceValue_support {n : ℕ} (i j : Fin (n+2)) (hj : j ≠ i)
    (x : horn i) (hx : x.val.weights j = 0) :
    faceValue i j hj x.val =
      (RealizationPrism.leg (Λ[n+1, i] : SSet.{0}) (supportIndex i x)).hom
        (ULift.up (supportCoordinates x.val)) := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.horn, OAI.Thomason.Construction.HornBarycentric.faceValue, OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.HornBarycentric.supportIndex, OAI.Thomason.Construction.HornBarycentric.supportCoordinates
theorem OAI.Thomason.Construction.HornBarycentric.faceValue_overlap line 516
Source documentation
The local face charts agree on every intersection, including degenerate points.
```
theorem faceValue_overlap {n : ℕ} (i j k : Fin (n+2)) (hj : j ≠ i) (hk : k ≠ i)
    (x : StdSimplex ℝ (Fin (n+2))) (hxj : x.weights j = 0) (hxk : x.weights k = 0) :
    faceValue i j hj x = faceValue i k hk x := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.faceValue
def OAI.Thomason.Construction.simplicialPointFiber line 541
Source documentation
The actual simplicial fibre over a vertex, in all degrees.
```
def simplicialPointFiber {E B : SSet.{0}} (p : E ⟶ B) (b : B _⦋0⦌) : E.Subcomplex :=
…
```
theorem OAI.Thomason.Construction.simplicialPointFiber_ι_comp line 545
def OAI.Thomason.Construction.simplicialPointFiberLift line 552
Source documentation
A map with constant projection factors through the literal point fibre.
```
def simplicialPointFiberLift {K E B : SSet.{0}} (p : E ⟶ B) (b : B _⦋0⦌)
    (f : K ⟶ E) (hf : f ≫ p = SSet.const b) : K ⟶ (simplicialPointFiber p b).toSSet :=
…
```
Mentions: OAI.Thomason.Construction.simplicialPointFiber
theorem OAI.Thomason.Construction.simplicialPointFiberLift_ι line 562

theorem OAI.Thomason.Construction.kan_fiber_deformation line 569

Source documentation

Lift a 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 {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (b : B _⦋0⦌)
    (H : SSet.Homotopy (𝟙 B) (SSet.const 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 (𝟙 E) (r ≫ (simplicialPointFiber p b).ι),
        (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 line 639
Source documentation
A stationary simplicial deformation gives the actual weak-equivalence statement on realization, without a Kan–Quillen input.
```
theorem simplicial_retraction_weak {A E : SSet.{0}} (i : A ⟶ E) (r : E ⟶ A)
    (hir : i ≫ r = 𝟙 A) (H : SSet.Homotopy (𝟙 E) (r ≫ i)) :
    realizationWeakEquivalences i := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.simplicialPointFiber_kan line 685
Source documentation
A literal vertex fibre of any Kan fibration is a Kan complex. The horn filler has constant projection, so it lies in the same fibre in all degrees.
```
theorem simplicialPointFiber_kan {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (b : B _⦋0⦌) :
    SSet.KanComplex (simplicialPointFiber p b).toSSet := by
…
```
Mentions: OAI.Thomason.Construction.simplicialPointFiber

theorem OAI.Thomason.Construction.kan_lifts_homotopic_relative line 725

Source documentation

Two lifts that agree on an anodyne subobject have a simplicial homotopy over the same base map, stationary on that entire subobject.

theorem kan_lifts_homotopic_relative {A K E B : SSet.{0}} (i : A ⟶ K)
    (hi : SSet.anodyneExtensions i) (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (f g : K ⟶ E) (hfg : f ≫ p = g ≫ p) (hA : i ≫ f = i ≫ g) :
    ∃ H : SSet.Homotopy f g,
      H.h ≫ p = fst K Δ[1] ≫ f ≫ p ∧
      i ▷ Δ[1] ≫ H.h = fst A Δ[1] ≫ i ≫ f := by
…

theorem OAI.Thomason.Construction.kan_product_snd_fibration line 769
Source documentation
Projection of a product with a Kan complex is a Kan fibration.
```
theorem kan_product_snd_fibration (F B : SSet.{0}) [SSet.KanComplex F] :
    HomotopicalAlgebra.Fibration (snd F B) := by
…
```
theorem OAI.Thomason.Construction.ConePrism.liftedBarycentric_zero line 798
Source documentation
The zero endpoint of the barycentric cone is the original last face.
```
theorem liftedBarycentric_zero (n : ℕ) :
    TopologicalInterval.sectionAt (SimplexCategory.toTop.{0}.obj (.mk n)) 0 ≫
      liftedBarycentric n =
    SimplexCategory.toTop.{0}.map (SimplexCategory.Hom.mk Fin.castSuccOrderEmb.toOrderHom) := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.ConePrism.liftedBarycentric
def OAI.Thomason.Construction.ConePrism.vertexPoint line 810
Source documentation
The actual point of the realization represented by the greatest vertex.
```
noncomputable def vertexPoint : SSet.toTop.obj (nerve P) :=
…
```
theorem OAI.Thomason.Construction.ConePrism.piece_zero line 814
Source documentation
Every original simplex is recovered at the zero endpoint.
```
theorem piece_zero (j : CostructuredArrow SSet.stdSimplex (nerve P)) :
    TopologicalInterval.sectionAt ((RealizationPrism.diagram (nerve P)).obj j) 0 ≫
      piece v hv j = RealizationPrism.leg (nerve P) j := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.ConePrism.piece, OAI.Thomason.Construction.RealizationPrism.leg
theorem OAI.Thomason.Construction.ConePrism.leg_final_vertex line 823
Source documentation
The new final vertex of each cone represents the chosen realization point.
```
theorem leg_final_vertex (j : CostructuredArrow SSet.stdSimplex (nerve P)) :
    (RealizationPrism.leg (nerve P) (coneIndex v hv j)).hom
      (ULift.up (.single (Fin.last (j.left.len+1)))) = vertexPoint v := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.ConePrism.coneIndex, OAI.Thomason.Construction.ConePrism.vertexPoint
theorem OAI.Thomason.Construction.ConePrism.piece_one line 834
Source documentation
Every cone piece reaches the same point at the one endpoint.
```
theorem piece_one (j : CostructuredArrow SSet.stdSimplex (nerve P)) :
    TopologicalInterval.sectionAt ((RealizationPrism.diagram (nerve P)).obj j) 1 ≫
      piece v hv j = TopCat.ofHom (ContinuousMap.const _ (vertexPoint v)) := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.ConePrism.piece, OAI.Thomason.Construction.ConePrism.vertexPoint
theorem OAI.Thomason.Construction.ConePrism.leg_cone_vertex_constant line 846
Source documentation
The entire cone simplex on the greatest vertex is constant in realization.
```
theorem leg_cone_vertex_constant
    (x : SimplexCategory.toTop.{0}.obj (.mk 1)) :
    (RealizationPrism.leg (nerve P) (coneIndex v hv (vertexIndex v))).hom x = vertexPoint v := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.ConePrism.coneIndex, OAI.Thomason.Construction.ConePrism.vertexIndex, OAI.Thomason.Construction.ConePrism.vertexPoint
theorem OAI.Thomason.Construction.ConePrism.realizationCone_vertex line 855
Source documentation
The assembled actual cone is stationary on its greatest vertex.
```
theorem realizationCone_vertex (t : unitInterval) :
    (realizationCone v hv).hom (vertexPoint v, t) = vertexPoint v := by
…
```
Mentions: OAI.Thomason.Construction.ConePrism.realizationCone, OAI.Thomason.Construction.ConePrism.vertexPoint
theorem OAI.Thomason.Construction.ConePrism.realized_vertex_constant line 881
Source documentation
The realization of the zero-simplex map is the constant map to its vertex.
```
theorem realized_vertex_constant (x : SSet.toTop.obj (SSet.stdSimplex.obj (.mk 0))) :
    (SSet.toTop.map (vertexIndex v).hom).hom x = vertexPoint v := by
…
```
Mentions: OAI.Thomason.Construction.ConePrism.vertexIndex, OAI.Thomason.Construction.ConePrism.vertexPoint
def OAI.Thomason.Construction.ConePrism.contraction line 890
Source documentation
The actual continuous homotopy from identity to the greatest vertex.
```
noncomputable def contraction :
    (ContinuousMap.id (SSet.toTop.obj (nerve P))).Homotopy
      (ContinuousMap.const _ (vertexPoint v)) :=
…
```
Mentions: OAI.Thomason.Construction.ConePrism.vertexPoint
theorem OAI.Thomason.Construction.ConePrism.greatest_vertex_weak line 902
Source documentation
The actual simplicial inclusion of the greatest vertex is a realization weak equivalence. No model structure or KQ input is used.
```
theorem greatest_vertex_weak : realizationWeakEquivalences (vertexIndex v).hom := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.ConePrism.vertexIndex
theorem OAI.Thomason.Construction.RealizationPrism.isOpen_iff_simplex line 944
Source documentation
Openness in realization is tested on all of its actual simplex maps.
```
theorem isOpen_iff_simplex (K : SSet.{0}) (U : Set (SSet.toTop.obj K)) :
    IsOpen U ↔ ∀ j, IsOpen ((leg K j).hom ⁻¹' U) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.leg
theorem OAI.Thomason.Construction.RealizationPrism.isClosed_iff_simplex line 949
Source documentation
Closedness in realization has the same simplexwise test.
```
theorem isClosed_iff_simplex (K : SSet.{0}) (A : Set (SSet.toTop.obj K)) :
    IsClosed A ↔ ∀ j, IsClosed ((leg K j).hom ⁻¹' A) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.leg
theorem OAI.Thomason.Construction.RealizationPrism.continuous_iff_simplex line 954
Source documentation
The final topology detects continuity of any proposed map out of realization.
```
theorem continuous_iff_simplex (K : SSet.{0}) {Y : Type*} [TopologicalSpace Y]
    (f : SSet.toTop.obj K → Y) :
    Continuous f ↔ ∀ j, Continuous (f ∘ (leg K j).hom) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.leg
abbrev OAI.Thomason.Construction.RealizationPrism.SimplexPoints line 960
Source documentation
The disjoint union of all simplex parameter spaces, with their given topologies.
```
abbrev SimplexPoints (K : SSet.{0}) :=
…
```
def OAI.Thomason.Construction.RealizationPrism.quotientProjection line 964
Source documentation
The canonical map from simplex representatives onto realization.
```
def quotientProjection (K : SSet.{0}) : SimplexPoints K → SSet.toTop.obj K :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.SimplexPoints
theorem OAI.Thomason.Construction.RealizationPrism.quotientProjection_surjective line 967
theorem OAI.Thomason.Construction.RealizationPrism.quotientProjection_isQuotientMap line 974
Source documentation
Geometric realization carries exactly the quotient topology of simplex representatives.
```
theorem quotientProjection_isQuotientMap (K : SSet.{0}) :
    IsQuotientMap (quotientProjection K) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.quotientProjection