OAI/GroupTheory/Congruence/Transfer.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Odd-index transfer, comparison of bar resolutions, and homology-coinvariant models.

  1. def OAI.CoboundaryExpanders.Transfer.inclusion line 23
  2. theorem OAI.CoboundaryExpanders.Transfer.inclusion_mk line 29
  3. theorem OAI.CoboundaryExpanders.Transfer.quotient_action_mk line 35
  4. def OAI.CoboundaryExpanders.Transfer.normTransfer line 39
  5. theorem OAI.CoboundaryExpanders.Transfer.normTransfer_mk line 47
  6. theorem OAI.CoboundaryExpanders.Transfer.inclusion_quotient_action line 53
  7. theorem OAI.CoboundaryExpanders.Transfer.inclusion_normTransfer line 61
  8. theorem OAI.CoboundaryExpanders.Transfer.inclusion_natural line 71
  9. theorem OAI.CoboundaryExpanders.Transfer.normTransfer_natural line 79
  10. abbrev OAI.CoboundaryExpanders.Transfer.subgroupCoinvariantsFunctor line 99
  11. def OAI.CoboundaryExpanders.Transfer.inclusionNatTrans line 102
  12. def OAI.CoboundaryExpanders.Transfer.transferNatTrans line 109
  13. theorem OAI.CoboundaryExpanders.Transfer.transfer_inclusion line 116
  14. abbrev OAI.CoboundaryExpanders.Transfer.subgroupChains line 124
  15. abbrev OAI.CoboundaryExpanders.Transfer.ambientChains line 127
  16. def OAI.CoboundaryExpanders.Transfer.chainInclusion line 130
  17. def OAI.CoboundaryExpanders.Transfer.chainTransfer line 134
  18. theorem OAI.CoboundaryExpanders.Transfer.chainTransfer_inclusion line 138
  19. theorem OAI.CoboundaryExpanders.Transfer.homology_chainInclusion_surjective line 147
  20. abbrev OAI.CoboundaryExpanders.BarComparison.restrictedBar line 169
  21. def OAI.CoboundaryExpanders.BarComparison.inclusionF line 172
  22. theorem OAI.CoboundaryExpanders.BarComparison.inclusionF_single line 179
  23. def OAI.CoboundaryExpanders.BarComparison.inclusion line 191
  24. lemma OAI.CoboundaryExpanders.BarComparison.diagonal_inv_single line 223
  25. theorem OAI.CoboundaryExpanders.BarComparison.bar_augmentation_single line 244
  26. theorem OAI.CoboundaryExpanders.BarComparison.inclusion_augmentation line 252
  27. def OAI.CoboundaryExpanders.BarComparison.inclusionHomotopy line 269
  28. def OAI.CoboundaryExpanders.BarComparison.inclusionEquiv line 281
  29. abbrev OAI.CoboundaryExpanders.CoinvariantModel.complex line 304
  30. def OAI.CoboundaryExpanders.CoinvariantModel.chainsIso line 307
  31. theorem OAI.CoboundaryExpanders.CoinvariantModel.chainsIso_hom_single line 314
  32. def OAI.CoboundaryExpanders.Transfer.barCoinvariantInclusion line 334
  33. def OAI.CoboundaryExpanders.Transfer.trivialInclusion line 339
  34. theorem OAI.CoboundaryExpanders.Transfer.chain_factorization line 343
  35. theorem OAI.CoboundaryExpanders.Transfer.homology_surjective_of_homotopyEquiv line 363
  36. theorem OAI.CoboundaryExpanders.Transfer.homology_barCoinvariantInclusion_surjective line 375
  37. theorem OAI.CoboundaryExpanders.Transfer.groupHomology_inclusion_surjective line 381
  38. theorem OAI.CoboundaryExpanders.Transfer.odd_index_groupHomology_inclusion_surjective line 409
  39. def OAI.CoboundaryExpanders.Transfer.trivialCoefficients line 422
  40. theorem OAI.CoboundaryExpanders.Transfer.homology_equiv_surjective line 427
  41. theorem OAI.CoboundaryExpanders.Transfer.nested_subgroup_inclusion_surjective line 438
  42. def OAI.CoboundaryExpanders.Transfer.quotientActionNatTrans line 463
  43. def OAI.CoboundaryExpanders.Transfer.chainQuotientAction line 476
  44. theorem OAI.CoboundaryExpanders.Transfer.normTransfer_inclusion line 480
  45. theorem OAI.CoboundaryExpanders.Transfer.chainInclusion_transfer line 487
  46. theorem OAI.CoboundaryExpanders.Transfer.homology_chainInclusion_injective line 501
  47. def OAI.CoboundaryExpanders.BarComparison.adjustedF line 528
  48. theorem OAI.CoboundaryExpanders.BarComparison.adjustedF_single line 535
  49. theorem OAI.CoboundaryExpanders.BarComparison.bar_d_single_coeff line 548
  50. def OAI.CoboundaryExpanders.BarComparison.adjusted line 563
  51. theorem OAI.CoboundaryExpanders.BarComparison.adjusted_augmentation line 590
  52. def OAI.CoboundaryExpanders.BarComparison.adjustedHomotopy line 607
  53. def OAI.CoboundaryExpanders.Transfer.barCoinvariantAdjusted line 622
  54. theorem OAI.CoboundaryExpanders.Transfer.homology_adjusted line 628
  55. theorem OAI.CoboundaryExpanders.Transfer.chain_conjugation_factorization line 634
  56. theorem OAI.CoboundaryExpanders.Transfer.homology_quotientAction_eq_id line 661
  57. theorem OAI.CoboundaryExpanders.Transfer.homology_injective_of_homotopyEquiv line 687
  58. theorem OAI.CoboundaryExpanders.Transfer.groupHomology_inclusion_injective line 699
  59. theorem OAI.CoboundaryExpanders.Transfer.subgroup_homology_isZero_of_conjugation line 724