Orbit algebras of permutation groups
DefinitionProduct of the reduced incidence algebra#✓fully proved
Let \(\Omega\) be a set. For functions \(f\) and \(g\) from the finite subsets of \(\Omega\) to \(\mathbb{Q}\), their product \(fg\) is the function on finite subsets given by \((fg)(X) = \sum_{Y \subseteq X} f(Y)\, g(X \setminus Y)\).
If \(f\) vanishes off the \(n\)-element subsets and \(g\) vanishes off the \(m\)-element subsets, this is the product of Kourovka Problem 13.29, and \(fg\) vanishes off the \((n+m)\)-element subsets.
DefinitionElements of the reduced incidence algebra#✓fully proved
Let \(\Omega\) be a set. A function \(f\) from the finite subsets of \(\Omega\) to \(\mathbb{Q}\) lies in the algebra \(A = \bigoplus_n V_n\), where \(V_n\) consists of the functions vanishing off the \(n\)-element subsets, when there is a natural number \(N\) such that \(f(X) = 0\) for every finite subset \(X\) of \(\Omega\) with more than \(N\) elements.
DefinitionInvariant functions on finite subsets#✓fully proved
Let \(G\) be a group of permutations of a set \(\Omega\). A function \(f\) from the finite subsets of \(\Omega\) to \(\mathbb{Q}\) is \(G\)-invariant when \(f(\sigma(X)) = f(X)\) for every \(\sigma \in G\) and every finite subset \(X\) of \(\Omega\), where \(\sigma(X)\) is the image of \(X\) under \(\sigma\).
def IsInvariant (G : Subgroup (Equiv.Perm Ω)) (f : Finset Ω → ℚ) : Prop :=
∀ σ ∈ G, ∀ X : Finset Ω, f (X.map σ.toEmbedding) = f X
DefinitionCameron's conjecture on invariant incidence algebras (Kourovka 13.29)#✓fully proved
The statement that for every infinite set \(\Omega\) and every group \(G\) of permutations of \(\Omega\) all of whose orbits are infinite, the following holds: if \(f\) and \(g\) are nonzero functions from the finite subsets of \(\Omega\) to \(\mathbb{Q}\) that are \(G\)-invariant (\(f(\sigma(X)) = f(X)\) for all \(\sigma \in G\) and all finite \(X\), and likewise for \(g\)) and that each vanish on all subsets of size larger than some bound, then their product \(fg\) in the reduced incidence algebra, given by \((fg)(X) = \sum_{Y \subseteq X} f(Y)\, g(X \setminus Y)\), is not identically zero. In other words, the algebra \(A^G\) of \(G\)-invariant elements of the reduced incidence algebra \(A\) has no zero divisors.
def invariantIncidenceAlgebraIsDomain : Prop :=
∀ (Ω : Type) [DecidableEq Ω] [Infinite Ω] (G : Subgroup (Equiv.Perm Ω)),
(∀ x : Ω, (MulAction.orbit G x).Infinite) →
∀ f g : Finset Ω → ℚ, IsInA f → IsInvariant G f → IsInA g → IsInvariant G g →
f ≠ 0 → g ≠ 0 → incMul f g ≠ 0
def IsInA (f : Finset Ω → ℚ) : Prop :=
∃ N : ℕ, ∀ X : Finset Ω, N < X.card → f X = 0
WantedExt/GroupTheory/ReducedIncidenceAlgebraDomainKourovka13Problem29Wanted.lean:54
def IsInvariant (G : Subgroup (Equiv.Perm Ω)) (f : Finset Ω → ℚ) : Prop :=
∀ σ ∈ G, ∀ X : Finset Ω, f (X.map σ.toEmbedding) = f X
WantedExt/GroupTheory/ReducedIncidenceAlgebraDomainKourovka13Problem29Wanted.lean:58
def incMul (f g : Finset Ω → ℚ) : Finset Ω → ℚ :=
fun X => ∑ Y ∈ X.powerset, f Y * g (X \ Y)
WantedExt/GroupTheory/ReducedIncidenceAlgebraDomainKourovka13Problem29Wanted.lean:50
Uses 3 · Used by 1
TheoremCameron's conjecture on invariant incidence algebras holds (Pouzet)#●ready to prove
Let \(\Omega\) be an infinite set and let \(G\) be a group of permutations of \(\Omega\) all of whose orbits are infinite. Let \(f\) and \(g\) be nonzero functions from the finite subsets of \(\Omega\) to \(\mathbb{Q}\) that are \(G\)-invariant (\(f(\sigma(X)) = f(X)\) for all \(\sigma \in G\) and all finite \(X\), and likewise for \(g\)) and that each vanish on all subsets of size larger than some bound. Then their product in the reduced incidence algebra, \((fg)(X) = \sum_{Y \subseteq X} f(Y)\, g(X \setminus Y)\), is not identically zero. In other words, the algebra \(A^G\) of \(G\)-invariant elements of the reduced incidence algebra \(A\) has no zero divisors.
public theorem_wanted invariantIncidenceAlgebraIsDomain_holds : invariantIncidenceAlgebraIsDomain
def invariantIncidenceAlgebraIsDomain : Prop :=
∀ (Ω : Type) [DecidableEq Ω] [Infinite Ω] (G : Subgroup (Equiv.Perm Ω)),
(∀ x : Ω, (MulAction.orbit G x).Infinite) →
∀ f g : Finset Ω → ℚ, IsInA f → IsInvariant G f → IsInA g → IsInvariant G g →
f ≠ 0 → g ≠ 0 → incMul f g ≠ 0
WantedExt/GroupTheory/ReducedIncidenceAlgebraDomainKourovka13Problem29Wanted.lean:64
Sources
- E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 13.29 (P. J. Cameron); resolution: M. Pouzet, Theor. Inform. Appl. 42 (2008), no. 1, 83-103, Kourovka Archive, Problem 13.29: the conjecture is proved.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.