FiniteCosieveAttachmentComparison.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The weak comparison for attachments of finite face-chain posets

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_chain_attachment_comparison line 20
Source documentation
Face-chain attachments satisfy the actual Street comparison, including the empty old face set. No retraction of the whole chain poset is used.
```
theorem finite_chain_attachment_comparison
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P] (S : Set P)
    {X Y : StrictOmegaCategory.{0}}
    {a : h.categorification.obj (nerve (ChainSieve.old S)) ⟶ X}
    {b : h.categorification.obj (nerve (NonemptyFiniteChains P)) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (h.posetMap (subposetInclusion (ChainSieve.old S))) a b j) :
    realizationWeakEquivalences (nervePushoutComparison h.streetNerve hp) := by
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.ChainSieve.old, OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.nervePushoutComparison

theorem OAI.Thomason.Construction.FiniteReflectionInput.containing_cosieve_attachment_comparison line 52

Source documentation

Couniversality on a containing cosieve controls the actual attachment comparison, with all pushouts taken in the finite category.

theorem containing_cosieve_attachment_comparison
    (g : PublishedSimplicialGluingInput) (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] (A Z C : Set P)
    (hZ : IsUpperSet Z) (hC : IsUpperSet C) (hAZ : A ⊆ Z)
    (hAC : ∀ x ∈ A, x ∉ C) (cover : ∀ x, x ∈ Z ∨ x ∈ C)
    (wZ : h.FiniteCouniversalStreetWeakEquivalence n
      (r.reflect.map (h.posetMap (subposetInclusionWithin A Z hAZ))))
    [Mono ((h.finiteStreetNerve (n+1)).map
      (r.reflect.map (h.posetMap (subposetInclusionWithin A Z hAZ))))]
    {X Y : Truncated.{0} (n+1)}
    {a : (r.categorification h).obj (nerve A) ⟶ X}
    {b : (r.categorification h).obj (nerve P) ⟶ Y} {j : X ⟶ Y}
…

Mentions: OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.subposetInclusionWithin

theorem OAI.Thomason.Construction.FiniteReflectionInput.finite_dwyer_attachment_comparison line 104

Source documentation

A right adjoint on the containing cosieve suffices in every positive finite dimension; the ambient poset need not retract onto the sieve.

theorem finite_dwyer_attachment_comparison
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P] (A Z : Set P)
    (hA : IsLowerSet A) (hZ : IsUpperSet Z) (hAZ : A ⊆ Z)
    (R : SieveRetraction {z : Z | z.val ∈ A})
    {X Y : Truncated.{0} (n+1)}
    {a : (r.categorification h).obj (nerve A) ⟶ X}
    {b : (r.categorification h).obj (nerve P) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (r.reflect.map (h.posetMap (subposetInclusion A))) a b j) :
…

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.SieveRetraction, OAI.Thomason.Construction.subposetInclusion

theorem OAI.Thomason.Construction.FiniteReflectionInput.finite_chain_attachment_comparison line 140

Source documentation

Actual finite-dimensional comparison for chains on any finite face set.

theorem finite_chain_attachment_comparison
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P] (S : Set P)
    {X Y : Truncated.{0} (n+1)}
    {a : (r.categorification h).obj (nerve (ChainSieve.old S)) ⟶ X}
    {b : (r.categorification h).obj (nerve (NonemptyFiniteChains P)) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (r.reflect.map (h.posetMap (subposetInclusion (ChainSieve.old S)))) a b j) :
    realizationWeakEquivalences (nervePushoutComparison (h.finiteStreetNerve (n+1)) hp) := 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.ChainSieve.old, OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.nervePushoutComparison