OAI/CategoryTheory/Thomason/AtomFibers.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Atom Fibers.

  1. theorem OAI.Thomason.finitePosetComparisonOfCore line 16
  2. def OAI.Thomason.finiteEndpointOfCore line 27
  3. def OAI.Thomason.exactEndpointTwo line 39
  4. theorem OAI.Thomason.endpointTwo line 45
  5. lemma OAI.Thomason.OmegaCategory.Functor.onCells_injective_mono line 61
  6. lemma OAI.Thomason.OmegaCategory.Functor.onCells_injective_of_map_injective line 71
  7. lemma OAI.Thomason.OmegaCategory.Functor.map_surjective_of_onCells_surjective line 76
  8. lemma OAI.Thomason.OmegaCategory.Functor.map_injective_of_onCells_injective line 83
  9. lemma OAI.Thomason.OmegaCategory.Functor.onCells_injective_of_isIso line 89
  10. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_finiteSimplex_surjective_of_lower_injective line 110
  11. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_finiteSimplex_isIso_of_injective line 129
  12. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_injective_of_higher_crossing line 138
  13. theorem OAI.Thomason.GrayRecursive.IntervalHom.fullMain_of_standard_higher_crossing_injective line 157
  14. theorem OAI.Thomason.GrayRecursive.IntervalHom.fullMain_of_standard_top_crossing_injective line 170
  15. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_precomp_bijective_of_injective line 187
  16. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_onCells_injective_of_iso line 201
  17. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_onCells_injective_of_standard line 222
  18. def OAI.Thomason.finiteEndpointOfStandardInjectivity line 246
  19. lemma OAI.Thomason.DirectedComplex.RankedAtoms.atom_face_coefficient_pos line 268
  20. lemma OAI.Thomason.DirectedComplex.RankedAtoms.basis_derivative_negative line 307
  21. lemma OAI.Thomason.DirectedComplex.RankedAtoms.maximal_transition_coefficient_le line 322
  22. lemma OAI.Thomason.DirectedComplex.RankedAtoms.top_coefficient_le_one line 361
  23. lemma OAI.Thomason.DirectedComplex.RankedAtoms.row_coefficient_zero_or_one line 422
  24. lemma OAI.Thomason.DirectedComplex.RankedAtoms.positive_cycle_zero line 442
  25. lemma OAI.Thomason.DirectedComplex.RankedAtoms.positiveAcyclic line 463
  26. lemma OAI.Thomason.DirectedComplex.RankedAtoms.positive_split_basis line 468
  27. lemma OAI.Thomason.DirectedComplex.RankedAtoms.atom_subrows_fixed line 499
  28. lemma OAI.Thomason.DirectedComplex.RankedAtoms.atom_indecomposable line 528
  29. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_lowers_dimension line 571
  30. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_reflects_dimension line 631
  31. lemma OAI.Thomason.DirectedComplex.CylinderTables.cross_vertical line 655
  32. lemma OAI.Thomason.DirectedComplex.CylinderTables.vertical_injective line 661
  33. lemma OAI.Thomason.DirectedComplex.CylinderTables.label_vertical line 668
  34. lemma OAI.Thomason.DirectedComplex.CylinderTables.vertical_ne_endpoint line 674
  35. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_atom_generator line 695
  36. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_atom_fiber_subsingleton line 739
  37. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_atom_unique line 755