Finite bounded hypergraph complexes

This file defines finite augmented complexes whose faces have cardinality at most a fixed rank. Unlike Mathlib's PreAbstractSimplicialComplex, a HypergraphComplex includes the empty face and records faces in finite cardinality levels. The conversions in this file identify bounded pre-abstract simplicial complexes with finitely many faces with these finite graded complexes after forgetting or adjoining the empty face. Neither conversion requires a finite ambient vertex type.

Use HypergraphComplex.ofPreAbstractSimplicialComplex to construct a finite graded complex and HypergraphComplex.toPreAbstractSimplicialComplex to forget its empty face and grading.

The grading uses face cardinality: a triple lies in level 3, corresponding to simplicial dimension 2.

structure TauCeti.HypergraphComplex (r : ℕ) (V : Type u_1) : Type u_1

A finite augmented complex of rank r on V.

Its level k is a finite collection of k-element faces, the collections are downward closed, and the empty face belongs to level zero.

• faces (k : ℕ) : k ≤ r → Finset (Finset V)

  The faces of cardinality k, for k ≤ r.

• face_card (k : ℕ) (hk : k ≤ r) (s : Finset V) : s ∈ self.faces k hk → s.card = k

  Every face in level k has cardinality k.

• down_closed (k : ℕ) (hk : k ≤ r) (s : Finset V) : s ∈ self.faces k hk → ∀ t ⊆ s, ∀ (htr : t.card ≤ r), t ∈ self.faces t.card htr

  Every subset of a face occurs in the level given by its cardinality.

• empty_mem : ∅ ∈ self.faces 0 ⋯

  The empty face belongs to every complex.

theorem TauCeti.HypergraphComplex.ext {r : ℕ} {V : Type u_1} {C D : HypergraphComplex r V} (h : ∀ (k : ℕ) (hk : k ≤ r), C.faces k hk = D.faces k hk) : C = D

A bounded hypergraph complex is determined by its graded face collections.

theorem TauCeti.HypergraphComplex.ext_iff {r : ℕ} {V : Type u_1} {C D : HypergraphComplex r V} : C = D ↔ ∀ (k : ℕ) (hk : k ≤ r), C.faces k hk = D.faces k hk

@[simp]

theorem TauCeti.HypergraphComplex.faces_zero {r : ℕ} {V : Type u_1} (C : HypergraphComplex r V) : C.faces 0 ⋯ = {∅}

The empty face is the unique face in level zero.

def TauCeti.HypergraphComplex.toPreAbstractSimplicialComplex {r : ℕ} {V : Type u_1} (C : HypergraphComplex r V) : PreAbstractSimplicialComplex V

Forget the empty face and finite grading of a hypergraph complex.

The resulting Mathlib complex consists of exactly the nonempty faces of the graded complex.

@[simp]

theorem TauCeti.HypergraphComplex.mem_toPreAbstractSimplicialComplex {r : ℕ} {V : Type u_1} (C : HypergraphComplex r V) (s : Finset V) : s ∈ C.toPreAbstractSimplicialComplex ↔ s.Nonempty ∧ ∃ (h : s.card ≤ r), s ∈ C.faces s.card h

The underlying pre-abstract simplicial complex contains exactly the nonempty graded faces.

theorem TauCeti.HypergraphComplex.card_le_of_mem_toPreAbstractSimplicialComplex {r : ℕ} {V : Type u_1} (C : HypergraphComplex r V) {s : Finset V} (hs : s ∈ C.toPreAbstractSimplicialComplex) : s.card ≤ r

Every face of the underlying pre-abstract simplicial complex has cardinality at most the rank.

theorem TauCeti.HypergraphComplex.finite_faces_toPreAbstractSimplicialComplex {r : ℕ} {V : Type u_1} (C : HypergraphComplex r V) : C.toPreAbstractSimplicialComplex.faces.Finite

Forgetting the empty face leaves finitely many faces, even on an infinite ambient type.

noncomputable def TauCeti.HypergraphComplex.ofPreAbstractSimplicialComplex {r : ℕ} {V : Type u_1} (K : PreAbstractSimplicialComplex V) (hfinite : K.faces.Finite) : HypergraphComplex r V

Keep the faces of cardinality at most r of a finite precomplex and adjoin the empty face. On a finite ambient type, the finiteness proof can be supplied by Set.toFinite _. With an expected HypergraphComplex r V type, use .ofPreAbstractSimplicialComplex K hfinite.

@[simp]

theorem TauCeti.HypergraphComplex.mem_faces_ofPreAbstractSimplicialComplex {r : ℕ} {V : Type u_1} (K : PreAbstractSimplicialComplex V) (hfinite : K.faces.Finite) (k : ℕ) (hk : k ≤ r) {s : Finset V} : s ∈ (ofPreAbstractSimplicialComplex K hfinite).faces k hk ↔ (s = ∅ ∨ s ∈ K) ∧ s.card = k

The finite conversion adds exactly the empty face and groups faces by cardinality.

@[simp]

theorem TauCeti.HypergraphComplex.toPreAbstractSimplicialComplex_ofPreAbstractSimplicialComplex {r : ℕ} {V : Type u_1} (K : PreAbstractSimplicialComplex V) (hfinite : K.faces.Finite) (hcard : ∀ s ∈ K, s.card ≤ r) : (ofPreAbstractSimplicialComplex K hfinite).toPreAbstractSimplicialComplex = K

Adjoining and then forgetting the empty face recovers the original finite precomplex.

@[simp]

theorem TauCeti.HypergraphComplex.ofPreAbstractSimplicialComplex_toPreAbstractSimplicialComplex {r : ℕ} {V : Type u_1} (C : HypergraphComplex r V) : ofPreAbstractSimplicialComplex C.toPreAbstractSimplicialComplex ⋯ = C

Forgetting and then adjoining the empty face recovers the finite graded complex, including rank zero.