Main.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Acyclic attachments of literal twice-subdivided simplex subcomplexes

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.subcomplex_attachment_acyclic line 134
Source documentation
The actual Thomason image of an acyclic simplex-subcomplex inclusion remains a Street weak equivalence under every individual attachment.
```
theorem subcomplex_attachment_acyclic
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {m : ℕ} (A : (Δ[m] : SSet.{0}).Subcomplex)
    (hA : realizationWeakEquivalences A.ι) :
    cobaseWeak h.streetWeakEquivalences (h.thomasonLeft.map A.ι) := by
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.FiniteReflectionInput.subcomplex_attachment_acyclic line 172
Source documentation
Finite reflection retains the same acyclic attachment theorem in the original category of strict (n+1)-categories.
```
theorem subcomplex_attachment_acyclic
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {m : ℕ} (A : (Δ[m] : SSet.{0}).Subcomplex)
    (hA : realizationWeakEquivalences A.ι) :
    cobaseWeak (thomasonWeakEquivalences (n := n) h) ((r.thomasonLeft h).map A.ι) := by
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.imageBoundaries_universal line 229
Source documentation
The literal generating boundaries universally preserve Street weak maps.
```
theorem imageBoundaries_universal
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0}) :
    imageBoundaries h.thomasonLeft ≤ universalWeakPreserving h.streetWeakEquivalences := by
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.imageBoundaries
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.imageHorns_pushouts_weak line 239
Source documentation
Every individual generating horn attachment is a Street weak equivalence.
```
theorem imageHorns_pushouts_weak
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0}) :
    (imageHorns h.thomasonLeft).pushouts ≤ h.streetWeakEquivalences := by
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.imageHorns
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.geometric_model_axioms line 253
Source documentation
The proper combinatorial structure is proved directly from the actual horn and boundary geometry, with no abstract transfer input.
```
theorem geometric_model_axioms
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0}) :
    ProperCombinatorialAxioms StrictOmegaCategory.{0} h.streetWeakEquivalences h.thomasonFibrations :=
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.ProperCombinatorialAxioms
theorem OAI.Thomason.Construction.FiniteReflectionInput.imageBoundaries_universal line 271
Source documentation
The literal finite-dimensional generating boundary test.
```
theorem imageBoundaries_universal
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0}) :
    imageBoundaries (r.thomasonLeft h) ≤
      universalWeakPreserving (thomasonWeakEquivalences (n := n) h) := by
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.imageBoundaries, OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences
theorem OAI.Thomason.Construction.FiniteReflectionInput.imageHorns_pushouts_weak line 283
Source documentation
Every original finite-dimensional generating horn attachment is weak.
```
theorem imageHorns_pushouts_weak
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0}) :
    (imageHorns (r.thomasonLeft h)).pushouts ≤ thomasonWeakEquivalences (n := n) h := by
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.imageHorns, OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences
theorem OAI.Thomason.Construction.FiniteReflectionInput.geometric_model_axioms line 297
Source documentation
The actual proper combinatorial axioms in each positive finite dimension.
```
theorem geometric_model_axioms
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0}) :
    ProperCombinatorialAxioms (Truncated.{0} (n+1))
      (thomasonWeakEquivalences (n := n) h) (thomasonFibrations (n := n) h) :=
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.ProperCombinatorialAxioms, OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences, OAI.Thomason.Construction.FiniteReflectionInput.thomasonFibrations
def OAI.Thomason.Construction.NormalizedSimplexIdentities.main_from_gray line 328
def OAI.Thomason.Construction.FiniteReflectionInput.main_from_gray line 347
theorem OAI.Thomason.Construction.main_with_two_published_inputs line 364
Source documentation
The omega and positive finite theorem family assuming Ara--Maltsiniotis's right Gray construction and Proposition A.29.
```
theorem main_with_two_published_inputs
    (G : RightGrayInput normalizedSimplexIdentities) (t : GrayTruncationInput G) :
    Nonempty (ThomasonModelResult normalizedSimplexIdentities.thomasonLeft
      normalizedSimplexIdentities.streetNerve constructedKanQuillenInput canonicalExtension_weak) ∧
      ∀ n, Nonempty (ThomasonModelResult
        ((constructedFiniteReflection n).thomasonLeft normalizedSimplexIdentities)
        (normalizedSimplexIdentities.finiteStreetNerve (n+1))
        constructedKanQuillenInput canonicalExtension_weak) := by
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.normalizedSimplexIdentities, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.ThomasonModelResult, OAI.Thomason.Construction.constructedKanQuillenInput, OAI.Thomason.Construction.canonicalExtension_weak, OAI.Thomason.Construction.constructedFiniteReflection, OAI.Thomason.thomasonLeft
theorem OAI.Thomason.Construction.thomason_model_structures_all_dimensions line 396
Source documentation
Proper combinatorial Thomason model structures and derived equivalences for strict omega categories and every positive finite dimension.
```
theorem thomason_model_structures_all_dimensions :
    Nonempty (ThomasonModelResult normalizedSimplexIdentities.thomasonLeft
      normalizedSimplexIdentities.streetNerve constructedKanQuillenInput canonicalExtension_weak) ∧
      ∀ n, Nonempty (ThomasonModelResult
        ((constructedFiniteReflection n).thomasonLeft normalizedSimplexIdentities)
        (normalizedSimplexIdentities.finiteStreetNerve (n+1))
        constructedKanQuillenInput canonicalExtension_weak) :=
…
```
Mentions: OAI.Thomason.Construction.ThomasonModelResult, OAI.Thomason.Construction.constructedKanQuillenInput, OAI.Thomason.Construction.canonicalExtension_weak, OAI.Thomason.Construction.constructedFiniteReflection, OAI.Thomason.thomasonLeft, OAI.Thomason.Construction.normalizedSimplexIdentities
theorem OAI.Thomason.Construction.finite_deletion_nerve_cover line 430
Source documentation
The finite deletion step in the couniversality proof gives an actual two-piece cover of the ordinary nerve. This is the ordinary-nerve side of the map of spans in Section 5 of the manuscript.
```
theorem finite_deletion_nerve_cover (R : SieveRetraction A)
    (hne : (Aᶜ).Nonempty)
    (hgreatest : ¬ ∃ x, SieveRetraction.GreatestNew (A := A) x) :
…
```
Mentions: OAI.Thomason.Construction.SieveRetraction, OAI.Thomason.Construction.SieveRetraction.GreatestNew
theorem OAI.Thomason.Construction.finite_deletion_nerve_pushout line 441
Source documentation
The same deletion step is a pushout square in actual simplicial sets.
```
theorem finite_deletion_nerve_pushout (R : SieveRetraction A)
    (hne : (Aᶜ).Nonempty)
    (hgreatest : ¬ ∃ x, SieveRetraction.GreatestNew (A := A) x) :
…
```
Mentions: OAI.Thomason.Construction.SieveRetraction, OAI.Thomason.Construction.SieveRetraction.GreatestNew