Documentation

LeanPool.BrillNoetherGraphs.Utilities.Grassmannian.GrassmannianShift

Arbitrary output shifts of Grassmannian ASP permutations #

The once-marked census may be normalized to degree g, but the full transmission theory naturally uses every shift chi. This file derives that family from the shift-zero Grassmannian constructor without reconstructing its inversion set a second time.

source
noncomputable def Utilities.shiftedGrassmannianPerm (lambda : YoungDiagram) (chi : ℤ) :
AspPerm

The Grassmannian permutation of lambda with ASP shift chi.

Equations
Instances For
    source
    @[simp]
    theorem Utilities.shiftedGrassmannianPerm_chi (lambda : YoungDiagram) (chi : ℤ) :
    (shiftedGrassmannianPerm lambda chi).χ = chi
    source
    @[simp]
    theorem Utilities.inv_set_shiftedGrassmannianPerm (lambda : YoungDiagram) (chi : ℤ) :
    invSet (shiftedGrassmannianPerm lambda chi).func = grassmannianInvSet lambda
    source
    theorem Utilities.ncard_inv_set_shiftedGrassmannianPerm (lambda : YoungDiagram) (chi : ℤ) :
    (invSet (shiftedGrassmannianPerm lambda chi).func).ncard = lambda.card
    source
    theorem Utilities.eq_shiftedGrassmannianPerm_of_inv_set_eq_of_chi_eq (tau : AspPerm) (lambda : YoungDiagram) (chi : ℤ) (hInv : invSet tau.func = grassmannianInvSet lambda) (hChi : tau.χ = chi) :
    tau = shiftedGrassmannianPerm lambda chi

    An ASP permutation is uniquely determined by its inversion set and shift. Thus any externally presented Grassmannian permutation with the Ferrers inversion set of lambda is definitionally the canonical shifted constructor used in this library.

    source
    theorem Utilities.shiftedGrassmannianPerm_apply_of_nonneg (lambda : YoungDiagram) (chi : ℤ) {n : ℤ} (hn : 0 ≤ n) :
    (shiftedGrassmannianPerm lambda chi).func n = n - ↑(lambda.rowLen n.toNat) - chi

    The usual shifted Grassmannian formula on nonnegative inputs.

    source
    theorem Utilities.shiftedGrassmannianPerm_s_at_row (lambda : YoungDiagram) (chi : ℤ) (i : ℕ) :
    (shiftedGrassmannianPerm lambda chi).s.func (↑i + 1 - chi - ↑(lambda.rowLen i)) 0 = ↑i + 1

    Every partition row retains its exact slipface value after translating the first coordinate by -chi.

    source
    theorem Utilities.transmissionExists_shiftedGrassmannianPerm_iff {G : CFGraph} (u v : G.V) (lambda : YoungDiagram) (chi : ℤ) :
    TransmissionExists G u v (shiftedGrassmannianPerm lambda chi) ↔ TransmissionExists G u v (grassmannianPermOfYoungDiagram lambda)

    Output normalization does not change existence of the associated transmission locus; witnesses differ by chi chips at the first mark.

    source
    theorem Utilities.transmissionExists_shiftedGrassmannianPerm_iff_onceMarkedBNExists_of_negativeEnvelope {G : CFGraph} (hG : graphConnected G) (u v : G.V) (lambda : YoungDiagram) (chi : ℤ) (hNegative : GrassmannianNegativeEnvelope lambda) :
    TransmissionExists G u v (shiftedGrassmannianPerm lambda chi) ↔ OnceMarkedBNExists G u lambda

    Conditional-on-the-explicit-Ferrers-envelope form of the arbitrary-shift Grassmannian/once-marked dictionary. The output shift changes the normalized degree of a transmission witness but not its existence problem.

    source
    theorem Utilities.transmissionExists_shiftedGrassmannianPerm_iff_onceMarkedBNExists {G : CFGraph} (hG : graphConnected G) (u v : G.V) (lambda : YoungDiagram) (chi : ℤ) :
    TransmissionExists G u v (shiftedGrassmannianPerm lambda chi) ↔ OnceMarkedBNExists G u lambda

    Arbitrary output normalization of the unconditional Grassmannian/ once-marked dictionary.

    source
    theorem Utilities.transmissionExists_iff_onceMarkedBNExists_of_grassmannian_inv_set {G : CFGraph} (hG : graphConnected G) (u v : G.V) (tau : AspPerm) (lambda : YoungDiagram) (chi : ℤ) (hInv : invSet tau.func = grassmannianInvSet lambda) (hChi : tau.χ = chi) :
    TransmissionExists G u v tau ↔ OnceMarkedBNExists G u lambda

    Presentation-independent dictionary. Any ASP permutation whose inversion set is the Ferrers set of lambda and whose shift is chi has exactly the once-marked transmission locus, even if it was not built with the canonical constructor.