Proposition 4.2: every elementary amenable group has property (P)
ProvedChou.hasPackingProperty_of_elementaryAmenableEvery elementary amenable group has property (P).
import Definitions.Def_Chou_ElementaryAmenable import Definitions.Def_Chou_Classes import Mathlib
namespace Chou
/-- Proposition 4.2: every group in `EG` has property (P). -/
theorem hasPackingProperty_of_elementaryAmenable {G : Type*} [Group G] (hG : ElementaryAmenable G) :
HasPackingProperty G := by
sorry
end Chou
Read-back
What the Lean code literally says, in plain math · claude-fable-5-1
Read-back: every elementary amenable group has the packing property
The statement in one sentence
Let be a group. If is elementary amenable in the inductive sense spelled out in §1 below, then has the packing property spelled out in §2 below. The statement is an implication only, not an equivalence.
Setting and binders
- is an arbitrary type equipped with a group structure (multiplication , identity , inverses). is implicit; it is not required to be finite, countable, or anything else beyond being a group. Being a type, is nonempty (it contains ). The type lives in an arbitrary universe; this only matters in one place, noted in §1.
- The single hypothesis is that satisfies the predicate "elementary amenable" of §1.
- The conclusion is the predicate "has the packing property" of §2.
There are no other hypotheses: no decidability, no finiteness, no countability, no choice of generating set.
1. The hypothesis: is elementary amenable
"Elementary amenable" is defined as an inductive predicate on groups. That is, it is the smallest property of groups that is closed under the seven rules listed next; a group satisfies it exactly when there is a finite derivation tree that establishes it from these rules. Nothing else makes a group elementary amenable.
The rules are:
-
Finite groups. If is finite (there is a bijection between and for some natural number ), then .
-
Commutative groups. If carries a commutative group structure, then holds for with the group structure underlying that commutative structure.
-
Isomorphism. If and are groups, is a group isomorphism (a bijection with ), and , then .
-
Subgroups. If is any subgroup of and , then , where carries the group structure inherited from .
-
Quotients. If is a normal subgroup of (i.e. for all , ) and , then . Here is the set of left cosets — two elements give the same coset exactly when — with the usual quotient group structure.
-
Extensions. If is a normal subgroup of , and , then .
-
Directed unions. Let be an index set and a family of subgroups of such that
- the family is directed: for all there exists with and ;
- the subgroup generated by is all of (literally: the supremum of the family in the lattice of subgroups equals the whole group);
- for every .
Then .
Remarks on rule 7. When is nonempty, directedness makes already a subgroup, so the second condition then says exactly that every element of lies in some . When is empty, directedness holds vacuously, the supremum is the trivial subgroup , and the second condition holds only if is the trivial group; so the empty case adds nothing beyond rule 1. Nothing requires the to be nested, distinct, proper, or finite.
Universe fine print. In every rule, every group mentioned ( in rules 3 and 4, and in rules 5–6, the index set in rule 7) is required to live in the same universe (the same "size class" of sets) as . In particular the index set of a directed union is a set of the same size class as the group. For a mathematician working in ordinary set theory this is no restriction.
Degenerate instances of the hypothesis. The trivial group satisfies the hypothesis (by rule 1 or rule 2). Every finite group and every abelian group satisfies it outright. The hypothesis is not vacuous; but note that the theorem asserts nothing about groups that fail it.
2. The conclusion: has the packing property
has the packing property means:
Here " finite" and " finite" mean the subset is in bijection with for some natural number (so , the empty set, is included). means every element of is an element of .
is a packing of means, literally, that the multiplication map
restricted to the Cartesian product is a bijection from onto all of . Unfolded, this is the conjunction of three conditions:
- (maps into) for every , — automatically true;
- (injective on ) for all , if then , i.e. and ;
- (surjective onto ) for every there exist and with .
Equivalently: every element of can be written in exactly one way as with and . Equivalently again: the left translates are pairwise disjoint and their union is (and, symmetrically, the right translates are pairwise disjoint with union ). The order of the factors matters: the element of is on the left and the element of on the right.
What the conclusion does and does not require.
- is not required to be finite; only is. No bound on the size of is asserted, and nothing relates to beyond .
- Because is nonempty and must be onto , both and are forced to be nonempty. Since with finite, itself must be finite, which is the standing hypothesis on .
- The case is included: then the requirement is only that some finite and some form a packing.
- Nothing constrains in terms of ; nothing says or is a subgroup, a transversal, or unique; the quantifier is "there exist", not "there exists a unique".
- If happens to be finite, a packing forces ; if is infinite and is finite, must be infinite.
- For the trivial group , the conclusion holds with for every (necessarily empty or equal to ) .
3. Assembled statement
For every group : if can be built from finite groups and commutative groups by finitely many applications of isomorphism, passing to subgroups, passing to quotients by normal subgroups, extension by a normal subgroup with quotient already built, and directed unions of already-built subgroups (rules 1–7 of §1), then for every finite set of elements of there is a finite set of elements of and a set of elements of such that every element of is for exactly one pair .
Confirmed by the mission captain (proposal self-audit).