Documentation

LeanPool.BrillNoetherGraphs.Bananas.Basics.MarkedIso

Second rank differences under marked graph isomorphism #

source
theorem Bananas.rankDelta_mapDiv_of_marks {M N : TwiceMarked} (φ : Utilities.CFGraphIso M.graph N.graph) (hu : φ.vertexEquiv M.u = N.u) (hv : φ.vertexEquiv M.v = N.v) (D : CFDiv M.graph) :
rankDelta N (φ.mapDiv D) = rankDelta M D

rankDelta is invariant under an isomorphism that carries the ordered marked pair to the ordered marked pair. Explicit marked structures avoid any dependently typed coercion through mark.

source
theorem Bananas.torsionWitness_mapDiv_of_marks_iff {M N : TwiceMarked} (φ : Utilities.CFGraphIso M.graph N.graph) (hu : φ.vertexEquiv M.u = N.u) (hv : φ.vertexEquiv M.v = N.v) (k : ℕ) :
TorsionWitness N k ↔ TorsionWitness M k
source
theorem Bananas.isTorsionOrder_map_of_marks_iff {M N : TwiceMarked} (φ : Utilities.CFGraphIso M.graph N.graph) (hu : φ.vertexEquiv M.u = N.u) (hv : φ.vertexEquiv M.v = N.v) (k : ℕ) :
IsTorsionOrder N k ↔ IsTorsionOrder M k
source
theorem Bananas.submodular_mapDiv_of_marks_iff {M N : TwiceMarked} (φ : Utilities.CFGraphIso M.graph N.graph) (hu : φ.vertexEquiv M.u = N.u) (hv : φ.vertexEquiv M.v = N.v) (D : CFDiv M.graph) :
Submodular N (φ.mapDiv D) ↔ Submodular M D
source
theorem Bananas.isTransmissionPermutation_mapDiv_of_marks_iff {M N : TwiceMarked} (φ : Utilities.CFGraphIso M.graph N.graph) (hu : φ.vertexEquiv M.u = N.u) (hv : φ.vertexEquiv M.v = N.v) (D : CFDiv M.graph) (τ : ℤ → ℤ) :
IsTransmissionPermutation N (φ.mapDiv D) τ ↔ IsTransmissionPermutation M D τ

The same integer transmission permutation witnesses the mapped divisor. This is the raw IsTransmissionPermutation counterpart of rank transport.

source
theorem Bananas.allSubmodular_map_of_marks_iff {M N : TwiceMarked} (φ : Utilities.CFGraphIso M.graph N.graph) (hu : φ.vertexEquiv M.u = N.u) (hv : φ.vertexEquiv M.v = N.v) :
AllSubmodular N ↔ AllSubmodular M

All-divisor submodularity is a marked graph-isomorphism invariant.

source
theorem Bananas.kGeneralTransmission_map_of_marks_iff {M N : TwiceMarked} (φ : Utilities.CFGraphIso M.graph N.graph) (hu : φ.vertexEquiv M.u = N.u) (hv : φ.vertexEquiv M.v = N.v) (k : ℕ) :
KGeneralTransmission N k ↔ KGeneralTransmission M k

General transmission is invariant under a certified isomorphism of ordered marked graphs.