HornWeakEquivalences.lean`

59 declarations, 0 contain sorry, 0 declared as axioms

Appended greatest vertices in the ordinary nerve

The cone construction is natural on the actual category of simplices. This supplies the indexing data for the topological cone prisms.

abbrev OAI.Thomason.Construction.ConePrism.coneIndex line 33

Source documentation

Append the greatest vertex to an original nerve simplex.

noncomputable abbrev coneIndex (j : CostructuredArrow SSet.stdSimplex (nerve P)) :
    CostructuredArrow SSet.stdSimplex (nerve P) :=
…

theorem OAI.Thomason.Construction.ConePrism.append_precomp line 39
Source documentation
Appending commutes with all ordinal operators after extending their final vertex.
```
theorem append_precomp {m n : ℕ} (s : Fin (n+1) →o P)
    (f : Fin (m+1) →o Fin (n+1)) :
    (append s v (hv _)).comp (ordinalMap f) = append (s.comp f) v (hv _) := by
…
```
Mentions: OAI.Thomason.Construction.ConePrism.append, OAI.Thomason.Construction.ConePrism.ordinalMap
def OAI.Thomason.Construction.ConePrism.coneMap line 50
Source documentation
The actual map of cone simplices extending an original simplex morphism.
```
noncomputable def coneMap {j k : CostructuredArrow SSet.stdSimplex (nerve P)} (f : j ⟶ k) :
    coneIndex v hv j ⟶ coneIndex v hv k :=
…
```
Mentions: OAI.Thomason.Construction.ConePrism.coneIndex
def OAI.Thomason.Construction.ConePrism.faceMap line 64
Source documentation
The original simplex includes as the face omitting the new final vertex.
```
noncomputable def faceMap (j : CostructuredArrow SSet.stdSimplex (nerve P)) :
    j ⟶ coneIndex v hv j :=
…
```
Mentions: OAI.Thomason.Construction.ConePrism.coneIndex
abbrev OAI.Thomason.Construction.ConePrism.vertexIndex line 80
Source documentation
The chosen greatest vertex, as an actual zero-simplex.
```
noncomputable abbrev vertexIndex : CostructuredArrow SSet.stdSimplex (nerve P) :=
…
```
def OAI.Thomason.Construction.ConePrism.vertexMap line 85
Source documentation
The greatest vertex is the new final vertex of each cone simplex.
```
noncomputable def vertexMap (j : CostructuredArrow SSet.stdSimplex (nerve P)) :
    vertexIndex v ⟶ coneIndex v hv j :=
…
```
Mentions: OAI.Thomason.Construction.ConePrism.vertexIndex, OAI.Thomason.Construction.ConePrism.coneIndex
def OAI.Thomason.Construction.ConePrism.collapseVertex line 96
Source documentation
The cone on the greatest vertex collapses back to that vertex.
```
noncomputable def collapseVertex : coneIndex v hv (vertexIndex v) ⟶ vertexIndex v :=
…
```
Mentions: OAI.Thomason.Construction.ConePrism.coneIndex, OAI.Thomason.Construction.ConePrism.vertexIndex
def OAI.Thomason.Construction.StrictOmegaCategory.liftToLabelFiber line 126
Source documentation
Factor a strict functor whose entire image has a fixed label through the full fibre.
```
def liftToLabelFiber (p : C ⟶ StrictPoset.category (Fin 2)) (e : Fin 2)
    (f : D ⟶ C) (hf : ∀ x, p.toFun (f.toFun x) = StrictPoset.identity e) :
    D ⟶ labelFiber p e where
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictPoset.identity, OAI.Thomason.Construction.StrictOmegaCategory.labelFiber
theorem OAI.Thomason.Construction.StrictOmegaCategory.liftToLabelFiber_inclusion line 133
theorem OAI.Thomason.Construction.StrictOmegaCategory.liftToLabelFiber_precomp line 140
Source documentation
Compatibility of a canonical fibre factor with precomposition, on all cells.
```
theorem liftToLabelFiber_precomp (p : C ⟶ StrictPoset.category (Fin 2)) (e : Fin 2)
    (f : D ⟶ C) (hf : ∀ x, p.toFun (f.toFun x) = StrictPoset.identity e)
    {B : StrictOmegaCategory.{0}} (g : B ⟶ D) :
    g ≫ liftToLabelFiber p e f hf =
      liftToLabelFiber p e (g ≫ f) (fun x => hf (g.toFun x)) := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictPoset.identity, OAI.Thomason.Construction.StrictOmegaCategory.liftToLabelFiber

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetMap_membership_zero line 155

Source documentation

A monotone map landing in the sieve sends every categorified cell into its full zero-fibre.

theorem posetMap_membership_zero {E P : Type} [PartialOrder E] [PartialOrder P]
    (A : Set P) (hA : IsLowerSet A) (f : E →o P) (hf : ∀ x, f x ∈ A)
    (x : h.categorification.obj (nerve E)) :
    (h.membershipLabel A hA).toFun ((h.posetMap f).toFun x) = StrictPoset.identity 0 := by
…

Mentions: OAI.Thomason.Construction.StrictPoset.identity

def OAI.Thomason.Construction.NormalizedSimplexIdentities.posetFiberMap line 166

Source documentation

The canonical strict map into a categorified sieve's actual full fibre.

noncomputable def posetFiberMap {P : Type} [PartialOrder P]
    (A : Set P) (hA : IsLowerSet A) :
    h.categorification.obj (nerve A) ⟶ labelFiber (h.membershipLabel A hA) 0 :=
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetFiberMap_inclusion line 173
Source documentation
The factor is the original inclusion after forgetting the fibre.
```
theorem posetFiberMap_inclusion {P : Type} [PartialOrder P]
    (A : Set P) (hA : IsLowerSet A) :
    h.posetFiberMap A hA ≫ labelFiberInclusion (h.membershipLabel A hA) 0 =
      h.posetMap (subposetInclusion A) := by
…
```
Mentions: OAI.Thomason.Construction.subposetInclusion

theorem OAI.Thomason.Construction.FiniteReflectionInput.posetObjectsEquiv_naturality line 188

Source documentation

Finite object names are natural for the original categorified monotone maps.

theorem posetObjectsEquiv_naturality {E F : Type} [PartialOrder E] [PartialOrder F]
    (f : E →o F) (x : Objects ((r.categorification h).obj (nerve E)).val) :
    r.posetObjectsEquiv h F ((r.reflect.map (h.posetMap f)).toOneFunctor.obj x) =
      f (r.posetObjectsEquiv h E x) := by
…

theorem OAI.Thomason.Construction.FiniteReflectionInput.membershipLabel_zero_iff line 201

Source documentation

The finite-dimensional full zero-fibre criterion holds on every cell.

theorem membershipLabel_zero_iff {E : Type} [PartialOrder E]
    (A : Set E) (hA : IsLowerSet A) (x : ((r.categorification h).obj (nerve E)).val) :
    (r.membershipLabel h A hA).toFun x = StrictPoset.identity 0 ↔
      r.posetObjectsEquiv h E (((r.categorification h).obj (nerve E)).val.boundaryObject false x) ∈ A ∧
      r.posetObjectsEquiv h E (((r.categorification h).obj (nerve E)).val.boundaryObject true x) ∈ A := by
…

Mentions: OAI.Thomason.Construction.StrictPoset.identity

theorem OAI.Thomason.Construction.FiniteReflectionInput.posetMap_membership_zero line 213

Source documentation

Reflected monotone maps landing in a sieve land in its actual full zero-fibre.

theorem posetMap_membership_zero {E P : Type} [PartialOrder E] [PartialOrder P]
    (A : Set P) (hA : IsLowerSet A) (f : E →o P) (hf : ∀ x, f x ∈ A)
    (x : ((r.categorification h).obj (nerve E)).val) :
    (r.membershipLabel h A hA).toFun ((r.reflect.map (h.posetMap f)).toFun x) =
      StrictPoset.identity 0 := by
…

Mentions: OAI.Thomason.Construction.StrictPoset.identity

def OAI.Thomason.Construction.FiniteReflectionInput.posetFiberMap line 230

Source documentation

The corresponding canonical map in the actual positive finite category.

noncomputable def posetFiberMap {P : Type} [PartialOrder P]
    (A : Set P) (hA : IsLowerSet A) :
    (r.categorification h).obj (nerve A) ⟶
      (finiteLabelFiberFunctor n 0).obj (Over.mk (r.membershipLabel h A hA)) :=
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.cosieveMembershipLabel_object line 253

Source documentation

The complement's membership label detects the objects of the cosieve at one.

theorem cosieveMembershipLabel_object {P : Type} [PartialOrder P]
    (A : Set P) (hA : IsUpperSet A) (x : Objects (h.categorification.obj (nerve P))) :
    (h.membershipLabel Aᶜ hA.compl).toFun x.val = StrictPoset.identity 1 ↔
      h.posetObjectsEquiv P x ∈ A := by
…

Mentions: OAI.Thomason.Construction.StrictPoset.identity

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.cosieveMembershipLabel_one_iff line 265
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetMap_cosieveMembership_one line 277
def OAI.Thomason.Construction.NormalizedSimplexIdentities.cosievePosetFiberMap line 287
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.cosievePosetFiberMap_inclusion line 293
def OAI.Thomason.Construction.CosieveSimplex.whole line 316
Source documentation
Every cell of a simplex in the cosieve belongs to its full one fibre.
```
noncomputable def whole {m : ℕ} (s : Fin (m+1) →o A) :
    h.object m ⟶ labelFiber (label A hA ((subposetInclusion A).comp s) h) 1 where
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.label, OAI.Thomason.Construction.subposetInclusion
theorem OAI.Thomason.Construction.CosieveSimplex.whole_cut_clamp line 327
Source documentation
The clamped vertex map of a simplex already in the cosieve is unchanged.
```
theorem whole_cut_clamp {m : ℕ} (s : Fin (m+1) →o A)
    (c : Cut A ((subposetInclusion A).comp s)) : c.clamp = s := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.Cut, OAI.Thomason.Construction.subposetInclusion
theorem OAI.Thomason.Construction.CosieveSimplex.whole_back line 335
Source documentation
On an entire cosieve simplex, the clamping inverse is its original colimit leg.
```
theorem whole_back {m : ℕ} (s : Fin (m+1) →o A) :
    whole A hA h s ≫ back A hA h ((subposetInclusion A).comp s) = h.posetLeg s := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.whole, OAI.Thomason.Construction.CosieveSimplex.back, OAI.Thomason.Construction.subposetInclusion
def OAI.Thomason.Construction.StrictOmegaCategory.maxLabel line 365
Source documentation
Combine the two ordered endpoint labels by maximum.
```
def maxLabel (p q : C ⟶ StrictPoset.category (Fin 2)) :
    C ⟶ StrictPoset.category (Fin 2) where
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.maxLabel_zero_iff line 388
Source documentation
A joint zero label is exactly simultaneous membership in the two fibres.
```
theorem maxLabel_zero_iff (p q : C ⟶ StrictPoset.category (Fin 2)) (x : C) :
    (maxLabel p q).toFun x = StrictPoset.identity 0 ↔
      p.toFun x = StrictPoset.identity 0 ∧ q.toFun x = StrictPoset.identity 0 := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.maxLabel, OAI.Thomason.Construction.StrictPoset.identity
theorem OAI.Thomason.Construction.StrictOmegaCategory.maxLabel_precomp line 412
Source documentation
Joint labels commute with precomposition on every cell.
```
theorem maxLabel_precomp (p q : C ⟶ StrictPoset.category (Fin 2)) (f : D ⟶ C) :
    f ≫ maxLabel p q = maxLabel (f ≫ p) (f ≫ q) := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.maxLabel
def OAI.Thomason.Construction.StrictOmegaCategory.maxLabelFiberIso line 418
Source documentation
The joint zero-fibre is the original full intersection.
```
def maxLabelFiberIso (p q : C ⟶ StrictPoset.category (Fin 2)) :
    labelFiber (maxLabel p q) 0 ≅
      C.fullOn ({x | p.toFun x = StrictPoset.identity 0} ∩
        {x | q.toFun x = StrictPoset.identity 0}) where
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.labelFiber, OAI.Thomason.Construction.StrictOmegaCategory.maxLabel, OAI.Thomason.Construction.StrictPoset.identity
theorem OAI.Thomason.Construction.StrictOmegaCategory.maxLabelFiberIso_inclusion line 438
Source documentation
The intersection identification preserves the original full inclusion.
```
theorem maxLabelFiberIso_inclusion (p q : C ⟶ StrictPoset.category (Fin 2)) :
    (maxLabelFiberIso p q).hom ≫ C.fullInclusion
      ({x | p.toFun x = StrictPoset.identity 0} ∩ {x | q.toFun x = StrictPoset.identity 0}) =
      labelFiberInclusion (maxLabel p q) 0 := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.maxLabelFiberIso, OAI.Thomason.Construction.StrictPoset.identity, OAI.Thomason.Construction.StrictOmegaCategory.labelFiberInclusion, OAI.Thomason.Construction.StrictOmegaCategory.maxLabel
theorem OAI.Thomason.Construction.RealizationPrism.point_representation line 458
Source documentation
The topological colimit is also a colimit of underlying sets.
```
theorem point_representation (K : SSet.{0}) (x : SSet.toTop.obj K) :
    ∃ (j : CostructuredArrow SSet.stdSimplex K) (p : (diagram K).obj j),
      (leg K j).hom p = x := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.RealizationPrism.leg
def OAI.Thomason.Construction.RealizationPrism.simplexPoint line 480
Source documentation
The continuous map from the standard barycentric simplex specified by a simplex of K.
```
def simplexPoint (K : SSet.{0}) {n : ℕ} (s : K.obj (.op (.mk n))) :
    C(StdSimplex ℝ (Fin (n+1)), SSet.toTop.obj K) :=
…
```
theorem OAI.Thomason.Construction.RealizationPrism.point_representation_simplex line 485

theorem OAI.Thomason.Construction.RealizationPrism.simplexPoint_map line 498

Source documentation

Evaluation commutes with the affine map of a simplex operator.

theorem simplexPoint_map (K : SSet.{0}) {m n : ℕ}
    (f : SimplexCategory.mk m ⟶ .mk n) (s : K.obj (.op (.mk n)))
    (x : StdSimplex ℝ (Fin (m+1))) :
    simplexPoint K (K.map f.op s) x = simplexPoint K s (StdSimplex.map f.toOrderHom x) := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint

theorem OAI.Thomason.Construction.RealizationPrism.simplexPoint_naturality line 512

Source documentation

Evaluation of a simplex is natural in the simplicial set.

theorem simplexPoint_naturality {K L : SSet.{0}} (f : K ⟶ L) {n : ℕ}
    (s : K.obj (.op (.mk n))) (x : StdSimplex ℝ (Fin (n+1))) :
    (SSet.toTop.map f).hom (simplexPoint K s x) = simplexPoint L (f.app _ s) x := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint

abbrev OAI.Thomason.Construction.RealizationPrism.NondegeneratePoints line 541
Source documentation
The disjoint union of the parameter spaces of nondegenerate simplices.
```
abbrev NondegeneratePoints (K : SSet.{0}) :=
…
```
def OAI.Thomason.Construction.RealizationPrism.nondegenerateProjection line 544
theorem OAI.Thomason.Construction.RealizationPrism.nondegenerateProjection_continuous line 547
theorem OAI.Thomason.Construction.RealizationPrism.nondegenerateProjection_surjective line 554
Source documentation
Every realized point has a representative on a nondegenerate simplex.
```
theorem nondegenerateProjection_surjective (K : SSet.{0}) :
    Function.Surjective (nondegenerateProjection K) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.nondegenerateProjection
theorem OAI.Thomason.Construction.RealizationPrism.compactSpace_of_finite line 563
Source documentation
A simplicial set with finitely many nondegenerate simplices has compact realization.
```
theorem compactSpace_of_finite (K : SSet.{0}) [K.Finite] :
    CompactSpace (SSet.toTop.obj K) := by
…
```
def OAI.Thomason.Construction.RealizedCylinder.piece line 593
Source documentation
The prism on an original simplex, mapped into the global simplicial cylinder.
```
def piece (K : SSet.{0}) (j : CostructuredArrow SSet.stdSimplex K) :
    TopologicalInterval.cylinder.obj ((RealizationPrism.diagram K).obj j) ⟶
      SSet.toTop.obj (K ⊗ Δ[1]) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.diagram
theorem OAI.Thomason.Construction.RealizedCylinder.piece_naturality line 598
def OAI.Thomason.Construction.RealizedCylinder.comparison line 610
Source documentation
The canonical continuous comparison from the topological cylinder to realization of the actual simplicial cylinder.
```
def comparison (K : SSet.{0}) :
    TopologicalInterval.cylinder.obj (SSet.toTop.obj K) ⟶ SSet.toTop.obj (K ⊗ Δ[1]) :=
…
```
theorem OAI.Thomason.Construction.RealizedCylinder.piece_zero line 614
theorem OAI.Thomason.Construction.RealizedCylinder.piece_one line 626
def OAI.Thomason.Construction.RealizedCylinder.homotopy line 639
Source documentation
Realization turns every simplicial homotopy into an actual continuous homotopy.
```
def homotopy {K L : SSet.{0}} {f g : K ⟶ L} (H : SSet.Homotopy f g) :
    (SSet.toTop.map f).hom.Homotopy (SSet.toTop.map g).hom :=
…
```
theorem OAI.Thomason.Construction.RealizedCylinder.weakEquivalence_iff line 650
Source documentation
The actual realization weak-equivalence test is invariant under any simplicial homotopy, independently of Kan–Quillen.
```
theorem weakEquivalence_iff {K L : SSet.{0}} {f g : K ⟶ L} (H : SSet.Homotopy f g) :
    realizationWeakEquivalences f ↔ realizationWeakEquivalences g :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
def OAI.Thomason.Construction.HornContraction.clamp line 676
def OAI.Thomason.Construction.HornContraction.upper line 680
theorem OAI.Thomason.Construction.HornContraction.clamp_le_upper line 683

def OAI.Thomason.Construction.HornContraction.interpolate line 690

Source documentation

The two homotopies from the lower clamping map.

def interpolate {n d : ℕ} (i : Fin (n+2)) (b : Bool)
    (s : Fin (d+1) →o Fin (n+2)) (θ : Fin (d+1) →o Fin 2) :
    Fin (d+1) →o Fin (n+2) :=
…

theorem OAI.Thomason.Construction.HornContraction.interpolate_vertex line 695

theorem OAI.Thomason.Construction.HornContraction.interpolate_mem line 712

Source documentation

Interpolation preserves every missing vertex other than the cone vertex.

theorem interpolate_mem {n : ℕ} (i : Fin (n+2)) (b : Bool)
    {m : SimplexCategoryᵒᵖ} (s : (Λ[n+1, i] : SSet.Subcomplex _).toSSet.obj m)
    (θ : (Δ[1] : SSet.{0}).obj m) :
    SSet.stdSimplex.objEquiv.symm (SimplexCategory.Hom.mk
      (interpolate i b (SSet.stdSimplex.objEquiv s.val).toOrderHom
        (SSet.stdSimplex.objEquiv θ).toOrderHom)) ∈ (Λ[n+1, i] : SSet.Subcomplex _).obj m := by
…

Mentions: OAI.Thomason.Construction.HornContraction.interpolate

def OAI.Thomason.Construction.HornContraction.lowerMap line 731
Source documentation
The lower clamping endomorphism of the horn.
```
def lowerMap {n : ℕ} (i : Fin (n+2)) : (Λ[n+1, i] : SSet.{0}) ⟶ Λ[n+1, i] where
…
```
def OAI.Thomason.Construction.HornContraction.vertex line 741
Source documentation
The cone vertex belongs to every nonempty-dimensional horn.
```
def vertex {n : ℕ} (i : Fin (n+2)) : (Λ[n+1, i] : SSet.{0}) _⦋0⦌ :=
…
```
def OAI.Thomason.Construction.HornContraction.homotopy line 750
Source documentation
The horn contracts to its cone vertex through two simplicial homotopies.
```
def homotopy {n : ℕ} (i : Fin (n+2)) (b : Bool) :
    SSet.Homotopy (lowerMap i) (if b then SSet.const (vertex i) else 𝟙 _) where
…
```
Mentions: OAI.Thomason.Construction.HornContraction.lowerMap, OAI.Thomason.Construction.HornContraction.vertex
theorem OAI.Thomason.Construction.HornContraction.toPoint_weak line 805
Source documentation
The projection of a positive-dimensional horn to a point is weak.
```
theorem toPoint_weak {n : ℕ} (i : Fin (n+2)) :
    realizationWeakEquivalences
      (SSet.stdSimplex.isTerminalObj₀.from (Λ[n+1, i] : SSet.{0})) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.realization_horn_weak line 836
Source documentation
Every positive-dimensional horn inclusion satisfies the actual weak test.
```
theorem realization_horn_weak {n : ℕ} [NeZero n] (i : Fin (n+1)) :
    realizationWeakEquivalences (Λ[n, i].ι : _ ⟶ (Δ[n] : SSet.{0})) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.horn_generators_weak line 849
Source documentation
The full family of generating anodyne maps lies in the semantic weak class.
```
theorem horn_generators_weak :
    SSet.modelCategoryQuillen.J.{0} ≤ realizationWeakEquivalences := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences