# Documentation

Mathlib.GroupTheory.PushoutI

## 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)] [] (φ : (i : ι) → H →* G i) :
Con ()

The relation we quotient by to form the pushout

Equations
• = conGen fun (x y : ) => ∃ (i : ι) (x' : H), x = Monoid.Coprod.inl (Monoid.CoprodI.of ((φ i) x')) y = Monoid.Coprod.inr x'
Instances For
def Monoid.PushoutI {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [] (φ : (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.

Equations
Instances For
instance Monoid.PushoutI.mul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} :
Equations
• Monoid.PushoutI.mul = id inferInstance
instance Monoid.PushoutI.one {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} :
Equations
• Monoid.PushoutI.one = id inferInstance
instance Monoid.PushoutI.monoid {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} :
Equations
• One or more equations did not get rendered due to their size.
def Monoid.PushoutI.of {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} (i : ι) :
G i →*

The map from each indexing group into the pushout

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

The map from the base monoid into the pushout

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Monoid.PushoutI.lift_of {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [] [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} (f : (i : ι) → G i →* K) (k : H →* K) (hf : ∀ (i : ι), MonoidHom.comp (f i) (φ i) = k) {i : ι} (g : G 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} [] [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} (f : (i : ι) → G i →* K) (k : H →* K) (hf : ∀ (i : ι), MonoidHom.comp (f i) (φ i) = k) (g : H) :
() ( g) = k g
theorem Monoid.PushoutI.hom_ext {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [] [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} {f : } {g : } (h : ∀ (i : ι), ) (hbase : ) :
f = g
theorem Monoid.PushoutI.hom_ext_nonempty {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [] [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} [hn : ] {f : } {g : } (h : ∀ (i : ι), ) :
f = g
@[simp]
theorem Monoid.PushoutI.homEquiv_symm_apply {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [] [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} (f : { f : ((i : ι) → G i →* K) × (H →* K) // ∀ (i : ι), MonoidHom.comp (f.1 i) (φ i) = f.2 }) :
Monoid.PushoutI.homEquiv.symm f = Monoid.PushoutI.lift (f).1 (f).2 (_ : ∀ (i : ι), MonoidHom.comp ((f).1 i) (φ i) = (f).2)
@[simp]
theorem Monoid.PushoutI.homEquiv_apply_coe {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [] [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} (f : ) :
(Monoid.PushoutI.homEquiv f) = (fun (i : ι) => , )
def Monoid.PushoutI.homEquiv {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [] [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} :
() { f : ((i : ι) → G i →* K) × (H →* K) // ∀ (i : ι), MonoidHom.comp (f.1 i) (φ 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 satsifies a commutativity condition.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Monoid.PushoutI.ofCoprodI {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} :

The map from the coproduct into the pushout

Equations
• Monoid.PushoutI.ofCoprodI = Monoid.CoprodI.lift Monoid.PushoutI.of
Instances For
@[simp]
theorem Monoid.PushoutI.ofCoprodI_of {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} (i : ι) (g : G i) :
Monoid.PushoutI.ofCoprodI (Monoid.CoprodI.of g) = g
theorem Monoid.PushoutI.induction_on {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [] {φ : (i : ι) → H →* G i} {motive : } (x : ) (of : ∀ (i : ι) (g : G i), motive ( g)) (base : ∀ (h : H), motive ( h)) (mul : ∀ (x y : ), motive xmotive ymotive (x * y)) :
motive x
instance Monoid.PushoutI.instGroupPushoutIToMonoidToDivInvMonoidToMonoidToDivInvMonoid {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} :
Equations
• One or more equations did not get rendered due to their size.
structure Monoid.PushoutI.NormalWord.Transversal {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] (φ : (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 : ι),

The chosen element of the base group itself is the identity

• compl : ∀ (i : ι),

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

Instances For
theorem Monoid.PushoutI.NormalWord.transversal_nonempty {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] (φ : (i : ι) → H →* G i) (hφ : ∀ (i : ι), Function.Injective (φ i)) :
structure Monoid.PushoutI.NormalWord {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} extends :
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 : ls.toList, l.snd 1
• chain_ne : List.Chain' (fun (l l' : (i : ι) × G i) => l.fst l'.fst) s.toList

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), { fst := i, snd := g } s.toList

All letter in the word are in the transversal.

Instances For
structure Monoid.PushoutI.NormalWord.Pair {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} (i : ι) extends :
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).

• tail :
• fstIdx_ne : some i
• normalized : ∀ (i_1 : ι) (g : G i_1), { fst := i_1, snd := g } s.tail.toList

All letters in the word are in the transversal.

Instances For
@[simp]
theorem Monoid.PushoutI.NormalWord.empty_toList {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} :
Monoid.PushoutI.NormalWord.empty.toWord.toList = []
@[simp]
theorem Monoid.PushoutI.NormalWord.empty_head {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} :
def Monoid.PushoutI.NormalWord.empty {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance Monoid.PushoutI.NormalWord.instInhabitedNormalWord {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} :
Equations
• Monoid.PushoutI.NormalWord.instInhabitedNormalWord = { default := Monoid.PushoutI.NormalWord.empty }
instance Monoid.PushoutI.NormalWord.instInhabitedPair {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} (i : ι) :
Equations
• One or more equations did not get rendered due to their size.
theorem Monoid.PushoutI.NormalWord.ext {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} {w₁ : } {w₂ : } (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)] [] {φ : (i : ι) → H →* G i} {w₁ : } {w₂ : } :
theorem Monoid.PushoutI.NormalWord.eq_one_of_smul_normalized {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] (w : ) {i : ι} (h : H) (hw : ∀ (i : ι) (g : G i), { fst := i, snd := g } w.toList) (hφw : ∀ (j : ι) (g : G j), { fst := j, snd := g } (Monoid.CoprodI.of ((φ i) h) w).toList) :
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)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] {w₁ : } {w₂ : } (i : ι) (h : Monoid.CoprodI.of ((φ i) w₁.head) w₁.toWord = Monoid.CoprodI.of ((φ i) w₂.head) w₂.toWord) :
w₁ = w₂
@[simp]
theorem Monoid.PushoutI.NormalWord.cons_toList {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} {i : ι} (g : G i) (w : ) (hmw : Monoid.CoprodI.Word.fstIdx w.toWord some i) (hgr : gMonoidHom.range (φ i)) :
(Monoid.PushoutI.NormalWord.cons g w hmw hgr).toWord.toList = { fst := i, snd := (() (g * (φ i) w.head)).2 } :: w.toList
@[simp]
theorem Monoid.PushoutI.NormalWord.cons_head {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} {i : ι} (g : G i) (w : ) (hmw : Monoid.CoprodI.Word.fstIdx w.toWord some i) (hgr : gMonoidHom.range (φ i)) :
(Monoid.PushoutI.NormalWord.cons g w hmw hgr).head = (MulEquiv.symm (MonoidHom.ofInjective (_ : Function.Injective (φ i)))) (() (g * (φ i) w.head)).1
noncomputable def Monoid.PushoutI.NormalWord.cons {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} {i : ι} (g : G i) (w : ) (hmw : Monoid.CoprodI.Word.fstIdx w.toWord some i) (hgr : gMonoidHom.range (φ i)) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Monoid.PushoutI.NormalWord.rcons {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] (i : ι) (p : ) :

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Monoid.PushoutI.NormalWord.rcons_injective {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] {i : ι} :
noncomputable def Monoid.PushoutI.NormalWord.equivPair {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] (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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance Monoid.PushoutI.NormalWord.summandAction {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] (i : ι) :
MulAction (G i)
Equations
• One or more equations did not get rendered due to their size.
instance Monoid.PushoutI.NormalWord.baseAction {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} :
Equations
• One or more equations did not get rendered due to their size.
theorem Monoid.PushoutI.NormalWord.base_smul_def' {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} (h : H) (w : ) :
h w = { toWord := w.toWord, head := h * w.head, normalized := (_ : ∀ (i : ι) (g : G i), { fst := i, snd := g } w.toList) }
theorem Monoid.PushoutI.NormalWord.summand_smul_def' {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : ) :
g w = .symm (let src := ; { toPair := { head := g * .head, tail := src.tail, fstIdx_ne := (_ : Monoid.CoprodI.Word.fstIdx src.tail some i) }, normalized := (_ : ∀ (i_1 : ι) (g : G i_1), { fst := i_1, snd := g } src.tail.toList) })
noncomputable instance Monoid.PushoutI.NormalWord.mulAction {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] :
Equations
• One or more equations did not get rendered due to their size.
theorem Monoid.PushoutI.NormalWord.base_smul_def {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] (h : H) (w : ) :
h w = { toWord := w.toWord, head := h * w.head, normalized := (_ : ∀ (i : ι) (g : G i), { fst := i, snd := g } w.toList) }
theorem Monoid.PushoutI.NormalWord.summand_smul_def {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : ) :
g w = .symm (let src := ; { toPair := { head := g * .head, tail := src.tail, fstIdx_ne := (_ : Monoid.CoprodI.Word.fstIdx src.tail some i) }, normalized := (_ : ∀ (i_1 : ι) (g : G i_1), { fst := i_1, snd := g } src.tail.toList) })
theorem Monoid.PushoutI.NormalWord.of_smul_eq_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : ) :
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)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] (h : H) (w : ) :
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)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] {motive : } (w : ) (h_empty : motive Monoid.PushoutI.NormalWord.empty) (h_cons : (i : ι) → (g : G i) → (w : ) → (hmw : Monoid.CoprodI.Word.fstIdx w.toWord some i) → (hgr : gMonoidHom.range (φ i)) → w.head = 1motive wmotive (Monoid.PushoutI.NormalWord.cons g w hmw hgr)) (h_base : (h : H) → (w : ) → w.head = 1motive wmotive ( h w)) :
motive w

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Monoid.PushoutI.NormalWord.prod {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} (w : ) :

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

Equations
Instances For
theorem Monoid.PushoutI.NormalWord.cons_eq_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : ) (hmw : Monoid.CoprodI.Word.fstIdx w.toWord some i) (hgr : gMonoidHom.range (φ i)) :
@[simp]
theorem Monoid.PushoutI.NormalWord.prod_summand_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : ) :
@[simp]
theorem Monoid.PushoutI.NormalWord.prod_base_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} (h : H) (w : ) :
@[simp]
theorem Monoid.PushoutI.NormalWord.prod_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] (g : ) (w : ) :
@[simp]
theorem Monoid.PushoutI.NormalWord.prod_empty {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} :
Monoid.PushoutI.NormalWord.prod Monoid.PushoutI.NormalWord.empty = 1
@[simp]
theorem Monoid.PushoutI.NormalWord.prod_cons {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} {i : ι} (g : G i) (w : ) (hmw : Monoid.CoprodI.Word.fstIdx w.toWord some i) (hgr : gMonoidHom.range (φ i)) :
theorem Monoid.PushoutI.NormalWord.prod_smul_empty {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] (w : ) :
Monoid.PushoutI.NormalWord.empty = w
noncomputable def Monoid.PushoutI.NormalWord.equiv {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] :

The equivalence between normal forms and elements of the pushout

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Monoid.PushoutI.NormalWord.prod_injective {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} :
Function.Injective Monoid.PushoutI.NormalWord.prod
instance Monoid.PushoutI.NormalWord.instFaithfulSMulPushoutIToMonoidToDivInvMonoidToMonoidToDivInvMonoidNormalWordToSMulMonoidMulAction {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] :
Equations
• (_ : ) = (_ : )
instance Monoid.PushoutI.NormalWord.instFaithfulSMulNormalWordToSMulToMonoidToDivInvMonoidSummandAction {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} [] [(i : ι) → DecidableEq (G i)] (i : ι) :
Equations
• (_ : ) = (_ : )
instance Monoid.PushoutI.NormalWord.instFaithfulSMulNormalWordToSMulToMonoidToDivInvMonoidBaseAction {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} :
Equations
• (_ : ) = (_ : )
theorem Monoid.PushoutI.of_injective {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective (φ i)) (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)] [] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective (φ i)) :
def Monoid.PushoutI.Reduced {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] (φ : (i : ι) → H →* G i) (w : ) :

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

Equations
Instances For
theorem Monoid.PushoutI.Reduced.exists_normalWord_prod_eq {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [] {φ : (i : ι) → H →* G i} {w : } (hw : ) :
∃ (w' : ), = Monoid.PushoutI.ofCoprodI 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)] [] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective (φ i)) {w : } (hw : ) (h : Monoid.PushoutI.ofCoprodI ) :
w = Monoid.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)] [] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective (φ i)) {i : ι} {j : ι} (hij : i j) :

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.