RealizedSimplexWeakEquivalences.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Choosing the decomposition level of a generated expression

The second-highest generator occurrence determines the normalization level in Steiner 2004, Proposition 4.2. Multiplicity is retained: two occurrences of the same generator count as two occurrences.

def OAI.Thomason.Construction.StrictOmegaCategory.ExpressionDegree.highCount line 25
Source documentation
Number of generator occurrences strictly above the chosen level.
```
def highCount (d : I → ℕ) (r : ℕ) (xs : List I) : ℕ :=
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.ExpressionDegree.maximum line 29
Source documentation
A finite upper bound for every generator occurrence.
```
def maximum (d : I → ℕ) : List I → ℕ
  | [] => 0
  | i :: xs => max (d i) (maximum d xs)
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.ExpressionDegree.le_maximum line 33
theorem OAI.Thomason.Construction.StrictOmegaCategory.ExpressionDegree.highCount_append line 42
theorem OAI.Thomason.Construction.StrictOmegaCategory.ExpressionDegree.highCount_zero line 46
theorem OAI.Thomason.Construction.StrictOmegaCategory.ExpressionDegree.exists_critical_level line 56
Source documentation
The critical level has at least two higher occurrences, and at most one occurrence strictly above its successor.
```
theorem exists_critical_level (d : I → ℕ) (xs : List I) (n : ℕ)
    (hn : 2 ≤ highCount d n xs) :
    ∃ r, n ≤ r ∧ 2 ≤ highCount d r xs ∧ highCount d (r+1) xs ≤ 1 := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.ExpressionDegree.highCount
theorem OAI.Thomason.Construction.StrictOmegaCategory.comp_eq_left_of_dimensionLE line 96

inductive OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression line 104

Source documentation

A generated expression with every identity factor removed.

inductive EssentialExpression (C : StrictOmegaCategory.{0}) {I : Type} (g : I → C) :
    C → Type
  | generator (i : I) : EssentialExpression C g (g i)
  | comp {x y : C} (r : ℕ) (hxy : C.target r x = C.source r y)
      (tx : EssentialExpression C g x) (ty : EssentialExpression C g y)
      (hx : ¬ C.DimensionLE r x) (hy : ¬ C.DimensionLE r y) :
      EssentialExpression C g (C.comp r x y hxy)

namespace EssentialExpression

def OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression.expression line 114
def OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression.levelsLE line 119
Source documentation
Every internal composition level is at most the given bound.
```
def levelsLE (r : ℕ) {x : C} : EssentialExpression C g x → Prop
  | .generator _ => True
  | .comp n _ tx ty _ _ => n ≤ r ∧ tx.levelsLE r ∧ ty.levelsLE r

end EssentialExpression

namespace CompositionExpression

/-- Unit laws remove all inessential composition nodes. -/
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression, OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression
theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression.exists_essential line 128
Source documentation
Unit laws remove all inessential composition nodes.
```
theorem exists_essential {x : C} (t : CompositionExpression C g x) :
    Nonempty (EssentialExpression C g x) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression, OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression
theorem OAI.Thomason.Construction.StrictOmegaCategory.ExpressionDegree.highCount_eq_zero_iff line 148
theorem OAI.Thomason.Construction.StrictOmegaCategory.ExpressionDegree.highCount_pos_of_not_dimensionLE line 153
theorem OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression.levelsLE_of_highCount line 169
Source documentation
With at most one generator above r+1, essential compositions occur only at levels at most r.
```
theorem levelsLE_of_highCount (d : I → ℕ)
    (hg : ∀ i, C.DimensionLE (d i) (g i)) {x : C}
    (t : EssentialExpression C g x) (r : ℕ)
    (hcount : highCount d (r+1) t.expression.labels ≤ 1) : t.levelsLE r := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression
theorem OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression.generator_or_critical line 193
Source documentation
A nongenerator essential expression has a critical level with at least two higher occurrences, at most one above the next level, and no composition above the critical level.
```
theorem generator_or_critical (d : I → ℕ)
    (hg : ∀ i, C.DimensionLE (d i) (g i)) {x : C}
    (t : EssentialExpression C g x) :
    (∃ i, x = g i) ∨ ∃ r,
      2 ≤ highCount d r t.expression.labels ∧
      highCount d (r+1) t.expression.labels ≤ 1 ∧ t.levelsLE r := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression

inductive OAI.Thomason.Construction.StrictOmegaCategory.HighGeneratorString line 234

Source documentation

An r-string with exactly one generator of degree greater than r in each factor. Its length is retained for the normalization induction.

inductive HighGeneratorString (C : StrictOmegaCategory.{0}) {I : Type}
    (g : I → C) (d : I → ℕ) (r : ℕ) : C → ℕ → Prop
  | singleton {x : C} (t : CompositionExpression C g x)
      (ht : highCount d r t.labels = 1) : HighGeneratorString C g d r x 1
  | cons {x y : C} {n : ℕ} (t : CompositionExpression C g x)
      (ht : highCount d r t.labels = 1)
      (tail : HighGeneratorString C g d r y n)
      (hxy : C.target r x = C.source r y) :
      HighGeneratorString C g d r (C.comp r x y hxy) (n+1)

namespace HighGeneratorString
…

Mentions: OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression

theorem OAI.Thomason.Construction.StrictOmegaCategory.HighGeneratorString.length_pos line 248
theorem OAI.Thomason.Construction.StrictOmegaCategory.HighGeneratorString.exists_list line 252
Source documentation
Forgetting the expressions gives a literal strict composite list.
```
theorem exists_list {x : C} {n : ℕ} (h : HighGeneratorString C g d r x n) :
    ∃ xs : List C, xs.length = n ∧ CompositeList C r xs x ∧
      ∀ y ∈ xs, ∃ t : CompositionExpression C g y, highCount d r t.labels = 1 := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.HighGeneratorString, OAI.Thomason.Construction.StrictOmegaCategory.CompositeList, OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression
theorem OAI.Thomason.Construction.StrictOmegaCategory.HighGeneratorString.append line 268
Source documentation
Concatenation retains the one-generator condition on each factor.
```
theorem append {x y : C} {n m : ℕ}
    (hx : HighGeneratorString C g d r x n)
    (hy : HighGeneratorString C g d r y m)
    (hxy : C.target r x = C.source r y) :
    HighGeneratorString C g d r (C.comp r x y hxy) (n+m) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.HighGeneratorString
theorem OAI.Thomason.Construction.StrictOmegaCategory.HighGeneratorString.whisker_right line 287
Source documentation
Right whiskering by an r-dimensional expression distributes over an r-string and introduces no higher generator.
```
theorem whisker_right {x y : C} {n m : ℕ}
    (hx : HighGeneratorString C g d r x n)
    (ty : CompositionExpression C g y)
    (hty : highCount d r ty.labels = 0) (hy : C.DimensionLE r y)
    (hmr : m < r) (hxy : C.target m x = C.source m y) :
    HighGeneratorString C g d r (C.comp m x y hxy) n := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.HighGeneratorString, OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression
theorem OAI.Thomason.Construction.StrictOmegaCategory.HighGeneratorString.whisker_left line 328
Source documentation
Left whiskering by an r-dimensional expression likewise preserves the number and higher-generator content of the factors.
```
theorem whisker_left {x y : C} {n m : ℕ}
    (ty : HighGeneratorString C g d r y n)
    (tx : CompositionExpression C g x)
    (htx : highCount d r tx.labels = 0) (hx : C.DimensionLE r x)
    (hmr : m < r) (hxy : C.target m x = C.source m y) :
    HighGeneratorString C g d r (C.comp m x y hxy) n := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.HighGeneratorString, OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression

def OAI.Thomason.Construction.DirectedComplex.RightCylinder.intervalCellTable line 386

Source documentation

The full table of the tensor of a globular cell with the oriented edge.

def intervalCellTable (x : Cell K) (a : Bool) : (n : ℕ) → (rightCylinder K).group n
  | 0 => if a then (0, x.table a 0) else (x.table a 0, 0)
  | n + 1 =>
      if Even n then
        if a then (x.table a (n + 1), 0, x.table a n)
        else (0, x.table a (n + 1), x.table a n)
      else
        if a then (0, x.table a (n + 1), x.table a n)
        else (x.table a (n + 1), 0, x.table a n)

/-- The alternating endpoint table has the required tensor differential. -/

Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.RightCylinder.group, OAI.Thomason.Construction.DirectedComplex.RightCylinder.endpoint

theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.intervalCellTable_boundary line 397
Source documentation
The alternating endpoint table has the required tensor differential.
```
theorem intervalCellTable_boundary (x : Cell K) (a : Bool) (n : ℕ) :
    (rightCylinder K).differential n (intervalCellTable x a (n + 1)) =
      intervalCellTable x true n - intervalCellTable x false n := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.RightCylinder.differential, OAI.Thomason.Construction.DirectedComplex.RightCylinder.intervalCellTable
def OAI.Thomason.Construction.DirectedComplex.RightCylinder.intervalCell line 426
Source documentation
Tensoring a cell with the edge produces an actual positive globular cell.
```
def intervalCell (x : Cell K) : Cell (rightCylinder K) where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.rightCylinder
theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.intervalCell_source line 457
Source documentation
The source is the initial endpoint applied to the old source.
```
theorem intervalCell_source (x : Cell K) :
    (intervalCell x).face false 0 = Cell.map (endpoint K false) (x.face false 0) := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.RightCylinder.intervalCell, OAI.Thomason.Construction.DirectedComplex.Cell.map, OAI.Thomason.Construction.DirectedComplex.RightCylinder.endpoint
theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.intervalCell_target line 469
Source documentation
The target is the final endpoint applied to the old target.
```
theorem intervalCell_target (x : Cell K) :
    (intervalCell x).face true 0 = Cell.map (endpoint K true) (x.face true 0) := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.RightCylinder.intervalCell, OAI.Thomason.Construction.DirectedComplex.Cell.map, OAI.Thomason.Construction.DirectedComplex.RightCylinder.endpoint
def OAI.Thomason.Construction.PointedHomotopyGroups.pointedRetractArrow line 502
instance OAI.Thomason.Construction.(instance at line 524) line 524
Source documentation
Weak equivalences of spaces are closed under retracts, for their actual component and based homotopy-group definition.
```
instance : topologicalWeakEquivalences.{u}.IsStableUnderRetracts where
…
```
instance OAI.Thomason.Construction.(instance at line 546) line 546
Source documentation
The same unconditional retract law holds for geometric realizations.
```
instance : realizationWeakEquivalences.{u}.IsStableUnderRetracts :=
…
```
theorem OAI.Thomason.Construction.IsWeakHomotopyEquivalence.of_postcomp line 573
theorem OAI.Thomason.Construction.IsWeakHomotopyEquivalence.of_precomp_of_surjective line 582
instance OAI.Thomason.Construction.(instance at line 595) line 595
instance OAI.Thomason.Construction.(instance at line 599) line 599

theorem OAI.Thomason.Construction.topologicalWeakEquivalences_of_precomp_of_surjective line 607

Source documentation

A weak surjective continuous map can be cancelled on the source side.

theorem topologicalWeakEquivalences_of_precomp_of_surjective
    {X Y Z : TopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : topologicalWeakEquivalences f) (hfg : topologicalWeakEquivalences (f ≫ g))
    (hs : Function.Surjective f.hom) : topologicalWeakEquivalences g :=
…

Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences

def OAI.Thomason.Construction.HomotopyMaps.basedLoopHomotopy line 635
Source documentation
A homotopy fixed at the basepoint gives homotopic postcomposed loops.
```
def basedLoopHomotopy (H : f.HomotopyRel g {x}) (ef : f x = y) (eg : g x = y)
    {N : Type*} (p : GenLoop N X x) :
    (basedLoopMap f ef p).val.HomotopyRel (basedLoopMap g eg p).val (Cube.boundary N) where
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.basedLoopMap
theorem OAI.Thomason.Construction.HomotopyMaps.basedGroupMap_homotopy line 645
Source documentation
The induced maps agree, including the explicit target-basepoint transports.
```
theorem basedGroupMap_homotopy (H : f.HomotopyRel g {x})
    (ef : f x = y) (eg : g x = y) (n : ℕ) :
    basedGroupMap f ef n = basedGroupMap g eg n := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.basedGroupMap
theorem OAI.Thomason.Construction.HomotopyMaps.componentsMap_homotopy line 653
Source documentation
Unbased homotopies give the same function on path components.
```
theorem componentsMap_homotopy (H : f.Homotopy g) : componentsMap f = componentsMap g := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.HomotopyMaps.groupMap_bijective_homotopy_iff line 665
Source documentation
A based homotopy preserves the bijectivity test at that basepoint.
```
theorem groupMap_bijective_homotopy_iff (H : f.HomotopyRel g {x}) (n : ℕ) :
    Function.Bijective (groupMap f n x) ↔ Function.Bijective (groupMap g n x) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap
def OAI.Thomason.Construction.SimplexComplex.basisWeights line 690
Source documentation
The decreasing ternary exponents associated to a simplex basis.
```
def basisWeights {m p : ℕ} (b : Basis m p) : List ℕ :=
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis
theorem OAI.Thomason.Construction.SimplexComplex.basisWeights_decreasing line 693

theorem OAI.Thomason.Construction.SimplexComplex.ofFn_succAbove line 704

Source documentation

Removing an entry from a finite tuple agrees with skipping its index.

theorem ofFn_succAbove {α : Type*} {n : ℕ} (f : Fin (n+1) → α) (i : Fin (n+1)) :
    List.ofFn (fun j : Fin n => f (i.succAbove j)) = (List.ofFn f).eraseIdx i.val := by
…

theorem OAI.Thomason.Construction.SimplexComplex.basisWeights_deleteVertex line 719
def OAI.Thomason.Construction.SimplexComplex.basisHeight line 724
Source documentation
A common height on the normalized bases of every degree.
```
def basisHeight {m p : ℕ} (b : Basis m p) : ℤ := alternatingHeight (basisWeights b)
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.alternatingHeight, OAI.Thomason.Construction.SimplexComplex.basisWeights
theorem OAI.Thomason.Construction.SimplexComplex.basisHeight_deleteVertex line 727
Source documentation
Every literal face has the sign dictated by its position in the boundary.
```
theorem basisHeight_deleteVertex {m p : ℕ} (b : Basis m (p+1)) (i : Fin (p+2)) :
    0 < (-1 : ℤ)^i.val * (basisHeight (deleteVertex b i) - basisHeight b) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.basisHeight, OAI.Thomason.Construction.SimplexComplex.deleteVertex
theorem OAI.Thomason.Construction.SimplexComplex.deleteVertex_injective line 735
Source documentation
Distinct deleted vertices give distinct normalized boundary bases.
```
theorem deleteVertex_injective {m p : ℕ} (b : Basis m (p+1)) :
    Function.Injective (deleteVertex b) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.deleteVertex
theorem OAI.Thomason.Construction.SimplexComplex.differentialBasis_face line 747
Source documentation
The coefficient of a literal face is exactly its alternating sign.
```
theorem differentialBasis_face {m p : ℕ} (b : Basis m (p+1)) (i : Fin (p+2)) :
    differentialBasis m p b (deleteVertex b i) = (-1 : ℤ)^i.val := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differentialBasis, OAI.Thomason.Construction.SimplexComplex.deleteVertex
theorem OAI.Thomason.Construction.SimplexComplex.exists_deleteVertex_of_boundary_ne_zero line 758
Source documentation
Every nonzero boundary entry has an explicit deleted-vertex witness.
```
theorem exists_deleteVertex_of_boundary_ne_zero {m p : ℕ} (b : Basis m (p+1))
    (c : Basis m p) (hc : differentialBasis m p b c ≠ 0) :
    ∃ i, deleteVertex b i = c := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differentialBasis, OAI.Thomason.Construction.SimplexComplex.deleteVertex
theorem OAI.Thomason.Construction.SimplexComplex.boundary_signed_height line 771
Source documentation
The boundary incidence matrix is strictly ordered by the concrete height.
```
theorem boundary_signed_height {m p : ℕ} (b : Basis m (p+1)) (c : Basis m p)
    (hc : differentialBasis m p b c ≠ 0) :
    0 < differentialBasis m p b c * (basisHeight c - basisHeight b) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differentialBasis, OAI.Thomason.Construction.SimplexComplex.basisHeight
theorem OAI.Thomason.Construction.SimplexComplex.negative_boundary_height line 778
theorem OAI.Thomason.Construction.SimplexComplex.positive_boundary_height line 785

theorem OAI.Thomason.Construction.HomotopyMaps.basedGroupMap_comp line 817

Source documentation

Composition with explicit basepoint equalities.

theorem basedGroupMap_comp (f : C(X, Y)) (g : C(Y, Z))
    {x : X} {y : Y} {z : Z} (ef : f x = y) (eg : g y = z) (n : ℕ) :
    basedGroupMap (g.comp f) ((congrArg g ef).trans eg) n =
      basedGroupMap g eg n ∘ basedGroupMap f ef n := by
…

Mentions: OAI.Thomason.Construction.HomotopyMaps.basedGroupMap

theorem OAI.Thomason.Construction.HomotopyMaps.basedGroupMap_id line 830
theorem OAI.Thomason.Construction.weakEquivalence_of_strongDeformationRetract line 837
Source documentation
A stationary deformation retraction gives a weak equivalence on its inclusion, proved using the actual loop quotients at every source basepoint.
```
theorem weakEquivalence_of_strongDeformationRetract
    {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y]
    (i : C(X, Y)) (r : C(Y, X)) (hi : r.comp i = ContinuousMap.id X)
    (H : (i.comp r).HomotopyRel (ContinuousMap.id Y) (Set.range i)) :
    IsWeakHomotopyEquivalence i := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

def OAI.Thomason.Construction.HomotopyMaps.simplexLoopContraction line 910

Source documentation

The explicit straight-line nullhomotopy of a based simplex-valued loop.

noncomputable def simplexLoopContraction (x : StdSimplex ℝ M) {N : Type v}
    (p : GenLoop N (StdSimplex ℝ M) x) :
    p.val.HomotopyRel (GenLoop.const (N := N) (x := x)).val (Cube.boundary N) where
…

instance OAI.Thomason.Construction.HomotopyMaps.simplex_homotopyGroup_subsingleton line 939
Source documentation
Every positive-dimensional homotopy group of a finite simplex is trivial.
```
instance simplex_homotopyGroup_subsingleton (x : StdSimplex ℝ M) (n : ℕ) :
    Subsingleton (HomotopyGroup.Pi n (StdSimplex ℝ M) x) := by
…
```
theorem OAI.Thomason.Construction.simplex_isWeakHomotopyEquivalence line 954
Source documentation
All continuous maps between nonempty finite topological simplices pass the actual component and homotopy-group weak-equivalence test.
```
theorem simplex_isWeakHomotopyEquivalence {M N : Type} [Finite M] [Finite N]
    [Nonempty M] [Nonempty N] (f : C(StdSimplex ℝ M, StdSimplex ℝ N)) :
    IsWeakHomotopyEquivalence f := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence
theorem OAI.Thomason.Construction.simplexCategory_toTop_map_weak line 982
Source documentation
Each map of topological standard simplices is weak, including the universe-lifted spaces used by the realization functor.
```
theorem simplexCategory_toTop_map_weak {n m : SimplexCategory} (f : n ⟶ m) :
    topologicalWeakEquivalences (SimplexCategory.toTop.{0}.map f) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences
theorem OAI.Thomason.Construction.realized_simplex_map_weak line 1006
Source documentation
Realization sends every ordinal-induced map of representables to a weak homotopy equivalence.
```
theorem realized_simplex_map_weak {n m : SimplexCategory} (f : n ⟶ m) :
    realizationWeakEquivalences (SSet.stdSimplex.{0}.map f) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences