OAI/CategoryTheory/Thomason/Transfer/TripleGlobeCylinderPushout.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thomason.Construction.realizedCoproductData line 26

   Source documentation

   Actual realization of a coproduct inherits the componentwise deformations.

   def realizedCoproductData {α : Type} {A B : α → SSet.{0}} (f : ∀ a, A a ⟶ B a)
       (d : ∀ a, TopologicalDeformation.Data (SSet.toTop.map (f a))) :
       TopologicalDeformation.Data (SSet.toTop.map (CategoryTheory.Limits.Sigma.map f)) :=
   …

   Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data

2. def OAI.Thomason.Construction.simultaneousHornData line 44

   Source documentation

   A coproduct of generating horns has a stationary realized deformation.

   def simultaneousHornData {α : Type} (n : α → ℕ) (i : ∀ a, Fin (n a+2)) :
       TopologicalDeformation.Data (SSet.toTop.map
         (CategoryTheory.Limits.Sigma.map (fun a =>
           (Λ[n a+1, i a].ι : _ ⟶ (Δ[n a+1] : SSet.{0}))))) :=
   …

   Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data

3. theorem OAI.Thomason.Construction.simultaneous_horn_attachment_weak line 51

   Source documentation

   Attaching any family of horns at once is an actual realization weak equivalence.

   theorem simultaneous_horn_attachment_weak {α : Type} (n : α → ℕ) (i : ∀ a, Fin (n a+2))
       {X P : SSet.{0}}
       {f : (∐ fun a => (Λ[n a+1, i a] : SSet.{0})) ⟶ X}
       {b : (∐ fun a => (Δ[n a+1] : SSet.{0})) ⟶ P} {j : X ⟶ P}
       (h : IsPushout (CategoryTheory.Limits.Sigma.map
         (fun a => (Λ[n a+1, i a].ι : _ ⟶ (Δ[n a+1] : SSet.{0})))) f b j) :
       realizationWeakEquivalences j :=
   …

   Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

4. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.generated_image line 76
5. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.pair_basisComparison line 89
6. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.last_basisComparison line 95
7. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.pair_atom_eq_lift line 101
8. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.last_atom_eq_lift line 116
9. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.pair_generated line 132
10. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.last_generated line 157
11. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.generated line 180
12. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.basisIso line 189
13. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.modelIso line 194
14. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.modelIso_hom line 198
15. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.isPushout line 203