Lemma 4.1 (b): extensions preserve property (P)
ProvedChou.hasPackingProperty_of_extensionIf is a normal subgroup of such that and have property (P), then has property (P).
import Definitions.Def_Chou_ElementaryAmenable import Definitions.Def_Chou_Classes import Mathlib
namespace Chou
/-- Lemma 4.1 (b): an extension of a group with property (P) by a group with property (P) has
property (P). -/
theorem hasPackingProperty_of_extension {G : Type*} [Group G] (N : Subgroup G) [N.Normal]
(hN : HasPackingProperty N) (hQ : HasPackingProperty (G ⧸ N)) : HasPackingProperty G := by
sorry
end Chou
Read-back
What the Lean code literally says, in plain math · claude-fable-5-1
Read-back: the packing property passes to extensions
This is a rendering of what the declaration literally asserts. It is self-contained: every definition the statement depends on is spelled out below, and every hypothesis, including the ones the formal statement carries silently, is listed.
The setting
Throughout, is a group. No further structure is assumed on : it may be finite or infinite, countable or uncountable, abelian or not; nothing is assumed about its cardinality or its universe level.
is a normal subgroup of . Normality is taken in the usual sense: for every and every , the conjugate lies in . The two extreme cases and are both allowed by the statement.
Two further groups are built from this data, and the statement treats each as a group in its own right:
-
as a group. Its elements are the elements of , and its multiplication is the multiplication of restricted to (so for , the product of and in the group is the element of , which lies in ).
-
The quotient group . Its elements are the left cosets with ; two elements represent the same coset exactly when . Every element of is of the form for some . The multiplication is , which is well defined because is normal.
Definition: packing
Let be any group and let be two subsets (any subsets: no finiteness, no closure property, no requirement that they contain the identity). The pair is called a packing of when the multiplication map
is a bijection from the cartesian product onto the whole of . Unwinding the bijection, this says exactly two things:
- (Every element is reached.) For every there exist and with .
- (Reached only once.) If and satisfy , then and .
Together: every element of can be written as with and in exactly one way. The order of the factors matters: it is on the left and on the right, and nothing is said about products .
An equivalent way to say the same thing: the left translates , for ranging over , are pairwise disjoint and their union is all of . (Disjointness of the translates gives in condition 2, and then follows by cancellation.)
Edge cases that follow directly from the definition:
- Since contains its identity element, condition 1 forces both and to be nonempty. Neither the empty set nor a pair with an empty member is ever a packing.
- The pair , is a packing of every group .
- is not required to be finite, to be a subgroup, or to be related to in any way beyond conditions 1 and 2.
Definition: the packing property
A group has the packing property when the following holds:
For every finite subset there exist subsets such that
Points to note in this definition:
- "Finite" means: there is a natural number and a bijection between the set and . The empty set is finite.
- The finite set is required to be contained in (the left factor), not in .
- must be finite; is unconstrained apart from being a packing. In particular may be infinite, and when is infinite and is finite, is necessarily infinite.
- The case is included. For it, and always work, so that instance of the condition is satisfied in every group.
- The quantifier is , not "exists uniquely": there is no claim about how many such pairs exist.
When this definition is applied to the group (as a group in its own right), the sets , , are subsets of , products are computed in (equivalently, in ), and the packing must cover all of , not all of . When it is applied to , the sets are sets of cosets and products are coset products.
The statement
Let be a group and a normal subgroup of . Assume:
- (H1) the group has the packing property, and
- (H2) the quotient group has the packing property.
Then has the packing property. Written out in full, the conclusion is:
For every finite subset there exist subsets with , with finite, and such that every element of can be written as with , in exactly one way.
Complete list of what is quantified and assumed
- : an arbitrary group (universally quantified; the group structure is part of the data).
- : an arbitrary subgroup of (universally quantified).
- The hypothesis that is normal in .
- Hypothesis (H1): has the packing property.
- Hypothesis (H2): has the packing property.
There are no other hypotheses. Nothing is assumed about finiteness, countability, finite generation, commutativity, or torsion of , , or .
Degenerate instances covered by the statement
- . Then is the trivial group, which has the packing property (for any finite take ), and is isomorphic to via .
- . Then is the trivial group, which has the packing property, and hypothesis (H1) is the packing property for itself.
- finite. Then every subset is finite; for any one may take and , so every finite group has the packing property, and each of (H1), (H2), and the conclusion is satisfied.
The statement is an implication, not an equivalence: it does not assert that the packing property of implies anything about or .
Confirmed by the mission captain (proposal self-audit).