OAI/Algebra/GroupRing/RelationSplit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.RelationSplit.sectionWord line 15
2. lemma OAI.TorsionFreeZeroDivisors.RelationSplit.sectionWord_q line 16
3. def OAI.TorsionFreeZeroDivisors.RelationSplit.loop line 18
4. lemma OAI.TorsionFreeZeroDivisors.RelationSplit.loop_one line 21
5. lemma OAI.TorsionFreeZeroDivisors.RelationSplit.loop_mul line 24
6. lemma OAI.TorsionFreeZeroDivisors.RelationSplit.area_loop_mul line 30
7. lemma OAI.TorsionFreeZeroDivisors.RelationSplit.area_loop_inv line 34
8. def OAI.TorsionFreeZeroDivisors.RelationSplit.retract line 40
9. lemma OAI.TorsionFreeZeroDivisors.RelationSplit.retract_single line 42
10. lemma OAI.TorsionFreeZeroDivisors.RelationSplit.retract_fox line 46
11. lemma OAI.TorsionFreeZeroDivisors.RelationSplit.area_rel line 56
12. lemma OAI.TorsionFreeZeroDivisors.RelationSplit.retract_d₂_single line 64
13. lemma OAI.TorsionFreeZeroDivisors.RelationSplit.retract_d₂ line 76

    Source documentation

    The actual integral physical-cell boundary is a split injection as an abelian-group map. The splitting uses genuine normal-closure expansions, not a hypothesis of cellular acyclicity.

    lemma retract_d₂ (x : CellModule.Module (G rel) I) : retract rel (d₂ rel x)=x := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.CellModule.Module, OAI.TorsionFreeZeroDivisors.RelationSplit.retract

14. lemma OAI.TorsionFreeZeroDivisors.RelationSplit.d₂_injective line 84