Coherent colors on ordered distinct pairs

A PairColorSystem colors ordered pairs of distinct vertices. Its palette carries an involution describing how colors change when the vertices are exchanged. This permits both symmetric colors and genuinely oriented colors in the lower skeleton of a hypergraph complex.

PairColorSystem.colorOfPair extends the coloring to all vertex pairs with values in Option: only diagonal pairs have color none. PairColorSystem.ofRaw makes any directed coloring coherent by recording its colors in both orientations, using the product palette. PairColorSystem.relabel renames the palette along an equivalence. PairColorSystem.split refines a coloring by a symmetric labelling of the unordered pairs. PairColorSystem.comap restricts a coloring along a vertex embedding, preserving the palette. coordPair extracts the ordered distinct pair of two coordinates of an injective tuple, and card_filter_coordPair_mem_le counts the injective triples with a coordinate pair in a given set.

structure TauCeti.PairColorSystem (κ : Type u_1) (V : Type u_2) : Type (max u_1 u_2)

A coloring of ordered distinct pairs, coherent with an involution of the palette.

• color : { p : V × V // p.1 ≠ p.2 } → κ

  The color of an ordered distinct pair.

• rev : κ → κ

  Palette reversal.

• rev_involutive : Function.Involutive self.rev

  Reversing a color twice recovers it.

• color_rev (p : { p : V × V // p.1 ≠ p.2 }) : self.color ⟨(↑p).swap, ⋯⟩ = self.rev (self.color p)

  Exchanging the vertices reverses their color.

theorem TauCeti.PairColorSystem.ext {κ : Type u_1} {V : Type u_2} {S T : PairColorSystem κ V} (hcolor : ∀ (p : { p : V × V // p.1 ≠ p.2 }), S.color p = T.color p) (hrev : ∀ (c : κ), S.rev c = T.rev c) : S = T

Pair-color systems are determined by their coloring and palette reversal.

theorem TauCeti.PairColorSystem.ext_iff {κ : Type u_1} {V : Type u_2} {S T : PairColorSystem κ V} : S = T ↔ (∀ (p : { p : V × V // p.1 ≠ p.2 }), S.color p = T.color p) ∧ ∀ (c : κ), S.rev c = T.rev c

@[simp]

theorem TauCeti.PairColorSystem.rev_rev {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (c : κ) : S.rev (S.rev c) = c

noncomputable def TauCeti.PairColorSystem.colorOfPair {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (u v : V) : Option κ

The total pair color, with none exactly on the diagonal.

@[simp]

theorem TauCeti.PairColorSystem.colorOfPair_self {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (u : V) : S.colorOfPair u u = none

@[simp]

theorem TauCeti.PairColorSystem.colorOfPair_of_ne {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) {u v : V} (h : u ≠ v) : S.colorOfPair u v = some (S.color ⟨(u, v), h⟩)

Off the diagonal, the total color is the original color.

@[simp]

theorem TauCeti.PairColorSystem.colorOfPair_eq_none_iff {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (u v : V) : S.colorOfPair u v = none ↔ u = v

theorem TauCeti.PairColorSystem.colorOfPair_eq_some_iff {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (u v : V) (c : κ) : S.colorOfPair u v = some c ↔ ∃ (h : u ≠ v), S.color ⟨(u, v), h⟩ = c

A prescribed pair color implies distinctness and identifies the underlying color.

theorem TauCeti.PairColorSystem.colorOfPair_swap {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (u v : V) : S.colorOfPair v u = Option.map S.rev (S.colorOfPair u v)

Exchanging vertices applies palette reversal to the total color.

theorem TauCeti.PairColorSystem.colorOfPair_swap_eq_some_iff {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (u v : V) (c : κ) : S.colorOfPair v u = some (S.rev c) ↔ S.colorOfPair u v = some c

A reversed pair has the reversed color exactly when the original pair has that color.

def TauCeti.PairColorSystem.ofRaw {κ : Type u_1} {V : Type u_2} (color : { p : V × V // p.1 ≠ p.2 } → κ) : PairColorSystem (κ × κ) V

Make a directed coloring coherent by retaining the colors in both orientations. The palette is κ × κ, and reversal exchanges the coordinates.

@[simp]

theorem TauCeti.PairColorSystem.ofRaw_color {κ : Type u_1} {V : Type u_2} (color : { p : V × V // p.1 ≠ p.2 } → κ) (p : { p : V × V // p.1 ≠ p.2 }) : (ofRaw color).color p = (color p, color ⟨(↑p).swap, ⋯⟩)

@[simp]

theorem TauCeti.PairColorSystem.ofRaw_rev {κ : Type u_1} {V : Type u_2} (color : { p : V × V // p.1 ≠ p.2 } → κ) (c : κ × κ) : (ofRaw color).rev c = c.swap

def TauCeti.PairColorSystem.relabel {κ : Type u_1} {V : Type u_2} {κ' : Type u_3} (S : PairColorSystem κ V) (e : κ ≃ κ') : PairColorSystem κ' V

Rename the palette of a coherent coloring along an equivalence, conjugating the reversal.

@[simp]

theorem TauCeti.PairColorSystem.relabel_color {κ : Type u_1} {V : Type u_2} {κ' : Type u_3} (S : PairColorSystem κ V) (e : κ ≃ κ') (p : { p : V × V // p.1 ≠ p.2 }) : (S.relabel e).color p = e (S.color p)

@[simp]

theorem TauCeti.PairColorSystem.relabel_rev {κ : Type u_1} {V : Type u_2} {κ' : Type u_3} (S : PairColorSystem κ V) (e : κ ≃ κ') (c : κ') : (S.relabel e).rev c = e (S.rev (e.symm c))

def TauCeti.PairColorSystem.split {κ : Type u_1} {V : Type u_2} {ι : Type u_3} (S : PairColorSystem κ V) (f : Sym2 V → ι) : PairColorSystem (κ × ι) V

Split a coherent pair coloring by a symmetric labelling of the unordered vertex pairs: the color of an ordered distinct pair (u, v) becomes its original color together with the label of s(u, v). Reversal reverses the original color and keeps the label.

@[simp]

theorem TauCeti.PairColorSystem.split_color {κ : Type u_1} {V : Type u_2} {ι : Type u_3} (S : PairColorSystem κ V) (f : Sym2 V → ι) (p : { p : V × V // p.1 ≠ p.2 }) : (S.split f).color p = (S.color p, f s((↑p).1, (↑p).2))

@[simp]

theorem TauCeti.PairColorSystem.split_rev {κ : Type u_1} {V : Type u_2} {ι : Type u_3} (S : PairColorSystem κ V) (f : Sym2 V → ι) (c : κ × ι) : (S.split f).rev c = (S.rev c.1, c.2)

theorem TauCeti.PairColorSystem.colorOfPair_split {κ : Type u_1} {V : Type u_2} {ι : Type u_3} (S : PairColorSystem κ V) (f : Sym2 V → ι) (u v : V) : (S.split f).colorOfPair u v = Option.map (fun (c : κ) => (c, f s(u, v))) (S.colorOfPair u v)

The total split color is the total original color together with the label of the pair.

@[simp]

theorem TauCeti.PairColorSystem.colorOfPair_split_eq_some_iff {κ : Type u_1} {V : Type u_2} {ι : Type u_3} (S : PairColorSystem κ V) (f : Sym2 V → ι) (u v : V) (c : κ) (i : ι) : (S.split f).colorOfPair u v = some (c, i) ↔ S.colorOfPair u v = some c ∧ f s(u, v) = i

def TauCeti.PairColorSystem.comap {κ : Type u_1} {V : Type u_2} {W : Type u_4} (S : PairColorSystem κ W) (f : V ↪ W) : PairColorSystem κ V

Restrict a coherent pair coloring along a vertex embedding. The palette and its reversal are unchanged.

@[simp]

theorem TauCeti.PairColorSystem.comap_color {κ : Type u_1} {V : Type u_2} {W : Type u_4} (S : PairColorSystem κ W) (f : V ↪ W) (p : { p : V × V // p.1 ≠ p.2 }) : (S.comap f).color p = S.color ⟨(f (↑p).1, f (↑p).2), ⋯⟩

@[simp]

theorem TauCeti.PairColorSystem.comap_rev {κ : Type u_1} {V : Type u_2} {W : Type u_4} (S : PairColorSystem κ W) (f : V ↪ W) (c : κ) : (S.comap f).rev c = S.rev c

@[simp]

theorem TauCeti.PairColorSystem.colorOfPair_comap {κ : Type u_1} {V : Type u_2} {W : Type u_4} (S : PairColorSystem κ W) (f : V ↪ W) (u v : V) : (S.comap f).colorOfPair u v = S.colorOfPair (f u) (f v)

@[simp]

theorem TauCeti.PairColorSystem.comap_refl {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) : S.comap (Function.Embedding.refl V) = S

@[simp]

theorem TauCeti.PairColorSystem.comap_comap {κ : Type u_1} {V : Type u_2} {W : Type u_4} {U : Type u_5} (S : PairColorSystem κ U) (g : W ↪ U) (f : V ↪ W) : (S.comap g).comap f = S.comap (f.trans g)

def TauCeti.coordPair {ι : Type u_1} {V : Type u_2} (x : { x : ι → V // Function.Injective x }) (i j : ι) (hij : i ≠ j) : { p : V × V // p.1 ≠ p.2 }

The ordered distinct pair formed by two coordinates of an injective tuple.

@[simp]

theorem TauCeti.coe_coordPair {ι : Type u_1} {V : Type u_2} (x : { x : ι → V // Function.Injective x }) (i j : ι) (hij : i ≠ j) : ↑(coordPair x i j hij) = (↑x i, ↑x j)

The underlying pair of coordPair x i j hij consists of the ith and jth coordinates.

theorem TauCeti.PairColorSystem.color_coordPair_eq_iff {ι : Type u_1} {κ : Type u_2} {V : Type u_3} (C : PairColorSystem κ V) {x : { x : ι → V // Function.Injective x }} {i j : ι} (hij : i ≠ j) {k : κ} : C.color (coordPair x i j hij) = k ↔ C.colorOfPair (↑x i) (↑x j) = some k

The color of a coordinate pair is the total pair color of the two coordinates.

theorem TauCeti.card_filter_coordPair_mem_le {V : Type u_1} [Fintype V] [DecidableEq V] (E : Finset { p : V × V // p.1 ≠ p.2 }) {i j k : Fin 3} (hij : i ≠ j) (hl : ∀ (l : Fin 3), l = i ∨ l = j ∨ l = k) : {x : { x : Fin 3 → V // Function.Injective x } | coordPair x i j hij ∈ E}.card ≤ E.card * Fintype.card V

The injective triples whose coordinate pair on the roles i and j lies in E are at most |E| |V| many: such a triple is determined by that pair and its third coordinate k.