Rank and transmission transport along harmonic pullback

The rank-one fibre argument is only the first consequence of a harmonic map. Whenever pullback preserves principal divisors, it does not decrease the rank of any target divisor. The proof pushes an arbitrary effective rank test to the target, wins there, and observes that pulling the pushed test back dominates the original source test.

This file also records the marked consequence at the natural level of generality. If the two marked one-chip divisors are exact pullbacks, every ASP transmission row pulls back. An additional effective source divisor may be added, so the degree can be adjusted independently; only the final transmission-degree equation remains to be supplied.

def MarkedGraphs.IndexedHarmonicData.pushforward {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (D : CFDiv G) : CFDiv H

Push a divisor forward by summing its coefficients over target fibres.

Equations

• f.pushforward D z = ∑ x : G.V, if f.vertexMap x = z then D x else 0

theorem MarkedGraphs.IndexedHarmonicData.deg_pushforward {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (D : CFDiv G) : CFDiv.degree (f.pushforward D) = CFDiv.degree D

Pushforward preserves total degree.

theorem MarkedGraphs.IndexedHarmonicData.pushforward_effective {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) {D : CFDiv G} (hD : effective D) : effective (f.pushforward D)

Pushforward preserves effectivity.

theorem MarkedGraphs.IndexedHarmonicData.pullback_effective {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) {A : CFDiv H} (hA : effective A) : effective (f.pullback A)

Pullback preserves effectivity.

theorem MarkedGraphs.IndexedHarmonicData.pullback_add {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (A B : CFDiv H) : f.pullback (A + B) = f.pullback A + f.pullback B

Pullback is additive.

theorem MarkedGraphs.IndexedHarmonicData.pullback_zsmul {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (a : ℤ) (A : CFDiv H) : f.pullback (a • A) = a • f.pullback A

Pullback commutes with integral scalar multiplication.

theorem MarkedGraphs.IndexedHarmonicData.pullback_pushforward_sub_effective {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) {D : CFDiv G} (hD : effective D) : effective (f.pullback (f.pushforward D) - D)

For an effective divisor, pulling its pushforward back dominates it.

The local degree is positive, and the fibre sum at x contains the summand at x; these are exactly the two inequalities used in the proof.

theorem MarkedGraphs.IndexedHarmonicData.winnable_pullback {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hPullback : f.PullbackPrincipalCompatible) {A : CFDiv H} (hA : winnable H A) : winnable G (f.pullback A)

Winnability transports along any pullback compatible with principal divisors.

theorem MarkedGraphs.IndexedHarmonicData.rank_pullback_ge {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hPullback : f.PullbackPrincipalCompatible) (A : CFDiv H) : rank G (f.pullback A) ≥ rank H A

Harmonic pullback does not decrease Baker--Norine rank.

def MarkedGraphs.IndexedHarmonicData.PullsBackMark {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (u : G.V) (p : H.V) : Prop

A source mark is an exact unramified singleton pullback of a target mark. The equation is the precise condition needed by the marked rank formulas and is often cheaper to check than separately spelling singleton and local-degree conditions.

Equations

• f.PullsBackMark u p = (f.pullback (oneChip p) = oneChip u)

theorem MarkedGraphs.IndexedHarmonicData.pullback_markedTwist {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) {u v : G.V} {p q : H.V} (hu : f.PullsBackMark u p) (hv : f.PullsBackMark v q) (A : CFDiv H) (a b : ℤ) : f.pullback (A + a • oneChip p - b • oneChip q) = f.pullback A + a • oneChip u - b • oneChip v

Marked twists commute with pullback at two exact marked fibres.

theorem MarkedGraphs.IndexedHarmonicData.transmissionInequality_pullback {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hPullback : f.PullbackPrincipalCompatible) {u v : G.V} {p q : H.V} (hu : f.PullsBackMark u p) (hv : f.PullsBackMark v q) (τ : AspPerm) (A : CFDiv H) (a b : ℤ) (hRow : Utilities.TransmissionInequality H p q τ A a b) : Utilities.TransmissionInequality G u v τ (f.pullback A) a b

Every individual ASP transmission inequality transports through harmonic pullback at exact marked fibres.

theorem MarkedGraphs.IndexedHarmonicData.transmissionInequality_pullback_add_effective {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hPullback : f.PullbackPrincipalCompatible) {u v : G.V} {p q : H.V} (hu : f.PullsBackMark u p) (hv : f.PullsBackMark v q) (τ : AspPerm) (A : CFDiv H) (E : CFDiv G) (a b : ℤ) (hE : effective E) (hRow : Utilities.TransmissionInequality H p q τ A a b) : Utilities.TransmissionInequality G u v τ (f.pullback A + E) a b

Adding an effective correction after pullback still preserves every marked transmission row.

theorem MarkedGraphs.IndexedHarmonicData.satisfiesTransmissionOn_pullback {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hPullback : f.PullbackPrincipalCompatible) {u v : G.V} {p q : H.V} (hu : f.PullsBackMark u p) (hv : f.PullsBackMark v q) (τ : AspPerm) (A : CFDiv H) (S : Set (ℤ × ℤ)) (hA : Utilities.SatisfiesTransmissionOn H p q τ A S) : Utilities.SatisfiesTransmissionOn G u v τ (f.pullback A) S

Restricted arbitrary-ASP transmission profiles pull back row by row.

theorem MarkedGraphs.IndexedHarmonicData.satisfiesTransmission_pullback {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hPullback : f.PullbackPrincipalCompatible) {u v : G.V} {p q : H.V} (hu : f.PullsBackMark u p) (hv : f.PullsBackMark v q) (τ : AspPerm) (A : CFDiv H) (hA : Utilities.SatisfiesTransmission H p q τ A) (hDegree : CFDiv.degree (f.pullback A) = G.genus + τ.χ) : Utilities.SatisfiesTransmission G u v τ (f.pullback A)

Full arbitrary-ASP transmission pulls back once the resulting divisor has the source graph's required transmission degree.

theorem MarkedGraphs.IndexedHarmonicData.satisfiesTransmission_pullback_add_effective {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hPullback : f.PullbackPrincipalCompatible) {u v : G.V} {p q : H.V} (hu : f.PullsBackMark u p) (hv : f.PullsBackMark v q) (τ : AspPerm) (A : CFDiv H) (E : CFDiv G) (hA : Utilities.SatisfiesTransmission H p q τ A) (hE : effective E) (hDegree : CFDiv.degree (f.pullback A + E) = G.genus + τ.χ) : Utilities.SatisfiesTransmission G u v τ (f.pullback A + E)

An effective source correction may adjust the pullback degree without spoiling any arbitrary-ASP transmission row.

theorem MarkedGraphs.IndexedHarmonicData.transmissionExists_of_pullback_add_effective {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hPullback : f.PullbackPrincipalCompatible) {u v : G.V} {p q : H.V} (hu : f.PullsBackMark u p) (hv : f.PullsBackMark v q) (τ : AspPerm) (A : CFDiv H) (E : CFDiv G) (hA : Utilities.SatisfiesTransmission H p q τ A) (hE : effective E) (hDegree : CFDiv.degree (f.pullback A + E) = G.genus + τ.χ) : Utilities.TransmissionExists G u v τ

Existence form of effective-corrected marked harmonic pullback.

def MarkedGraphs.IndexedHarmonicData.HarmonicTransmissionProfile {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (u v : G.V) (p q : H.V) (τ : AspPerm) (A : CFDiv H) (D : CFDiv G) : Prop

Row-wise comparison data for transporting a transmission divisor through a harmonic map. Unlike PullsBackMark, this permits ramified or nonsingleton marked fibres: for each row, the source twist need only be the corresponding target pullback plus an effective correction.

Equations

• One or more equations did not get rendered due to their size.

theorem MarkedGraphs.IndexedHarmonicData.satisfiesTransmission_of_harmonicProfile {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hPullback : f.PullbackPrincipalCompatible) (u v : G.V) (p q : H.V) (τ : AspPerm) (A : CFDiv H) (D : CFDiv G) (hTarget : Utilities.SatisfiesTransmission H p q τ A) (hProfile : f.HarmonicTransmissionProfile u v p q τ A D) : Utilities.SatisfiesTransmission G u v τ D

A harmonic transmission profile and a target transmission witness give a source witness for the same arbitrary ASP permutation.

theorem MarkedGraphs.IndexedHarmonicData.transmissionExists_of_harmonicProfile {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hPullback : f.PullbackPrincipalCompatible) (u v : G.V) (p q : H.V) (τ : AspPerm) (A : CFDiv H) (D : CFDiv G) (hTarget : Utilities.SatisfiesTransmission H p q τ A) (hProfile : f.HarmonicTransmissionProfile u v p q τ A D) : Utilities.TransmissionExists G u v τ

Existence wrapper for an arbitrary-ASP harmonic transmission profile.