OAI/CategoryTheory/Thomason/OrientalCounit.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Oriental Counit.

  1. def OAI.Thomason.DirectedComplex.Table.removeContextRow line 16
  2. lemma OAI.Thomason.DirectedComplex.Table.removeContextRow_middle line 22
  3. lemma OAI.Thomason.DirectedComplex.Table.removeContextRow_top line 27
  4. lemma OAI.Thomason.DirectedComplex.Table.removeContextRow_other line 31
  5. def OAI.Thomason.DirectedComplex.Table.removeContext line 35
  6. lemma OAI.Thomason.DirectedComplex.Table.removeContext_row line 82
  7. lemma OAI.Thomason.DirectedComplex.Table.removeContext_dimension line 88
  8. lemma OAI.Thomason.DirectedComplex.Table.factor_context line 116
  9. lemma OAI.Thomason.NormalizedChains.positive_common_context line 201
  10. lemma OAI.Thomason.NormalizedChains.filter_mem_grade line 220
  11. lemma OAI.Thomason.NormalizedChains.filter_positive line 228
  12. def OAI.Thomason.NormalizedChains.rankBefore line 236
  13. def OAI.Thomason.NormalizedChains.rankAfter line 239
  14. lemma OAI.Thomason.NormalizedChains.rankBefore_add_rankAfter line 242
  15. lemma OAI.Thomason.NormalizedChains.boundary_nonneg_of_before line 245
  16. lemma OAI.Thomason.NormalizedChains.boundary_nonpos_of_after line 258
  17. lemma OAI.Thomason.NormalizedChains.rankBefore_boundary_nonneg line 271
  18. lemma OAI.Thomason.NormalizedChains.rankAfter_boundary_nonpos line 279
  19. lemma OAI.Thomason.NormalizedChains.rank_cut_positive line 287
  20. lemma OAI.Thomason.NormalizedChains.positive_augmentation_zero line 332
  21. inductive OAI.Thomason.NormalizedChains.AtomPasting line 355
  22. lemma OAI.Thomason.NormalizedChains.common_atom_context line 361
  23. lemma OAI.Thomason.NormalizedChains.atom_context_pasting line 383
  24. lemma OAI.Thomason.NormalizedChains.rows_above_top_agree line 467
  25. lemma OAI.Thomason.NormalizedChains.oriental_atomic_pasting line 478
  26. lemma OAI.Thomason.NormalizedChains.oriental_all_atomic line 518
  27. lemma OAI.Thomason.DirectedComplex.Table.dimension_of_rows_above_zero line 532
  28. lemma OAI.Thomason.NormalizedChains.positive_add_zero line 562
  29. lemma OAI.Thomason.NormalizedChains.comp_dimension_factors line 572
  30. lemma OAI.Thomason.NormalizedChains.oriental_functor_ext line 601
  31. def OAI.Thomason.NormalizedChains.basisLambda line 629
  32. lemma OAI.Thomason.NormalizedChains.basisLambda_cons line 641
  33. def OAI.Thomason.NormalizedChains.atomCounitInverse line 648
  34. lemma OAI.Thomason.NormalizedChains.atomCounitInverse_bracket line 652
  35. lemma OAI.Thomason.NormalizedChains.simplexAtom_dimension_le line 658
  36. lemma OAI.Thomason.NormalizedChains.atomCounitInverse_top line 674
  37. lemma OAI.Thomason.NormalizedChains.oriental_lambdaCounit_leftInverse line 721
  38. lemma OAI.Thomason.NormalizedChains.oriental_lambdaCounit_injective line 731