Indexed joins of abstract simplicial complexes

For a family of types A : ι → Type*, the indexed join is the abstract simplicial complex on Σ i, A i whose faces are the nonempty finite sets containing at most one vertex over each index. We give its face and barycentric-coordinate descriptions, its functoriality in the family, and the inclusions of the subjoins supported on finite sets of indices. Finally, adjoining a vertex over a fresh index makes a finite vertex restriction of the join a cone.

Main definitions

• TauCeti.indexedJoin: the join of a type-valued family.
• TauCeti.indexedJoinMap: maps induced by injective changes of indices and family maps.
• TauCeti.finiteSubjoin: the join restricted to a finite set of indices.
• TauCeti.subjoinInclusion: the simplicial inclusion of the join on a subset of indices.

Main results

• TauCeti.isCone_restrict_indexedJoin_insert: adjoining a vertex over a fresh index makes a finite vertex restriction of an indexed join a cone.

def TauCeti.indexedJoin {ι : Type u} (A : ι → Type v) : AbstractSimplicialComplex ((i : ι) × A i)

The indexed join of a family of types. Its vertices are pairs ⟨i, a⟩, and a nonempty finite set is a face exactly when it contains at most one vertex with each first coordinate.

@[simp]

theorem TauCeti.mem_indexedJoin_iff {ι : Type u} {A : ι → Type v} {σ : Finset ((i : ι) × A i)} : σ ∈ indexedJoin A ↔ σ.Nonempty ∧ Set.InjOn Sigma.fst ↑σ

A finite set is a face of the indexed join exactly when it is nonempty and its vertices have pairwise distinct indices.

theorem TauCeti.card_image_fst_eq_of_mem_indexedJoin {ι : Type u} {A : ι → Type v} {σ : Finset ((i : ι) × A i)} (hσ : σ ∈ indexedJoin A) : (Finset.image Sigma.fst σ).card = σ.card

The number of indices represented by a face of an indexed join is its number of vertices.

theorem TauCeti.eq_of_mem_indexedJoin {ι : Type u} {A : ι → Type v} {σ : Finset ((i : ι) × A i)} (hσ : σ ∈ indexedJoin A) {v w : (i : ι) × A i} (hv : v ∈ σ) (hw : w ∈ σ) (h : v.fst = w.fst) : v = w

Two vertices of a face of an indexed join with the same index are equal.

def TauCeti.indexedJoinMap {ι : Type u} {κ : Type u₁} {A : ι → Type v} {B : κ → Type w} (e : ι → κ) (he : Function.Injective e) (f : (i : ι) → A i → B (e i)) : (indexedJoin A).SimplicialMap (indexedJoin B).toPreAbstractSimplicialComplex

An injective map of indices and maps of the family members induce a simplicial map of indexed joins. The maps of the family members need not be injective.

@[simp]

theorem TauCeti.indexedJoinMap_apply {ι : Type u} {κ : Type u₁} {A : ι → Type v} {B : κ → Type w} (e : ι → κ) (he : Function.Injective e) (f : (i : ι) → A i → B (e i)) (v : (i : ι) × A i) : (indexedJoinMap e he f) v = ⟨e v.fst, f v.fst v.snd⟩

The vertex function underlying an indexed-join map.

@[simp]

theorem TauCeti.indexedJoinMap_id {ι : Type u} {A : ι → Type v} : (indexedJoinMap id ⋯ fun (x : ι) (x_1 : A x) => x_1) = PreAbstractSimplicialComplex.SimplicialMap.id (indexedJoin A).toPreAbstractSimplicialComplex

The identity on indices and family members induces the identity simplicial map.

@[simp]

theorem TauCeti.indexedJoinMap_comp {ι : Type u} {κ : Type u₁} {μ : Type u₂} {A : ι → Type v} {B : κ → Type w} {C : μ → Type z} (e : ι → κ) (he : Function.Injective e) (g : κ → μ) (hg : Function.Injective g) (h : (j : κ) → B j → C (g j)) (f : (i : ι) → A i → B (e i)) : (indexedJoinMap (g ∘ e) ⋯ fun (i : ι) (x : A i) => h (e i) (f i x)) = (indexedJoinMap g hg h).comp (indexedJoinMap e he f)

Indexed-join maps preserve composition of injective index maps and family maps.

theorem TauCeti.mem_indexedJoin_realization_iff {ι : Type u} {A : ι → Type v} {x : (i : ι) × A i →₀ ℝ} : x ∈ (indexedJoin A).standardGeometricComplex.space ↔ (∀ (v : (i : ι) × A i), 0 ≤ x v) ∧ (x.sum fun (x : (i : ι) × A i) (r : ℝ) => r) = 1 ∧ ∀ (v w : (i : ι) × A i), x v ≠ 0 → x w ≠ 0 → v.fst = w.fst → v = w

Barycentric-coordinate characterization of the realization of an indexed join. Besides the usual nonnegativity and sum-one conditions, the nonzero coordinates have distinct indices.

theorem TauCeti.realization_support_injOn_fst {ι : Type u} {A : ι → Type v} (x : (indexedJoin A).Realization) : Set.InjOn Sigma.fst ↑(↑x).support

The carrier of a point in an indexed join contains at most one vertex over each index.

theorem TauCeti.realization_apply_eq_zero_of_fst_eq {ι : Type u} {A : ι → Type v} {x : (indexedJoin A).Realization} {v w : (i : ι) × A i} (hvw : v.fst = w.fst) (hne : v ≠ w) : ↑x v = 0 ∨ ↑x w = 0

Two different vertices over the same index cannot both have nonzero barycentric coordinate in the realization of an indexed join.

@[reducible, inline]

abbrev TauCeti.finiteSubjoin {ι : Type u} (A : ι → Type v) (s : Finset ι) : AbstractSimplicialComplex ((i : ↥s) × A ↑i)

The subjoin of a family supported on a finite set of indices.

theorem TauCeti.mem_finiteSubjoin_iff {ι : Type u} {A : ι → Type v} {s : Finset ι} {σ : Finset ((i : ↥s) × A ↑i)} : σ ∈ finiteSubjoin A s ↔ σ.Nonempty ∧ Set.InjOn (fun (v : (i : ↥s) × A ↑i) => ↑v.fst) ↑σ

A face of a finite subjoin is a nonempty set of vertices with distinct underlying indices.

def TauCeti.subjoinInclusion {ι : Type u} (A : ι → Type v) (s : Set ι) : (indexedJoin fun (i : ↑s) => A ↑i).SimplicialMap (indexedJoin A).toPreAbstractSimplicialComplex

The simplicial inclusion of the subjoin on any subset of indices into the full join.

@[simp]

theorem TauCeti.subjoinInclusion_apply {ι : Type u} (A : ι → Type v) (s : Set ι) (v : (i : ↑s) × A ↑i) : (subjoinInclusion A s) v = ⟨↑v.fst, v.snd⟩

A subjoin inclusion preserves the labelled vertex.

theorem TauCeti.subjoinInclusion_injective {ι : Type u} (A : ι → Type v) (s : Set ι) : Function.Injective ⇑(subjoinInclusion A s)

The subjoin inclusion is injective on vertices.

noncomputable def TauCeti.finiteSubjoinRealizationInclusion {ι : Type u} (A : ι → Type v) (s : Finset ι) : C((finiteSubjoin A s).Realization, (indexedJoin A).Realization)

The continuous inclusion of the realization of a finite subjoin into the realization of the full indexed join.

@[simp]

theorem TauCeti.finiteSubjoinRealizationInclusion_val {ι : Type u} (A : ι → Type v) (s : Finset ι) (x : (finiteSubjoin A s).Realization) : ↑((finiteSubjoinRealizationInclusion A s) x) = Finsupp.mapDomain ⇑(subjoinInclusion A ↑s) ↑x

The realization inclusion pushes barycentric coordinates forward along the vertex inclusion.

theorem TauCeti.finiteSubjoinRealizationInclusion_injective {ι : Type u} (A : ι → Type v) (s : Finset ι) : Function.Injective ⇑(finiteSubjoinRealizationInclusion A s)

The realization map of a finite-subjoin inclusion is injective.

@[simp]

theorem TauCeti.finiteSubjoinRealizationInclusion_vertex {ι : Type u} (A : ι → Type v) (s : Finset ι) (v : (i : ↥s) × A ↑i) : (finiteSubjoinRealizationInclusion A s) ((finiteSubjoin A s).vertex v) = (indexedJoin A).vertex ⟨↑v.fst, v.snd⟩

The realization inclusion of a finite subjoin sends each vertex to the corresponding vertex of the full indexed join.

theorem TauCeti.isCone_restrict_indexedJoin_insert {ι : Type u} {A : ι → Type v} (V : Finset ((i : ι) × A i)) (i : ι) (a : A i) (hi : i ∉ Finset.image Sigma.fst V) : ((indexedJoin A).restrict (↑V ∪ {⟨i, a⟩})).IsCone ⟨⟨i, a⟩, ⋯⟩

Adjoining a vertex over an index absent from a finite vertex set makes the corresponding restriction of an indexed join a cone.