OAI/CategoryTheory/Thomason/FiniteGluing.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Finite Gluing.

  1. lemma OAI.Thomason.DirectedComplex.RankedAtoms.positive_add_zero line 17
  2. lemma OAI.Thomason.DirectedComplex.RankedAtoms.comp_dimension_factors line 28
  3. lemma OAI.Thomason.DirectedComplex.RankedAtoms.atom_dimension_le line 54
  4. inductive OAI.Thomason.DirectedComplex.RankedAtoms.BoundedPasting line 62
  5. lemma OAI.Thomason.DirectedComplex.RankedAtoms.bounded_pasting line 68
  6. lemma OAI.Thomason.DirectedComplex.RankedAtoms.functor_ext line 82
  7. lemma OAI.Thomason.DirectedComplex.RankedAtoms.surjective_onCells_of_lower_injective line 94
  8. lemma OAI.Thomason.DirectedComplex.RankedAtoms.epi_of_atoms_in_range line 120
  9. def OAI.Thomason.DirectedComplex.RankedAtoms.transport line 143
  10. lemma OAI.Thomason.NormalizedChains.complexMap_orderIso_inverse line 191
  11. def OAI.Thomason.NormalizedChains.Prism.Basis.ofOrderIso line 201
  12. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_atom_lift line 223
  13. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_finiteSimplex_epi line 253
  14. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_finiteSimplex_three_surjective line 266
  15. def OAI.Thomason.OmegaCategory.Functor.liftNCell line 298
  16. lemma OAI.Thomason.OmegaCategory.Functor.map_liftNCell line 301
  17. lemma OAI.Thomason.OmegaCategory.Functor.liftNCell_unique line 306
  18. lemma OAI.Thomason.OmegaCategory.Functor.liftNCell_source line 312
  19. lemma OAI.Thomason.OmegaCategory.Functor.liftNCell_target_lt line 318
  20. lemma OAI.Thomason.OmegaCategory.Functor.map_liftNCell_map line 325
  21. lemma OAI.Thomason.OmegaCategory.Functor.map_liftNCell_faces line 330
  22. def OAI.Thomason.OmegaCategory.Functor.descendTruncated line 347
  23. lemma OAI.Thomason.OmegaCategory.Functor.descendTruncated_fac line 392
  24. lemma OAI.Thomason.OmegaCategory.Functor.precomp_injective_of_cells_surjective line 399
  25. theorem OAI.Thomason.OmegaCategory.Functor.precomp_bijective_truncated line 411
  26. structure OAI.Thomason.RightIntervalCore line 428
  27. def OAI.Thomason.GrayRecursive.IntervalHom.intervalCore line 462
  28. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_precomp_bijective_two line 478
  29. lemma OAI.Thomason.RightIntervalCore.internalHom_truncated line 498
  30. def OAI.Thomason.RightIntervalCore.truncatedCylinderEquiv line 534
  31. lemma OAI.Thomason.RightIntervalCore.truncatedCylinderEquiv_apply line 542
  32. lemma OAI.Thomason.RightIntervalCore.truncatedCylinderEquiv_endpoint line 553
  33. def OAI.Thomason.RightIntervalCore.finiteInternalHom line 576
  34. def OAI.Thomason.RightIntervalCore.finiteTranspose line 582
  35. def OAI.Thomason.RightIntervalCore.finiteGlue line 591
  36. lemma OAI.Thomason.RightIntervalCore.finiteGlue_left line 602
  37. lemma OAI.Thomason.RightIntervalCore.finiteGlue_right line 612
  38. lemma OAI.Thomason.RightIntervalCore.finiteCylinder_hom_ext line 623
  39. lemma OAI.Thomason.RightIntervalCore.finiteGlue_endpoint_left line 637
  40. lemma OAI.Thomason.RightIntervalCore.finiteGlue_endpoint_right line 649
  41. theorem OAI.Thomason.RightIntervalCore.finite_stationary_gluing line 663
  42. lemma OAI.Thomason.RightIntervalCore.finite_stationary_gluing_natural line 706