TruncationCongruence.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Boundary lifting constructs actual simplicial deformation data

No weak-equivalence assertion is used in the construction. It uses only the proved generation of monomorphisms by boundaries and two concrete lifts.

structure OAI.Thomason.Construction.BoundaryRetraction line 27
Source documentation
A section and an actual simplicial homotopy to its other composite.
```
structure BoundaryRetraction {X Y : SSet.{u}} (f : X ⟶ Y) where
…
```
def OAI.Thomason.Construction.boundaryRetraction line 34
Source documentation
Every map lifting against boundaries admits explicit simplicial retraction data.
```
noncomputable def boundaryRetraction {X Y : SSet.{u}} (f : X ⟶ Y) (hf : I.rlp f) :
    BoundaryRetraction f := by
…
```
Mentions: OAI.Thomason.Construction.BoundaryRetraction
def OAI.Thomason.Construction.intervalBoundaryFamily line 87
Source documentation
Assemble two maps on the two components of an interval boundary.
```
def intervalBoundaryFamily {K X : SSet.{u}} (f₀ f₁ : K ⟶ X) :
    K ⊗ (SSet.boundary 1 : SSet.{u}) ⟶ X where
…
```
theorem OAI.Thomason.Construction.intervalBoundaryFamily_zero line 108
theorem OAI.Thomason.Construction.intervalBoundaryFamily_one line 123
theorem OAI.Thomason.Construction.intervalBoundaryFamily_naturality line 138
theorem OAI.Thomason.Construction.intervalBoundaryFamily_restriction line 148
theorem OAI.Thomason.Construction.intervalBoundaryFamily_endpoints line 157
theorem OAI.Thomason.Construction.anodyne_right_cancellation line 194
theorem OAI.Thomason.Construction.anodyne_subcomplex_congr line 258
theorem OAI.Thomason.Construction.finite_anodyne_union_aux line 266

theorem OAI.Thomason.Construction.finite_anodyne_union line 353

Source documentation

A finite family closed under intersections glues relative anodyne inclusions into an anodyne inclusion of its union.

theorem finite_anodyne_union {X : SSet.{0}} (F : Finset X.Subcomplex)
    (C : Set X.Subcomplex) (J : X.Subcomplex)
    (hC : ∀ A ∈ C, ∀ B ∈ C, A ⊓ B ∈ C)
    (hJ : ∀ A ∈ C, SSet.anodyneExtensions (SSet.Subcomplex.homOfLE
      (show J ⊓ A ≤ A from inf_le_right)))
    (hFC : ∀ A ∈ F, A ∈ C) :
    SSet.anodyneExtensions (SSet.Subcomplex.homOfLE
      (show J ≤ J ⊔ F.sup id from le_sup_left)) :=
…

theorem OAI.Thomason.Construction.anodyne_of_arrow_homotopies line 389

Source documentation

Compatible homotopies from a pair map through an anodyne arrow to the identity transport every exact Kan lifting problem. No retraction identities for the intervening pair maps are needed.

theorem anodyne_of_arrow_homotopies {A B C D : SSet.{0}}
    (i : A ⟶ B) [Mono i] (j : C ⟶ D) (hj : SSet.anodyneExtensions j)
    (rA : A ⟶ C) (rB : B ⟶ D) (sA : C ⟶ A) (sB : D ⟶ B)
    (hr : i ≫ rB = rA ≫ j) (hs : j ≫ sB = sA ≫ i)
    (HA : SSet.Homotopy (rA ≫ sA) (𝟙 A))
    (HB : SSet.Homotopy (rB ≫ sB) (𝟙 B))
    (hH : i ▷ Δ[1] ≫ HB.h = HA.h ≫ i) : SSet.anodyneExtensions i := by
…

theorem OAI.Thomason.Construction.anodyne_of_arrow_homotopies_reverse line 424

Source documentation

The same transport works for compatible homotopies with the opposite orientation, using the final-endpoint cylinder lifting property.

theorem anodyne_of_arrow_homotopies_reverse {A B C D : SSet.{0}}
    (i : A ⟶ B) [Mono i] (j : C ⟶ D) (hj : SSet.anodyneExtensions j)
    (rA : A ⟶ C) (rB : B ⟶ D) (sA : C ⟶ A) (sB : D ⟶ B)
    (hr : i ≫ rB = rA ≫ j) (hs : j ≫ sB = sA ≫ i)
    (HA : SSet.Homotopy (𝟙 A) (rA ≫ sA))
    (HB : SSet.Homotopy (𝟙 B) (rB ≫ sB))
    (hH : i ▷ Δ[1] ≫ HB.h = HA.h ≫ i) : SSet.anodyneExtensions i := by
…

theorem OAI.Thomason.Construction.anodyne_of_arrow_homotopy_zigzag line 459

Source documentation

A two-step compatible zigzag of homotopies of pairs also transports anodyne lifting. This is the shape of the elementary face-poset collapse.

theorem anodyne_of_arrow_homotopy_zigzag {A B C D : SSet.{0}}
    (i : A ⟶ B) [Mono i] (j : C ⟶ D) (hj : SSet.anodyneExtensions j)
    (rA : A ⟶ C) (rB : B ⟶ D) (sA : C ⟶ A) (sB : D ⟶ B)
    (hr : i ≫ rB = rA ≫ j) (hs : j ≫ sB = sA ≫ i)
    (uA : A ⟶ A) (uB : B ⟶ B)
    (HA : SSet.Homotopy (rA ≫ sA) uA) (HB : SSet.Homotopy (rB ≫ sB) uB)
    (hH : i ▷ Δ[1] ≫ HB.h = HA.h ≫ i)
    (GA : SSet.Homotopy (𝟙 A) uA) (GB : SSet.Homotopy (𝟙 B) uB)
    (hG : i ▷ Δ[1] ≫ GB.h = GA.h ≫ i) : SSet.anodyneExtensions i := by
…

theorem OAI.Thomason.Construction.anodyne_of_arrow_homotopy_cospan line 530

Source documentation

The reversed orientation of the two-step pair homotopy also transports anodyne lifting. This is the orientation of the explicit horn contraction.

theorem anodyne_of_arrow_homotopy_cospan {A B C D : SSet.{0}}
    (i : A ⟶ B) [Mono i] (j : C ⟶ D) (hj : SSet.anodyneExtensions j)
    (rA : A ⟶ C) (rB : B ⟶ D) (sA : C ⟶ A) (sB : D ⟶ B)
    (hr : i ≫ rB = rA ≫ j) (hs : j ≫ sB = sA ≫ i)
    (uA : A ⟶ A) (uB : B ⟶ B)
    (HA : SSet.Homotopy uA (rA ≫ sA)) (HB : SSet.Homotopy uB (rB ≫ sB))
    (hH : i ▷ Δ[1] ≫ HB.h = HA.h ≫ i)
    (GA : SSet.Homotopy uA (𝟙 A)) (GB : SSet.Homotopy uB (𝟙 B))
    (hG : i ▷ Δ[1] ≫ GB.h = GA.h ≫ i) : SSet.anodyneExtensions i := by
…

theorem OAI.Thomason.Construction.intervalBoundary_endpoints line 601

theorem OAI.Thomason.Construction.exists_kan_fixed_endpoint_lift line 620

Source documentation

An anodyne parameter extension lifts a cylinder over a Kan fibration while preserving two specified constant endpoints exactly.

theorem exists_kan_fixed_endpoint_lift {A K E B : SSet.{u}}
    (i : A ⟶ K) (hi : SSet.anodyneExtensions i)
    (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (x₀ x₁ : E _⦋0⦌) (a : A ⊗ Δ[1] ⟶ E) (b : K ⊗ Δ[1] ⟶ B)
    (ha₀ : SSet.ι₀ ≫ a = SSet.const x₀) (ha₁ : SSet.ι₁ ≫ a = SSet.const x₁)
    (hb₀ : SSet.ι₀ ≫ b = SSet.const (p.app _ x₀))
    (hb₁ : SSet.ι₁ ≫ b = SSet.const (p.app _ x₁))
    (hab : a ≫ p = i ▷ Δ[1] ≫ b) :
    ∃ e : K ⊗ Δ[1] ⟶ E, i ▷ Δ[1] ≫ e = a ∧ e ≫ p = b ∧
      SSet.ι₀ ≫ e = SSet.const x₀ ∧ SSet.ι₁ ≫ e = SSet.const x₁ := by
…

def OAI.Thomason.Construction.SimplexComplex.AboveAtomOrZero line 663
Source documentation
The upper table is zero or agrees with one higher-dimensional atom.
```
def AboveAtomOrZero (h : NormalizedSimplexIdentities) {m : ℕ}
    (r : ℕ) (X : h.object m) : Prop :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities
theorem OAI.Thomason.Construction.SimplexComplex.eq_vertex_atom_of_above_zero line 670
Source documentation
A cell with no positive-dimensional chains is the corresponding vertex atom.
```
theorem eq_vertex_atom_of_above_zero (h : NormalizedSimplexIdentities) {m : ℕ}
    (X : h.object m) (hz : ∀ n, 0 < n → ∀ side, X.table side n = 0) :
    ∃ b : Basis m 0, X = basisAtom h b := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.basisAtom
theorem OAI.Thomason.Construction.SimplexComplex.upper_atom_decomposition line 692
Source documentation
Lowering one degree expresses the upper table as a finite sum of atoms.
```
theorem upper_atom_decomposition (h : NormalizedSimplexIdentities) {m : ℕ}
    (r : ℕ) (X : h.object m) (hx : AboveAtomOrZero h (r+1) X) :
    ∃ as : List (AtomIndex m),
      (∀ a ∈ as, r < a.1) ∧
      ∀ n, r < n → ∀ side, X.table side n =
        (Cell.PositiveTable.ofCells (as.map (atomCell h))).table side n := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.AboveAtomOrZero, OAI.Thomason.Construction.SimplexComplex.AtomIndex, OAI.Thomason.Construction.SimplexComplex.atomCell

theorem OAI.Thomason.Construction.SimplexComplex.predicate_of_upper_atom_sum line 744

Source documentation

Sorting an upper atom sum supplies actual iterated strict composites.

theorem predicate_of_upper_atom_sum (h : NormalizedSimplexIdentities) {m : ℕ}
    (r : ℕ) (P : h.object m → Prop)
    (hbase : ∀ X, AboveAtomOrZero h r X → P X)
    (hcomp : ∀ n x y hxy, P x → P y → P ((h.object m).comp n x y hxy))
    (as : List (AtomIndex m)) (hd : ∀ a ∈ as, r < a.1)
    (X : h.object m)
    (he : ∀ n, r < n → ∀ side, X.table side n =
      (Cell.PositiveTable.ofCells (as.map (atomCell h))).table side n) : P X := by
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.AboveAtomOrZero, OAI.Thomason.Construction.SimplexComplex.AtomIndex, OAI.Thomason.Construction.SimplexComplex.atomCell

theorem OAI.Thomason.Construction.SimplexComplex.generated_by_basisAtoms line 771
Source documentation
Every composition-closed predicate containing the constructed atoms contains every cell of the concrete oriental.
```
theorem generated_by_basisAtoms (h : NormalizedSimplexIdentities) (m : ℕ)
    (P : h.object m → Prop)
    (hatom : ∀ p (b : Basis m p), P (basisAtom h b))
    (hcomp : ∀ n x y hxy, P x → P y → P ((h.object m).comp n x y hxy)) :
    ∀ X, P X := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.basisAtom
theorem OAI.Thomason.Construction.simplexGenerationInput line 800
Source documentation
Normalized simplex complexes satisfy the basis-atom generation property.
```
theorem simplexGenerationInput (h : NormalizedSimplexIdentities) :
    PublishedSimplexGenerationInput h where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.PublishedSimplexGenerationInput
def OAI.Thomason.Construction.simplexAtoms line 806
Source documentation
All atom data, including generation, are constructed from normalized simplex identities.
```
noncomputable def simplexAtoms (h : NormalizedSimplexIdentities) : SimplexAtomsInput h :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput
theorem OAI.Thomason.Construction.SimplexComplex.hom_ext_atoms line 823
Source documentation
Atom generation detects equality of strict functors into any strict omega-category, including the naturality squares for the Gray comparison.
```
theorem hom_ext_atoms (h : NormalizedSimplexIdentities) {m : ℕ}
    {D : StrictOmegaCategory} (F G : h.object m ⟶ D)
    (he : ∀ p (b : Basis m p), F.toFun (basisAtom h b) = G.toFun (basisAtom h b)) : F = G := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictOmegaCategory, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.basisAtom
theorem OAI.Thomason.Construction.anodyne_of_simplicial_deformation line 858
Source documentation
A monomorphism with an actual simplicial retraction and stationary simplicial deformation has the left lifting property against every Kan fibration. No realization-to-simplicial approximation is assumed.
```
theorem anodyne_of_simplicial_deformation {A B : SSet.{0}} (i : A ⟶ B) [Mono i]
    (r : B ⟶ A) (hir : i ≫ r = 𝟙 A)
    (H : SSet.Homotopy (r ≫ i) (𝟙 B))
    (hs : i ▷ Δ[1] ≫ H.h = fst A Δ[1] ≫ i) : SSet.anodyneExtensions i := by
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.topFace line 915

inductive OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Rel line 919

Source documentation

The least composition congruence killing all cells above dimension n.

inductive Rel : C.bounded n → C.bounded n → Prop
  | refl (x) : Rel x x
  | symm {x y} : Rel x y → Rel y x
  | trans {x y z} : Rel x y → Rel y z → Rel x z
  | collapse (x : C) : Rel (topFace C n false x) (topFace C n true x)
  | compose (m : ℕ) (x y x' y' : C.bounded n)
      (h : (C.bounded n).target m x = (C.bounded n).source m y)
      (h' : (C.bounded n).target m x' = (C.bounded n).source m y') :
      Rel x x' → Rel y y' →
        Rel ((C.bounded n).comp m x y h) ((C.bounded n).comp m x' y' h')

variable {C n}

Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.topFace, OAI.Thomason.Construction.StrictOmegaCategory.target, OAI.Thomason.Construction.StrictOmegaCategory.source, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.comp

theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Rel.lower_faces line 933
Source documentation
The generating identifications never change a surviving lower face.
```
theorem Rel.lower_faces {x y : C.bounded n} (h : Rel C n x y)
    (a : Bool) (k : ℕ) (hk : k < n) : C.face a k x.val = C.face a k y.val := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Rel
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Rel.eq_of_dimensionLE line 958
Source documentation
Equivalence at the top dimension is equality on lower-dimensional cells.
```
theorem Rel.eq_of_dimensionLE {x y : C.bounded n} (h : Rel C n x y)
    {k : ℕ} (hk : k < n) (hx : C.DimensionLE k x.val) (hy : C.DimensionLE k y.val) :
    x = y := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Rel
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Rel.map_eq line 965
Source documentation
Every strict functor into dimension n kills exactly the imposed generators.
```
theorem Rel.map_eq {D : StrictOmegaCategory.{0}} (hD : D.IsTruncated n) (f : C ⟶ D)
    {x y : C.bounded n} (h : Rel C n x y) : f.toFun x.val = f.toFun y.val := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Rel
instance OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.truncationSetoid line 986
abbrev OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.Cell line 991
Source documentation
Carrier of the intelligent truncation, before equipping its operations.
```
abbrev Cell (C : StrictOmegaCategory.{0}) (n : ℕ) := Quotient (truncationSetoid (C := C) (n := n))
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.truncationSetoid