Injectivity lemmas for indexed free products

This file supplies two reusable criteria for injectivity of maps out of an indexed free product. The first says that the free product of a family of injective component maps is injective. The second reduces injectivity of a lift to nontriviality on every nonempty normal-form word.

def Monoid.CoprodI.letterMap {ι : Type u_1} {M : ι → Type u_2} {N : ι → Type u_3} [(i : ι) → Group (M i)] [(i : ι) → Group (N i)] (f : (i : ι) → M i →* N i) : (i : ι) × M i → (i : ι) × N i

Apply the factor homomorphism to a letter while retaining its factor label.

Equations

• Monoid.CoprodI.letterMap f ⟨i, x_1⟩ = ⟨i, (f i) x_1⟩

def Monoid.CoprodI.wordMap {ι : Type u_1} {M : ι → Type u_2} {N : ι → Type u_3} [(i : ι) → Group (M i)] [(i : ι) → Group (N i)] (f : (i : ι) → M i →* N i) (hf : ∀ (i : ι), Function.Injective ⇑(f i)) (w : Word M) : Word N

Map an indexed free-product normal word through injective component homomorphisms.

Equations

• Monoid.CoprodI.wordMap f hf w = { toList := List.map (Monoid.CoprodI.letterMap f) w.toList, ne_one := ⋯, chain_ne := ⋯ }

def Monoid.CoprodI.familyMap {ι : Type u_1} {M : ι → Type u_2} {N : ι → Type u_3} [(i : ι) → Group (M i)] [(i : ι) → Group (N i)] (f : (i : ι) → M i →* N i) : CoprodI M →* CoprodI N

The homomorphism between indexed free products induced componentwise by a family of homomorphisms.

Equations

• Monoid.CoprodI.familyMap f = Monoid.CoprodI.lift fun (i : ι) => Monoid.CoprodI.of.comp (f i)

theorem Monoid.CoprodI.familyMap_injective {ι : Type u_1} {M : ι → Type u_2} {N : ι → Type u_3} [(i : ι) → Group (M i)] [(i : ι) → Group (N i)] (f : (i : ι) → M i →* N i) (hf : ∀ (i : ι), Function.Injective ⇑(f i)) : Function.Injective ⇑(familyMap f)

Applying injective maps independently to the factors of an indexed free product gives an injective homomorphism of indexed free products.

theorem Monoid.CoprodI.lift_injective_of_neWord_nontrivial {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {Q : Type u_6} [Group Q] (f : (i : I) → H i →* Q) (hne : ∀ (i j : I) (u : NeWord H i j), (lift f) u.prod ≠ 1) : Function.Injective ⇑(lift f)

A lift from an indexed free product is injective if every nonempty normal-form word has nontrivial image.

def Monoid.CoprodI.NeWord.singletonZ {I : Type u_4} (i : I) (k : ℤ) (hk : k ≠ 0) : NeWord (fun (x : I) => Multiplicative ℤ) i i

A one-letter reduced word in an infinite cyclic factor, specified by a nonzero additive exponent.

Equations

• Monoid.CoprodI.NeWord.singletonZ i k hk = Monoid.CoprodI.NeWord.singleton (Multiplicative.ofAdd k) ⋯

def Monoid.CoprodI.NeWord.merge {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i j l : I} (u : NeWord H i j) (v : NeWord H j l) (h : u.last * v.head ≠ 1) : NeWord H i l

Concatenate two reduced nonempty words whose boundary letters lie in the same factor but have nontrivial product.

Equations

• (Monoid.CoprodI.NeWord.singleton x hx).merge v_2 h_2 = v_2.mulHead x ⋯
• (front.append hne tail).merge v h = front.append hne (tail.merge v ⋯)

@[simp]

theorem Monoid.CoprodI.NeWord.merge_prod {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i j l : I} (u : NeWord H i j) (v : NeWord H j l) (h : u.last * v.head ≠ 1) : (u.merge v h).prod = u.prod * v.prod

def Monoid.CoprodI.NeWord.IsAppend {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i j : I} : NeWord H i j → Prop

Whether a nonempty reduced word has at least two blocks.

Equations

• (Monoid.CoprodI.NeWord.singleton x_1 a).IsAppend = False
• (_w₁.append _hne _w₂).IsAppend = True

theorem Monoid.CoprodI.NeWord.cast_start_head {I : Type u_4} {G : Type u_6} [Group G] {i i' j : I} (h : i = i') (w : NeWord (fun (x : I) => G) i j) : (h ▸ w).head = w.head

theorem Monoid.CoprodI.NeWord.cast_start_last {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i i' j : I} (h : i = i') (w : NeWord H i j) : (h ▸ w).last = w.last

theorem Monoid.CoprodI.NeWord.cast_start_prod {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i i' j : I} (h : i = i') (w : NeWord H i j) : (h ▸ w).prod = w.prod

theorem Monoid.CoprodI.NeWord.cast_start_isAppend {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i i' j : I} (h : i = i') (w : NeWord H i j) : (h ▸ w).IsAppend ↔ w.IsAppend

theorem Monoid.CoprodI.NeWord.merge_head_of_isAppend_left {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i j k : I} (u : NeWord H i j) (v : NeWord H j k) (h : u.last * v.head ≠ 1) (hu : u.IsAppend) : (u.merge v h).head = u.head

theorem Monoid.CoprodI.NeWord.merge_last_of_isAppend_right {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i j k : I} (u : NeWord H i j) (v : NeWord H j k) (h : u.last * v.head ≠ 1) (hv : v.IsAppend) : (u.merge v h).last = v.last

theorem Monoid.CoprodI.NeWord.merge_isAppend_of_left {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i j k : I} (u : NeWord H i j) (v : NeWord H j k) (h : u.last * v.head ≠ 1) (hu : u.IsAppend) : (u.merge v h).IsAppend

theorem Monoid.CoprodI.NeWord.merge_isAppend_of_right {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i j k : I} (u : NeWord H i j) (v : NeWord H j k) (h : u.last * v.head ≠ 1) (hv : v.IsAppend) : (u.merge v h).IsAppend

theorem Monoid.CoprodI.NeWord.merge_head_singleton {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i j : I} (x : H i) (hx : x ≠ 1) (v : NeWord H i j) (h : x * v.head ≠ 1) : ((singleton x hx).merge v h).head = x * v.head

theorem Monoid.CoprodI.NeWord.merge_last_singleton {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i j : I} (u : NeWord H i j) (y : H j) (hy : y ≠ 1) (h : u.last * y ≠ 1) : (u.merge (singleton y hy) h).last = u.last * y

theorem Monoid.CoprodI.NeWord.prod_ne_one {I : Type u_4} {H : I → Type u_5} [(i : I) → Group (H i)] {i j : I} (w : NeWord H i j) : w.prod ≠ 1

The product of a nonempty reduced word in an indexed free product is nontrivial.

def Monoid.CoprodI.intOfFree (I : Type u_4) : FreeGroup I →* CoprodI fun (x : I) => Multiplicative ℤ

The map from a free group to the indexed free product of infinite cyclic groups that sends each free generator to the generator of its factor.

Equations

• Monoid.CoprodI.intOfFree I = FreeGroup.lift fun (i : I) => Monoid.CoprodI.of (Multiplicative.ofAdd 1)

def Monoid.CoprodI.intToFree (I : Type u_4) : (CoprodI fun (x : I) => Multiplicative ℤ) →* FreeGroup I

The inverse-on-generators map associated to intOfFree.

Equations

• Monoid.CoprodI.intToFree I = Monoid.CoprodI.lift fun (i : I) => (zpowersHom (FreeGroup I)) (FreeGroup.of i)

theorem Monoid.CoprodI.intOfFree_injective (I : Type u_4) : Function.Injective ⇑(intOfFree I)

theorem Monoid.CoprodI.of_int_eq_zpow {I : Type u_4} (i : I) (k : ℤ) : of (Multiplicative.ofAdd k) = of (Multiplicative.ofAdd 1) ^ k

theorem FreeGroup.unitGenerator_zpow_ne_one (k : ℤ) (hk : k ≠ 0) : of () ^ k ≠ 1

A nonzero power of the canonical generator of the rank-one free group is nontrivial.