Lemma 4.6 (a): property (P) from quotients separating finite sets
ProvedChou.hasPackingProperty_of_forall_finite_exists_quotientSuppose that for every finite subset of there is a normal subgroup such that has property (P) and distinct elements of have distinct images in . Then has property (P).
import Definitions.Def_Chou_ElementaryAmenable import Definitions.Def_Chou_Classes import Mathlib
namespace Chou
/-- Lemma 4.6 (a): if for each finite `F ⊆ G` there is a normal subgroup `K` such that `G ⧸ K`
has property (P) and `F` maps injectively into `G ⧸ K`, then `G` has property (P). -/
theorem hasPackingProperty_of_forall_finite_exists_quotient {G : Type*} [Group G]
(h : ∀ F : Set G, F.Finite → ∃ (K : Subgroup G) (_ : K.Normal),
HasPackingProperty (G ⧸ K) ∧ Set.InjOn (QuotientGroup.mk : G → G ⧸ K) F) :
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 descends from quotients that separate finite sets
Setting
Let be a group. Nothing else is assumed about : it may be finite or infinite, abelian or not, trivial or not. (The group is allowed to live in any set-theoretic universe; this has no mathematical content.)
All of the notions below are defined in the accompanying definition files rather than being standard library notions, so each is spelled out in full.
The notions used
Packings. For two subsets , say that is a packing of when the multiplication map
is a bijection from the Cartesian product onto all of . Unfolded, this is the conjunction of three conditions:
- (maps into ) for every , the product lies in — automatically true;
- (injective on ) whenever and satisfy , one has , i.e. and ;
- (onto ) every can be written as for some and some .
Equivalently: every element of has exactly one factorization with and . The order matters: the element of is the left factor and the element of is the right factor. Neither nor is required by the definition to be finite, nonempty, a subgroup, or anything else; the definition is purely the bijectivity of the multiplication map. (Since contains its identity element, condition 3 forces both and to be nonempty whenever a packing exists.)
The packing property. Say that has the packing property when: for every finite subset there exist subsets such that
Here "finite" means finite in the usual sense (in bijection with for some natural number , with allowed). Only is required to be finite; may be infinite. The subset is included in the quantifier, so having the packing property entails in particular that some finite and some form a packing of .
Normal subgroups. A subgroup is normal when for every and every , the conjugate lies in .
Quotient groups and the canonical map. For a subgroup , the quotient is the set of left cosets , i.e. the set of equivalence classes of under the relation . When is normal (as it is throughout the statement below), carries the usual quotient group structure, , and it is this group structure with respect to which " has the packing property" is asserted. The canonical map is
and holds exactly when .
Injective on a subset. A map is injective on a subset of its domain when for all , implies . Nothing is said about points outside . For the canonical map this reads: for all , if then ; equivalently, no two distinct elements of lie in the same coset of .
The statement
Hypothesis. For every finite subset there exists a normal subgroup (allowed to depend on ) such that both of the following hold:
- the quotient group has the packing property, i.e. for every finite subset there are subsets with , finite, and a packing of ; and
- the canonical map is injective on : for all , implies .
Conclusion. has the packing property: for every finite subset there exist with , finite, and every element of uniquely of the form with , .
The statement is an implication (hypothesis conclusion), not an equivalence.
Edge cases and fine print
- Dependence of on . The hypothesis is "for each finite there is some normal "; a single working for all at once is not required, and nothing relates the subgroups chosen for different .
- . The empty set is a finite subset, so the hypothesis includes: there is some normal subgroup with having the packing property (the injectivity condition is vacuous for ).
- Singletons. For the injectivity condition is again automatic, so the hypothesis for singletons also only asks for a normal with having the packing property.
- Extreme choices of . The trivial subgroup is normal, is injective on every subset, and is a group isomorphic to . The whole group is normal with the one-element group, and is injective on exactly when has at most one element. Both choices fall within the quantifier "there exists a normal subgroup ".
- The packing property of the quotient is quantified over subsets of , not over subsets of : the sets in the first bullet of the hypothesis are sets of cosets.
- Finiteness. In both the hypothesis and the conclusion, finiteness is demanded only of (given) and (to be found); is unconstrained.
- No uniqueness or bound. The conclusion asserts existence of some and ; it does not say or is unique, does not bound the size of in terms of , and does not relate the , found for to any packing of a quotient.
Confirmed by the mission captain (proposal self-audit).