PastingGlobeCylinderPath.lean`

55 declarations, 0 contain sorry, 0 declared as axioms

The positive globe complex represents bounded cells

Evaluation of a positive chain map at the universal top table is an actual bijection with bounded cells. In particular the chain parameter used by the right interval remembers every cell entry, not only its endpoints.

theorem OAI.Thomason.Construction.DirectedGlobeComplex.chainHom_ext line 23
theorem OAI.Thomason.Construction.DirectedGlobeComplex.topTable_eq_single line 33
theorem OAI.Thomason.Construction.DirectedGlobeComplex.cellMap_top_inverse line 51
Source documentation
Reading the top table and extending its entries recovers the original positive chain map on every degree and basis element.
```
theorem cellMap_top_inverse {K : DirectedComplex.{0}} (n : ℕ) (F : Hom (complex n) K) :
    cellMap n (F.realization.toFun (topCell n)) = F := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex, OAI.Thomason.Construction.DirectedGlobeComplex.cellMap, OAI.Thomason.Construction.DirectedGlobeComplex.topCell
def OAI.Thomason.Construction.DirectedGlobeComplex.homEquiv line 74
Source documentation
Positive maps from the globe complex are exactly bounded cells in Steiner's actual strict realization.
```
def homEquiv (n : ℕ) (K : DirectedComplex.{0}) :
    Hom (complex n) K ≃ {x : K.realization // K.realization.DimensionLE n x} where
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex
abbrev OAI.Thomason.Construction.DirectedGlobeComplex.chainTable line 102
theorem OAI.Thomason.Construction.DirectedGlobeComplex.chain_eq_pair line 105
theorem OAI.Thomason.Construction.DirectedGlobeComplex.chain_eq_top line 113
theorem OAI.Thomason.Construction.DirectedGlobeComplex.weight_eq_pair line 126
theorem OAI.Thomason.Construction.DirectedGlobeComplex.weight_eq_top line 131
theorem OAI.Thomason.Construction.DirectedGlobeComplex.positive_weight_nonneg line 136
theorem OAI.Thomason.Construction.DirectedGlobeComplex.positive_eq_zero_of_weight_zero line 146
theorem OAI.Thomason.Construction.DirectedGlobeComplex.cell_weight_eq line 162
theorem OAI.Thomason.Construction.DirectedGlobeComplex.cell_weight_succ_le line 170
theorem OAI.Thomason.Construction.DirectedGlobeComplex.cell_dimension line 186
Source documentation
Every cell of the globe chain realization has the expected bound.
```
theorem cell_dimension (n : ℕ) (x : Cell (complex n)) :
    (complex n).realization.DimensionLE n x := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex
theorem OAI.Thomason.Construction.DirectedGlobeComplex.cell_weight_le_one line 192
theorem OAI.Thomason.Construction.DirectedGlobeComplex.cell_weight_bounds line 203
theorem OAI.Thomason.Construction.DirectedGlobeComplex.positive_weight_one line 232
theorem OAI.Thomason.Construction.DirectedGlobeComplex.cell_weight_antitone line 257
theorem OAI.Thomason.Construction.DirectedGlobeComplex.minimal_dimension_weight_one line 268
Source documentation
The least dimension of a cell has positive weight one.
```
theorem minimal_dimension_weight_one {n d : ℕ} (x : Cell (complex n))
    (hd : (complex n).realization.DimensionLE d x)
    (hmin : ∀ k < d, ¬ (complex n).realization.DimensionLE k x) :
    weight n d (chainTable x false d) = 1 := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex, OAI.Thomason.Construction.DirectedGlobeComplex.weight, OAI.Thomason.Construction.DirectedGlobeComplex.chainTable
theorem OAI.Thomason.Construction.DirectedGlobeComplex.cell_lower_table line 293
Source documentation
Weight one at an upper degree forces the signed lower boundaries.
```
theorem cell_lower_table {n d k : ℕ} (x : Cell (complex n))
    (hdn : d ≤ n) (hkd : k < d)
    (hd : weight n d (chainTable x false d) = 1) (a : Bool) :
    chainTable x a k = topTable n a k := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex, OAI.Thomason.Construction.DirectedGlobeComplex.weight, OAI.Thomason.Construction.DirectedGlobeComplex.chainTable, OAI.Thomason.Construction.DirectedGlobeComplex.topTable
theorem OAI.Thomason.Construction.DirectedGlobeComplex.exists_topCell_face line 334
Source documentation
Every table is an actual face of the universal top cell.
```
theorem exists_topCell_face (n : ℕ) (x : Cell (complex n)) :
    ∃ (d : ℕ) (s : Basis n d), (topCell n).face s.val d = x := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex, OAI.Thomason.Construction.DirectedGlobeComplex.Basis, OAI.Thomason.Construction.DirectedGlobeComplex.topCell
theorem OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe_surjective line 371
Source documentation
The canonical free globe map is surjective on every strict cell.
```
theorem fromGlobe_surjective (n : ℕ) : Function.Surjective (fromGlobe n).toFun := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.positive_summand_of_single line 403
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atom_summand_descend line 437
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atom_summands line 496
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atom_comp_identity_factor line 520
Source documentation
A binary expression for an atom has an identity factor at its composition degree.
```
theorem atom_comp_identity_factor (a : B.AtomIndex) (Y Z : Cell K) (r : ℕ)
    (hyz : Y.face true r = Z.face false r)
    (he : Cell.comp Y Z r hyz = B.atomCell a) :
    K.realization.DimensionLE r Y ∨ K.realization.DimensionLE r Z := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.comp
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.aboveAtomOrZero_comp_identity_factor line 557
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atomCell_injective line 600
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.comp_eq_left line 630
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atom_preimage_of_expression line 637

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.unique_preimage_level_zero line 663

Source documentation

Every level-zero positive cell has exactly one preimage. This is the base of the free-gluing induction on upper-table decomposition levels.

theorem unique_preimage_level_zero {C : StrictOmegaCategory.{0}}
    (g : B.AtomIndex → C) (F : C ⟶ K.realization)
    (hg : ∀ a, F.toFun (g a) = B.atomCell a)
    (hd : ∀ a, C.DimensionLE a.1 (g a))
    (hgen : ∀ x : C, Nonempty (CompositionExpression C g x))
    (X : Cell K) (hX : B.AboveAtomOrZero 0 X) : ∃! x : C, F.toFun x = X := by
…

Mentions: OAI.Thomason.Construction.DirectedComplex.Cell

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.lift_composite_of_unique_faces line 694
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.exists_preimage_successor line 724
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.lifted_compositeList_factors_unique line 790
abbrev OAI.Thomason.Construction.DirectedComplex.RightPath.rawGroup line 842
def OAI.Thomason.Construction.DirectedComplex.RightPath.rawDifferential line 844
def OAI.Thomason.Construction.DirectedComplex.RightPath.zeroGroup line 856
theorem OAI.Thomason.Construction.DirectedComplex.RightPath.rawDifferential_zero_mem line 871
theorem OAI.Thomason.Construction.DirectedComplex.RightPath.rawDifferential_squared line 877
abbrev OAI.Thomason.Construction.DirectedComplex.RightPath.group line 881
def OAI.Thomason.Construction.DirectedComplex.RightPath.differential line 885
theorem OAI.Thomason.Construction.DirectedComplex.RightPath.differential_squared line 892
def OAI.Thomason.Construction.DirectedComplex.RightPath.augmentation line 898
def OAI.Thomason.Construction.DirectedComplex.RightPath.rawPositive line 903
def OAI.Thomason.Construction.DirectedComplex.RightPath.positive line 906
abbrev OAI.Thomason.Construction.DirectedComplex.RightPath.complex line 911
Source documentation
The path complex has the exact signed differential of the right tensor.
```
abbrev complex : DirectedComplex.{0} where
…
```
def OAI.Thomason.Construction.DirectedComplex.RightPath.endpoint line 922
Source documentation
The two endpoint restrictions of an arbitrary chain-cylinder map.
```
def endpoint (f : Hom (rightCylinder K) L) (a : Bool) : Hom K L :=
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder
def OAI.Thomason.Construction.DirectedComplex.RightPath.shifted line 926
Source documentation
Evaluation on the shifted interval summand.
```
def shifted (f : Hom (rightCylinder K) L) (n : ℕ) : K.group n →+ L.group (n+1) where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder
theorem OAI.Thomason.Construction.DirectedComplex.RightPath.apply_zero line 934
theorem OAI.Thomason.Construction.DirectedComplex.RightPath.apply_succ line 941
theorem OAI.Thomason.Construction.DirectedComplex.RightPath.shifted_differential_zero line 953
theorem OAI.Thomason.Construction.DirectedComplex.RightPath.shifted_differential_succ line 963
def OAI.Thomason.Construction.DirectedComplex.RightPath.curryRaw line 976
def OAI.Thomason.Construction.DirectedComplex.RightPath.curryApp line 981
def OAI.Thomason.Construction.DirectedComplex.RightPath.curry line 989
Source documentation
Currying is an actual positive augmented chain map into the path complex.
```
def curry (f : Hom (rightCylinder K) L) : Hom K (complex L) where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.RightPath.complex