OAI/Topology/EilenbergGanea/IntegralModules.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Group-ring augmentation and literal two-syzygy dimension criterion.

  1. theorem OAI.EilenbergGanea.projectiveDimension_le_two_of_syzygies line 22

    Source documentation

    Two successive projective syzygies give the literal integral upper bound.

    theorem projectiveDimension_le_two_of_syzygies
    (ε : P →ₗ[R] M) (hε : Function.Surjective ε)
    (d : Q →ₗ[R] LinearMap.ker ε) (hd : Function.Surjective d)
    [Module.Projective R P] [Module.Projective R Q]
    [Module.Projective R (LinearMap.ker d)] :
    CategoryTheory.projectiveDimension (ModuleCat.of R M) ≤ 2 := by
…
  2. abbrev OAI.EilenbergGanea.IntegralGroupRing line 39
  3. abbrev OAI.EilenbergGanea.IntegralTrivialModule line 40
  4. def OAI.EilenbergGanea.cayleyAugmentation line 43
  5. theorem OAI.EilenbergGanea.cayleyAugmentation_single line 47
  6. theorem OAI.EilenbergGanea.cayleyAugmentation_surjective line 56
  7. def OAI.EilenbergGanea.cayleyDifferential line 62
  8. theorem OAI.EilenbergGanea.cayleyDifferential_single line 66
  9. theorem OAI.EilenbergGanea.cayleyAugmentation_one line 70
  10. theorem OAI.EilenbergGanea.cayleyAugmentation_difference line 75
  11. theorem OAI.EilenbergGanea.cayleyDifferential_aug line 79
  12. theorem OAI.EilenbergGanea.cayleyGeneratorDifference_mem line 90
  13. theorem OAI.EilenbergGanea.cayleyAugmentation_normalize line 114
  14. theorem OAI.EilenbergGanea.cayley_exact line 135
  15. def OAI.EilenbergGanea.cayleySyzygyDifferential line 145
  16. theorem OAI.EilenbergGanea.cayleySyzygyDifferential_surjective line 152
  17. theorem OAI.EilenbergGanea.cayley_projectiveDimension_le_two line 162
  18. def OAI.EilenbergGanea.chainPackaging line 183

    Source documentation

    Reindex the actual integral edge chains as a free left group-ring module.

    def chainPackaging : BasedChains Γ S ≃ₗ[ℤ] S →₀ IntegralGroupRing Γ :=
…

    Mentions: OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.IntegralGroupRing

  19. theorem OAI.EilenbergGanea.chainPackaging_single line 187
  20. theorem OAI.EilenbergGanea.chainPackaging_symm_single line 192
  21. theorem OAI.EilenbergGanea.chainPackaging_translate line 198
  22. theorem OAI.EilenbergGanea.chainPackaging_boundary line 209
  23. theorem OAI.EilenbergGanea.chainPackaging_symm_translate line 224
  24. def OAI.EilenbergGanea.chainRingMap line 231

    Source documentation

    Equivariance on integral chains is exactly full group-ring linearity.

    def chainRingMap (A : BasedChains Γ S →ₗ[ℤ] BasedChains Γ T)
    (hA : ChainsEquivariant A) :
    (S →₀ IntegralGroupRing Γ) →ₗ[IntegralGroupRing Γ] T →₀ IntegralGroupRing Γ where
…

    Mentions: OAI.EilenbergGanea.BasedChains, OAI.EilenbergGanea.ChainsEquivariant, OAI.EilenbergGanea.IntegralGroupRing

  25. theorem OAI.EilenbergGanea.chainRingMap_apply line 247
  26. theorem OAI.EilenbergGanea.chainPackaging_mem_cycles line 251
  27. theorem OAI.EilenbergGanea.projective_cayley_cycles_of_boundary_basis line 263
  28. theorem OAI.EilenbergGanea.projectiveDimension_le_two_of_boundary_basis line 292