OAI/NumberTheory/Ostmann/Tree/ParallelCycle.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The two-edge cycle

Two leaves in the same component and the same quartet give a balanced sign vector supported on precisely those two leaves. No additional assumption is needed for this degenerate cycle.

  1. def OAI.Ostmann.parallelCycleSign line 18
  2. theorem OAI.Ostmann.parallelCycleSign_left line 21
  3. theorem OAI.Ostmann.parallelCycleSign_right line 24
  4. theorem OAI.Ostmann.parallelCycleSign_other line 27
  5. theorem OAI.Ostmann.sum_parallelCycleSign line 31
  6. theorem OAI.Ostmann.parallelCycleSign_balanced line 37

    Source documentation

    The same block membership cancels the two signs.

    theorem parallelCycleSign_balanced {I J : Type*} [Fintype I] [DecidableEq I] [DecidableEq J]
    (block : I → J) (i j : I) (hij : block i = block j) (b : J) :
    (∑ k ∈ Finset.univ.filter (fun k => block k = b), parallelCycleSign i j k) = 0 := by
…

    Mentions: OAI.Ostmann.parallelCycleSign

  7. theorem OAI.Ostmann.parallelCycle_preserves_blocks line 44

    Source documentation

    Reciprocal multiplication on parallel leaves preserves every component product.

    theorem parallelCycle_preserves_blocks {I J G : Type*} [Fintype I] [DecidableEq I]
    [DecidableEq J] [CommGroup G] (block : I → J) (i j : I)
    (hij : block i = block j) (b : J) (z : G) (m : I → G) :
    (∏ k ∈ Finset.univ.filter (fun k => block k = b),
      cycleMultiply (parallelCycleSign i j) z m k) =
      ∏ k ∈ Finset.univ.filter (fun k => block k = b), m k := by
…

    Mentions: OAI.Ostmann.cycleMultiply, OAI.Ostmann.parallelCycleSign