English
Under ping-pong hypotheses for the generators of the free group, the lift from FreeGroup to G is injective.
Русский
При условиях Пинг-Понг для образующих свободной группы отображение из FreeGroup в G инъективно.
LaTeX
$$$\text{Injective}(\mathrm{FreeGroup.lift}\ a)$ under the ping-pong hypotheses$$
Lean4
/-- The Ping-Pong-Lemma.
Given a group action of `G` on `X` so that the generators of the free groups act in specific
ways on disjoint subsets `X i` and `Y i` we can prove that `lift f` is injective, and thus the image
of `lift f` is isomorphic to the free group.
Often the Ping-Pong-Lemma is stated with regard to group elements that generate the whole group;
we generalize to arbitrary group homomorphisms from the free group to `G` and do not require the
group to be generated by the elements.
-/
theorem _root_.FreeGroup.injective_lift_of_ping_pong : Function.Injective (FreeGroup.lift a) := by
-- Step one: express the free group lift via the free product lift
have :
FreeGroup.lift a =
(CoprodI.lift fun i => FreeGroup.lift fun _ => a i).comp (@freeGroupEquivCoprodI ι).toMonoidHom :=
by
ext i
simp
rw [this, MonoidHom.coe_comp]
clear this
refine
Function.Injective.comp ?_
(MulEquiv.injective freeGroupEquivCoprodI)
-- Step two: Invoke the ping-pong lemma for free products
change
Function.Injective
(lift fun i : ι => FreeGroup.lift fun _ => a i)
-- Prepare to instantiate lift_injective_of_ping_pong
let H : ι → Type _ := fun _i => FreeGroup Unit
let f : ∀ i, H i →* G := fun i => FreeGroup.lift fun _ => a i
let X' : ι → Set α := fun i => X i ∪ Y i
apply lift_injective_of_ping_pong f _ X'
· show ∀ i, (X' i).Nonempty
exact fun i => Set.Nonempty.inl (hXnonempty i)
· show Pairwise (Disjoint on X')
intro i j hij
simp only [X']
apply Disjoint.union_left <;> apply Disjoint.union_right
· exact hXdisj hij
· exact hXYdisj i j
· exact (hXYdisj j i).symm
· exact hYdisj hij
· change Pairwise fun i j => ∀ h : H i, h ≠ 1 → f i h • X' j ⊆ X' i
rintro i j hij
refine FreeGroup.freeGroupUnitEquivInt.forall_congr_left.mpr ?_
intro n hne1
change FreeGroup.lift (fun _ => a i) (FreeGroup.of () ^ n) • X' j ⊆ X' i
simp only [map_zpow, FreeGroup.lift_apply_of]
change a i ^ n • X' j ⊆ X' i
have hnne0 : n ≠ 0 := by
rintro rfl
apply hne1
simp [H, FreeGroup.freeGroupUnitEquivInt]
clear hne1
simp only [X']
-- Positive and negative powers separately
rcases (lt_or_gt_of_ne hnne0).symm with hlt | hgt
· have h1n : 1 ≤ n := hlt
calc
a i ^ n • X' j ⊆ a i ^ n • (Y i)ᶜ :=
smul_set_mono ((hXYdisj j i).union_left <| hYdisj hij.symm).subset_compl_right
_ ⊆ X i := by
clear hnne0 hlt
induction n, h1n using Int.le_induction with
| base => rw [zpow_one]; exact hX i
| succ n _hle hi =>
calc
a i ^ (n + 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ := by rw [zpow_add, zpow_one]
_ = a i ^ n • a i • (Y i)ᶜ := (MulAction.mul_smul _ _ _)
_ ⊆ a i ^ n • X i := (smul_set_mono <| hX i)
_ ⊆ a i ^ n • (Y i)ᶜ := (smul_set_mono (hXYdisj i i).subset_compl_right)
_ ⊆ X i := hi
_ ⊆ X' i := Set.subset_union_left
· have h1n : n ≤ -1 := by
apply Int.le_of_lt_add_one
simpa using hgt
calc
a i ^ n • X' j ⊆ a i ^ n • (X i)ᶜ :=
smul_set_mono ((hXdisj hij.symm).union_left (hXYdisj i j).symm).subset_compl_right
_ ⊆ Y i := by
clear hnne0 hgt
induction n, h1n using Int.le_induction_down with
| base => rw [zpow_neg, zpow_one]; exact hY i
| pred n hle hi =>
calc
a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ := by rw [zpow_sub, zpow_one]
_ = a i ^ n • (a i)⁻¹ • (X i)ᶜ := (MulAction.mul_smul _ _ _)
_ ⊆ a i ^ n • Y i := (smul_set_mono <| hY i)
_ ⊆ a i ^ n • (X i)ᶜ := (smul_set_mono (hXYdisj i i).symm.subset_compl_right)
_ ⊆ Y i := hi
_ ⊆ X' i := Set.subset_union_right
show _ ∨ ∃ i, 3 ≤ #(H i)
inhabit ι
right
use Inhabited.default
simp only [H]
rw [FreeGroup.freeGroupUnitEquivInt.cardinal_eq, Cardinal.mk_denumerable]
apply le_of_lt
exact nat_lt_aleph0 3
