OAI/CategoryTheory/Thomason/ModelTransfer.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Model Transfer.

  1. lemma OAI.Thomason.SimplicialGluing.under_weak line 15
  2. lemma OAI.Thomason.SimplicialGluing.span_weak line 95
  3. abbrev OAI.Thomason.AbstractTransfer.posetObj line 159
  4. abbrev OAI.Thomason.AbstractTransfer.inc line 160
  5. abbrev OAI.Thomason.AbstractTransfer.L line 163
  6. abbrev OAI.Thomason.AbstractTransfer.R line 164
  7. abbrev OAI.Thomason.AbstractTransfer.transferredAdjunction line 165
  8. abbrev OAI.Thomason.AbstractTransfer.W line 168
  9. abbrev OAI.Thomason.AbstractTransfer.Fib line 169
  10. abbrev OAI.Thomason.AbstractTransfer.Cof line 170
  11. lemma OAI.Thomason.AbstractTransfer.weak_iff_nerve line 172
  12. structure OAI.Thomason.AbstractTransfer.PosetComparison line 176
  13. lemma OAI.Thomason.AbstractTransfer.inc_mono line 196
  14. lemma OAI.Thomason.AbstractTransfer.unit_local_of_iso line 201
  15. lemma OAI.Thomason.AbstractTransfer.unit_local_initial line 212
  16. lemma OAI.Thomason.AbstractTransfer.unit_local_attachment line 222
  17. lemma OAI.Thomason.AbstractTransfer.boundary_unit_successor line 273
  18. lemma OAI.Thomason.AbstractTransfer.unit_local_skeleton line 304
  19. lemma OAI.Thomason.AbstractTransfer.skeleton_monos line 320
  20. theorem OAI.Thomason.AbstractTransfer.subdivided_unit_local line 332
  21. abbrev OAI.Thomason.AbstractTransfer.Horns.arrow line 384
  22. def OAI.Thomason.AbstractTransfer.Horns.Admissible line 386
  23. instance OAI.Thomason.AbstractTransfer.Horns.(instance at line 389) line 389
  24. lemma OAI.Thomason.AbstractTransfer.Horns.horn_admissible line 395
  25. def OAI.Thomason.AbstractTransfer.Horns.posetCoprodIso line 422
  26. def OAI.Thomason.AbstractTransfer.Horns.oldCoprodIso line 427
  27. lemma OAI.Thomason.AbstractTransfer.Horns.posetCoprodIso_ι line 431
  28. lemma OAI.Thomason.AbstractTransfer.Horns.oldCoprodIso_ι line 438
  29. lemma OAI.Thomason.AbstractTransfer.Horns.coprod_inc line 449
  30. instance OAI.Thomason.AbstractTransfer.Horns.admissible_coproducts line 464
  31. instance OAI.Thomason.AbstractTransfer.Horns.(instance at line 487) line 487
  32. lemma OAI.Thomason.AbstractTransfer.Horns.poset_attachment_local line 493
  33. lemma OAI.Thomason.AbstractTransfer.Horns.admissible_pushout line 524
  34. lemma OAI.Thomason.AbstractTransfer.Horns.coproduct_horn_pushout line 541
  35. lemma OAI.Thomason.AbstractTransfer.sequential_horn_weak line 569
  36. theorem OAI.Thomason.AbstractTransfer.horn_acyclicity line 620
  37. lemma OAI.Thomason.AbstractTransfer.first_wfs_aux line 632
  38. lemma OAI.Thomason.AbstractTransfer.first_left_class line 636
  39. theorem OAI.Thomason.AbstractTransfer.first_wfs line 649
  40. def OAI.Thomason.AbstractTransfer.model line 655