Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A nonfactorizable doubled triangle

Abstract

A doubled triangle with simultaneous exchange of edge copies has no local factorization.

Vertices are indexed by Fin (n + 1). A and B denote the specified actions on vertices and multifacets, respectively. Membership proofs in subtype constructors are implicit; these proofs do not affect values.

Definition 1.1 (Weighted simplicial complexes).

Formalization. D5/S3/Quantum/TensorNetworks/NonFactorizableDoubledTriangle.WeightedSimplicialComplex (✓ std3).

Citation. Gemma De las Cuevas; Andreas Klingler; Tim Netzer (2024). Polynomial decompositions with invariance and positivity inspired by tensors. DOI: 10.1016/j.laa.2024.05.025. URL: https://arxiv.org/abs/2109.06680v2.

Commentary.

A natural weight is assigned to every vertex subset. Weights divide the weights of larger subsets, and every singleton has nonzero weight. These are the divisibility condition and standing singleton assumption of Definition def:wsc, TeX lines 318–327.

Definition 1.2 (Distinct copies of each facet).

Formalization. D5/S3/Quantum/TensorNetworks/NonFactorizableDoubledTriangle.Multifacet (✓ std3).

Citation. Gemma De las Cuevas; Andreas Klingler; Tim Netzer (2024). Polynomial decompositions with invariance and positivity inspired by tensors. DOI: 10.1016/j.laa.2024.05.025. URL: https://arxiv.org/abs/2109.06680v2.

Commentary.

A facet is a vertex subset maximal among those of nonzero weight. A multifacet consists of a facet F and an index in Fin (ω F), giving exactly ω F distinct copies. This is the multifacet multiset of Definition def:wsc, TeX lines 327–332, expressed as a dependent sum.

Definition 1.3 (Forgetting the copy index).

Formalization. D5/S3/Quantum/TensorNetworks/NonFactorizableDoubledTriangle.collapse (✓ std3).

Citation. Gemma De las Cuevas; Andreas Klingler; Tim Netzer (2024). Polynomial decompositions with invariance and positivity inspired by tensors. DOI: 10.1016/j.laa.2024.05.025. URL: https://arxiv.org/abs/2109.06680v2.

Commentary.

Collapse sends a multifacet to its underlying vertex subset by projecting its facet and then its subset. It is the canonical collapse map of TeX line 332.

Definition 1.4 (Multifacets incident to a vertex).

Formalization. D5/S3/Quantum/TensorNetworks/NonFactorizableDoubledTriangle.Incident (✓ std3).

Citation. Gemma De las Cuevas; Andreas Klingler; Tim Netzer (2024). Polynomial decompositions with invariance and positivity inspired by tensors. DOI: 10.1016/j.laa.2024.05.025. URL: https://arxiv.org/abs/2109.06680v2.

Commentary.

The local multifacets at i are exactly the multifacets whose underlying facet contains i. This retains each copy separately, as in TeX lines 330–332.

Definition 1.5 (Compatible vertex and multifacet actions).

Formalization. D5/S3/Quantum/TensorNetworks/NonFactorizableDoubledTriangle.Compatible (✓ std3).

Citation. Gemma De las Cuevas; Andreas Klingler; Tim Netzer (2024). Polynomial decompositions with invariance and positivity inspired by tensors. DOI: 10.1016/j.laa.2024.05.025. URL: https://arxiv.org/abs/2109.06680v2.

Commentary.

The vertex action preserves every weight, and collapse intertwines the multifacet action with the induced action on vertex subsets. These are precisely the two requirements in the definition of an action on a weighted simplicial complex, TeX lines 425–435. No finiteness assumption on G is needed here.

Definition 1.6 (Inverse pullback of local labels).

Formalization. D5/S3/Quantum/TensorNetworks/NonFactorizableDoubledTriangle.transport (✓ std3).

Citation. Gemma De las Cuevas; Andreas Klingler; Tim Netzer (2024). Polynomial decompositions with invariance and positivity inspired by tensors. DOI: 10.1016/j.laa.2024.05.025. URL: https://arxiv.org/abs/2109.06680v2.

Commentary.

A local labeling β at i is transported to the labeling at g i that evaluates β on the inverse translate of each multifacet. Collapse compatibility ensures that this inverse translate is incident to i. This is the inverse pullback action on functions and translated subsets of TeX lines 405–413.

Definition 1.7 (The stabilizer count).

Formalization. D5/S3/Quantum/TensorNetworks/NonFactorizableDoubledTriangle.K (✓ std3).

Citation. Gemma De las Cuevas; Andreas Klingler; Tim Netzer (2024). Polynomial decompositions with invariance and positivity inspired by tensors. DOI: 10.1016/j.laa.2024.05.025. URL: https://arxiv.org/abs/2109.06680v2.

Commentary.

For a labeling α, count all global labelings γ whose restriction at each vertex can be changed into the restriction of α by an element fixing that vertex. The group element may be chosen independently at every vertex. This is K in TeX lines 1519–1521. The definition uses Nat.card for an arbitrary label type ι; the factorization equations below use finite label types.

Definition 1.8 (Positive equivariant local factorization).

Formalization. D5/S3/Quantum/TensorNetworks/NonFactorizableDoubledTriangle.Factorizable (✓ std3).

Citation. Gemma De las Cuevas; Andreas Klingler; Tim Netzer (2024). Polynomial decompositions with invariance and positivity inspired by tensors. DOI: 10.1016/j.laa.2024.05.025. URL: https://arxiv.org/abs/2109.06680v2.

Commentary.

For every natural m, choose a real factor C i β for each vertex and each local labeling by Fin m. Every factor must be positive, transported local labelings must have the same factor, and the product over vertices must equal the reciprocal of K for every global labeling. K is cast from ℕ to ℝ before inversion. Fin m represents every finite label set, including the empty one. The group is finite. These are the equations and inequalities of TeX lines 1515–1522.

Definition 1.9 (Universal factorizability).

Formalization. D5/S3/Quantum/TensorNetworks/NonFactorizableDoubledTriangle.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. Gemma De las Cuevas; Andreas Klingler; Tim Netzer (2024). Polynomial decompositions with invariance and positivity inspired by tensors. DOI: 10.1016/j.laa.2024.05.025. URL: https://arxiv.org/abs/2109.06680v2.

Commentary.

Every weighted simplicial complex on Fin (n + 1), with every finite group and every compatible pair of actions, is asserted to be factorizable. Its negation supplies a nonfactorizable structure and hence answers the existence question at TeX lines 1544–1549 affirmatively.

Theorem 1.10 (The doubled triangle is not factorizable).

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/NonFactorizableDoubledTriangle.result (✓ std3). ∎

Resolves. Problems/delascuevas-klingler-netzer-2024-nonfactorizable-doubled-triangle (refuted) by D5/S3/Quantum/TensorNetworks/NonFactorizableDoubledTriangle.result.

Source. Repository-derived.

Acknowledgement. Gemma De las Cuevas; Andreas Klingler; Tim Netzer (2024). Polynomial decompositions with invariance and positivity inspired by tensors. DOI: 10.1016/j.laa.2024.05.025. URL: https://arxiv.org/abs/2109.06680v2.

Commentary.

On the vertices 0, 1, 2, give the empty set and singletons weight 1, the three edges weight 2, and the full vertex set weight 0. These weights satisfy divisibility and the singleton condition. The facets are exactly the complements of the single vertices. Index their copies by pairs (e,k) in Fin 3 × Fin 2, where the underlying edge omits e. This indexing is bijective, and a copy is incident to i exactly when i differs from e.

Use MulAction.ofEndHom with the constant identity endomorphism homomorphism to let Multiplicative (ZMod 2) fix every vertex. Its identity fixes every copy, and its other element reverses the Fin 2 index on each edge simultaneously. Reversal is an involution, so these maps define a group action. They preserve each underlying edge, while the vertex action preserves every weight; the two actions are therefore compatible.

For a,b,c in Fin 2, define αₐᵦ𝒸 by labeling copy 0 of every edge with 0 and copy 1 of the edges omitting 0, 1, 2 with a, b, c, respectively. In these coordinates, equality of the local pullbacks means that, at each vertex i, γ agrees with αₐᵦ𝒸 on all copies of edges not omitting i, either directly or after reversing both copy indices. These are the only two possibilities because the group has two elements, each equal to its inverse. The bijection of copies transfers K to the cardinality of this set of binary functions. Enumerating the eight choices of a,b,c and the binary functions gives K(α₀₀₀) = 1 and K(αₐᵦ𝒸) = 2 for all other choices.

For any real local factors C, let Pₐᵦ𝒸 be their product over the three vertices at the restrictions of αₐᵦ𝒸. The restriction at vertex 0 is independent of a, the restriction at vertex 1 is independent of b, and the restriction at vertex 2 is independent of c: each vertex sees only the two edges that contain it. Consequently P₀₀₀ P₀₁₁ P₁₀₁ P₁₁₀ = P₀₀₁ P₀₁₀ P₁₀₀ P₁₁₁. For each vertex, the factors on either side contain each possible pair of the other two binary coordinates exactly once; expanding the products and commuting real factors proves the identity.

If the structure were factorizable, take m = 2 in its defining equations. They give P₀₀₀ = 1 and Pₐᵦ𝒸 = 1/2 for all other choices. Substitution into the parity identity yields 1/8 = 1/16, a contradiction. Thus even the product equations have no solution; positivity and equivariance cannot restore one. Finally, applying universal factorizability to n = 2, these weights, this finite group and these compatible actions would give the impossible factorization. Hence claim is false.

References