Swapping the marks of a graph with general transmission

Swapping the two marked vertices replaces a raw transmission permutation tau by its reflected inverse

b |-> -tau^{-1}(-b).

This file proves that affine inversion count is unchanged by this operation and consequently that KGeneralTransmission is independent of the ordering of the two marks.

noncomputable def Bananas.rawInverse (tau : ℤ → ℤ) : ℤ → ℤ

The inverse of a bijection, kept at the raw-function level used by IsTransmissionPermutation.

Equations

• Bananas.rawInverse tau = Function.invFun tau

@[simp]

theorem Bananas.rawInverse_apply_apply (tau : ℤ → ℤ) (hBij : Function.Bijective tau) (n : ℤ) : rawInverse tau (tau n) = n

theorem Bananas.apply_rawInverse_apply (tau : ℤ → ℤ) (hBij : Function.Bijective tau) (n : ℤ) : tau (rawInverse tau n) = n

theorem Bananas.IsKAffine.rawInverse {k : ℕ} {tau : ℤ → ℤ} (hAffine : IsKAffine k tau) (hBij : Function.Bijective tau) : IsKAffine k (Bananas.rawInverse tau)

Inverting a bijective affine function preserves its period.

def Bananas.rawAffineReflection (tau : ℤ → ℤ) : ℤ → ℤ

Reflection in both the domain and range.

Equations

• Bananas.rawAffineReflection tau n = -tau (-n)

noncomputable def Bananas.swapTransmissionPermutation (tau : ℤ → ℤ) : ℤ → ℤ

The reflected inverse is the raw transmission permutation after swapping the two marks.

Equations

• Bananas.swapTransmissionPermutation tau = Bananas.rawAffineReflection (Bananas.rawInverse tau)

def Bananas.shiftPair (k : ℕ) (q : ℤ) (p : ℤ × ℤ) : ℤ × ℤ

Simultaneously translate a pair by an integral number of periods.

Equations

• Bananas.shiftPair k q p = (p.1 + q * ↑k, p.2 + q * ↑k)

def Bananas.normalizeFirstPair (k : ℕ) (p : ℤ × ℤ) : ℤ × ℤ

Normalize the first coordinate of a pair into the standard period.

Equations

• Bananas.normalizeFirstPair k p = (p.1 % ↑k, p.2 - p.1 / ↑k * ↑k)

theorem Bananas.normalizeFirstPair_eq_shiftPair (k : ℕ) (p : ℤ × ℤ) : normalizeFirstPair k p = shiftPair k (-(p.1 / ↑k)) p

theorem Bananas.normalizeFirstPair_shiftPair_of_fundamental {k : ℕ} (hk : 0 < k) (p : ℤ × ℤ) (hp0 : 0 ≤ p.1) (hpk : p.1 < ↑k) (q : ℤ) : normalizeFirstPair k (shiftPair k q p) = p

Normalization removes any simultaneous period translate from a pair whose first coordinate is already in the standard period.

theorem Bananas.IsKAffine.map_shiftPair {k : ℕ} {tau : ℤ → ℤ} (hAffine : IsKAffine k tau) (q : ℤ) (p : ℤ × ℤ) : (tau (shiftPair k q p).1, tau (shiftPair k q p).2) = shiftPair k q (tau p.1, tau p.2)

Applying an affine function to a simultaneous period translate translates both values by the same period.

noncomputable def Bananas.inverseInversionPair (tau : ℤ → ℤ) (p : ℤ × ℤ) : ℤ × ℤ

The pair map taking an inversion of an inverse permutation back to the corresponding inversion of the original permutation.

Equations

• Bananas.inverseInversionPair tau p = (Bananas.rawInverse tau p.2, Bananas.rawInverse tau p.1)

def Bananas.inversionInversePair (tau : ℤ → ℤ) (p : ℤ × ℤ) : ℤ × ℤ

The pair map taking an inversion to the corresponding inversion of the inverse permutation.

Equations

• Bananas.inversionInversePair tau p = (tau p.2, tau p.1)

theorem Bananas.inverseInversionPair_inversionInversePair (tau : ℤ → ℤ) (hBij : Function.Bijective tau) (p : ℤ × ℤ) : inverseInversionPair tau (inversionInversePair tau p) = p

theorem Bananas.inversionInversePair_inverseInversionPair (tau : ℤ → ℤ) (hBij : Function.Bijective tau) (p : ℤ × ℤ) : inversionInversePair tau (inverseInversionPair tau p) = p

noncomputable def Bananas.normalizedInverseToOriginal (k : ℕ) (tau : ℤ → ℤ) (p : ℤ × ℤ) : ℤ × ℤ

Normalize the inversion of the original permutation associated to an inversion of its inverse.

Equations

• Bananas.normalizedInverseToOriginal k tau p = Bananas.normalizeFirstPair k (Bananas.inverseInversionPair tau p)

def Bananas.normalizedOriginalToInverse (k : ℕ) (tau : ℤ → ℤ) (p : ℤ × ℤ) : ℤ × ℤ

Normalize the inversion of the inverse permutation associated to an inversion of the original.

Equations

• Bananas.normalizedOriginalToInverse k tau p = Bananas.normalizeFirstPair k (Bananas.inversionInversePair tau p)

theorem Bananas.inverseInversionPair_shiftPair {k : ℕ} {tau : ℤ → ℤ} (hBij : Function.Bijective tau) (hAffine : IsKAffine k tau) (q : ℤ) (p : ℤ × ℤ) : inverseInversionPair tau (shiftPair k q p) = shiftPair k q (inverseInversionPair tau p)

theorem Bananas.inversionInversePair_shiftPair {k : ℕ} {tau : ℤ → ℤ} (hAffine : IsKAffine k tau) (q : ℤ) (p : ℤ × ℤ) : inversionInversePair tau (shiftPair k q p) = shiftPair k q (inversionInversePair tau p)

theorem Bananas.normalizedInverseToOriginal_mem {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hBij : Function.Bijective tau) (hAffine : IsKAffine k tau) {p : ℤ × ℤ} (hp : p ∈ kInversions k (rawInverse tau)) : normalizedInverseToOriginal k tau p ∈ kInversions k tau

theorem Bananas.normalizedOriginalToInverse_mem {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hBij : Function.Bijective tau) (hAffine : IsKAffine k tau) {p : ℤ × ℤ} (hp : p ∈ kInversions k tau) : normalizedOriginalToInverse k tau p ∈ kInversions k (rawInverse tau)

theorem Bananas.normalizedInverseToOriginal_normalizedOriginalToInverse {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hBij : Function.Bijective tau) (hAffine : IsKAffine k tau) {p : ℤ × ℤ} (hp : p ∈ kInversions k tau) : normalizedInverseToOriginal k tau (normalizedOriginalToInverse k tau p) = p

theorem Bananas.normalizedOriginalToInverse_normalizedInverseToOriginal {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hBij : Function.Bijective tau) (hAffine : IsKAffine k tau) {p : ℤ × ℤ} (hp : p ∈ kInversions k (rawInverse tau)) : normalizedOriginalToInverse k tau (normalizedInverseToOriginal k tau p) = p

theorem Bananas.kInversionCount_rawInverse {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hBij : Function.Bijective tau) (hAffine : IsKAffine k tau) : kInversionCount k (rawInverse tau) = kInversionCount k tau

Inversion preserves the number of affine-period inversion classes.

theorem Bananas.affineReflection_bijective {tau : ℤ → ℤ} (hBij : Function.Bijective tau) : Function.Bijective (rawAffineReflection tau)

Reflection in the origin preserves bijectivity.

theorem Bananas.IsKAffine.affineReflection {k : ℕ} {tau : ℤ → ℤ} (hAffine : IsKAffine k tau) : IsKAffine k (rawAffineReflection tau)

Reflection in the origin preserves a positive affine period.

def Bananas.reflectionInversionPair (p : ℤ × ℤ) : ℤ × ℤ

Reverse a pair and negate both entries. This carries inversions of a reflected permutation to inversions of the original permutation.

Equations

• Bananas.reflectionInversionPair p = (-p.2, -p.1)

theorem Bananas.reflectionInversionPair_involutive : Function.Involutive reflectionInversionPair

theorem Bananas.reflectionInversionPair_shiftPair (k : ℕ) (q : ℤ) (p : ℤ × ℤ) : reflectionInversionPair (shiftPair k q p) = shiftPair k (-q) (reflectionInversionPair p)

def Bananas.normalizedReflectionInversion (k : ℕ) (p : ℤ × ℤ) : ℤ × ℤ

Normalize the original inversion corresponding to an inversion of the reflected permutation. The same map, with source and target exchanged, is its inverse.

Equations

• Bananas.normalizedReflectionInversion k p = Bananas.normalizeFirstPair k (Bananas.reflectionInversionPair p)

theorem Bananas.normalizedReflectionInversion_mem {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k tau) {p : ℤ × ℤ} (hp : p ∈ kInversions k (rawAffineReflection tau)) : normalizedReflectionInversion k p ∈ kInversions k tau

theorem Bananas.normalizedReflectionInversion_mem_reflection {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k tau) {p : ℤ × ℤ} (hp : p ∈ kInversions k tau) : normalizedReflectionInversion k p ∈ kInversions k (rawAffineReflection tau)

theorem Bananas.normalizedReflectionInversion_involutive_on_kInversions {k : ℕ} (hk : 0 < k) {p : ℤ × ℤ} (hp : 0 ≤ p.1 ∧ p.1 < ↑k) : normalizedReflectionInversion k (normalizedReflectionInversion k p) = p

theorem Bananas.kInversionCount_affineReflection {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k tau) : kInversionCount k (rawAffineReflection tau) = kInversionCount k tau

Reflection in the origin preserves the number of affine-period inversion classes.

theorem Bananas.kInversionCount_swapTransmissionPermutation {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hBij : Function.Bijective tau) (hAffine : IsKAffine k tau) : kInversionCount k (swapTransmissionPermutation tau) = kInversionCount k tau

Swapping a raw transmission permutation preserves its affine inversion count.

theorem Bananas.rawInverse_bijective {tau : ℤ → ℤ} (hBij : Function.Bijective tau) : Function.Bijective (rawInverse tau)

theorem Bananas.swapTransmissionPermutation_bijective {tau : ℤ → ℤ} (hBij : Function.Bijective tau) : Function.Bijective (swapTransmissionPermutation tau)

theorem Bananas.IsKAffine.swapTransmissionPermutation {k : ℕ} {tau : ℤ → ℤ} (hAffine : IsKAffine k tau) (hBij : Function.Bijective tau) : IsKAffine k (Bananas.swapTransmissionPermutation tau)

theorem Bananas.rankDelta_mark_swap (G : CFGraph) (u v : G.V) (D : CFDiv G) : rankDelta (mark G v u) D = rankDelta (mark G u v) D

The marked second rank difference is symmetric in the ordered marks.

theorem Bananas.IsTransmissionPermutation.swap_marks {G : CFGraph} (u v : G.V) (D : CFDiv G) {tau : ℤ → ℤ} (hTau : IsTransmissionPermutation (mark G u v) D tau) : IsTransmissionPermutation (mark G v u) D (swapTransmissionPermutation tau)

The reflected inverse is exactly the raw transmission permutation after the order of the two marked vertices is exchanged.

theorem Bananas.torsionWitness_swap {G : CFGraph} (u v : G.V) {k : ℕ} (h : TorsionWitness (mark G u v) k) : TorsionWitness (mark G v u) k

A torsion period is unchanged when the two marked vertices are exchanged.

theorem Bananas.torsionWitness_swap_iff {G : CFGraph} (u v : G.V) {k : ℕ} : TorsionWitness (mark G v u) k ↔ TorsionWitness (mark G u v) k

theorem Bananas.allSubmodular_swap_iff {G : CFGraph} (u v : G.V) : AllSubmodular (mark G v u) ↔ AllSubmodular (mark G u v)

Submodularity of every divisor is unchanged by ordering the marks.

theorem Bananas.KGeneralTransmission.swap_marks {G : CFGraph} (u v : G.V) {k : ℕ} (hK : KGeneralTransmission (mark G u v) k) : KGeneralTransmission (mark G v u) k

k-general transmission is independent of the ordering of the two marked vertices.

theorem Bananas.kGeneralTransmission_swap_iff {G : CFGraph} (u v : G.V) {k : ℕ} : KGeneralTransmission (mark G v u) k ↔ KGeneralTransmission (mark G u v) k