OAI/Algebra/GroupRing/TreeCentroid.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.next_of_adj line 14
2. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.branch_head line 17
3. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.branch_boundary line 21

   Source documentation

   A tree branch has exactly one possible directed edge leaving it.

   lemma branch_boundary {c n x y : V} (hx : x∈branch h c n) (hy : y∉branch h c n)
       (he : G.Adj x y) : x=n ∧ y=c := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.TreeCentroid.branch

4. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.branch_walk_boundary line 31
5. def OAI.TorsionFreeZeroDivisors.TreeCentroid.descendants line 44

   Source documentation

   Descendants are defined by the actual branch beyond the parent edge.

   def descendants (root v : V) : Finset V := branch h (next h v root) v

   Mentions: OAI.TorsionFreeZeroDivisors.TreeCentroid.branch, OAI.TorsionFreeZeroDivisors.TreeCentroid.next

6. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.root_not_descendants line 46
7. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.self_mem_descendants line 54
8. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.descendant_mem_root_path line 57
9. def OAI.TorsionFreeZeroDivisors.TreeCentroid.rootPath line 61
10. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.root_mem_rootPath line 63
11. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.self_mem_rootPath line 66
12. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.rootPath_card line 69
13. theorem OAI.TorsionFreeZeroDivisors.TreeCentroid.two_root_paths_card line 76

    Source documentation

    Two root paths share the root, yielding the sharp 2r+1 count rather than an erroneous 2r+2 or a three-path 3r+1 bound.

    theorem two_root_paths_card (root v w : V) (r : ℕ)
        (hv : G.dist root v≤r) (hw : G.dist root w≤r) :
        (rootPath h root v∪rootPath h root w).card≤2*r+1 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.TreeCentroid.rootPath

14. def OAI.TorsionFreeZeroDivisors.MapEuler.touchGraph line 95

    Source documentation

    Dual edges incident to a specified set of primal vertices.

    def touchGraph (S : Set (Cycle σ)) : SimpleGraph (Cycle φ) where
    …

15. lemma OAI.TorsionFreeZeroDivisors.MapEuler.touchGraph_le line 106
16. lemma OAI.TorsionFreeZeroDivisors.MapEuler.touchGraph_contour_step line 110
17. theorem OAI.TorsionFreeZeroDivisors.MapEuler.touchGraph_connected_of_contour line 123

    Source documentation

    A subtree interval in the primal contour gives actual connectivity through only those dual edges incident to the subtree.

    theorem touchGraph_connected_of_contour (θ : Equiv.Perm O) (hθ : γ*θ=φ)
        (hc : Nat.card (Cycle θ)=1) (S : Set (Cycle σ)) (p : O)
        (hout : ∀ x,cycle σ x∈S → cycle σ (θ x)∉S → x=p)
        {x y : O} (hx : cycle σ x∈S) (hy : cycle σ y∈S) :
        (touchGraph σ φ γ hγ S).Reachable (cycle φ x) (cycle φ y) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.touchGraph

18. theorem OAI.TorsionFreeZeroDivisors.MapEuler.branch_contour_exit line 143

    Source documentation

    Every rooted tree branch has a unique possible exit in the actual contour.

    theorem branch_contour_exit {c n : Cycle σ} (he : T.Adj n c) :
        ∃ p : O,∀ x,cycle σ x∈TreeCentroid.branch ht c n →
          cycle σ ((subgraphPair σ α ha T hT*σ) x)∉TreeCentroid.branch ht c n → x=p := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.TreeCentroid.branch, OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair

19. theorem OAI.TorsionFreeZeroDivisors.MapEuler.branch_dual_touch_connected line 164

    Source documentation

    Literal face connectivity around a primal tree branch in a genus-zero map, using only cotree edges touching that branch.

    theorem branch_dual_touch_connected (hz : GenusZero σ α) {c n : Cycle σ}
        (he : T.Adj n c) {x y : O}
        (hx : cycle σ x∈TreeCentroid.branch ht c n)
        (hy : cycle σ y∈TreeCentroid.branch ht c n) :
        (touchGraph σ (α*σ) (α*subgraphPair σ α ha T hT)
          (complement_involutive α _ ha (subgraphPair_involutive σ α ha T hT)
            (subgraphPair_subpairing σ α ha T hT))
          (↑(TreeCentroid.branch ht c n) : Set (Cycle σ))).Reachable
          (cycle (α*σ) x) (cycle (α*σ) y) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.TreeCentroid.branch, OAI.TorsionFreeZeroDivisors.MapEuler.touchGraph, OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair, OAI.TorsionFreeZeroDivisors.MapEuler.complement_involutive, OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_involutive, OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_subpairing

20. def OAI.TorsionFreeZeroDivisors.MapEuler.supportedRealize line 186
21. lemma OAI.TorsionFreeZeroDivisors.MapEuler.supportedRealize_injective line 188
22. lemma OAI.TorsionFreeZeroDivisors.MapEuler.supportedRealize_surjective line 191
23. lemma OAI.TorsionFreeZeroDivisors.MapEuler.nonfixed_adj_of_edge_count line 201

    Source documentation

    When there are as many support darts as graph darts, no nonfixed dart is a loop and no two different paired edges can realize the same simple edge.

    lemma nonfixed_adj_of_edge_count
        (he : 2*Nat.card (graph σ α ha).edgeSet=α.support.card) {x : O} (hx : α x≠x) :
        (graph σ α ha).Adj (cycle σ x) (cycle σ (α x)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.graph

24. lemma OAI.TorsionFreeZeroDivisors.MapEuler.dart_unique_of_edge_count line 209
25. lemma OAI.TorsionFreeZeroDivisors.MapEuler.edge_count_of_tree_support line 225
26. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.branch_mem_iff_adj_of_avoid line 240
27. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.branch_mem_iff_reachable_of_avoid line 253
28. lemma OAI.TorsionFreeZeroDivisors.MapEuler.touchGraph_avoids_edge line 267
29. def OAI.TorsionFreeZeroDivisors.MapEuler.cotreeSide line 290
30. def OAI.TorsionFreeZeroDivisors.MapEuler.fundamentalVertices line 293
31. lemma OAI.TorsionFreeZeroDivisors.MapEuler.root_mem_fundamentalVertices line 297
32. lemma OAI.TorsionFreeZeroDivisors.MapEuler.endpoints_not_descendants line 301
33. theorem OAI.TorsionFreeZeroDivisors.MapEuler.outside_fundamental_sameSide line 325

    Source documentation

    Outside the two actual root paths, all incident faces of a primal vertex lie on the same side of the deleted cotree edge.

    theorem outside_fundamental_sameSide {root v : Cycle σ} {d x y : O}
        (hv : v∉fundamentalVertices σ α T ht root d)
        (hx : cycle σ x=v) (hy : cycle σ y=v) :
        cycle φ x∈cotreeSide σ α ha T hT hz ht d ↔
        cycle φ y∈cotreeSide σ α ha T hT hz ht d := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.fundamentalVertices, OAI.TorsionFreeZeroDivisors.MapEuler.cotreeSide

34. lemma OAI.TorsionFreeZeroDivisors.MapEuler.edge_common_face line 344

    Source documentation

    Endpoints of a primal edge have incident occurrences on a common face.

    lemma edge_common_face (x : O) : cycle φ (σ.symm x)=cycle φ (α x) := by
    …

35. theorem OAI.TorsionFreeZeroDivisors.MapEuler.fundamental_no_crossing line 350

    Source documentation

    The two-root-path vertex set really separates the corresponding dual sides, including original loops, parallel edges, and tree edges.

    theorem fundamental_no_crossing {root : Cycle σ} {d : O} {v w : Cycle σ}
        (hv : v∉fundamentalVertices σ α T ht root d)
        (hw : w∉fundamentalVertices σ α T ht root d)
        (he : (graph σ α ha).Adj v w) {x y : O}
        (hx : cycle σ x=v) (hy : cycle σ y=w) :
        cycle φ x∈cotreeSide σ α ha T hT hz ht d ↔
        cycle φ y∈cotreeSide σ α ha T hT hz ht d := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.fundamentalVertices, OAI.TorsionFreeZeroDivisors.MapEuler.graph, OAI.TorsionFreeZeroDivisors.MapEuler.cotreeSide