Totally colored three-uniform hypergraphs

A Colored3Graph κ V assigns one color to each unordered three-element set of vertices. In particular, symmetry is built into the domain of the coloring. An absent edge can be represented by a distinguished palette value, so color-preserving injections preserve nonedges as well as edges. No finiteness assumption on the vertex type or palette is needed.

Restriction along a vertex embedding is provided by Colored3Graph.comap. Colored3Graph.extend adds vertices using a default color on all new triples.

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

A total coloring of unordered triples. Nonedges, when present, are palette values.

• color : ↑(Set.powersetCard V 3) → κ

  The color of each three-element vertex set.

theorem TauCeti.Colored3Graph.ext {κ : Type u_1} {V : Type u_2} {x y : Colored3Graph κ V} (color : x.color = y.color) : x = y

theorem TauCeti.Colored3Graph.ext_iff {κ : Type u_1} {V : Type u_2} {x y : Colored3Graph κ V} : x = y ↔ x.color = y.color

def TauCeti.Colored3Graph.const {κ : Type u_1} {V : Type u_2} (c : κ) : Colored3Graph κ V

The coloring in which every triple has color c.

@[simp]

theorem TauCeti.Colored3Graph.color_const {κ : Type u_1} {V : Type u_2} (c : κ) (s : ↑(Set.powersetCard V 3)) : (const c).color s = c

def TauCeti.Colored3Graph.comap {κ : Type u_1} {V : Type u_2} {W : Type u_3} (H : Colored3Graph κ V) (f : W ↪ V) : Colored3Graph κ W

Restrict a coloring along an injective vertex map.

@[simp]

theorem TauCeti.Colored3Graph.color_comap {κ : Type u_1} {V : Type u_2} {W : Type u_3} (H : Colored3Graph κ V) (f : W ↪ V) (s : ↑(Set.powersetCard W 3)) : (H.comap f).color s = H.color (Set.powersetCard.map 3 f s)

@[simp]

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

@[simp]

theorem TauCeti.Colored3Graph.comap_comap {κ : Type u_1} {V : Type u_2} {W : Type u_3} {U : Type u_4} (H : Colored3Graph κ V) (f : W ↪ V) (g : U ↪ W) : (H.comap f).comap g = H.comap (g.trans f)

@[simp]

theorem TauCeti.Colored3Graph.comap_const {κ : Type u_1} {V : Type u_2} {W : Type u_3} (c : κ) (f : W ↪ V) : (const c).comap f = const c

noncomputable def TauCeti.Colored3Graph.extend {κ : Type u_1} {V : Type u_2} {W : Type u_3} (H : Colored3Graph κ V) (f : V ↪ W) (c : κ) : Colored3Graph κ W

Extend a coloring along a vertex embedding, assigning c to triples not wholly in its image.

@[simp]

theorem TauCeti.Colored3Graph.color_extend_map {κ : Type u_1} {V : Type u_2} {W : Type u_3} (H : Colored3Graph κ V) (f : V ↪ W) (c : κ) (s : ↑(Set.powersetCard V 3)) : (H.extend f c).color (Set.powersetCard.map 3 f s) = H.color s

Extension preserves the color of every original triple.

@[simp]

theorem TauCeti.Colored3Graph.color_extend_of_notMem_range {κ : Type u_1} {V : Type u_2} {W : Type u_3} (H : Colored3Graph κ V) (f : V ↪ W) (c : κ) (s : ↑(Set.powersetCard W 3)) (hs : s ∉ Set.range (Set.powersetCard.map 3 f)) : (H.extend f c).color s = c

A triple outside the image of the induced triple map receives the default color.

@[simp]

theorem TauCeti.Colored3Graph.comap_extend {κ : Type u_1} {V : Type u_2} {W : Type u_3} (H : Colored3Graph κ V) (f : V ↪ W) (c : κ) : (H.extend f c).comap f = H

Restricting an extension to the original vertices recovers the original coloring.

@[simp]

theorem TauCeti.Colored3Graph.extend_refl {κ : Type u_1} {V : Type u_2} (H : Colored3Graph κ V) (c : κ) : H.extend (Function.Embedding.refl V) c = H

Extending along the identity embedding adds no triples.

@[simp]

theorem TauCeti.Colored3Graph.extend_const {κ : Type u_1} {V : Type u_2} {W : Type u_3} (c : κ) (f : V ↪ W) : (const c).extend f c = const c

Extending a constant coloring by the same color remains constant.