Documentation

LeanPool.BrillNoetherGraphs.Utilities.Subdivision.CoreExpansionClosed

Closed faces carried by a core expansion #

The positive expansion certificate in CoreExpansion assigns length one to slots internal to a fibre and then contracts them topologically. A closed row construction instead assigns those slots length zero. The bridge between the two descriptions is the following fibre theorem: the equivalence relation generated by the slots tagged contracted is exactly equality under the expansion's fibre map.

This statement is genus-independent and contains no finite atlas data. It is the combinatorial heart of lowering a closed construction on a trivalent expansion back to the smaller core.

source
def Utilities.Subdivision.CoreExpansion.ExpansionData.contractedSlots {n p N Q : ℕ} (D : ExpansionData n p N Q) :
Finset (Fin Q)

Slots which disappear in the closed face associated to an expansion.

Equations
Instances For
    source
    @[simp]
    theorem Utilities.Subdivision.CoreExpansion.ExpansionData.mem_contractedSlots {n p N Q : ℕ} (D : ExpansionData n p N Q) (e : Fin Q) :
    e ∈ D.contractedSlots ↔ D.kind e = SlotKind.contracted
    source
    theorem Utilities.Subdivision.CoreExpansion.ExpansionData.fib_eq_of_adjInContracted {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (hCond : D.Conditions C) {a b : Fin N} (hab : Certificate.ContractionForestCensusGeneral.AdjInList D.bigCore (Certificate.ContractionForestCensusGeneral.edgeList D.contractedSlots) a b) :
    D.fib a = D.fib b

    Direct adjacency through a contracted slot stays in one fibre.

    source
    theorem Utilities.Subdivision.CoreExpansion.ExpansionData.fib_eq_of_reachInContracted {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (hCond : D.Conditions C) {a b : Fin N} (hab : Certificate.ContractionForestCensusGeneral.ReachIn D.bigCore D.contractedSlots a b) :
    D.fib a = D.fib b

    A chain of contracted slots stays in one fibre.

    source
    theorem Utilities.Subdivision.CoreExpansion.ExpansionData.reachInContracted_of_fib_eq {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (hCond : D.Conditions C) {a b : Fin N} (hab : D.fib a = D.fib b) :
    Certificate.ContractionForestCensusGeneral.ReachIn D.bigCore D.contractedSlots a b

    Conversely, the finite-cut fibre condition in ExpansionData.Conditions forces every two vertices of one fibre to be joined by contracted slots.

    source
    theorem Utilities.Subdivision.CoreExpansion.ExpansionData.compFold_eq_iff_fib_eq {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (hCond : D.Conditions C) (a b : Fin N) :
    Certificate.ContractionForestCensusGeneral.compFold D.bigCore D.contractedSlots a = Certificate.ContractionForestCensusGeneral.compFold D.bigCore D.contractedSlots b ↔ D.fib a = D.fib b

    Expansion fibre theorem. The union-find quotient generated by the contracted expansion slots has exactly the fibres prescribed by D.fib.