OAI/Analysis/SphereIsometry/SpernerBoundary.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Boundary labels and restriction of the finite Sperner count

Admissible labels lie in the union of the vertex carriers. A good boundary facet therefore has exactly the carrier omitting the last coordinate. Mapping lower-dimensional faces through a vertex embedding preserves the label count after the coordinate embedding Fin.castSucc.

  1. theorem OAI.Tingley.sperner_label_image_subset_carrier line 22

    Source documentation

    Vertexwise carrier membership implies membership in the face carrier.

    theorem sperner_label_image_subset_carrier (label : V → I)
    (carrier : V → Finset I) (σ : Finset V)
    (hlabel : ∀ v ∈ σ, label v ∈ carrier v) :
    σ.image label ⊆ σ.biUnion carrier := by
…
  2. theorem OAI.Tingley.carrier_eq_spernerSmallLabels line 33

    Source documentation

    A good boundary facet can only lie on the original face missing the last coordinate. The conclusion follows from containment and equal cardinality.

    theorem carrier_eq_spernerSmallLabels {m : ℕ} (label : V → Fin (m + 1))
    (carrier : V → Finset (Fin (m + 1))) (σ : Finset V)
    (hlabel : ∀ v ∈ σ, label v ∈ carrier v)
    (hgood : σ.image label = spernerSmallLabels m)
    (hcard : (σ.biUnion carrier).card = m) :
    σ.biUnion carrier = spernerSmallLabels m := by
…

    Mentions: OAI.Tingley.spernerSmallLabels

  3. theorem OAI.Tingley.good_carrier_card_iff_last_not_mem line 48

    Source documentation

    For a good face, the boundary cardinality condition is equivalent to omission of the last coordinate from its carrier.

    theorem good_carrier_card_iff_last_not_mem {m : ℕ} (label : V → Fin (m + 1))
    (carrier : V → Finset (Fin (m + 1))) (σ : Finset V)
    (hlabel : ∀ v ∈ σ, label v ∈ carrier v)
    (hgood : σ.image label = spernerSmallLabels m) :
    (σ.biUnion carrier).card = m ↔ Fin.last m ∉ σ.biUnion carrier := by
…

    Mentions: OAI.Tingley.spernerSmallLabels

  4. theorem OAI.Tingley.good_boundary_filter_eq_last_face_filter line 71

    Source documentation

    Among good faces, all boundary faces are exactly those on the last face. This is the filter identity used before transporting the incidence count.

    theorem good_boundary_filter_eq_last_face_filter {m : ℕ}
    (label : V → Fin (m + 1)) (carrier : V → Finset (Fin (m + 1)))
    (faces : Finset (Finset V)) (hlabel : ∀ v, label v ∈ carrier v) :
    faces.filter (fun σ => σ.image label = spernerSmallLabels m ∧
        (σ.biUnion carrier).card = m) =
      (faces.filter (fun σ => Fin.last m ∉ σ.biUnion carrier)).filter
        (fun σ => σ.image label = spernerSmallLabels m) := by
…

    Mentions: OAI.Tingley.spernerSmallLabels

  5. def OAI.Tingley.spernerRestrictedLabel line 90

    Source documentation

    Remove the last coordinate from labels on an embedded boundary face.

    def spernerRestrictedLabel {n : ℕ} (e : W ↪ V) (label : V → Fin (n + 1))
    (hne : ∀ w, label (e w) ≠ Fin.last n) : W → Fin n :=
…
  6. theorem OAI.Tingley.castSucc_spernerRestrictedLabel line 95
  7. theorem OAI.Tingley.image_univ_castSucc_eq_spernerSmallLabels line 101

    Source documentation

    The smaller label set is exactly the image of the smaller coordinate type.

    theorem image_univ_castSucc_eq_spernerSmallLabels (n : ℕ) :
    (Finset.univ : Finset (Fin n)).image Fin.castSucc = spernerSmallLabels n := by
…

    Mentions: OAI.Tingley.spernerSmallLabels

  8. theorem OAI.Tingley.mapped_label_image_eq line 114

    Source documentation

    Compatible vertex and coordinate embeddings commute with the label image.

    theorem mapped_label_image_eq {n : ℕ} (e : W ↪ V)
    (label : V → Fin (n + 1)) (lowerLabel : W → Fin n)
    (hlabel : ∀ w, label (e w) = (lowerLabel w).castSucc) (σ : Finset W) :
    (σ.map e).image label = (σ.image lowerLabel).image Fin.castSucc := by
…
  9. theorem OAI.Tingley.mapped_fully_labelled_iff line 125

    Source documentation

    A mapped face is good exactly when its lower-dimensional face is full.

    theorem mapped_fully_labelled_iff {n : ℕ} (e : W ↪ V)
    (label : V → Fin (n + 1)) (lowerLabel : W → Fin n)
    (hlabel : ∀ w, label (e w) = (lowerLabel w).castSucc) (σ : Finset W) :
    (σ.map e).image label = spernerSmallLabels n ↔
      σ.image lowerLabel = Finset.univ := by
…

    Mentions: OAI.Tingley.spernerSmallLabels

  10. theorem OAI.Tingley.restricted_label_mem_carrier line 137

    Source documentation

    Restricting an admissible embedded label preserves membership in the lower-dimensional carrier.

    theorem restricted_label_mem_carrier {n : ℕ} (e : W ↪ V)
    (label : V → Fin (n + 1)) (hne : ∀ w, label (e w) ≠ Fin.last n)
    (carrier : W → Finset (Fin n))
    (hlabel : ∀ w, label (e w) ∈ (carrier w).image Fin.castSucc) (w : W) :
    spernerRestrictedLabel e label hne w ∈ carrier w := by
…

    Mentions: OAI.Tingley.spernerRestrictedLabel

  11. theorem OAI.Tingley.mapped_family_filter_card line 151

    Source documentation

    A finite family of faces can be filtered before or after an injective vertex map, without changing its cardinality.

    theorem mapped_family_filter_card (e : W ↪ V)
    (lowerFamily : Finset (Finset W)) (higherFamily : Finset (Finset V))
    (p : Finset W → Prop) (q : Finset V → Prop)
    [DecidablePred p] [DecidablePred q]
    (hfamily : higherFamily = lowerFamily.image (fun σ => σ.map e))
    (hpred : ∀ σ ∈ lowerFamily, q (σ.map e) ↔ p σ) :
    (higherFamily.filter q).card = (lowerFamily.filter p).card := by
…
  12. theorem OAI.Tingley.mapped_good_family_card line 166

    Source documentation

    Exact transport of the good-face count under a raw face-family bijection.

    theorem mapped_good_family_card {n : ℕ} (e : W ↪ V)
    (label : V → Fin (n + 1)) (lowerLabel : W → Fin n)
    (hlabel : ∀ w, label (e w) = (lowerLabel w).castSucc)
    (lowerFamily : Finset (Finset W)) (higherFamily : Finset (Finset V))
    (hfamily : higherFamily = lowerFamily.image (fun σ => σ.map e)) :
    (higherFamily.filter (fun τ => τ.image label = spernerSmallLabels n)).card =
      (lowerFamily.filter (fun σ => σ.image lowerLabel = Finset.univ)).card := by
…

    Mentions: OAI.Tingley.spernerSmallLabels

  13. theorem OAI.Tingley.mapped_good_family_card_of_map line 180

    Source documentation

    Count transport in the Finset.map form produced by the subdivision restriction theorem.

    theorem mapped_good_family_card_of_map {n : ℕ} (e : W ↪ V)
    (label : V → Fin (n + 1)) (lowerLabel : W → Fin n)
    (hlabel : ∀ w, label (e w) = (lowerLabel w).castSucc)
    (lowerFamily : Finset (Finset W)) (higherFamily : Finset (Finset V))
    (hfamily : higherFamily = lowerFamily.map (Finset.mapEmbedding e).toEmbedding) :
    (higherFamily.filter (fun τ => τ.image label = spernerSmallLabels n)).card =
      (lowerFamily.filter (fun σ => σ.image lowerLabel = Finset.univ)).card := by
…

    Mentions: OAI.Tingley.spernerSmallLabels

  14. theorem OAI.Tingley.mapped_good_family_card_of_mem_iff line 196

    Source documentation

    The same count transport with a membership characterization of the raw boundary family, rather than an equality already assembled by the caller.

    theorem mapped_good_family_card_of_mem_iff {n : ℕ} (e : W ↪ V)
    (label : V → Fin (n + 1)) (lowerLabel : W → Fin n)
    (hlabel : ∀ w, label (e w) = (lowerLabel w).castSucc)
    (lowerFamily : Finset (Finset W)) (higherFamily : Finset (Finset V))
    (hfamily : ∀ τ, τ ∈ higherFamily ↔ ∃ σ ∈ lowerFamily, σ.map e = τ) :
    (higherFamily.filter (fun τ => τ.image label = spernerSmallLabels n)).card =
      (lowerFamily.filter (fun σ => σ.image lowerLabel = Finset.univ)).card := by
…

    Mentions: OAI.Tingley.spernerSmallLabels

  15. theorem OAI.Tingley.good_boundary_family_card line 211

    Source documentation

    The exact good-boundary expression used in the incidence count becomes the fully labelled lower-dimensional expression.

    theorem good_boundary_family_card {n : ℕ} (e : W ↪ V)
    (label : V → Fin (n + 1)) (lowerLabel : W → Fin n)
    (hlabel : ∀ w, label (e w) = (lowerLabel w).castSucc)
    (lowerFamily : Finset (Finset W)) (higherFamily : Finset (Finset V))
    (boundary : Finset V → Prop) [DecidablePred boundary]
    (hfamily : higherFamily.filter boundary = lowerFamily.image (fun σ => σ.map e)) :
    (higherFamily.filter
      (fun τ => τ.image label = spernerSmallLabels n ∧ boundary τ)).card =
      (lowerFamily.filter (fun σ => σ.image lowerLabel = Finset.univ)).card := by
…

    Mentions: OAI.Tingley.spernerSmallLabels