Pushouts of Monoids and Groups

This file defines wide pushouts of monoids and groups and proves some properties of the amalgamated product of groups (i.e. the special case where all the maps in the diagram are injective).

Main definitions

• Monoid.PushoutI: the pushout of a diagram of monoids indexed by a type ι

• Monoid.PushoutI.base: the map from the amalgamating monoid to the pushout

• Monoid.PushoutI.of: the map from each Monoid in the family to the pushout

• Monoid.PushoutI.lift: the universal property used to define homomorphisms out of the pushout.

• Monoid.PushoutI.NormalWord: a normal form for words in the pushout

• Monoid.PushoutI.of_injective: if all the maps in the diagram are injective in a pushout of groups then so is of

• Monoid.PushoutI.Reduced.eq_empty_of_mem_range: For any word w in the coproduct, if w is reduced (i.e none its letters are in the image of the base monoid), and nonempty, then w itself is not in the image of the base monoid.

References

• The normal form theorem follows these notes from Queen Mary University

Tags

amalgamated product, pushout, group

def Monoid.PushoutI.con {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] (φ : (i : ι) → H →* G i) : Con (Coprod (CoprodI G) H)

The relation we quotient by to form the pushout

def Monoid.PushoutI {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] (φ : (i : ι) → H →* G i) : Type (max (max u_1 u_2) u_3)

The indexed pushout of monoids, which is the pushout in the category of monoids, or the category of groups.

instance Monoid.PushoutI.mul {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} : Mul (PushoutI φ)

instance Monoid.PushoutI.one {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} : One (PushoutI φ)

instance Monoid.PushoutI.monoid {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} : Monoid (PushoutI φ)

def Monoid.PushoutI.of {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (i : ι) : G i →* PushoutI φ

The map from each indexing group into the pushout

def Monoid.PushoutI.base {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] (φ : (i : ι) → H →* G i) : H →* PushoutI φ

The map from the base monoid into the pushout

theorem Monoid.PushoutI.of_comp_eq_base {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (i : ι) : (of i).comp (φ i) = base φ

theorem Monoid.PushoutI.of_apply_eq_base {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] (φ : (i : ι) → H →* G i) (i : ι) (x : H) : (of i) ((φ i) x) = (base φ) x

def Monoid.PushoutI.lift {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (f : (i : ι) → G i →* K) (k : H →* K) (hf : ∀ (i : ι), (f i).comp (φ i) = k) : PushoutI φ →* K

Define a homomorphism out of the pushout of monoids be defining it on each object in the diagram

@[simp]

theorem Monoid.PushoutI.lift_of {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (f : (i : ι) → G i →* K) (k : H →* K) (hf : ∀ (i : ι), (f i).comp (φ i) = k) {i : ι} (g : G i) : (lift f k hf) ((of i) g) = (f i) g

@[simp]

theorem Monoid.PushoutI.lift_base {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (f : (i : ι) → G i →* K) (k : H →* K) (hf : ∀ (i : ι), (f i).comp (φ i) = k) (g : H) : (lift f k hf) ((base φ) g) = k g

theorem Monoid.PushoutI.hom_ext {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} {f g : PushoutI φ →* K} (h : ∀ (i : ι), f.comp (of i) = g.comp (of i)) (hbase : f.comp (base φ) = g.comp (base φ)) : f = g

theorem Monoid.PushoutI.hom_ext_iff {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} {f g : PushoutI φ →* K} : f = g ↔ (∀ (i : ι), f.comp (of i) = g.comp (of i)) ∧ f.comp (base φ) = g.comp (base φ)

theorem Monoid.PushoutI.hom_ext_nonempty {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} [hn : Nonempty ι] {f g : PushoutI φ →* K} (h : ∀ (i : ι), f.comp (of i) = g.comp (of i)) : f = g

theorem Monoid.PushoutI.hom_ext_nonempty_iff {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} [hn : Nonempty ι] {f g : PushoutI φ →* K} : f = g ↔ ∀ (i : ι), f.comp (of i) = g.comp (of i)

def Monoid.PushoutI.homEquiv {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} : (PushoutI φ →* K) ≃ { f : ((i : ι) → G i →* K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }

The equivalence that is part of the universal property of the pushout. A hom out of the pushout is just a morphism out of all groups in the pushout that satisfies a commutativity condition.

@[simp]

theorem Monoid.PushoutI.homEquiv_apply_coe {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (f : PushoutI φ →* K) : ↑(homEquiv f) = (fun (i : ι) => f.comp (of i), f.comp (base φ))

@[simp]

theorem Monoid.PushoutI.homEquiv_symm_apply {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (f : { f : ((i : ι) → G i →* K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }) : homEquiv.symm f = lift (↑f).1 (↑f).2 ⋯

def Monoid.PushoutI.ofCoprodI {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} : CoprodI G →* PushoutI φ

The map from the coproduct into the pushout

@[simp]

theorem Monoid.PushoutI.ofCoprodI_of {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (i : ι) (g : G i) : ofCoprodI (CoprodI.of g) = (of i) g

theorem Monoid.PushoutI.induction_on {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} {motive : PushoutI φ → Prop} (x : PushoutI φ) (of : ∀ (i : ι) (g : G i), motive ((of i) g)) (base : ∀ (h : H), motive ((base φ) h)) (mul : ∀ (x y : PushoutI φ), motive x → motive y → motive (x * y)) : motive x

instance Monoid.PushoutI.instGroup {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} : Group (PushoutI φ)

structure Monoid.PushoutI.NormalWord.Transversal {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] (φ : (i : ι) → H →* G i) : Type (max u_1 u_2)

The data we need to pick a normal form for words in the pushout. We need to pick a canonical element of each coset. We also need all the maps in the diagram to be injective

• injective (i : ι) : Function.Injective ⇑(φ i)

  All maps in the diagram are injective

• set (i : ι) : Set (G i)

  The underlying set, containing exactly one element of each coset of the base group

• one_mem (i : ι) : 1 ∈ self.set i

  The chosen element of the base group itself is the identity

• compl (i : ι) : Subgroup.IsComplement (↑(φ i).range) (self.set i)

  We have exactly one element of each coset of the base group

theorem Monoid.PushoutI.NormalWord.transversal_nonempty {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] (φ : (i : ι) → H →* G i) (hφ : ∀ (i : ι), Function.Injective ⇑(φ i)) : Nonempty (Transversal φ)

structure Monoid.PushoutI.NormalWord {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (d : NormalWord.Transversal φ) extends Monoid.CoprodI.Word G : Type (max (max u_1 u_2) u_3)

The normal form for words in the pushout. Every element of the pushout is the product of an element of the base group and a word made up of letters each of which is in the transversal.

• toList : List ((i : ι) × G i)
• ne_one (l : (i : ι) × G i) : l ∈ self.toList → l.snd ≠ 1
• chain_ne : List.Chain' (fun (l l' : (i : ι) × G i) => l.fst ≠ l'.fst) self.toList
• head : H

  Every NormalWord is the product of an element of the base group and a word made up of letters each of which is in the transversal. head is that element of the base group.

• normalized (i : ι) (g : G i) : ⟨i, g⟩ ∈ self.toList → g ∈ d.set i

  All letter in the word are in the transversal.

structure Monoid.PushoutI.NormalWord.Pair {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (d : Transversal φ) (i : ι) extends Monoid.CoprodI.Word.Pair G i : Type (max u_1 u_2)

A Pair d i is a word in the coproduct, Coprod G, the tail, and an element of the group G i, the head. The first letter of the tail must not be an element of G i. Note that the head may be 1 Every letter in the tail must be in the transversal given by d. Similar to Monoid.CoprodI.Pair except every letter must be in the transversal (not including the head letter).

• head : G i
• tail : Word G
• fstIdx_ne : self.tail.fstIdx ≠ some i
• normalized (i : ι) (g : G i) : ⟨i, g⟩ ∈ self.tail.toList → g ∈ d.set i

  All letters in the word are in the transversal.

def Monoid.PushoutI.NormalWord.empty {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} : NormalWord d

The empty normalized word, representing the identity element of the group.

@[simp]

theorem Monoid.PushoutI.NormalWord.empty_head {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} : empty.head = 1

@[simp]

theorem Monoid.PushoutI.NormalWord.empty_toList {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} : empty.toList = []

instance Monoid.PushoutI.NormalWord.instInhabited {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} : Inhabited (NormalWord d)

instance Monoid.PushoutI.NormalWord.instInhabitedPair {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} (i : ι) : Inhabited (Pair d i)

theorem Monoid.PushoutI.NormalWord.ext {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} {w₁ w₂ : NormalWord d} (hhead : w₁.head = w₂.head) (hlist : w₁.toList = w₂.toList) : w₁ = w₂

theorem Monoid.PushoutI.NormalWord.ext_iff {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} {w₁ w₂ : NormalWord d} : w₁ = w₂ ↔ w₁.head = w₂.head ∧ w₁.toList = w₂.toList

instance Monoid.PushoutI.NormalWord.baseAction {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} : MulAction H (NormalWord d)

theorem Monoid.PushoutI.NormalWord.base_smul_def' {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} (h : H) (w : NormalWord d) : h • w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }

def Monoid.PushoutI.NormalWord.prod {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} (w : NormalWord d) : PushoutI φ

Take the product of a normal word as an element of the PushoutI. We show that this is bijective, in NormalWord.equiv.

@[simp]

theorem Monoid.PushoutI.NormalWord.prod_base_smul {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} (h : H) (w : NormalWord d) : (h • w).prod = (base φ) h * w.prod

@[simp]

theorem Monoid.PushoutI.NormalWord.prod_empty {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} : empty.prod = 1

noncomputable def Monoid.PushoutI.NormalWord.cons {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} {i : ι} (g : G i) (w : NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range) : NormalWord d

A constructor that multiplies a NormalWord by an element, with condition to make sure the underlying list does get longer.

@[simp]

theorem Monoid.PushoutI.NormalWord.cons_head {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} {i : ι} (g : G i) (w : NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range) : (cons g w hmw hgr).head = (MonoidHom.ofInjective ⋯).symm (⋯.equiv (g * (φ i) w.head)).1

@[simp]

theorem Monoid.PushoutI.NormalWord.cons_toList {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} {i : ι} (g : G i) (w : NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range) : (cons g w hmw hgr).toList = ⟨i, ↑(⋯.equiv (g * (φ i) w.head)).2⟩ :: w.toList

@[simp]

theorem Monoid.PushoutI.NormalWord.prod_cons {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} {i : ι} (g : G i) (w : NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range) : (cons g w hmw hgr).prod = (of i) g * w.prod

theorem Monoid.PushoutI.NormalWord.eq_one_of_smul_normalized {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (w : CoprodI.Word G) {i : ι} (h : H) (hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) (hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → g ∈ d.set j) : h = 1

Given a word in CoprodI, if every letter is in the transversal and when we multiply by an element of the base group it still has this property, then the element of the base group we multiplied by was one.

theorem Monoid.PushoutI.NormalWord.ext_smul {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {w₁ w₂ : NormalWord d} (i : ι) (h : CoprodI.of ((φ i) w₁.head) • w₁.toWord = CoprodI.of ((φ i) w₂.head) • w₂.toWord) : w₁ = w₂

noncomputable def Monoid.PushoutI.NormalWord.rcons {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (i : ι) (p : Pair d i) : NormalWord d

Given a pair (head, tail), we can form a word by prepending head to tail, but putting head into normal form first, by making sure it is expressed as an element of the base group multiplied by an element of the transversal.

theorem Monoid.PushoutI.NormalWord.rcons_injective {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} : Function.Injective (rcons i)

noncomputable def Monoid.PushoutI.NormalWord.equivPair {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (i : ι) : NormalWord d ≃ Pair d i

The equivalence between NormalWords and pairs. We can turn a NormalWord into a pair by taking the head of the List if it is in G i and multiplying it by the element of the base group.

noncomputable instance Monoid.PushoutI.NormalWord.summandAction {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (i : ι) : MulAction (G i) (NormalWord d)

theorem Monoid.PushoutI.NormalWord.summand_smul_def' {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : NormalWord d) : g • w = (equivPair i).symm (let __src := (equivPair i) w; { head := g * ((equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯, normalized := ⋯ })

noncomputable instance Monoid.PushoutI.NormalWord.mulAction {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] : MulAction (PushoutI φ) (NormalWord d)

theorem Monoid.PushoutI.NormalWord.base_smul_def {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (h : H) (w : NormalWord d) : (base φ) h • w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }

theorem Monoid.PushoutI.NormalWord.summand_smul_def {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : NormalWord d) : (of i) g • w = (equivPair i).symm (let __src := (equivPair i) w; { head := g * ((equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯, normalized := ⋯ })

theorem Monoid.PushoutI.NormalWord.of_smul_eq_smul {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : NormalWord d) : (of i) g • w = g • w

theorem Monoid.PushoutI.NormalWord.base_smul_eq_smul {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (h : H) (w : NormalWord d) : (base φ) h • w = h • w

noncomputable def Monoid.PushoutI.NormalWord.consRecOn {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {motive : NormalWord d → Sort u_5} (w : NormalWord d) (empty : motive empty) (cons : (i : ι) → (g : G i) → (w : NormalWord d) → (hmw : w.fstIdx ≠ some i) → g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (cons g w hmw hgr)) (base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((base φ) h • w)) : motive w

Induction principle for NormalWord, that corresponds closely to inducting on the underlying list.

theorem Monoid.PushoutI.NormalWord.cons_eq_smul {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range) : cons g w hmw hgr = (of i) g • w

@[simp]

theorem Monoid.PushoutI.NormalWord.prod_summand_smul {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : NormalWord d) : (g • w).prod = (of i) g * w.prod

@[simp]

theorem Monoid.PushoutI.NormalWord.prod_smul {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (g : PushoutI φ) (w : NormalWord d) : (g • w).prod = g * w.prod

theorem Monoid.PushoutI.NormalWord.prod_smul_empty {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (w : NormalWord d) : w.prod • empty = w

noncomputable def Monoid.PushoutI.NormalWord.equiv {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] : PushoutI φ ≃ NormalWord d

The equivalence between normal forms and elements of the pushout

theorem Monoid.PushoutI.NormalWord.prod_injective {H : Type u_3} [Group H] {ι : Type u_5} {G : ι → Type u_6} [(i : ι) → Group (G i)] {φ : (i : ι) → H →* G i} {d : Transversal φ} : Function.Injective prod

instance Monoid.PushoutI.NormalWord.instFaithfulSMul {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] : FaithfulSMul (PushoutI φ) (NormalWord d)

instance Monoid.PushoutI.NormalWord.instFaithfulSMul_1 {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (i : ι) : FaithfulSMul (G i) (NormalWord d)

instance Monoid.PushoutI.NormalWord.instFaithfulSMul_2 {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Transversal φ} : FaithfulSMul H (NormalWord d)

theorem Monoid.PushoutI.of_injective {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective ⇑(φ i)) (i : ι) : Function.Injective ⇑(of i)

All maps into the PushoutI, or amalgamated product of groups are injective, provided all maps in the diagram are injective.

See also base_injective

theorem Monoid.PushoutI.base_injective {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective ⇑(φ i)) : Function.Injective ⇑(base φ)

def Monoid.PushoutI.Reduced {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] (φ : (i : ι) → H →* G i) (w : CoprodI.Word G) : Prop

A word in CoprodI is reduced if none of its letters are in the base group.

theorem Monoid.PushoutI.Reduced.exists_normalWord_prod_eq {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (d : NormalWord.Transversal φ) {w : CoprodI.Word G} (hw : Reduced φ w) : ∃ (w' : NormalWord d), w'.prod = ofCoprodI w.prod ∧ List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList

theorem Monoid.PushoutI.Reduced.eq_empty_of_mem_range {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective ⇑(φ i)) {w : CoprodI.Word G} (hw : Reduced φ w) (h : ofCoprodI w.prod ∈ (base φ).range) : w = CoprodI.Word.empty

For any word w in the coproduct, if w is reduced (i.e none its letters are in the image of the base monoid), and nonempty, then w itself is not in the image of the base group.

theorem Monoid.PushoutI.inf_of_range_eq_base_range {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective ⇑(φ i)) {i j : ι} (hij : i ≠ j) : (of i).range ⊓ (of j).range = (base φ).range

The intersection of the images of the maps from any two distinct groups in the diagram into the amalgamated product is the image of the map from the base group in the diagram.