OAI/CategoryTheory/Thomason/Transfer/FiveInputMainTheorem.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thomason.Construction.main_with_five_published_inputs line 15

   Source documentation

   The all-dimensions theorem with five published-input hypotheses. The canonical-extension weak equivalence follows from the subdivision homotopy and its realization comparison.

   theorem main_with_five_published_inputs
       (G : RightGrayInput normalizedSimplexIdentities) (t : GrayTruncationInput G)
       (hk : PublishedAcyclicKanLifting)
       (transfer : PublishedThomasonReduction normalizedSimplexIdentities)
       (loc : PublishedStreetLocalizationInput normalizedSimplexIdentities) :
       let kq := kanQuillenInput_of_acyclic_kan_lifting hk
   …

   Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.normalizedSimplexIdentities, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.PublishedAcyclicKanLifting, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.PublishedStreetLocalizationInput, OAI.Thomason.Construction.kanQuillenInput_of_acyclic_kan_lifting