Triadic polyads

A Polyad3 records three vertex cells of a lower skeleton and one pair color for each of the three canonically oriented role pairs. Its support is computed from this data: it consists of the role-ordered injective triples in the chosen cells whose coordinate pairs have the chosen colors. Thus a polyad carries no independently chosen support. Conversely, an injective triple determines the unique polyad Polyad3.ofTriple whose support contains it, so the supports of distinct polyads are disjoint and split every finite set of injective triples (Polyad3.sum_card_inter_support).

The three pair supports expose the colored bigraphs whose arbitrary subgraphs form subpolyads. The faceKey convention translates colors indexed by role pairs to the omitted-coordinate indexing used by face-based descriptions of triads.

References

• V. Rödl and M. Schacht, Regular partitions of hypergraphs: regularity lemmas.
• B. Nagle, V. Rödl and M. Schacht, The counting lemma for regular k-uniform hypergraphs.

structure TauCeti.Polyad3 {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairSkeleton3 κ V) : Type (max u_1 u_2)

A triadic polyad over a lower skeleton: three vertex cells and the colors of the three canonically oriented pairs of roles. Its support is derived from these six data fields.

• c₀ : Finset V

  The vertex cell at role zero.

• c₁ : Finset V

  The vertex cell at role one.

• c₂ : Finset V

  The vertex cell at role two.

• hc₀ : self.c₀ ∈ S.vertexPart.parts

  The role-zero cell belongs to the skeleton partition.

• hc₁ : self.c₁ ∈ S.vertexPart.parts

  The role-one cell belongs to the skeleton partition.

• hc₂ : self.c₂ ∈ S.vertexPart.parts

  The role-two cell belongs to the skeleton partition.

• color₀₁ : κ

  The color on the ordered role pair (0, 1).

• color₀₂ : κ

  The color on the ordered role pair (0, 2).

• color₁₂ : κ

  The color on the ordered role pair (1, 2).

noncomputable def TauCeti.polyadSupport {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (C : PairColorSystem κ V) (c₀ c₁ c₂ : Finset V) (k₀₁ k₀₂ k₁₂ : κ) : Finset { x : Fin 3 → V // Function.Injective x }

The injective triples in specified cells whose three canonically oriented coordinate pairs have the specified colors.

@[simp]

theorem TauCeti.mem_polyadSupport {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {C : PairColorSystem κ V} {c₀ c₁ c₂ : Finset V} {k₀₁ k₀₂ k₁₂ : κ} {x : { x : Fin 3 → V // Function.Injective x }} : x ∈ polyadSupport C c₀ c₁ c₂ k₀₁ k₀₂ k₁₂ ↔ ↑x 0 ∈ c₀ ∧ ↑x 1 ∈ c₁ ∧ ↑x 2 ∈ c₂ ∧ C.colorOfPair (↑x 0) (↑x 1) = some k₀₁ ∧ C.colorOfPair (↑x 0) (↑x 2) = some k₀₂ ∧ C.colorOfPair (↑x 1) (↑x 2) = some k₁₂

Membership in a computed polyad support.

noncomputable def TauCeti.Polyad3.support {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) : Finset { x : Fin 3 → V // Function.Injective x }

The support of a polyad, computed from its cells and pair colors.

@[simp]

theorem TauCeti.Polyad3.mem_support {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) (x : { x : Fin 3 → V // Function.Injective x }) : x ∈ P.support ↔ ↑x 0 ∈ P.c₀ ∧ ↑x 1 ∈ P.c₁ ∧ ↑x 2 ∈ P.c₂ ∧ S.pairColors.colorOfPair (↑x 0) (↑x 1) = some P.color₀₁ ∧ S.pairColors.colorOfPair (↑x 0) (↑x 2) = some P.color₀₂ ∧ S.pairColors.colorOfPair (↑x 1) (↑x 2) = some P.color₁₂

Membership in a polyad's computed support.

theorem TauCeti.Polyad3.card_support_le {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) : P.support.card ≤ P.c₀.card * P.c₁.card * P.c₂.card

The support of a polyad has at most as many triples as the product of its three cells.

theorem TauCeti.Polyad3.ext_data {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P Q : Polyad3 S} (h₀ : P.c₀ = Q.c₀) (h₁ : P.c₁ = Q.c₁) (h₂ : P.c₂ = Q.c₂) (hk₀₁ : P.color₀₁ = Q.color₀₁) (hk₀₂ : P.color₀₂ = Q.color₀₂) (hk₁₂ : P.color₁₂ = Q.color₁₂) : P = Q

Two polyads are equal when their three cells and three pair colors agree.

theorem TauCeti.Polyad3.ext_data_iff {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P Q : Polyad3 S} : P = Q ↔ P.c₀ = Q.c₀ ∧ P.c₁ = Q.c₁ ∧ P.c₂ = Q.c₂ ∧ P.color₀₁ = Q.color₀₁ ∧ P.color₀₂ = Q.color₀₂ ∧ P.color₁₂ = Q.color₁₂

@[instance_reducible]

noncomputable instance TauCeti.Polyad3.instDecidableEq {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} [DecidableEq κ] : DecidableEq (Polyad3 S)

Polyads have decidable equality when the pair palette does.

@[instance_reducible]

noncomputable instance TauCeti.Polyad3.instFintype {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} [Fintype κ] : Fintype (Polyad3 S)

There are finitely many polyads over a finite pair palette.

def TauCeti.Polyad3.ofData {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (c₀ c₁ c₂ : Finset V) (h₀ : c₀ ∈ S.vertexPart.parts) (h₁ : c₁ ∈ S.vertexPart.parts) (h₂ : c₂ ∈ S.vertexPart.parts) (k₀₁ k₀₂ k₁₂ : κ) : Polyad3 S

The polyad determined by three cells of the skeleton and three pair colors.

@[simp]

theorem TauCeti.Polyad3.ofData_c₀ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (c₀ c₁ c₂ : Finset V) (h₀ : c₀ ∈ S.vertexPart.parts) (h₁ : c₁ ∈ S.vertexPart.parts) (h₂ : c₂ ∈ S.vertexPart.parts) (k₀₁ k₀₂ k₁₂ : κ) : (ofData c₀ c₁ c₂ h₀ h₁ h₂ k₀₁ k₀₂ k₁₂).c₀ = c₀

The role-zero cell of ofData is the given one.

@[simp]

theorem TauCeti.Polyad3.ofData_c₁ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (c₀ c₁ c₂ : Finset V) (h₀ : c₀ ∈ S.vertexPart.parts) (h₁ : c₁ ∈ S.vertexPart.parts) (h₂ : c₂ ∈ S.vertexPart.parts) (k₀₁ k₀₂ k₁₂ : κ) : (ofData c₀ c₁ c₂ h₀ h₁ h₂ k₀₁ k₀₂ k₁₂).c₁ = c₁

The role-one cell of ofData is the given one.

@[simp]

theorem TauCeti.Polyad3.ofData_c₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (c₀ c₁ c₂ : Finset V) (h₀ : c₀ ∈ S.vertexPart.parts) (h₁ : c₁ ∈ S.vertexPart.parts) (h₂ : c₂ ∈ S.vertexPart.parts) (k₀₁ k₀₂ k₁₂ : κ) : (ofData c₀ c₁ c₂ h₀ h₁ h₂ k₀₁ k₀₂ k₁₂).c₂ = c₂

The role-two cell of ofData is the given one.

@[simp]

theorem TauCeti.Polyad3.ofData_color₀₁ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (c₀ c₁ c₂ : Finset V) (h₀ : c₀ ∈ S.vertexPart.parts) (h₁ : c₁ ∈ S.vertexPart.parts) (h₂ : c₂ ∈ S.vertexPart.parts) (k₀₁ k₀₂ k₁₂ : κ) : (ofData c₀ c₁ c₂ h₀ h₁ h₂ k₀₁ k₀₂ k₁₂).color₀₁ = k₀₁

The color on roles zero and one of ofData is the given one.

@[simp]

theorem TauCeti.Polyad3.ofData_color₀₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (c₀ c₁ c₂ : Finset V) (h₀ : c₀ ∈ S.vertexPart.parts) (h₁ : c₁ ∈ S.vertexPart.parts) (h₂ : c₂ ∈ S.vertexPart.parts) (k₀₁ k₀₂ k₁₂ : κ) : (ofData c₀ c₁ c₂ h₀ h₁ h₂ k₀₁ k₀₂ k₁₂).color₀₂ = k₀₂

The color on roles zero and two of ofData is the given one.

@[simp]

theorem TauCeti.Polyad3.ofData_color₁₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (c₀ c₁ c₂ : Finset V) (h₀ : c₀ ∈ S.vertexPart.parts) (h₁ : c₁ ∈ S.vertexPart.parts) (h₂ : c₂ ∈ S.vertexPart.parts) (k₀₁ k₀₂ k₁₂ : κ) : (ofData c₀ c₁ c₂ h₀ h₁ h₂ k₀₁ k₀₂ k₁₂).color₁₂ = k₁₂

The color on roles one and two of ofData is the given one.

noncomputable def TauCeti.Polyad3.pairSupport₀₁ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) : Finset { p : V × V // p.1 ≠ p.2 }

The pair graph of a polyad on roles zero and one.

noncomputable def TauCeti.Polyad3.pairSupport₀₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) : Finset { p : V × V // p.1 ≠ p.2 }

The pair graph of a polyad on roles zero and two.

noncomputable def TauCeti.Polyad3.pairSupport₁₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) : Finset { p : V × V // p.1 ≠ p.2 }

The pair graph of a polyad on roles one and two.

@[simp]

theorem TauCeti.Polyad3.mem_pairSupport₀₁ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) (p : { p : V × V // p.1 ≠ p.2 }) : p ∈ P.pairSupport₀₁ ↔ (↑p).1 ∈ P.c₀ ∧ (↑p).2 ∈ P.c₁ ∧ S.pairColors.color p = P.color₀₁

Membership in the pair support on roles zero and one: the pair has its endpoints in the corresponding cells and carries the corresponding color.

@[simp]

theorem TauCeti.Polyad3.mem_pairSupport₀₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) (p : { p : V × V // p.1 ≠ p.2 }) : p ∈ P.pairSupport₀₂ ↔ (↑p).1 ∈ P.c₀ ∧ (↑p).2 ∈ P.c₂ ∧ S.pairColors.color p = P.color₀₂

Membership in the pair support on roles zero and two: the pair has its endpoints in the corresponding cells and carries the corresponding color.

@[simp]

theorem TauCeti.Polyad3.mem_pairSupport₁₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) (p : { p : V × V // p.1 ≠ p.2 }) : p ∈ P.pairSupport₁₂ ↔ (↑p).1 ∈ P.c₁ ∧ (↑p).2 ∈ P.c₂ ∧ S.pairColors.color p = P.color₁₂

Membership in the pair support on roles one and two: the pair has its endpoints in the corresponding cells and carries the corresponding color.

theorem TauCeti.card_polyad3_le {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairSkeleton3 κ V) [Fintype κ] : Fintype.card (Polyad3 S) ≤ S.vertexPart.parts.card ^ 3 * Fintype.card κ ^ 3

The number of polyads is bounded by the number of choices of three vertex cells and three pair colors.

def TauCeti.faceKey {κ : Type u_1} (k₀₁ k₀₂ k₁₂ : κ) : Fin 3 → κ

Translate role-pair colors to the face-key convention indexed by the omitted coordinate.

@[simp]

theorem TauCeti.faceKey_zero {κ : Type u_1} (k₀₁ k₀₂ k₁₂ : κ) : faceKey k₀₁ k₀₂ k₁₂ 0 = k₁₂

@[simp]

theorem TauCeti.faceKey_one {κ : Type u_1} (k₀₁ k₀₂ k₁₂ : κ) : faceKey k₀₁ k₀₂ k₁₂ 1 = k₀₂

@[simp]

theorem TauCeti.faceKey_two {κ : Type u_1} (k₀₁ k₀₂ k₁₂ : κ) : faceKey k₀₁ k₀₂ k₁₂ 2 = k₀₁

theorem TauCeti.coordPair_mem_pairSupport₀₁ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {x : { x : Fin 3 → V // Function.Injective x }} (hx : x ∈ P.support) : coordPair x 0 1 coordPair_mem_pairSupport₀₁._proof_1 ∈ P.pairSupport₀₁

The (0, 1) coordinate pair of a supported triple lies in the corresponding pair support.

theorem TauCeti.coordPair_mem_pairSupport₀₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {x : { x : Fin 3 → V // Function.Injective x }} (hx : x ∈ P.support) : coordPair x 0 2 coordPair_mem_pairSupport₀₂._proof_1 ∈ P.pairSupport₀₂

The (0, 2) coordinate pair of a supported triple lies in the corresponding pair support.

theorem TauCeti.coordPair_mem_pairSupport₁₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {x : { x : Fin 3 → V // Function.Injective x }} (hx : x ∈ P.support) : coordPair x 1 2 coordPair_mem_pairSupport₁₂._proof_1 ∈ P.pairSupport₁₂

The (1, 2) coordinate pair of a supported triple lies in the corresponding pair support.

theorem TauCeti.Polyad3.mem_support_iff_coordPair_mem {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {x : { x : Fin 3 → V // Function.Injective x }} : x ∈ P.support ↔ coordPair x 0 1 coordPair_mem_pairSupport₀₁._proof_1 ∈ P.pairSupport₀₁ ∧ coordPair x 0 2 coordPair_mem_pairSupport₀₂._proof_1 ∈ P.pairSupport₀₂ ∧ coordPair x 1 2 coordPair_mem_pairSupport₁₂._proof_1 ∈ P.pairSupport₁₂

A triple lies in the support of a polyad exactly when its three canonically oriented coordinate pairs lie in the corresponding pair supports.

noncomputable def TauCeti.Polyad3.ofTriple {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairSkeleton3 κ V) (x : { x : Fin 3 → V // Function.Injective x }) : Polyad3 S

The polyad of an injective triple: the vertex cells containing its three coordinates and the colors of its three canonically oriented coordinate pairs.

@[simp]

theorem TauCeti.Polyad3.ofTriple_c₀ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (x : { x : Fin 3 → V // Function.Injective x }) : (ofTriple S x).c₀ = S.vertexPart.part (↑x 0)

The role-zero cell of ofTriple is the cell containing the zeroth coordinate.

@[simp]

theorem TauCeti.Polyad3.ofTriple_c₁ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (x : { x : Fin 3 → V // Function.Injective x }) : (ofTriple S x).c₁ = S.vertexPart.part (↑x 1)

The role-one cell of ofTriple is the cell containing the first coordinate.

@[simp]

theorem TauCeti.Polyad3.ofTriple_c₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (x : { x : Fin 3 → V // Function.Injective x }) : (ofTriple S x).c₂ = S.vertexPart.part (↑x 2)

The role-two cell of ofTriple is the cell containing the second coordinate.

@[simp]

theorem TauCeti.Polyad3.ofTriple_color₀₁ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (x : { x : Fin 3 → V // Function.Injective x }) : (ofTriple S x).color₀₁ = S.pairColors.color (coordPair x 0 1 coordPair_mem_pairSupport₀₁._proof_1)

The color on roles zero and one of ofTriple is the color of the coordinate pair (0, 1).

@[simp]

theorem TauCeti.Polyad3.ofTriple_color₀₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (x : { x : Fin 3 → V // Function.Injective x }) : (ofTriple S x).color₀₂ = S.pairColors.color (coordPair x 0 2 coordPair_mem_pairSupport₀₂._proof_1)

The color on roles zero and two of ofTriple is the color of the coordinate pair (0, 2).

@[simp]

theorem TauCeti.Polyad3.ofTriple_color₁₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (x : { x : Fin 3 → V // Function.Injective x }) : (ofTriple S x).color₁₂ = S.pairColors.color (coordPair x 1 2 coordPair_mem_pairSupport₁₂._proof_1)

The color on roles one and two of ofTriple is the color of the coordinate pair (1, 2).

@[simp]

theorem TauCeti.Polyad3.mem_support_ofTriple {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (x : { x : Fin 3 → V // Function.Injective x }) : x ∈ (ofTriple S x).support

An injective triple lies in the support of its own polyad. The high priority lets this lemma fire before the general mem_support unfolds the support into color conditions.

theorem TauCeti.Polyad3.mem_support_iff_eq_ofTriple {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {x : { x : Fin 3 → V // Function.Injective x }} : x ∈ P.support ↔ P = ofTriple S x

A triple determines its polyad. An injective triple lies in the support of exactly one polyad over a given lower skeleton, namely Polyad3.ofTriple.

theorem TauCeti.Polyad3.ofTriple_eq_ofTriple_of_le {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {κ' : Type u_3} {T : PairSkeleton3 κ' V} (hV : T.vertexPart ≤ S.vertexPart) (f : κ' → κ) (hf : ∀ (p : { p : V × V // p.1 ≠ p.2 }), S.pairColors.color p = f (T.pairColors.color p)) {x y : { x : Fin 3 → V // Function.Injective x }} (h : ofTriple T x = ofTriple T y) : ofTriple S x = ofTriple S y

Polyads under a refined skeleton. If the vertex cells of T refine those of S and the pair colors of S factor through those of T, then two injective triples with the same polyad over T have the same polyad over S.

theorem TauCeti.Polyad3.ofTriple_relabel_eq_ofTriple_relabel_iff {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {κ' : Type u_3} (e : κ ≃ κ') {x y : { x : Fin 3 → V // Function.Injective x }} : ofTriple (S.relabel e) x = ofTriple (S.relabel e) y ↔ ofTriple S x = ofTriple S y

Relabeling the pair palette does not change which injective triples share a polyad.

theorem TauCeti.Polyad3.pairwise_disjoint_support {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} : Pairwise (Function.onFun Disjoint support)

Distinct polyads over the same lower skeleton have disjoint supports.

theorem TauCeti.Polyad3.sum_card_inter_support {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} [Fintype κ] (s : Finset { x : Fin 3 → V // Function.Injective x }) : ∑ P : Polyad3 S, (s ∩ P.support).card = s.card

The polyad supports over a lower skeleton partition the injective triples, so they split every finite set of injective triples.

theorem TauCeti.Polyad3.sum_comp_ofTriple {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} [Fintype κ] {M : Type u_3} [AddCommMonoid M] (φ : Polyad3 S → M) : ∑ x : { x : Fin 3 → V // Function.Injective x }, φ (ofTriple S x) = ∑ P : Polyad3 S, P.support.card • φ P

Summing a function of the polyad of each injective triple over all injective triples gives the support-weighted sum of that function over the polyads.