TopologicalIntervalCylinder.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Top endpoint and prism cells generate all globe-cylinder atoms

Every lower atom is the image of a top endpoint or prism under the literal globular face map. These formulas allow induction on the dimension of a cell in the source of the extended cylinder.

def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.modelGlobeIso line 30
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.modelGlobeIso_naturality line 34
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.modelGlobeIso_inv_naturality line 40
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.chainMap_faceMap line 47
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpointTop line 57
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.prismTop line 62
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpointTop_dimension line 65
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.prismTop_dimension line 70
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpointTop_face line 75
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.prismTop_face line 99
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpointTop_modelAtom line 111
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.prismTop_modelAtom line 117
theorem OAI.Thomason.Construction.StrictOmegaCategory.cell_injective_of_mono line 137
Source documentation
A monic strict functor is injective on cells, as tested by finite globes.
```
theorem cell_injective_of_mono {C D : StrictOmegaCategory.{0}} (f : C ⟶ D) [Mono f] :
    Function.Injective f.toFun := by
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.isIso_of_cell_bijective line 149
Source documentation
A bijective strict functor has a strict inverse.
```
theorem isIso_of_cell_bijective {C D : StrictOmegaCategory.{0}} (f : C ⟶ D)
    (hf : Function.Bijective f.toFun) : IsIso f := by
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.globes line 154
instance OAI.Thomason.Construction.StrictOmegaCategory.globes_small line 156
theorem OAI.Thomason.Construction.StrictOmegaCategory.globes_isSeparating line 160
theorem OAI.Thomason.Construction.StrictOmegaCategory.globes_isStrongGenerator line 169
theorem OAI.Thomason.Construction.StrictOmegaCategory.matching_face_right line 199
theorem OAI.Thomason.Construction.StrictOmegaCategory.matching_face_left line 206
theorem OAI.Thomason.Construction.StrictOmegaCategory.matching_faces line 213
def OAI.Thomason.Construction.StrictOmegaCategory.rightWhisker line 220
def OAI.Thomason.Construction.StrictOmegaCategory.leftWhisker line 224
theorem OAI.Thomason.Construction.StrictOmegaCategory.whiskered_forward_matching line 228
theorem OAI.Thomason.Construction.StrictOmegaCategory.whiskered_reverse_matching line 244
theorem OAI.Thomason.Construction.StrictOmegaCategory.whiskered_forward_comp line 260
theorem OAI.Thomason.Construction.StrictOmegaCategory.whiskered_reverse_comp line 280
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.map_face_table_above line 319
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.rightWhisker_table_above line 330
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.leftWhisker_table_above line 353
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.reflect_binary_factors line 376
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.matching_of_unique_lower_faces line 419
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.reflect_forward_whiskers line 434
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.reflect_reverse_whiskers line 460

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.adjacent_transpose line 488

Source documentation

A reverse-disjoint neighbouring pair may be exchanged without changing its actual strict composite. Only preceding-level uniqueness is used.

theorem adjacent_transpose {C : StrictOmegaCategory.{0}}
    (F : C ⟶ K.realization) (s : ℕ)
    (hunique : ∀ X, B.AboveAtomOrZero (s+1) X → ∃! x : C, F.toFun x = X)
    {p q : ℕ} (a : B.Index p) (b : B.Index q) (hp : s+1 < p) (hq : s+1 < q)
    (y z : C) (hyz : C.target (s+1) y = C.source (s+1) z)
    (hy : ∀ n, s+1 < n → ∀ side, (F.toFun y).table side n = (B.atom p a).table side n)
    (hz : ∀ n, s+1 < n → ∀ side, (F.toFun z).table side n = (B.atom q b).table side n)
    (hdis : ∀ e, B.coordinates (s+1) ((B.atom p a).table true (s+1)) e = 0 ∨
      B.coordinates (s+1) ((B.atom q b).table false (s+1)) e = 0) :
    ∃ (y' z' : C) (h : C.target (s+1) y' = C.source (s+1) z'),
      C.comp (s+1) y' z' h = C.comp (s+1) y z hyz ∧
      (∀ n, s+1 < n → ∀ side, (F.toFun y').table side n = (B.atom q b).table side n) ∧
…

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.adjacent_transpose_of_height line 561

Source documentation

The height order supplies the reverse disjointness condition. A degree zero inversion is impossible by augmentation, so this applies uniformly to every composition degree.

theorem adjacent_transpose_of_height {C : StrictOmegaCategory.{0}}
    (F : C ⟶ K.realization) (r : ℕ)
    (hunique : ∀ X, B.AboveAtomOrZero r X → ∃! x : C, F.toFun x = X)
    (a b : B.AtomIndex) (ha : r < a.1) (hb : r < b.1)
    (hheight : B.atomHeight b ≤ B.atomHeight a)
    (y z : C) (hyz : C.target r y = C.source r z)
    (hy : ∀ n, r < n → ∀ side, (F.toFun y).table side n = (B.atomCell a).table side n)
    (hz : ∀ n, r < n → ∀ side, (F.toFun z).table side n = (B.atomCell b).table side n) :
    ∃ (y' z' : C) (h : C.target r y' = C.source r z'),
      C.comp r y' z' h = C.comp r y z hyz ∧
      (∀ n, r < n → ∀ side, (F.toFun y').table side n = (B.atomCell b).table side n) ∧
      (∀ n, r < n → ∀ side, (F.toFun z').table side n = (B.atomCell a).table side n) := by
…

inductive OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AtomComposite line 606
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AtomComposite.nonempty line 621
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AtomComposite.degree line 624
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AtomComposite.to_compositeList line 635
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AtomComposite.of_compositeList line 645
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AtomComposite.upper_sum line 658
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AtomComposite.swap_first line 692
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AtomComposite.move_minimal_first line 727
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AtomComposite.of_sorted_perm line 748
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AtomComposite.total_unique line 794
def OAI.Thomason.Construction.TopologicalInterval.cylinder line 844
Source documentation
Product with the ordinary unit interval.
```
def cylinder : TopCat.{u} ⥤ TopCat.{u} where
…
```
def OAI.Thomason.Construction.TopologicalInterval.pathSpace line 849
Source documentation
Paths with the compact-open topology.
```
def pathSpace : TopCat.{u} ⥤ TopCat.{u} where
…
```
def OAI.Thomason.Construction.TopologicalInterval.homEquiv line 854
Source documentation
Currying and uncurrying are inverse on actual continuous maps.
```
def homEquiv (X Y : TopCat.{u}) : (cylinder.obj X ⟶ Y) ≃ (X ⟶ pathSpace.obj Y) where
…
```
def OAI.Thomason.Construction.TopologicalInterval.adjunction line 867
Source documentation
The interval cylinder is left adjoint to compact-open paths.
```
def adjunction : cylinder.{u} ⊣ pathSpace :=
…
```
Mentions: OAI.Thomason.Construction.TopologicalInterval.pathSpace
instance OAI.Thomason.Construction.TopologicalInterval.(instance at line 885) line 885
instance OAI.Thomason.Construction.TopologicalInterval.(instance at line 887) line 887
def OAI.Thomason.Construction.TopologicalInterval.sectionAt line 891
Source documentation
The section at a chosen interval point.
```
def sectionAt (X : TopCat.{u}) (t : unitInterval) : X ⟶ cylinder.obj X :=
…
```
def OAI.Thomason.Construction.TopologicalInterval.projection line 895
Source documentation
The cylinder projection.
```
def projection (X : TopCat.{u}) : cylinder.obj X ⟶ X :=
…
```
theorem OAI.Thomason.Construction.TopologicalInterval.section_projection line 899
def OAI.Thomason.Construction.TopologicalInterval.sectionDeformation line 903
Source documentation
A straight-line deformation to the section, stationary on that section.
```
noncomputable def sectionDeformation (X : TopCat.{u}) (t : unitInterval) :
    ((sectionAt X t).hom.comp (projection X).hom).HomotopyRel
      (ContinuousMap.id (X × unitInterval)) (Set.range (sectionAt X t).hom) where
…
```
Mentions: OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.TopologicalInterval.projection
theorem OAI.Thomason.Construction.TopologicalInterval.section_weak line 938
Source documentation
Every cylinder section satisfies the actual weak-equivalence definition.
```
theorem section_weak (X : TopCat.{u}) (t : unitInterval) :
    topologicalWeakEquivalences (sectionAt X t) :=
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.TopologicalInterval.sectionAt
theorem OAI.Thomason.Construction.TopologicalInterval.projection_weak line 943
Source documentation
The cylinder projection is weak at every source basepoint.
```
theorem projection_weak (X : TopCat.{u}) : topologicalWeakEquivalences (projection X) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.TopologicalInterval.projection