Section 5: symmetries of transmission permutations #
The two symmetry arguments are deliberately carried out at the raw
IsTransmissionPermutation level. This keeps the graph relabeling and
linear-equivalence transports independent of the ASP packaging.
theorem
Bananas.sectionFive_tau_involutive_of_dual_automorphism_connected
{M : TwiceMarked}
(hconn : _root_.graphConnected M.graph)
(phi : MarkedPointSwap M)
{D : CFDiv M.graph}
{tau : ℤ → ℤ}
(hTau : IsTransmissionPermutation M D tau)
(hDual : linearEquiv M.graph (phi.iso.mapDiv D) (Utilities.transmissionDualDivisor M.u M.v D))
(a b : ℤ)
:
Corrected Lemma 5.3(1): Riemann--Roch duality needs connectedness. The statement ledger's unqualified version is therefore deliberately not used: a disconnected chip-firing graph has no such duality theorem.
theorem
Bananas.sectionFive_tau_reflection_of_twisted_automorphism_proved
{M : TwiceMarked}
(phi : MarkedPointSwap M)
{D : CFDiv M.graph}
{tau : ℤ → ℤ}
(n : ℤ)
(hTau : IsTransmissionPermutation M D tau)
(hTwist : linearEquiv M.graph (phi.iso.mapDiv D - D) (n • (oneChip M.u - oneChip M.v)))
(a b : ℤ)
:
Lemma 5.3(2), at the raw transmission level.