SkeletalWeakEquivalences.lean`

77 declarations, 0 contain sorry, 0 declared as axioms

Natural barycentric coordinates on the vertices of a simplicial set

def OAI.Thomason.Construction.RealizationPrism.vertexOperator line 29
theorem OAI.Thomason.Construction.RealizationPrism.vertexOperator_comp line 32
def OAI.Thomason.Construction.RealizationPrism.simplexVertex line 39
theorem OAI.Thomason.Construction.RealizationPrism.simplexVertex_map line 43
theorem OAI.Thomason.Construction.RealizationPrism.simplexVertex_naturality line 50
def OAI.Thomason.Construction.RealizationPrism.simplexVertexCoordinates line 56
Source documentation
Repeated vertices receive the sum of their barycentric coordinates.
```
def simplexVertexCoordinates (K : SSet.{0}) {n : ℕ} (s : K.obj (.op (.mk n))) :
    C(StdSimplex ℝ (Fin (n+1)), StdSimplex ℝ (K.obj (.op (.mk 0)))) :=
…
```
theorem OAI.Thomason.Construction.RealizationPrism.simplexVertexCoordinates_map line 60
theorem OAI.Thomason.Construction.RealizationPrism.simplexVertexCoordinates_naturality line 72
def OAI.Thomason.Construction.RealizationPrism.vertexCoordinateCocone line 100
def OAI.Thomason.Construction.RealizationPrism.vertexCoordinates line 118
Source documentation
The barycentric mass at each vertex, with repeated vertices combined. The target has finite support even when K has infinitely many vertices.
```
def vertexCoordinates (K : SSet.{0}) :
    C(SSet.toTop.obj K, StdSimplex ℝ (K.obj (.op (.mk 0)))) :=
…
```
theorem OAI.Thomason.Construction.RealizationPrism.vertexCoordinates_leg line 122
theorem OAI.Thomason.Construction.RealizationPrism.vertexCoordinates_simplexPoint line 128
theorem OAI.Thomason.Construction.RealizationPrism.vertexCoordinates_naturality line 137
Source documentation
Vertex coordinates commute with every actual simplicial map.
```
theorem vertexCoordinates_naturality {K L : SSet.{0}} (f : K ⟶ L)
    (x : SSet.toTop.obj K) :
    vertexCoordinates L ((SSet.toTop.map f).hom x) =
      StdSimplex.map (f.app (.op (.mk 0))) (vertexCoordinates K x) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexCoordinates
def OAI.Thomason.Construction.RealizationPrism.vertexStar line 166
theorem OAI.Thomason.Construction.RealizationPrism.vertexStar_isOpen line 169
theorem OAI.Thomason.Construction.RealizationPrism.vertexStar_cover line 175
Source documentation
Every point lies in the star of one of its positive-mass vertices.
```
theorem vertexStar_cover (K : SSet.{0}) : ⋃ v, vertexStar K v = Set.univ := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexStar
theorem OAI.Thomason.Construction.RealizationPrism.simplexPoint_mem_vertexStar_iff line 192
Source documentation
On each characteristic simplex, the star criterion is exactly that some positive coordinate is assigned to the indicated vertex.
```
theorem simplexPoint_mem_vertexStar_iff (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) (p : StdSimplex ℝ (Fin (n+1)))
    (v : K.obj (.op (.mk 0))) :
    simplexPoint K s p ∈ vertexStar K v ↔
      ∃ i, 0 < p.weights i ∧ simplexVertex K s i = v := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint, OAI.Thomason.Construction.RealizationPrism.vertexStar, OAI.Thomason.Construction.RealizationPrism.simplexVertex

def OAI.Thomason.Construction.realizedHomotopyEquivOfSimplicial line 234

Source documentation

The specified simplicial homotopy inverses realize to actual continuous homotopy inverses, with those same forward and inverse maps.

def realizedHomotopyEquivOfSimplicial {X Y : SSet.{0}} (f : X ⟶ Y) (g : Y ⟶ X)
    (H : SSet.Homotopy (𝟙 X) (f ≫ g)) (K : SSet.Homotopy (𝟙 Y) (g ≫ f)) :
    ContinuousMap.HomotopyEquiv (SSet.toTop.obj X) (SSet.toTop.obj Y) where
…

theorem OAI.Thomason.Construction.simplicial_homotopy_inverse_weak_pair line 246
Source documentation
A constructed simplicial homotopy inverse gives the full actual weak homotopy-equivalence test, independently of the Kan–Quillen model input.
```
theorem simplicial_homotopy_inverse_weak_pair {X Y : SSet.{0}} (f : X ⟶ Y) (g : Y ⟶ X)
    (H : SSet.Homotopy (𝟙 X) (f ≫ g)) (K : SSet.Homotopy (𝟙 Y) (g ≫ f)) :
    realizationWeakEquivalences f ∧ realizationWeakEquivalences g :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

def OAI.Thomason.Construction.overBaseChangeMap line 270

Source documentation

The actual pullback map of a morphism over a fixed base.

def overBaseChangeMap {E F A B : SSet.{0}} (p : E ⟶ B) (q : F ⟶ B) (g : A ⟶ B)
    (f : E ⟶ F) (hf : f ≫ q = p) : pullback p g ⟶ pullback q g :=
…

theorem OAI.Thomason.Construction.overBaseChangeMap_fst line 275
theorem OAI.Thomason.Construction.overBaseChangeMap_snd line 280
theorem OAI.Thomason.Construction.overBaseChangeMap_id line 285
theorem OAI.Thomason.Construction.overBaseChangeMap_comp line 290

def OAI.Thomason.Construction.overBaseChangeHomotopy line 301

Source documentation

A homotopy over the base pulls back to an actual simplicial homotopy. It does not require a fibration or preservation of pullbacks by realization.

def overBaseChangeHomotopy {E F A B : SSet.{0}}
    (p : E ⟶ B) (q : F ⟶ B) (g : A ⟶ B) {f₀ f₁ : E ⟶ F}
    (h₀ : f₀ ≫ q = p) (h₁ : f₁ ≫ q = p) (H : SSet.Homotopy f₀ f₁)
    (hH : H.h ≫ q = fst E Δ[1] ≫ p) :
    SSet.Homotopy (overBaseChangeMap p q g f₀ h₀) (overBaseChangeMap p q g f₁ h₁) := by
…

Mentions: OAI.Thomason.Construction.overBaseChangeMap

theorem OAI.Thomason.Construction.overBaseChange_homotopy_inverse_weak line 353

Source documentation

Fibrewise simplicial homotopy inverses stay inverse after arbitrary base change, hence their actual base-change maps are weak equivalences.

theorem overBaseChange_homotopy_inverse_weak {E F A B : SSet.{0}}
    (p : E ⟶ B) (q : F ⟶ B) (g : A ⟶ B)
    (f : E ⟶ F) (r : F ⟶ E) (hf : f ≫ q = p) (hr : r ≫ p = q)
    (H : SSet.Homotopy (𝟙 E) (f ≫ r)) (K : SSet.Homotopy (𝟙 F) (r ≫ f))
    (hH : H.h ≫ p = fst E Δ[1] ≫ p) (hK : K.h ≫ q = fst F Δ[1] ≫ q) :
    realizationWeakEquivalences (overBaseChangeMap p q g f hf) ∧
      realizationWeakEquivalences (overBaseChangeMap q p g r hr) := by
…

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

def OAI.Thomason.Construction.naturalTransformationPrism line 392
theorem OAI.Thomason.Construction.naturalTransformationPrism_zero line 395
theorem OAI.Thomason.Construction.naturalTransformationPrism_one line 405
def OAI.Thomason.Construction.nerveNaturalHomotopy line 416
Source documentation
A natural transformation gives an actual simplicial interval homotopy.
```
def nerveNaturalHomotopy (α : F ⟶ G) :
    SSet.Homotopy (nerveMap F) (nerveMap G) where
…
```
theorem OAI.Thomason.Construction.nerveNaturalHomotopy_weak_iff line 450
Source documentation
Natural transformations preserve the actual realization weak test.
```
theorem nerveNaturalHomotopy_weak_iff (α : F ⟶ G) :
    realizationWeakEquivalences (nerveMap F) ↔ realizationWeakEquivalences (nerveMap G) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
def OAI.Thomason.Construction.FaceSimplexResolution.Append.semiMap line 477
theorem OAI.Thomason.Construction.FaceSimplexResolution.Append.semiMap_castSucc line 483
theorem OAI.Thomason.Construction.FaceSimplexResolution.Append.semiMap_last line 490
theorem OAI.Thomason.Construction.FaceSimplexResolution.Append.semiMap_id line 495
theorem OAI.Thomason.Construction.FaceSimplexResolution.Append.semiMap_comp line 505
abbrev OAI.Thomason.Construction.FaceSimplexResolution.Append.object line 517
def OAI.Thomason.Construction.FaceSimplexResolution.Append.operator line 522
theorem OAI.Thomason.Construction.FaceSimplexResolution.Append.operator_naturality line 525
def OAI.Thomason.Construction.FaceSimplexResolution.Append.appendedOperator line 529
abbrev OAI.Thomason.Construction.FaceSimplexResolution.Append.appendedObject line 534
def OAI.Thomason.Construction.FaceSimplexResolution.Append.homOfSemi line 537
theorem OAI.Thomason.Construction.FaceSimplexResolution.Append.homOfSemi_projection line 547
theorem OAI.Thomason.Construction.FaceSimplexResolution.Append.hom_ext line 553
theorem OAI.Thomason.Construction.FaceSimplexResolution.Append.appendedOperator_naturality line 560
def OAI.Thomason.Construction.FaceSimplexResolution.Append.appendedMap line 587
def OAI.Thomason.Construction.FaceSimplexResolution.Append.functor line 591
def OAI.Thomason.Construction.FaceSimplexResolution.Append.prefixSemi line 606
def OAI.Thomason.Construction.FaceSimplexResolution.Append.prefixMap line 609
theorem OAI.Thomason.Construction.FaceSimplexResolution.Append.prefixSemi_naturality line 618
def OAI.Thomason.Construction.FaceSimplexResolution.Append.prefixTransformation line 627
def OAI.Thomason.Construction.FaceSimplexResolution.Append.finalObject line 637
def OAI.Thomason.Construction.FaceSimplexResolution.Append.finalSemi line 640
def OAI.Thomason.Construction.FaceSimplexResolution.Append.finalMap line 648
theorem OAI.Thomason.Construction.FaceSimplexResolution.Append.finalSemi_naturality line 658
def OAI.Thomason.Construction.FaceSimplexResolution.Append.finalTransformation line 667
theorem OAI.Thomason.Construction.FaceSimplexResolution.Append.collapse_weak line 678
Source documentation
The point collapse of the actual resolution of a standard simplex is weak.
```
theorem collapse_weak (n : SimplexCategory) :
    realizationWeakEquivalences
      (SSet.stdSimplex.isTerminalObj₀.from (nerve (Face (SSet.stdSimplex.obj n)))) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.FaceSimplexResolution.Face
theorem OAI.Thomason.Construction.FaceSimplexResolution.augmentation_standard_weak line 711
Source documentation
The resolution augmentation is weak on every representable, including all degenerate faces in its face-simplex category.
```
theorem augmentation_standard_weak (n : SimplexCategory) :
    realizationWeakEquivalences (augmentation (SSet.stdSimplex.obj n)) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.FaceSimplexResolution.augmentation
theorem OAI.Thomason.Construction.NonsingularLastVertex.faceUnion_eq_of_greatest line 747
theorem OAI.Thomason.Construction.NonsingularLastVertex.greatest_collapse_weak line 755
Source documentation
The actual collapse from any nerve with a greatest element is weak.
```
theorem greatest_collapse_weak (P : Type) [PartialOrder P]
    (m : P) (hm : ∀ p, p ≤ m) :
    realizationWeakEquivalences (SSet.stdSimplex.isTerminalObj₀.from (nerve P)) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.NonsingularLastVertex.restrictedMap_weak_of_greatest line 780
Source documentation
The comparison is weak over every collection with a greatest face.
```
theorem restrictedMap_weak_of_greatest (S : Set X.N) (m : S)
    (hm : ∀ s : S, s ≤ m) : realizationWeakEquivalences (restrictedMap S) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.NonsingularLastVertex.restrictedMap
theorem OAI.Thomason.Construction.NonsingularLastVertex.restrictedMap_weak_of_empty line 796
theorem OAI.Thomason.Construction.SimplicialSpan.Cofibration.comp line 830
Source documentation
Composition of relative cofibrations follows from the explicit second pushout square, applied with C equal to the final A.
```
theorem Cofibration.comp {X Y Z : Diagram} {f : X ⟶ Y} {g : Y ⟶ Z}
    (hf : Cofibration f) (hg : Cofibration g) (kq : KanQuillenPublishedInput.{0}) :
    Cofibration (f ≫ g) := by
…
```
Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram, OAI.Thomason.Construction.SimplicialSpan.Cofibration
abbrev OAI.Thomason.Construction.SimplicialSpan.sum line 863
Source documentation
Pointwise coproduct of the two spans.
```
noncomputable abbrev sum (X Y : Diagram) : Diagram where
…
```
Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram
abbrev OAI.Thomason.Construction.SimplicialSpan.inl line 870
abbrev OAI.Thomason.Construction.SimplicialSpan.inr line 873
def OAI.Thomason.Construction.SimplicialSpan.desc line 876
theorem OAI.Thomason.Construction.SimplicialSpan.inl_desc line 881
theorem OAI.Thomason.Construction.SimplicialSpan.inr_desc line 889
theorem OAI.Thomason.Construction.SimplicialSpan.inl_relative_isPushout line 910
theorem OAI.Thomason.Construction.SimplicialSpan.inr_relative_isPushout line 936
theorem OAI.Thomason.Construction.SimplicialSpan.inl_cofibration line 964
Source documentation
The other summand needs a monomorphic left leg; there is no restriction on either right leg.
```
theorem inl_cofibration (X Y : Diagram) [Mono Y.left]
    (kq : KanQuillenPublishedInput.{0}) : Cofibration (inl X Y) := by
…
```
Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram, OAI.Thomason.Construction.SimplicialSpan.Cofibration, OAI.Thomason.Construction.SimplicialSpan.inl
theorem OAI.Thomason.Construction.SimplicialSpan.inr_cofibration line 976
theorem OAI.Thomason.Construction.RealizationPrism.image_skeleton_le line 1003
Source documentation
A simplicial map carries the actual n-skeleton into the n-skeleton.
```
theorem image_skeleton_le {K L : SSet.{0}} (f : K ⟶ L) (n : ℕ) :
    (K.skeleton n).image f ≤ L.skeleton n := by
…
```
def OAI.Thomason.Construction.RealizationPrism.skeletalMap line 1013
Source documentation
The induced map of skeletal subcomplexes, with its literal inclusion square rather than an unspecified comparison isomorphism.
```
def skeletalMap {K L : SSet.{0}} (f : K ⟶ L) (n : ℕ) :
    (K.skeleton n : SSet) ⟶ (L.skeleton n : SSet) :=
…
```
theorem OAI.Thomason.Construction.RealizationPrism.skeletalMap_inclusion line 1017
theorem OAI.Thomason.Construction.RealizationPrism.realization_weak_of_skeletal line 1022
Source documentation
Stagewise skeletal comparison suffices for all actual homotopy groups, without a Kan assumption on either simplicial set.
```
theorem realization_weak_of_skeletal {K L : SSet.{0}} (f : K ⟶ L)
    (hf : ∀ n, realizationWeakEquivalences (skeletalMap f n)) :
    realizationWeakEquivalences f :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.RealizationPrism.skeletalMap