ThomasonLeftProperness.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Weak preservation from the actual nerve attachment comparison

theorem OAI.Thomason.Construction.attachment_weak_of_nerve_comparison line 30

Source documentation

A weak attaching nerve and the actual weak comparison give a weak attachment in the original category.

theorem attachment_weak_of_nerve_comparison
    {A B X Y : C} {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) [Mono (N.map i)]
    (wi : realizationWeakEquivalences (N.map i))
    (wc : realizationWeakEquivalences (nervePushoutComparison N hp)) :
    realizationWeakEquivalences (N.map j) := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.nervePushoutComparison

theorem OAI.Thomason.Construction.universalWeakPreserving_of_nerve_comparisons line 44
Source documentation
Weak nerve comparisons for all attachments imply universal preservation of weak equivalences. This is the local geometric input to left properness.
```
theorem universalWeakPreserving_of_nerve_comparisons
    {A B : C} (i : A ⟶ B) [Mono (N.map i)]
    (hcomp : ∀ {X Y : C} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
      (hp : IsPushout i a b j), realizationWeakEquivalences (nervePushoutComparison N hp)) :
    universalWeakPreserving (realizationWeakEquivalences.inverseImage N) i := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.nervePushoutComparison
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_chain_attachment_universal line 105
theorem OAI.Thomason.Construction.FiniteReflectionInput.finite_chain_attachment_universal line 124
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomason_leftProper_of_individual_boundaries line 170
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.properCombinatorialAxioms_of_individual_attachments line 183
Source documentation
The complete proper combinatorial axioms follow from the two individual geometric attachment tests, with no abstract transfer theorem.
```
theorem properCombinatorialAxioms_of_individual_attachments
    (hb : imageBoundaries h.thomasonLeft ≤ universalWeakPreserving h.streetWeakEquivalences)
    (hj : (imageHorns h.thomasonLeft).pushouts ≤ h.streetWeakEquivalences) :
    ProperCombinatorialAxioms StrictOmegaCategory.{0} h.streetWeakEquivalences
      h.thomasonFibrations where
…
```
Mentions: OAI.Thomason.Construction.imageBoundaries, OAI.Thomason.Construction.imageHorns, OAI.Thomason.Construction.ProperCombinatorialAxioms
theorem OAI.Thomason.Construction.FiniteReflectionInput.thomason_leftProper_of_individual_boundaries line 211
theorem OAI.Thomason.Construction.FiniteReflectionInput.properCombinatorialAxioms_of_individual_attachments line 230
Source documentation
The same single-generator tests give the prescribed proper model axioms in every positive finite dimension.
```
theorem properCombinatorialAxioms_of_individual_attachments
    (hb : imageBoundaries (thomasonLeft r h) ≤
      universalWeakPreserving (thomasonWeakEquivalences (n := n) h))
…
```
Mentions: OAI.Thomason.Construction.imageBoundaries, OAI.Thomason.Construction.FiniteReflectionInput.thomasonLeft, OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences