SpernerIncidence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Counting labelled incidences in a finite complex

The two orders of summation count the same actual top-cell/facet pairs. Local facet parity leaves the fully labelled top cells on one side. Degree two facets cancel on the other side, leaving only the degree one boundary facets.

theorem OAI.Tingley.FiniteComplex.goodFacets_eq_codim_filter line 21

theorem OAI.Tingley.FiniteComplex.sperner_count_mod_two line 38

Source documentation

Finite incidence parity, before the boundary restriction is identified with the lower-dimensional simplex. All hypotheses concern finite face incidence.

theorem sperner_count_mod_two (K : FiniteComplex V) (m : ℕ)
    (label : V → Fin (m + 1)) (boundary : Finset V → Prop)
    [DecidablePred boundary]
    (hdegree : ∀ τ ∈ K.codimFaces m,
      (K.incidentTop m τ).card = if boundary τ then 1 else 2) :
    (((K.topCells m).filter (fun σ => σ.image label = Finset.univ)).card : ZMod 2) =
      (((K.codimFaces m).filter
        (fun τ => τ.image label = spernerSmallLabels m ∧ boundary τ)).card : ZMod 2) := by
…

Mentions: OAI.Tingley.FiniteComplex, OAI.Tingley.spernerSmallLabels

theorem OAI.Tingley.FiniteComplex.sperner_odd_of_boundary_odd line 88

Source documentation

An odd number of good boundary facets gives an odd number of fully labelled cells.

theorem sperner_odd_of_boundary_odd (K : FiniteComplex V) (m : ℕ)
    (label : V → Fin (m + 1)) (boundary : Finset V → Prop)
    [DecidablePred boundary]
    (hdegree : ∀ τ ∈ K.codimFaces m,
      (K.incidentTop m τ).card = if boundary τ then 1 else 2)
    (hboundary : Odd (((K.codimFaces m).filter
      (fun τ => τ.image label = spernerSmallLabels m ∧ boundary τ)).card)) :
    Odd (((K.topCells m).filter (fun σ => σ.image label = Finset.univ)).card) := by
…

Mentions: OAI.Tingley.FiniteComplex, OAI.Tingley.spernerSmallLabels