SimplexCylinderGeneration.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

Relative cylinder lifting for genuine Kan fibrations

theorem OAI.Thomason.Construction.exists_kan_cylinder_lift line 31

Source documentation

A Kan fibration lifts a cylinder with both its initial map and a prescribed subobject cylinder fixed. This is the pushout-product lifting property.

theorem exists_kan_cylinder_lift {A K E B : SSet.{u}}
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (f : K ⟶ E) (h : A ⊗ Δ[1] ⟶ E) (b : K ⊗ Δ[1] ⟶ B)
    (h₀ : SSet.ι₀ ≫ h = i ≫ f)
    (hb : h ≫ p = i ▷ Δ[1] ≫ b) (hf : f ≫ p = SSet.ι₀ ≫ b) :
    ∃ e : K ⊗ Δ[1] ⟶ E,
      SSet.ι₀ ≫ e = f ∧ i ▷ Δ[1] ≫ e = h ∧ e ≫ p = b := by
…

theorem OAI.Thomason.Construction.whisker_one_face line 95
theorem OAI.Thomason.Construction.intervalBoundary_restriction line 113

theorem OAI.Thomason.Construction.exists_kan_boundary_cylinder_lift line 130

Source documentation

An anodyne map times an interval can be lifted while prescribing the whole interval boundary. This uses only the proved pushout-product theorem.

theorem exists_kan_boundary_cylinder_lift {A K E B : SSet.{u}}
    (i : A ⟶ K) (hi : SSet.anodyneExtensions i)
    (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (a : A ⊗ Δ[1] ⟶ E) (c : K ⊗ (SSet.boundary 1 : SSet.{u}) ⟶ E)
    (b : K ⊗ Δ[1] ⟶ B)
    (hc : i ▷ (SSet.boundary 1 : SSet.{u}) ≫ c = A ◁ (SSet.boundary 1).ι ≫ a)
    (ha : a ≫ p = i ▷ Δ[1] ≫ b) (hb : c ≫ p = K ◁ (SSet.boundary 1).ι ≫ b) :
    ∃ e : K ⊗ Δ[1] ⟶ E,
      i ▷ Δ[1] ≫ e = a ∧ K ◁ (SSet.boundary 1).ι ≫ e = c ∧ e ≫ p = b := by
…

theorem OAI.Thomason.Construction.zeroFaceSection_one_face line 178

theorem OAI.Thomason.Construction.exists_kan_cylinder_lift_one line 183

Source documentation

Final-endpoint lifting, with the prescribed subobject fixed throughout.

theorem exists_kan_cylinder_lift_one {A K E B : SSet.{u}}
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (f : K ⟶ E) (h : A ⊗ Δ[1] ⟶ E) (b : K ⊗ Δ[1] ⟶ B)
    (h₀ : SSet.ι₁ ≫ h = i ≫ f)
    (hb : h ≫ p = i ▷ Δ[1] ≫ b) (hf : f ≫ p = SSet.ι₁ ≫ b) :
    ∃ e : K ⊗ Δ[1] ⟶ E,
      SSet.ι₁ ≫ e = f ∧ i ▷ Δ[1] ≫ e = h ∧ e ≫ p = b := by
…

theorem OAI.Thomason.Construction.RelativePrismData.piece_stationary line 251

Source documentation

A local piece lying entirely in the old subposet is strictly stationary.

theorem piece_stationary {m : ℕ} (s : Fin (m + 1) →o E) (hs : ∀ i, s i ∈ D.old) :
    D.piece h G s = G.projection.app (h.object m) ≫ h.posetLeg (D.first.comp s) := by
…

def OAI.Thomason.Construction.RelativePrismData.oldInclusion line 280
Source documentation
The monotone inclusion of the old subposet.
```
def oldInclusion : D.old →o E where
…
```

theorem OAI.Thomason.Construction.RelativePrismData.prism_stationary line 285

Source documentation

The whole assembled cylinder is stationary on the old subposet.

theorem prism_stationary :
    G.cylinder.map (h.categorification.map (nerveMap D.oldInclusion.monotone.functor)) ≫ D.prism h G =
      G.projection.app (h.categorification.obj (nerve D.old)) ≫
        h.categorification.map (nerveMap (D.first.comp D.oldInclusion).monotone.functor) := by
…

theorem OAI.Thomason.Construction.FiniteReflectionInput.unit_hom_ext line 341

Source documentation

Reflection units detect maps to every finite-dimensional target.

theorem unit_hom_ext (X : StrictOmegaCategory.{0})
    (Y : StrictOmegaCategory.Truncated.{0} (n + 1))
    {f g : (r.reflect.obj X).val ⟶ Y.val}
    (he : r.adjunction.unit.app X ≫ f = r.adjunction.unit.app X ≫ g) : f = g := by
…

theorem OAI.Thomason.Construction.RightGrayInput.factor_cylinder_stationary line 361

Source documentation

Descent preserves strict stationarity, as an equation on the whole reflected cylinder.

theorem factor_cylinder_stationary (A X : StrictOmegaCategory.{0})
    (i v : A ⟶ X) (P : G.cylinder.obj X ⟶ X)
    (Q : G.cylinder.obj (r.reflect.obj X).val ⟶ (r.reflect.obj X).val)
    (hQ : G.cylinder.map (r.adjunction.unit.app X) ≫ Q = P ≫ r.adjunction.unit.app X)
    (hP : G.cylinder.map i ≫ P = G.projection.app A ≫ v) :
    G.cylinder.map ((StrictOmegaCategory.inclusion (n + 1)).map (r.reflect.map i)) ≫ Q =
      G.projection.app (r.reflect.obj A).val ≫
        (StrictOmegaCategory.inclusion (n + 1)).map (r.reflect.map v) := by
…

Mentions: OAI.Thomason.Construction.StrictOmegaCategory.inclusion

def OAI.Thomason.Construction.RelativePrismData.finitePrism line 404
Source documentation
Compose the omega prism with the finite reflection unit, then descend its source cylinder by the published internal-hom truncation theorem.
```
noncomputable def finitePrism :
    G.cylinder.obj (r.reflect.obj (h.categorification.obj (nerve E))).val ⟶
      (r.reflect.obj (h.categorification.obj (nerve E))).val :=
…
```
theorem OAI.Thomason.Construction.RelativePrismData.finitePrism_restrict line 410

theorem OAI.Thomason.Construction.RelativePrismData.finitePrism_endpoint line 418

Source documentation

The descended endpoints are the actual finite categorification maps.

theorem finitePrism_endpoint (a : Bool) :
    (G.endpoint a).app (r.reflect.obj (h.categorification.obj (nerve E))).val ≫
      D.finitePrism h G t r =
    (StrictOmegaCategory.inclusion (n + 1)).map
      (r.reflect.map (h.posetMap (if a then D.last else D.first))) := by
…

Mentions: OAI.Thomason.Construction.StrictOmegaCategory.inclusion

theorem OAI.Thomason.Construction.RelativePrismData.finitePrism_stationary line 433

Source documentation

The finite relative prism is stationary on the entire reflected old cylinder.

theorem finitePrism_stationary :
    G.cylinder.map ((StrictOmegaCategory.inclusion (n + 1)).map
      (r.reflect.map (h.posetMap D.oldInclusion))) ≫ D.finitePrism h G t r =
    G.projection.app (r.reflect.obj (h.categorification.obj (nerve D.old))).val ≫
      (StrictOmegaCategory.inclusion (n + 1)).map
        (r.reflect.map (h.posetMap (D.first.comp D.oldInclusion))) :=
…

Mentions: OAI.Thomason.Construction.StrictOmegaCategory.inclusion

def OAI.Thomason.Construction.SieveRetraction.upperPrismData line 458
def OAI.Thomason.Construction.SieveRetraction.lowerPrismData line 467

theorem OAI.Thomason.Construction.SieveRetraction.greatest_new_cylinders line 480

Source documentation

The common upper map gives two strict cylinders, both stationary on all cells of the old part. Their endpoints are id ≤ upper ≥ lower.

theorem greatest_new_cylinders :
    ∃ P Q : G.cylinder.obj (h.categorification.obj (nerve E)) ⟶ h.categorification.obj (nerve E),
      (G.endpoint false).app _ ≫ P = 𝟙 _ ∧
      (G.endpoint true).app _ ≫ P = h.posetMap (R.upperCollapse hx) ∧
      (G.endpoint false).app _ ≫ Q = h.posetMap (R.oldCollapse hx) ∧
      (G.endpoint true).app _ ≫ Q = h.posetMap (R.upperCollapse hx) ∧
      G.cylinder.map (h.posetMap (subposetInclusion A)) ≫ P =
        G.projection.app _ ≫ h.posetMap (subposetInclusion A) ∧
      G.cylinder.map (h.posetMap (subposetInclusion A)) ≫ Q =
        G.projection.app _ ≫ h.posetMap (subposetInclusion A) := by
…

Mentions: OAI.Thomason.Construction.subposetInclusion

theorem OAI.Thomason.Construction.SieveRetraction.oldCollapse_posetMap_retraction line 506

Source documentation

The old-valued collapse is an actual retraction after categorification.

theorem oldCollapse_posetMap_retraction :
    h.posetMap (subposetInclusion A) ≫ h.posetMap (R.oldCollapseRetraction hx) = 𝟙 _ ∧
      h.posetMap (R.oldCollapseRetraction hx) ≫ h.posetMap (subposetInclusion A) =
        h.posetMap (R.oldCollapse hx) := by
…

Mentions: OAI.Thomason.Construction.subposetInclusion

theorem OAI.Thomason.Construction.SimplexComplex.signedPart_single_sub line 535
Source documentation
The two parts of a boundary with distinct positive and negative basis terms.
```
theorem signedPart_single_sub {m p : ℕ} (a : Bool) (b c : Basis m p) (hbc : b ≠ c) :
    signedPart a (Finsupp.single b 1 - Finsupp.single c 1) =
      if a then Finsupp.single b 1 else Finsupp.single c 1 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.signedPart
theorem OAI.Thomason.Construction.SimplexComplex.principalCell_bottom line 545
Source documentation
The bottom chains of the constructed principal cells are their endpoint vertices.
```
theorem principalCell_bottom (h : NormalizedSimplexIdentities) (m : ℕ) (a : Bool) :
    (principalCell h m).table a 0 =
      if a then Finsupp.single (vertexBasis (Fin.last m)) 1
        else Finsupp.single (vertexBasis 0) 1 := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.principalCell, OAI.Thomason.Construction.SimplexComplex.vertexBasis
theorem OAI.Thomason.Construction.SimplexComplex.principalCell_signedPart_zero line 556
Source documentation
The zero-dimensional signed-boundary formula follows from the two distinct endpoints.
```
theorem principalCell_signedPart_zero (h : NormalizedSimplexIdentities) (m : ℕ) (a : Bool) :
    signedPart a (differential (m + 1) 0 ((principalCell h (m + 1)).table a 1)) =
      (principalCell h (m + 1)).table a 0 := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.signedPart, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.principalCell
theorem OAI.Thomason.Construction.SimplexComplex.principalCell_isBasisAtom line 576
Source documentation
The entire downward-recursive atom table is proved, not postulated.
```
theorem principalCell_isBasisAtom (h : NormalizedSimplexIdentities) (m : ℕ) :
    IsBasisAtom h (topBasis m) (principalCell h m) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.IsBasisAtom, OAI.Thomason.Construction.SimplexComplex.topBasis, OAI.Thomason.Construction.SimplexComplex.principalCell
structure OAI.Thomason.Construction.PublishedSimplexGenerationInput line 600
Source documentation
Steiner 2004, Theorem 5.6, restricted to generation by the simplex atoms explicitly constructed here. Atom existence, tables and endpoints are proved.
```
structure PublishedSimplexGenerationInput (h : NormalizedSimplexIdentities) : Prop where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities
def OAI.Thomason.Construction.PublishedSimplexGenerationInput.toSimplexAtomsInput line 608
Source documentation
The signed-part formulas and composition generation give the simplex-atom data.
```
noncomputable def PublishedSimplexGenerationInput.toSimplexAtomsInput
    {h : NormalizedSimplexIdentities} (g : PublishedSimplexGenerationInput h) : SimplexAtomsInput h where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.PublishedSimplexGenerationInput, OAI.Thomason.Construction.SimplexAtomsInput
def OAI.Thomason.Construction.SimplexComplex.basisPostcompose line 632
Source documentation
Postcomposition with an increasing tuple embeds every normalized basis.
```
def basisPostcompose {m p : ℕ} (b : Basis m p) (q : ℕ) : Basis p q ↪ Basis m q where
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis
theorem OAI.Thomason.Construction.SimplexComplex.mapChains_embedding line 640
Source documentation
An injective simplex operator has no degenerate or colliding images.
```
theorem mapChains_embedding {m p q : ℕ} (b : Basis m p) (x : Chains p q) :
    mapChains b.toOrderHom q x = Finsupp.embDomain (basisPostcompose b q) x := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.mapChains, OAI.Thomason.Construction.SimplexComplex.basisPostcompose
theorem OAI.Thomason.Construction.SimplexComplex.mapChains_embedding_signedPart line 656
Source documentation
Signed parts commute with these actual basis embeddings.
```
theorem mapChains_embedding_signedPart {m p q : ℕ} (b : Basis m p) (side : Bool)
    (x : Chains p q) :
    mapChains b.toOrderHom q (signedPart side x) =
      signedPart side (mapChains b.toOrderHom q x) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.mapChains, OAI.Thomason.Construction.SimplexComplex.signedPart
theorem OAI.Thomason.Construction.SimplexComplex.basisAtom_embedding line 666
Source documentation
Every face image of the principal atom satisfies the full recursive signed-boundary table formula.
```
theorem basisAtom_embedding (h : NormalizedSimplexIdentities) {m p : ℕ}
    (b : Basis m p) (x : h.object p) (hx : IsBasisAtom h (topBasis p) x) :
    IsBasisAtom h b ((h.map b.toOrderHom).toFun x) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.IsBasisAtom, OAI.Thomason.Construction.SimplexComplex.topBasis
def OAI.Thomason.Construction.SimplexComplex.basisAtom line 684
Source documentation
The concrete atom attached to any normalized basis element.
```
noncomputable def basisAtom (h : NormalizedSimplexIdentities) {m p : ℕ} (b : Basis m p) :
    h.object m := (h.map b.toOrderHom).toFun (principalCell h p)
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.principalCell
theorem OAI.Thomason.Construction.SimplexComplex.basisAtom_isBasisAtom line 687
theorem OAI.Thomason.Construction.SimplexComplex.positive_augmentation_zero line 709
Source documentation
A positive zero-chain of augmentation zero vanishes coefficientwise.
```
theorem positive_augmentation_zero {m : ℕ} (z : Chains m 0)
    (hz : z ∈ positive m 0) (he : augmentation m z = 0) : z = 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, OAI.Thomason.Construction.SimplexComplex.augmentation

theorem OAI.Thomason.Construction.SimplexComplex.atom_residual_sides line 723

Source documentation

Equal next-degree chains give the same residual on both sides.

theorem atom_residual_sides {h : NormalizedSimplexIdentities} {m : ℕ}
    (X A : h.object m) (r : ℕ)
    (he : X.table false (r+1) = A.table false (r+1)) :
    X.table false r - A.table false r = X.table true r - A.table true r := by
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

theorem OAI.Thomason.Construction.SimplexComplex.atom_residual_positive line 739
Source documentation
The extra chain below a common atom is positive; no generation input is needed for this subtraction.
```
theorem atom_residual_positive {h : NormalizedSimplexIdentities} {m p : ℕ}
    {b : Basis m p} (X A : h.object m) (hA : IsBasisAtom h b A)
    (r : ℕ) (hr : r < p)
    (he : X.table false (r+1) = A.table false (r+1)) :
    X.table false r - A.table false r ∈ positive m r := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.IsBasisAtom, OAI.Thomason.Construction.SimplexComplex.positive
theorem OAI.Thomason.Construction.SimplexComplex.eq_atom_of_above_zero line 754
Source documentation
There is no lower-dimensional freedom below the zero-chains of an atom: augmentation one removes the positive residual.
```
theorem eq_atom_of_above_zero {h : NormalizedSimplexIdentities} {m p : ℕ}
    {b : Basis m p} (X A : h.object m) (hA : IsBasisAtom h b A) (hp : 0 < p)
    (he : ∀ n, 0 < n → ∀ side, X.table side n = A.table side n) : X = A := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.IsBasisAtom
abbrev OAI.Thomason.Construction.SimplexComplex.AtomIndex line 791
Source documentation
An atom retains both its degree and its increasing vertex tuple.
```
abbrev AtomIndex (m : ℕ) := Σ p, Basis m p
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis
def OAI.Thomason.Construction.SimplexComplex.atomCell line 793
def OAI.Thomason.Construction.SimplexComplex.atomHeight line 796
theorem OAI.Thomason.Construction.SimplexComplex.atomCell_isBasisAtom line 798
def OAI.Thomason.Construction.SimplexComplex.chainAtomIndices line 802
Source documentation
A finite integral positive chain specifies a finite list of atoms.
```
noncomputable def chainAtomIndices {m p : ℕ} (z : Chains m p) : List (AtomIndex m) :=
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.AtomIndex
theorem OAI.Thomason.Construction.SimplexComplex.chainAtomIndices_degree line 805
theorem OAI.Thomason.Construction.SimplexComplex.sum_map_flatMap line 812
theorem OAI.Thomason.Construction.SimplexComplex.chainAtomIndices_table line 821
Source documentation
The top chains of the listed atoms sum to precisely the original chain.
```
theorem chainAtomIndices_table (h : NormalizedSimplexIdentities) {m p : ℕ}
    (z : Chains m p) (hz : z ∈ positive m p) (side : Bool) :
    (Cell.PositiveTable.ofCells ((chainAtomIndices z).map (atomCell h))).table side p = z := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, OAI.Thomason.Construction.SimplexComplex.chainAtomIndices, OAI.Thomason.Construction.SimplexComplex.atomCell
theorem OAI.Thomason.Construction.SimplexComplex.chainAtomIndices_above line 845
Source documentation
No listed atom contributes above the degree of the chain.
```
theorem chainAtomIndices_above (h : NormalizedSimplexIdentities) {m p : ℕ}
    (z : Chains m p) (n : ℕ) (hn : p < n) (side : Bool) :
    (Cell.PositiveTable.ofCells ((chainAtomIndices z).map (atomCell h))).table side n = 0 := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.chainAtomIndices, OAI.Thomason.Construction.SimplexComplex.atomCell
def OAI.Thomason.Construction.SimplexComplex.sortAtoms line 857
Source documentation
Height sorting is a permutation, so it retains every positive table.
```
noncomputable def sortAtoms {m : ℕ} (as : List (AtomIndex m)) : List (AtomIndex m) :=
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.AtomIndex
theorem OAI.Thomason.Construction.SimplexComplex.sortAtoms_perm line 860
theorem OAI.Thomason.Construction.SimplexComplex.sortAtoms_pairwise line 863
theorem OAI.Thomason.Construction.SimplexComplex.sortAtoms_table line 873
def OAI.Thomason.Construction.SimplexComplex.orderedAtomBasis line 895
Source documentation
Every field is the corresponding literal normalized-chain construction. No generation assertion is required by this interface.
```
noncomputable def orderedAtomBasis (h : NormalizedSimplexIdentities) (m : ℕ) :
    OrderedAtomBasis (directedComplex m (h.squared m)) where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.directedComplex
def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinderOrderedAtomBasis line 927
theorem OAI.Thomason.Construction.SimplexComplex.orderedAtomBasis_sideHeight line 945
def OAI.Thomason.Construction.SimplexComplex.cylinderOrderedAtomBasis line 953
Source documentation
The concrete right interval tensor on each normalized simplex has an actual ordered atom basis, including all mixed prisms.
```
noncomputable def cylinderOrderedAtomBasis (h : NormalizedSimplexIdentities) (m : ℕ) :
    OrderedAtomBasis (rightCylinder (directedComplex m (h.squared m))) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.directedComplex
theorem OAI.Thomason.Construction.SimplexComplex.cylinder_generated line 959
Source documentation
Every strict cell of the actual simplex-chain cylinder is generated by its explicit endpoint atoms and mixed prism atoms.
```
theorem cylinder_generated (h : NormalizedSimplexIdentities) (m : ℕ)
    (P : Cell (rightCylinder (directedComplex m (h.squared m))) → Prop)
    (hatom : ∀ p b, P ((cylinderOrderedAtomBasis h m).atom p b))
    (hcomp : ∀ n x y hxy, P x → P y → P (Cell.comp x y n hxy)) : ∀ X, P X :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.directedComplex, OAI.Thomason.Construction.SimplexComplex.cylinderOrderedAtomBasis