OAI/CategoryTheory/Thomason/Transfer/GridGlobeCylinderPushout.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual chain-cylinder model preserves the interchange pushout

  1. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.generated_image line 16
  2. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.row_atom_eq_lift line 29
  3. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.row_generated line 44
  4. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.generated line 69
  5. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.basisIso line 79
  6. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.modelIso line 84
  7. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.modelIso_hom line 88
  8. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.isPushout line 93