DoubleSubdivisionStability.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transport of attachment stability to the literal Thomason generators

theorem OAI.Thomason.Construction.DoubleSubdivisionPairs.map_property_iff line 21
Source documentation
Every property respecting arrow isomorphisms sees the literal twice subdivided inclusion as the finite old-chain inclusion.
```
theorem map_property_iff {C : Type*} [Category* C] (F : SSet.{0} ⥤ C)
    (W : MorphismProperty C) [W.RespectsIso]
    {m : ℕ} (A : (Δ[m] : SSet.{0}).Subcomplex) :
    W (F.map (SSet.sd.map (SSet.sd.map A.ι))) ↔
      W (F.map (nerveMap (subposetInclusion (ChainSieve.old (oldFaces A))).monotone.functor)) := by
…
```
Mentions: OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.ChainSieve.old, OAI.Thomason.Construction.DoubleSubdivisionPairs.oldFaces
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.subcomplex_attachment_universal line 39
Source documentation
The actual twice-subdivided inclusion of any simplex subcomplex universally preserves Street weak equivalences under attachment.
```
theorem subcomplex_attachment_universal
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {m : ℕ} (A : (Δ[m] : SSet.{0}).Subcomplex) :
    universalWeakPreserving 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
theorem OAI.Thomason.Construction.FiniteReflectionInput.subcomplex_attachment_universal line 60
Source documentation
The same literal-generator transport in every positive finite dimension.
```
theorem subcomplex_attachment_universal
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {m : ℕ} (A : (Δ[m] : SSet.{0}).Subcomplex) :
    universalWeakPreserving (thomasonWeakEquivalences (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.FiniteReflectionInput.thomasonWeakEquivalences