OAI/Algebra/GroupRing/ChainActiveStages.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TorsionFreeZeroDivisors.ChainActiveStages.ActiveChain line 22
  2. def OAI.TorsionFreeZeroDivisors.ChainActiveStages.activeOrientation line 26

    Source documentation

    Literal active chain orientations, with no padding by inactive chains.

    def activeOrientation (j : ℕ) : ActiveD m j ≃ A j × Bool where
…
  3. lemma OAI.TorsionFreeZeroDivisors.ChainActiveStages.edges_card line 48
  4. def OAI.TorsionFreeZeroDivisors.ChainActiveStages.first line 55
  5. def OAI.TorsionFreeZeroDivisors.ChainActiveStages.last line 59
  6. lemma OAI.TorsionFreeZeroDivisors.ChainActiveStages.incident line 64
  7. theorem OAI.TorsionFreeZeroDivisors.ChainActiveStages.exponent_nonpos line 86

    Source documentation

    The signed exponent counted by the chain expectation is exactly the one bounded by immersed path incidence, including the first-stage root saving.

    theorem exponent_nonpos (hp : ∀ i,paths i≠[]) (cyclic : P → Bool)
    (hc : ∀ i,(paths i).IsChain (WeightedMoore.PortWalk.step (S).origin (S).reverse))
    (hclose : ∀ i,cyclic i=true → ∀ᵉ (x∈(paths i).getLast?) (y∈(paths i).head?),
      WeightedMoore.PortWalk.step (S).origin (S).reverse x y)
    (M : ℕ) (hM : 0<M) (hm : ∀ c : R,ChunkComparisons.multiplicity col c ≤ M) :
    (∑ j : Fin M, ((Fintype.card (ActiveV (S) m j.val):ℤ)-Fintype.card (A j.val)-
      if j.val=0 then Fintype.card {i : P // cyclic i=false} else 0)) ≤ 0 := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.step, OAI.TorsionFreeZeroDivisors.ChunkComparisons.multiplicity

  8. abbrev OAI.TorsionFreeZeroDivisors.SubdivisionRestriction.length line 110
  9. def OAI.TorsionFreeZeroDivisors.SubdivisionRestriction.firstPoint line 111
  10. def OAI.TorsionFreeZeroDivisors.SubdivisionRestriction.lastPoint line 112
  11. def OAI.TorsionFreeZeroDivisors.SubdivisionRestriction.vertex line 117
  12. def OAI.TorsionFreeZeroDivisors.SubdivisionRestriction.dart line 121
  13. lemma OAI.TorsionFreeZeroDivisors.SubdivisionRestriction.vertex_injective line 123
  14. lemma OAI.TorsionFreeZeroDivisors.SubdivisionRestriction.dart_injective line 143
  15. lemma OAI.TorsionFreeZeroDivisors.SubdivisionRestriction.point_map line 154
  16. lemma OAI.TorsionFreeZeroDivisors.SubdivisionRestriction.origin_map line 161
  17. lemma OAI.TorsionFreeZeroDivisors.SubdivisionRestriction.reverse_map line 170
  18. abbrev OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.length line 191
  19. abbrev OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.graph line 192
  20. abbrev OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.active line 196
  21. def OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.marked line 197
  22. lemma OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.marked_injective line 202
  23. def OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.vertexLift line 207
  24. lemma OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.vertexLift_injective line 212
  25. lemma OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.point_lift line 232
  26. def OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.vertexMap line 241
  27. def OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.dartMap line 244
  28. lemma OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.vertexMap_injective line 248
  29. lemma OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.dartMap_injective line 252
  30. lemma OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.origin_map line 256
  31. lemma OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.reverse_map line 273
  32. theorem OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.immersed line 285

    Source documentation

    Restricting an immersed realization keeps every active chain vertex and port injective, without ever trying to embed inactive marked vertices.

    theorem immersed {T : Type*} (label : D → T)
    (hlabel : Injective (fun d => (Γ.origin d,label d))) :
    Injective (fun d => ((Q).origin d,label (dartMap Γ mark h2 paths j d))) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ChainStageEmbedding.dartMap

  33. def OAI.TorsionFreeZeroDivisors.RootPins.pin line 305

    Source documentation

    At most one prescribed root. All other vertices remain unpinned.

    def pin (root : Option V) (target : T) (v : V) : Option T :=
…
  34. def OAI.TorsionFreeZeroDivisors.RootPins.free line 308
  35. lemma OAI.TorsionFreeZeroDivisors.RootPins.free_none line 311
  36. lemma OAI.TorsionFreeZeroDivisors.RootPins.free_some line 314
  37. lemma OAI.TorsionFreeZeroDivisors.RootPins.free_cast line 321
  38. lemma OAI.TorsionFreeZeroDivisors.RootPins.respects line 331
  39. lemma OAI.TorsionFreeZeroDivisors.ActiveRoot.occurrence_positive line 349
  40. def OAI.TorsionFreeZeroDivisors.ActiveRoot.vertex line 355

    Source documentation

    The actual initial vertex belongs to the first active stage.

    def vertex (p : P) : ActiveV Γ (ListStageExponents.mult Γ paths) 0 :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.ListStageExponents.mult

  41. lemma OAI.TorsionFreeZeroDivisors.ActiveRoot.vertex_val line 360