Documentation

LeanPool.RegtsSevenster.RS.Novel.Coordinates.EdgeSign

The edge-sign sector #

Flipping the odd colouring converts the diagonal cap pairing's per-edge signs into the Definition 5 orientation signs, up to the count of edges whose representative is incoming.

source
noncomputable def RS.inRepCount (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) :
ℕ

The participating edges whose representative flag is incoming.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem RS.repFlag_symm_castAdd (W : ClosedFragment) (i : Fin (edgeCount W)) :
    repFlag W ((starFlagEnum W).symm (Fin.castAdd (edgeCount W) i)) = (starFlagEnum W).symm (Fin.castAdd (edgeCount W) i)

    Representative slots are their own edge representatives.

    source
    theorem RS.edge_sign_sector {ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) :
    (∏ i : Fin (edgeCount W), if h : (starFlagEnum W).symm (Fin.castAdd (edgeCount W) i) ∈ F.flags then -↑(oddPartnerSign ℓ (↑(EdgeSubset.OddColouring.flip F (outRepSet W F o) ⋯ φ) ⟨(starFlagEnum W).symm (Fin.castAdd (edgeCount W) i), h⟩)) else 1) = (-1) ^ inRepCount W F o * ∏ i : Fin (edgeCount W), if h : (starFlagEnum W).symm (Fin.castAdd (edgeCount W) i) ∈ F.flags then ↑(oddPartnerSign ℓ (↑φ ⟨(starFlagEnum W).symm (Fin.castAdd (edgeCount W) i), h⟩)) else 1

    The edge-sign sector: the flipped diagonal signs are the orientation signs times the incoming-representative parity.