TruncationQuotientComposition.lean`

59 declarations, 0 contain sorry, 0 declared as axioms

Normalizing generated expressions at a fixed composition level

An essential expression whose compositions occur at levels at most r is an actual r-string with exactly one generator above r in every factor. The length equals the number of higher generator occurrences. Endpoint expressions are supplied by dimensionwise composition generation.

def OAI.Thomason.Construction.StrictOmegaCategory.DimensionwiseGenerated line 28
Source documentation
The exact dimensionwise generation hypothesis used in Steiner's normalization argument. It follows from exists_bounded_expression for the positive-table comparisons.
```
def DimensionwiseGenerated (C : StrictOmegaCategory.{0}) {I : Type}
    (g : I → C) (d : I → ℕ) : Prop :=
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression.highGeneratorString line 35
theorem OAI.Thomason.Construction.StrictOmegaCategory.exists_normalized_generator_string line 108
Source documentation
The fixed-level form of the generated-expression normalization theorem. Every factor retains its actual expression and has exactly one higher generator.
```
theorem exists_normalized_generator_string
    (hg : ∀ i, C.DimensionLE (d i) (g i))
    (hgen : DimensionwiseGenerated C g d) {x : C}
    (t : EssentialExpression C g x) (r : ℕ) (hlevels : t.levelsLE r)
    (hcount : 0 < highCount d r t.expression.labels) :
    ∃ xs : List C, xs.length = highCount d r t.expression.labels ∧
      CompositeList C r xs x ∧
      ∀ y ∈ xs, ∃ e : CompositionExpression C g y, highCount d r e.labels = 1 :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.DimensionwiseGenerated, OAI.Thomason.Construction.StrictOmegaCategory.EssentialExpression, OAI.Thomason.Construction.StrictOmegaCategory.CompositeList, OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression
theorem OAI.Thomason.Construction.StrictOmegaCategory.generator_or_normalized_string line 120
Source documentation
Every generated cell is either one of the chosen generators or a nontrivial string whose factors each contain exactly one higher generator.
```
theorem generator_or_normalized_string
    (hg : ∀ i, C.DimensionLE (d i) (g i))
    (hgen : DimensionwiseGenerated C g d) {x : C}
    (t : CompositionExpression C g x) :
    (∃ i, x = g i) ∨ ∃ (r : ℕ) (xs : List C), 2 ≤ xs.length ∧
      CompositeList C r xs x ∧
      ∀ y ∈ xs, ∃ e : CompositionExpression C g y, highCount d r e.labels = 1 := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.DimensionwiseGenerated, OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression, OAI.Thomason.Construction.StrictOmegaCategory.CompositeList
def OAI.Thomason.Construction.HomotopyMaps.BasepointInvariant line 152
Source documentation
Bijectivity is unchanged along a path of source basepoints in this degree.
```
def BasepointInvariant (n : ℕ) : Prop :=
…
```
theorem OAI.Thomason.Construction.HomotopyMaps.homotopy_bijective_iff_of_basepoint line 161
Source documentation
Moving the source basepoint along the cylinder proves unbased homotopy invariance of the bijectivity test, in the specified degree.
```
theorem homotopy_bijective_iff_of_basepoint {n : ℕ} (h : BasepointInvariant.{u} n)
    {f g : C(X, Y)} (H : f.Homotopy g) (x : X) :
    Function.Bijective (groupMap f (n+1) x) ↔ Function.Bijective (groupMap g (n+1) x) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap
theorem OAI.Thomason.Construction.HomotopyMaps.homotopyEquiv_bijective_of_basepoint line 193
Source documentation
A homotopy equivalence induces a bijection in the specified degree once basepoint invariance is known in that degree.
```
theorem homotopyEquiv_bijective_of_basepoint {n : ℕ} (h : BasepointInvariant.{u} n)
    (e : ContinuousMap.HomotopyEquiv X Y) (x : X) :
    Function.Bijective (groupMap e.toFun (n+1) x) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap
theorem OAI.Thomason.Construction.HomotopyMaps.loopDimensionShift_bijective_iff line 239
Source documentation
The natural dimension shift preserves exactly the bijectivity test.
```
theorem loopDimensionShift_bijective_iff (f : C(X, Y)) (n : ℕ) (x : X) :
    Function.Bijective (groupMap f (n+1) x) ↔
      Function.Bijective (groupMap (PathSpace.map f) n (Path.refl x)) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap, OAI.Thomason.Construction.PathSpace.map
theorem OAI.Thomason.Construction.HomotopyMaps.basepointInvariant_succ line 254
Source documentation
Passing to path spaces advances basepoint invariance by one degree.
```
theorem basepointInvariant_succ {n : ℕ} (h : BasepointInvariant.{u} n) :
    BasepointInvariant.{u} (n+1) := by
…
```
theorem OAI.Thomason.Construction.HomotopyMaps.groupMap_bijective_path line 286
Source documentation
Bijectivity in every positive degree depends only on the source path component.
```
theorem groupMap_bijective_path (n : ℕ) : BasepointInvariant.{u} n := by
…
```
theorem OAI.Thomason.Construction.IsWeakHomotopyEquivalence.of_precomp line 318
Source documentation
A weak precomposition can be cancelled without pointwise surjectivity.
```
theorem of_precomp (hf : IsWeakHomotopyEquivalence f)
    (hfg : IsWeakHomotopyEquivalence (g.comp f)) : IsWeakHomotopyEquivalence g := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence
instance OAI.Thomason.Construction.(instance at line 334) line 334
instance OAI.Thomason.Construction.(instance at line 338) line 338
instance OAI.Thomason.Construction.(instance at line 343) line 343
instance OAI.Thomason.Construction.(instance at line 350) line 350
theorem OAI.Thomason.Construction.simplicialHomotopy_weak_iff_of_endpoints line 376
Source documentation
Two weak endpoint inclusions suffice for homotopy invariance on that source.
```
theorem simplicialHomotopy_weak_iff_of_endpoints {X Y : SSet.{u}} {f g : X ⟶ Y}
    (h₀ : realizationWeakEquivalences (SSet.ι₀ (X := X)))
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.BoundaryRetraction.weakEquivalence line 393
Source documentation
Explicit retraction data and weak endpoints imply the map is weak.
```
theorem BoundaryRetraction.weakEquivalence {X Y : SSet.{u}} {f : X ⟶ Y}
    (d : BoundaryRetraction f)
    (h₀ : realizationWeakEquivalences (SSet.ι₀ (X := X)))
…
```
Mentions: OAI.Thomason.Construction.BoundaryRetraction, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.boundary_rlp_weak_of_endpoints line 412
Source documentation
Boundary lifting satisfies the actual weak test as soon as the two cylinder endpoints do; no model structure is assumed.
```
theorem boundary_rlp_weak_of_endpoints {X Y : SSet.{u}} (f : X ⟶ Y) (hf : I.rlp f)
    (h₀ : realizationWeakEquivalences (SSet.ι₀ (X := X)))
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.IsWeakHomotopyEquivalence.middle_of_two_composites line 437
Source documentation
If the two overlapping composites are weak, then the middle map is weak. Surjectivity on components brings every base point into the image where the two given homotopy-group tests apply.
```
theorem middle_of_two_composites {X Y Z T : Type u}
    [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace T]
    (f : C(X, Y)) (g : C(Y, Z)) (h : C(Z, T))
    (hfg : IsWeakHomotopyEquivalence (g.comp f))
    (hgh : IsWeakHomotopyEquivalence (h.comp g)) :
    IsWeakHomotopyEquivalence g := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

theorem OAI.Thomason.Construction.topologicalWeakEquivalences_two_out_of_six line 481

Source documentation

Two overlapping weak composites force all three maps, and their full composite, to be actual topological weak equivalences.

theorem topologicalWeakEquivalences_two_out_of_six {A B C D : TopCat.{u}}
    (a : A ⟶ B) (b : B ⟶ C) (c : C ⟶ D)
    (hab : topologicalWeakEquivalences (a ≫ b))
    (hbc : topologicalWeakEquivalences (b ≫ c)) :
    topologicalWeakEquivalences a ∧ topologicalWeakEquivalences b ∧
      topologicalWeakEquivalences c ∧ topologicalWeakEquivalences (a ≫ b ≫ c) := by
…

Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences

theorem OAI.Thomason.Construction.realizationWeakEquivalences_two_out_of_six line 495

Source documentation

The same saturated cancellation applies to the actual realization weak-equivalence class, with no Kan--Quillen hypothesis.

theorem realizationWeakEquivalences_two_out_of_six {A B C D : SSet.{u}}
    (a : A ⟶ B) (b : B ⟶ C) (c : C ⟶ D)
    (hab : realizationWeakEquivalences (a ≫ b))
    (hbc : realizationWeakEquivalences (b ≫ c)) :
    realizationWeakEquivalences a ∧ realizationWeakEquivalences b ∧
      realizationWeakEquivalences c ∧ realizationWeakEquivalences (a ≫ b ≫ c) := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.homotopyEquiv_isWeakHomotopyEquivalence line 529
Source documentation
An actual topological homotopy equivalence is a weak homotopy equivalence.
```
theorem homotopyEquiv_isWeakHomotopyEquivalence (e : ContinuousMap.HomotopyEquiv X Y) :
    IsWeakHomotopyEquivalence e.toFun := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence
theorem OAI.Thomason.Construction.isWeakHomotopyEquivalence_homotopy_iff line 547
Source documentation
Unbased homotopies preserve the full semantic weak-equivalence test.
```
theorem isWeakHomotopyEquivalence_homotopy_iff {f g : C(X, Y)} (H : f.Homotopy g) :
    IsWeakHomotopyEquivalence f ↔ IsWeakHomotopyEquivalence g := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence
theorem OAI.Thomason.Construction.pathConjugation_isWeakHomotopyEquivalence line 557
Source documentation
Loop-space conjugation is weak in the actual all-degree sense.
```
theorem pathConjugation_isWeakHomotopyEquivalence {x y : X} (p : Path x y) :
    IsWeakHomotopyEquivalence (PathSpace.conjugate p) :=
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.PathSpace.conjugate
theorem OAI.Thomason.Construction.HomotopyMaps.loopDimensionShift_surjective_iff line 575
theorem OAI.Thomason.Construction.HomotopyMaps.groupMap_one_surjective_path line 589
def OAI.Thomason.Construction.HomotopyMaps.SurjectiveBasepointInvariant line 599
theorem OAI.Thomason.Construction.HomotopyMaps.surjectiveBasepoint_succ line 605
theorem OAI.Thomason.Construction.HomotopyMaps.groupMap_surjective_path line 634
Source documentation
Surjectivity in every positive degree depends only on the source path component.
```
theorem groupMap_surjective_path (n : ℕ) (f : C(X, Y)) {x y : X} (p : Path x y) :
    Function.Surjective (groupMap f (n+1) x) ↔
      Function.Surjective (groupMap f (n+1) y) := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap
def OAI.Thomason.Construction.continuousFiber line 660
Source documentation
The literal continuous fibre, with its subspace topology.
```
def continuousFiber {X B : TopCat.{0}} (p : X ⟶ B) (b : B) : TopCat.{0} :=
…
```
def OAI.Thomason.Construction.continuousFiberInclusion line 663
def OAI.Thomason.Construction.continuousFiberMap line 667
Source documentation
Any exact map over the base restricts to each literal fibre.
```
def continuousFiberMap {X Y B : TopCat.{0}} (p : X ⟶ B) (q : Y ⟶ B)
    (b : B) (f : X ⟶ Y) (hf : f ≫ q = p) : continuousFiber p b ⟶ continuousFiber q b :=
…
```
Mentions: OAI.Thomason.Construction.continuousFiber
theorem OAI.Thomason.Construction.continuousFiberMap_inclusion line 673
def OAI.Thomason.Construction.continuousFiberIso line 679
Source documentation
An isomorphism over the base restricts to an isomorphism of fibres.
```
def continuousFiberIso {X Y B : TopCat.{0}} (p : X ⟶ B) (q : Y ⟶ B)
    (b : B) (e : X ≅ Y) (he : e.hom ≫ q = p) :
    continuousFiber p b ≅ continuousFiber q b where
…
```
Mentions: OAI.Thomason.Construction.continuousFiber
theorem OAI.Thomason.Construction.continuousFiberInclusion_weak_of_iso line 699
Source documentation
A change of coordinates over the base preserves the weak-equivalence property of the literal fibre inclusion.
```
theorem continuousFiberInclusion_weak_of_iso {X Y B : TopCat.{0}}
    (p : X ⟶ B) (q : Y ⟶ B) (b : B) (e : X ≅ Y) (he : e.hom ≫ q = p)
    (hq : topologicalWeakEquivalences (continuousFiberInclusion q b)) :
    topologicalWeakEquivalences (continuousFiberInclusion p b) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousFiberInclusion

def OAI.Thomason.Construction.continuousFiberHomotopy line 711

Source documentation

The full parameterized homotopy restricts to the fibre when its base coordinate is constant throughout.

def continuousFiberHomotopy {X Y B : TopCat.{0}} (p : X ⟶ B) (q : Y ⟶ B)
    (b : B) (f g : X ⟶ Y) (hf : f ≫ q = p) (hg : g ≫ q = p)
    (H : f.hom.Homotopy g.hom) (hH : ∀ t x, q.hom (H (t,x)) = p.hom x) :
    (continuousFiberMap p q b f hf).hom.Homotopy
      (continuousFiberMap p q b g hg).hom where
…

Mentions: OAI.Thomason.Construction.continuousFiberMap

def OAI.Thomason.Construction.continuousFiberHomotopyEquiv line 725

Source documentation

A homotopy equivalence with both homotopies over the base induces an actual homotopy equivalence on every continuous fibre.

def continuousFiberHomotopyEquiv {X Y B : TopCat.{0}} (p : X ⟶ B) (q : Y ⟶ B)
    (b : B) (f : X ⟶ Y) (g : Y ⟶ X) (hf : f ≫ q = p) (hg : g ≫ p = q)
    (H : (ContinuousMap.id X).Homotopy (g.hom.comp f.hom))
    (K : (ContinuousMap.id Y).Homotopy (f.hom.comp g.hom))
    (hH : ∀ t x, p.hom (H (t,x)) = p.hom x)
    (hK : ∀ t y, q.hom (K (t,y)) = q.hom y) :
    ContinuousMap.HomotopyEquiv (continuousFiber p b) (continuousFiber q b) where
…

Mentions: OAI.Thomason.Construction.continuousFiber

theorem OAI.Thomason.Construction.continuousFiberMap_weak_of_over_equivalence line 740

Source documentation

The induced fibre map is a weak equivalence in all homotopy degrees.

theorem continuousFiberMap_weak_of_over_equivalence {X Y B : TopCat.{0}}
    (p : X ⟶ B) (q : Y ⟶ B) (b : B) (f : X ⟶ Y) (g : Y ⟶ X)
    (hf : f ≫ q = p) (hg : g ≫ p = q)
    (H : (ContinuousMap.id X).Homotopy (g.hom.comp f.hom))
    (K : (ContinuousMap.id Y).Homotopy (f.hom.comp g.hom))
    (hH : ∀ t x, p.hom (H (t,x)) = p.hom x)
    (hK : ∀ t y, q.hom (K (t,y)) = q.hom y) :
    topologicalWeakEquivalences (continuousFiberMap p q b f hf) :=
…

Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousFiberMap

def OAI.Thomason.Construction.continuousFiberBaseChangeMap line 769
Source documentation
A genuinely commutative square induces the literal map on its point fibres, retaining the total-space point and the specified base point.
```
def continuousFiberBaseChangeMap {X Y A B : TopCat.{0}} (p : X ⟶ A) (q : Y ⟶ B)
    (f : X ⟶ Y) (g : A ⟶ B) (h : f ≫ q = p ≫ g) (b : A) :
    continuousFiber p b ⟶ continuousFiber q (g.hom b) :=
…
```
Mentions: OAI.Thomason.Construction.continuousFiber
theorem OAI.Thomason.Construction.continuousFiberBaseChangeMap_inclusion line 777

theorem OAI.Thomason.Construction.continuousFiberBaseChangeMap_weak line 785

Source documentation

When both fibre inclusions and the total-space map are weak, the specified map of literal fibres is weak as well.

theorem continuousFiberBaseChangeMap_weak {X Y A B : TopCat.{0}}
    (p : X ⟶ A) (q : Y ⟶ B) (f : X ⟶ Y) (g : A ⟶ B)
    (h : f ≫ q = p ≫ g) (b : A)
    (hf : topologicalWeakEquivalences f)
    (hp : topologicalWeakEquivalences (continuousFiberInclusion p b))
    (hq : topologicalWeakEquivalences (continuousFiberInclusion q (g.hom b))) :
    topologicalWeakEquivalences (continuousFiberBaseChangeMap p q f g h b) := by
…

Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousFiberInclusion, OAI.Thomason.Construction.continuousFiberBaseChangeMap

def OAI.Thomason.Construction.TopologicalProduct.mappingSpace line 813
Source documentation
Compact-open maps out of the fixed parameter space.
```
def mappingSpace (B : TopCat.{u}) : TopCat.{u} ⥤ TopCat.{u} where
…
```
def OAI.Thomason.Construction.TopologicalProduct.homEquiv line 819
Source documentation
The ordinary compact-open exponential law, specialized to the parameter spaces used in finite realization approximations.
```
def homEquiv (B : TopCat.{u}) [LocallyCompactSpace B] (X Y : TopCat.{u}) :
    ((tensorRight B).obj X ⟶ Y) ≃ (X ⟶ (mappingSpace B).obj Y) where
…
```
Mentions: OAI.Thomason.Construction.TopologicalProduct.mappingSpace
def OAI.Thomason.Construction.TopologicalProduct.adjunction line 838
Source documentation
Product with a locally compact parameter is left adjoint to its compact-open mapping-space functor.
```
def adjunction (B : TopCat.{u}) [LocallyCompactSpace B] :
    tensorRight B ⊣ mappingSpace B :=
…
```
Mentions: OAI.Thomason.Construction.TopologicalProduct.mappingSpace
theorem OAI.Thomason.Construction.TopologicalProduct.preservesColimits line 857
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Rel.map_face line 873
abbrev OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.mk line 889
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.face line 891
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.face_mk line 895
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.matching_of_quotient line 899
Source documentation
Below the truncation level, quotient equality of boundaries is actual equality.
```
theorem matching_of_quotient {m : ℕ} (hm : m < n) (x y : C.bounded n)
    (h : face true m (mk x) = face false m (mk y)) :
    (C.bounded n).target m x = (C.bounded n).source m y := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.face, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.mk, OAI.Thomason.Construction.StrictOmegaCategory.target, OAI.Thomason.Construction.StrictOmegaCategory.source
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.face_of_le line 906
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.globular line 915
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.representative line 936
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.mk_representative line 938
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.representatives_match line 942
Source documentation
Below the surviving dimension the quotient does not invent matching boundaries.
```
theorem representatives_match {m : ℕ} (hm : m < n) (x y : Cell C n)
    (h : face true m x = face false m y) :
    (C.bounded n).target m (representative x) = (C.bounded n).source m (representative y) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Cell, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.face, OAI.Thomason.Construction.StrictOmegaCategory.target, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.representative, OAI.Thomason.Construction.StrictOmegaCategory.source
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.comp line 948
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.comp_mk line 954
Source documentation
Every choice of matching representatives computes the same quotient composite.
```
theorem comp_mk (m : ℕ) (x y : C.bounded n)
    (h : (C.bounded n).target m x = (C.bounded n).source m y)
    (h' : face true m (mk x) = face false m (mk y)) :
    comp m (mk x) (mk y) h' = mk ((C.bounded n).comp m x y h) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.target, OAI.Thomason.Construction.StrictOmegaCategory.source, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.face, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.mk, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.comp
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.source_comp line 975
Source documentation
Source compatibility, including identity levels above the cutoff.
```
theorem source_comp (m : ℕ) (x y : Cell C n)
    (h : face true m x = face false m y) :
    face false m (comp m x y h) = face false m x := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Cell, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.face, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.comp
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.target_comp line 989
Source documentation
Target compatibility uses the original matching condition.
```
theorem target_comp (m : ℕ) (x y : Cell C n)
    (h : face true m x = face false m y) :
    face true m (comp m x y h) = face true m y := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Cell, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.face, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.comp