OAI/Algebra/GroupRing/MapRestrict.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TorsionFreeZeroDivisors.MapRestrict.componentInclude line 20
  2. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.componentInclude_component line 24
  3. def OAI.TorsionFreeZeroDivisors.MapRestrict.componentRaw line 27
  4. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.componentRaw_rotation line 30
  5. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.componentRaw_partner line 37
  6. def OAI.TorsionFreeZeroDivisors.MapRestrict.componentEquiv line 44
  7. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.component_card line 65
  8. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.mul_invariant line 70
  9. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.perm_mul line 72
  10. theorem OAI.TorsionFreeZeroDivisors.MapRestrict.genusZero line 77

    Source documentation

    Restriction to any invariant union of map components preserves actual Euler genus zero. The proof uses decomposition and the universal Euler upper bound on BOTH complementary pieces.

    theorem genusZero (hi : Function.Involutive α) (hz : GenusZero σ α) : GenusZero σP αP := by
…
  11. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.cycleInclude_injective line 97
  12. def OAI.TorsionFreeZeroDivisors.MapRestrict.internalPair line 100
  13. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.internalPair_involutive line 102
  14. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.rotation_invariant line 105
  15. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.pairing_invariant line 107
  16. def OAI.TorsionFreeZeroDivisors.MapRestrict.rotation line 113
  17. def OAI.TorsionFreeZeroDivisors.MapRestrict.pairing line 114
  18. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.pairing_involutive line 116
  19. def OAI.TorsionFreeZeroDivisors.MapRestrict.vertexEquiv line 119
  20. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.vertexEquiv_cycle line 129
  21. def OAI.TorsionFreeZeroDivisors.MapRestrict.graphIso line 133

    Source documentation

    The restricted dart system realizes precisely the induced simple graph.

    def graphIso : graph (rotation σ S) (pairing σ α hi S) (pairing_involutive σ α hi S) ≃g
    (graph σ α hi).induce S where
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapRestrict.rotation, OAI.TorsionFreeZeroDivisors.MapRestrict.pairing, OAI.TorsionFreeZeroDivisors.MapRestrict.pairing_involutive

  22. theorem OAI.TorsionFreeZeroDivisors.MapRestrict.induced_genusZero line 167
  23. def OAI.TorsionFreeZeroDivisors.MapContract.treePair line 187
  24. lemma OAI.TorsionFreeZeroDivisors.MapContract.treePair_inside line 191
  25. lemma OAI.TorsionFreeZeroDivisors.MapContract.treePair_outside line 192
  26. lemma OAI.TorsionFreeZeroDivisors.MapContract.treePair_invariant line 193
  27. lemma OAI.TorsionFreeZeroDivisors.MapContract.treePair_involutive line 194
  28. lemma OAI.TorsionFreeZeroDivisors.MapContract.treePair_subpairing line 202
  29. def OAI.TorsionFreeZeroDivisors.MapContract.rotation line 215
  30. def OAI.TorsionFreeZeroDivisors.MapContract.pairing line 216
  31. lemma OAI.TorsionFreeZeroDivisors.MapContract.pairing_involutive line 219
  32. theorem OAI.TorsionFreeZeroDivisors.MapContract.genusZero line 222
  33. lemma OAI.TorsionFreeZeroDivisors.MapContract.rotation_invariant line 230
  34. lemma OAI.TorsionFreeZeroDivisors.MapContract.rotation_inside line 233
  35. lemma OAI.TorsionFreeZeroDivisors.MapContract.inside_cycle_eq line 239
  36. lemma OAI.TorsionFreeZeroDivisors.MapContract.quotient_invariant line 247
  37. def OAI.TorsionFreeZeroDivisors.MapContract.quotient line 253
  38. lemma OAI.TorsionFreeZeroDivisors.MapContract.quotient_cycle line 256
  39. lemma OAI.TorsionFreeZeroDivisors.MapContract.quotient_surjective line 257
  40. def OAI.TorsionFreeZeroDivisors.MapContract.labelRaw line 262
  41. lemma OAI.TorsionFreeZeroDivisors.MapContract.labelRaw_invariant line 263
  42. def OAI.TorsionFreeZeroDivisors.MapContract.label line 268
  43. lemma OAI.TorsionFreeZeroDivisors.MapContract.label_quotient line 270
  44. lemma OAI.TorsionFreeZeroDivisors.MapContract.quotient_eq_iff line 274
  45. lemma OAI.TorsionFreeZeroDivisors.MapContract.cycle_treePair line 291
  46. lemma OAI.TorsionFreeZeroDivisors.MapContract.quotient_adj line 297

    Source documentation

    Every original edge either contracts to a vertex or is an actual edge.

    lemma quotient_adj {v w : Cycle σ} (he : (graph σ α hi).Adj v w) :
    q v=q w ∨ (graph ρ γ (pairing_involutive σ α hi B T hT)).Adj (q v) (q w) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapContract.pairing_involutive

  47. lemma OAI.TorsionFreeZeroDivisors.MapContract.adj_lift line 307

    Source documentation

    No new nonloop adjacency is introduced by the literal contraction.

    lemma adj_lift {v w : Cycle ρ} (he : (graph ρ γ (pairing_involutive σ α hi B T hT)).Adj v w) :
    ∃ x y,(graph σ α hi).Adj x y ∧ q x=v ∧ q y=w := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapContract.pairing_involutive

  48. def OAI.TorsionFreeZeroDivisors.GraphBall.vertices line 327
  49. def OAI.TorsionFreeZeroDivisors.GraphBall.rootVertex line 328
  50. lemma OAI.TorsionFreeZeroDivisors.GraphBall.exists_walk line 331
  51. lemma OAI.TorsionFreeZeroDivisors.GraphBall.connected line 348
  52. lemma OAI.TorsionFreeZeroDivisors.GraphBall.dist_root line 354