Documentation

Mathlib.GroupTheory.CoprodI

The coproduct (a.k.a. the free product) of groups or monoids #

Given an ι-indexed family M of monoids, we define their coproduct (a.k.a. free product) Monoid.CoprodI M. As usual, we use the suffix I for an indexed (co)product, leaving Coprod for the coproduct of two monoids.

When ι and all M i have decidable equality, the free product bijects with the type Monoid.CoprodI.Word M of reduced words. This bijection is constructed by defining an action of Monoid.CoprodI M on Monoid.CoprodI.Word M.

When M i are all groups, Monoid.CoprodI M is also a group (and the coproduct in the category of groups).

Main definitions #

Remarks #

There are many answers to the question "what is the coproduct of a family M of monoids?", and they are all equivalent but not obviously equivalent. We provide two answers. The first, almost tautological answer is given by Monoid.CoprodI M, which is a quotient of the type of words in the alphabet Σ i, M i. It's straightforward to define and easy to prove its universal property. But this answer is not completely satisfactory, because it's difficult to tell when two elements x y : Monoid.CoprodI M are distinct since Monoid.CoprodI M is defined as a quotient.

The second, maximally efficient answer is given by Monoid.CoprodI.Word M. An element of Monoid.CoprodI.Word M is a word in the alphabet Σ i, M i, where the letter ⟨i, 1⟩ doesn't occur and no adjacent letters share an index i. Since we only work with reduced words, there is no need for quotienting, and it is easy to tell when two elements are distinct. However it's not obvious that this is even a monoid!

We prove that every element of Monoid.CoprodI M can be represented by a unique reduced word, i.e. Monoid.CoprodI M and Monoid.CoprodI.Word M are equivalent types. This means that Monoid.CoprodI.Word M can be given a monoid structure, and it lets us tell when two elements of Monoid.CoprodI M are distinct.

There is also a completely tautological, maximally inefficient answer given by MonCat.Colimits.ColimitType. Whereas Monoid.CoprodI M at least ensures that (any instance of) associativity holds by reflexivity, in this answer associativity holds because of quotienting. Yet another answer, which is constructively more satisfying, could be obtained by showing that Monoid.CoprodI.Rel is confluent.

References #

van der Waerden, Free products of groups

inductive Monoid.CoprodI.Rel {ι : Type u_1} (M : ιType u_2) [(i : ι) → Monoid (M i)] :
FreeMonoid ((i : ι) × M i)FreeMonoid ((i : ι) × M i)Prop

A relation on the free monoid on alphabet Σ i, M i, relating ⟨i, 1⟩ with 1 and ⟨i, x⟩ * ⟨i, y⟩ with ⟨i, x * y⟩.

Instances For
    def Monoid.CoprodI {ι : Type u_1} (M : ιType u_2) [(i : ι) → Monoid (M i)] :
    Type (max u_1 u_2)

    The free product (categorical coproduct) of an indexed family of monoids.

    Equations
    Instances For
      instance instMonoidCoprodI {ι : Type u_1} (M : ιType u_2) [(i : ι) → Monoid (M i)] :
      Equations
      instance instInhabitedCoprodI {ι : Type u_1} (M : ιType u_2) [(i : ι) → Monoid (M i)] :
      Equations
      structure Monoid.CoprodI.Word {ι : Type u_1} (M : ιType u_2) [(i : ι) → Monoid (M i)] :
      Type (max u_1 u_2)

      The type of reduced words. A reduced word cannot contain a letter 1, and no two adjacent letters can come from the same summand.

      • toList : List ((i : ι) × M i)

        A Word is a List (Σ i, M i), such that 1 is not in the list, and no two adjacent letters are from the same summand

      • ne_one : lself.toList, l.snd 1

        A reduced word does not contain 1

      • chain_ne : List.Chain' (fun (l l' : (i : ι) × M i) => l.fst l'.fst) self.toList

        Adjacent letters are not from the same summand.

      Instances For
        theorem Monoid.CoprodI.Word.ext {ι : Type u_1} {M : ιType u_2} :
        ∀ {inst : (i : ι) → Monoid (M i)} {x y : Monoid.CoprodI.Word M}, x.toList = y.toListx = y
        theorem Monoid.CoprodI.Word.ne_one {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] (self : Monoid.CoprodI.Word M) (l : (i : ι) × M i) :
        l self.toListl.snd 1

        A reduced word does not contain 1

        theorem Monoid.CoprodI.Word.chain_ne {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] (self : Monoid.CoprodI.Word M) :
        List.Chain' (fun (l l' : (i : ι) × M i) => l.fst l'.fst) self.toList

        Adjacent letters are not from the same summand.

        def Monoid.CoprodI.of {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} :

        The inclusion of a summand into the free product.

        Equations
        Instances For
          theorem Monoid.CoprodI.of_apply {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} (m : M i) :
          Monoid.CoprodI.of m = (conGen (Monoid.CoprodI.Rel M)).mk' (FreeMonoid.of i, m)
          theorem Monoid.CoprodI.ext_hom {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {N : Type u_3} [Monoid N] (f : Monoid.CoprodI M →* N) (g : Monoid.CoprodI M →* N) (h : ∀ (i : ι), f.comp Monoid.CoprodI.of = g.comp Monoid.CoprodI.of) :
          f = g

          See note [partially-applied ext lemmas].

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

          A map out of the free product corresponds to a family of maps out of the summands. This is the universal property of the free product, characterizing it as a categorical coproduct.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem Monoid.CoprodI.lift_symm_apply {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {N : Type u_3} [Monoid N] (f : Monoid.CoprodI M →* N) :
            ∀ (x : ι), Monoid.CoprodI.lift.symm f x = f.comp Monoid.CoprodI.of
            @[simp]
            theorem Monoid.CoprodI.lift_comp_of {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {N : Type u_4} [Monoid N] (fi : (i : ι) → M i →* N) (i : ι) :
            (Monoid.CoprodI.lift fi).comp Monoid.CoprodI.of = fi i
            @[simp]
            theorem Monoid.CoprodI.lift_of {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {N : Type u_4} [Monoid N] (fi : (i : ι) → M i →* N) {i : ι} (m : M i) :
            (Monoid.CoprodI.lift fi) (Monoid.CoprodI.of m) = (fi i) m
            @[simp]
            theorem Monoid.CoprodI.lift_comp_of' {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {N : Type u_4} [Monoid N] (f : Monoid.CoprodI M →* N) :
            (Monoid.CoprodI.lift fun (i : ι) => f.comp Monoid.CoprodI.of) = f
            @[simp]
            theorem Monoid.CoprodI.lift_of' {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] :
            (Monoid.CoprodI.lift fun (i : ι) => Monoid.CoprodI.of) = MonoidHom.id (Monoid.CoprodI M)
            theorem Monoid.CoprodI.of_leftInverse {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] (i : ι) :
            Function.LeftInverse (Monoid.CoprodI.lift (Pi.mulSingle i (MonoidHom.id (M i)))) Monoid.CoprodI.of
            theorem Monoid.CoprodI.of_injective {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] (i : ι) :
            Function.Injective Monoid.CoprodI.of
            theorem Monoid.CoprodI.mrange_eq_iSup {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {N : Type u_4} [Monoid N] (f : (i : ι) → M i →* N) :
            MonoidHom.mrange (Monoid.CoprodI.lift f) = ⨆ (i : ι), MonoidHom.mrange (f i)
            theorem Monoid.CoprodI.lift_mrange_le {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {N : Type u_4} [Monoid N] (f : (i : ι) → M i →* N) {s : Submonoid N} :
            MonoidHom.mrange (Monoid.CoprodI.lift f) s ∀ (i : ι), MonoidHom.mrange (f i) s
            @[simp]
            theorem Monoid.CoprodI.iSup_mrange_of {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] :
            ⨆ (i : ι), MonoidHom.mrange Monoid.CoprodI.of =
            @[simp]
            theorem Monoid.CoprodI.mclosure_iUnion_range_of {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] :
            Submonoid.closure (⋃ (i : ι), Set.range Monoid.CoprodI.of) =
            theorem Monoid.CoprodI.induction_left {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {C : Monoid.CoprodI MProp} (m : Monoid.CoprodI M) (one : C 1) (mul : ∀ {i : ι} (m : M i) (x : Monoid.CoprodI M), C xC (Monoid.CoprodI.of m * x)) :
            C m
            theorem Monoid.CoprodI.induction_on {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {C : Monoid.CoprodI MProp} (m : Monoid.CoprodI M) (h_one : C 1) (h_of : ∀ (i : ι) (m : M i), C (Monoid.CoprodI.of m)) (h_mul : ∀ (x y : Monoid.CoprodI M), C xC yC (x * y)) :
            C m
            instance Monoid.CoprodI.instInv {ι : Type u_1} (G : ιType u_4) [(i : ι) → Group (G i)] :
            Equations
            theorem Monoid.CoprodI.inv_def {ι : Type u_1} (G : ιType u_4) [(i : ι) → Group (G i)] (x : Monoid.CoprodI G) :
            x⁻¹ = MulOpposite.unop ((Monoid.CoprodI.lift fun (i : ι) => (MonoidHom.op Monoid.CoprodI.of).comp (MulEquiv.inv' (G i)).toMonoidHom) x)
            instance Monoid.CoprodI.instGroup {ι : Type u_1} (G : ιType u_4) [(i : ι) → Group (G i)] :
            Equations
            theorem Monoid.CoprodI.lift_range_le {ι : Type u_1} (G : ιType u_4) [(i : ι) → Group (G i)] {N : Type u_5} [Group N] (f : (i : ι) → G i →* N) {s : Subgroup N} (h : ∀ (i : ι), (f i).range s) :
            (Monoid.CoprodI.lift f).range s
            theorem Monoid.CoprodI.range_eq_iSup {ι : Type u_1} (G : ιType u_4) [(i : ι) → Group (G i)] {N : Type u_5} [Group N] (f : (i : ι) → G i →* N) :
            (Monoid.CoprodI.lift f).range = ⨆ (i : ι), (f i).range
            def Monoid.CoprodI.Word.empty {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] :

            The empty reduced word.

            Equations
            • Monoid.CoprodI.Word.empty = { toList := [], ne_one := , chain_ne := }
            Instances For
              @[simp]
              theorem Monoid.CoprodI.Word.empty_toList {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] :
              Monoid.CoprodI.Word.empty.toList = []
              instance Monoid.CoprodI.Word.instInhabited {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] :
              Equations
              • Monoid.CoprodI.Word.instInhabited = { default := Monoid.CoprodI.Word.empty }
              def Monoid.CoprodI.Word.prod {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] (w : Monoid.CoprodI.Word M) :

              A reduced word determines an element of the free product, given by multiplication.

              Equations
              • w.prod = (List.map (fun (l : (i : ι) × M i) => Monoid.CoprodI.of l.snd) w.toList).prod
              Instances For
                @[simp]
                theorem Monoid.CoprodI.Word.prod_empty {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] :
                Monoid.CoprodI.Word.empty.prod = 1
                def Monoid.CoprodI.Word.fstIdx {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] (w : Monoid.CoprodI.Word M) :

                fstIdx w is some i if the first letter of w is ⟨i, m⟩ with m : M i. If w is empty then it's none.

                Equations
                Instances For
                  theorem Monoid.CoprodI.Word.fstIdx_ne_iff {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {w : Monoid.CoprodI.Word M} {i : ι} :
                  w.fstIdx some i lw.toList.head?, i l.fst
                  structure Monoid.CoprodI.Word.Pair {ι : Type u_1} (M : ιType u_2) [(i : ι) → Monoid (M i)] (i : ι) :
                  Type (max u_1 u_2)

                  Given an index i : ι, Pair M i is the type of pairs (head, tail) where head : M i and tail : Word M, subject to the constraint that first letter of tail can't be ⟨i, m⟩. By prepending head to tail, one obtains a new word. We'll show that any word can be uniquely obtained in this way.

                  • head : M i

                    An element of M i, the first letter of the word.

                  • The remaining letters of the word, excluding the first letter

                  • fstIdx_ne : self.tail.fstIdx some i

                    The index first letter of tail of a Pair M i is not equal to i

                  Instances For
                    theorem Monoid.CoprodI.Word.Pair.ext {ι : Type u_1} {M : ιType u_2} :
                    ∀ {inst : (i : ι) → Monoid (M i)} {i : ι} {x y : Monoid.CoprodI.Word.Pair M i}, x.head = y.headx.tail = y.tailx = y
                    theorem Monoid.CoprodI.Word.Pair.fstIdx_ne {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} (self : Monoid.CoprodI.Word.Pair M i) :
                    self.tail.fstIdx some i

                    The index first letter of tail of a Pair M i is not equal to i

                    instance Monoid.CoprodI.Word.instInhabitedPair {ι : Type u_1} (M : ιType u_2) [(i : ι) → Monoid (M i)] (i : ι) :
                    Equations
                    def Monoid.CoprodI.Word.cons {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M) (hmw : w.fstIdx some i) (h1 : m 1) :

                    Construct a new Word without any reduction. The underlying list of cons m w _ _ is ⟨_, m⟩::w

                    Equations
                    Instances For
                      @[simp]
                      theorem Monoid.CoprodI.Word.cons_toList {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M) (hmw : w.fstIdx some i) (h1 : m 1) :
                      (Monoid.CoprodI.Word.cons m w hmw h1).toList = i, m :: w.toList
                      @[simp]
                      theorem Monoid.CoprodI.Word.fstIdx_cons {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M) (hmw : w.fstIdx some i) (h1 : m 1) :
                      (Monoid.CoprodI.Word.cons m w hmw h1).fstIdx = some i
                      @[simp]
                      theorem Monoid.CoprodI.Word.prod_cons {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] (i : ι) (m : M i) (w : Monoid.CoprodI.Word M) (h1 : m 1) (h2 : w.fstIdx some i) :
                      (Monoid.CoprodI.Word.cons m w h2 h1).prod = Monoid.CoprodI.of m * w.prod
                      def Monoid.CoprodI.Word.rcons {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [(i : ι) → DecidableEq (M i)] {i : ι} (p : Monoid.CoprodI.Word.Pair M i) :

                      Given a pair (head, tail), we can form a word by prepending head to tail, except if head is 1 : M i then we have to just return Word since we need the result to be reduced.

                      Equations
                      Instances For
                        @[simp]
                        theorem Monoid.CoprodI.Word.prod_rcons {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [(i : ι) → DecidableEq (M i)] {i : ι} (p : Monoid.CoprodI.Word.Pair M i) :
                        (Monoid.CoprodI.Word.rcons p).prod = Monoid.CoprodI.of p.head * p.tail.prod
                        theorem Monoid.CoprodI.Word.rcons_inj {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [(i : ι) → DecidableEq (M i)] {i : ι} :
                        Function.Injective Monoid.CoprodI.Word.rcons
                        theorem Monoid.CoprodI.Word.mem_rcons_iff {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [(i : ι) → DecidableEq (M i)] {i : ι} {j : ι} (p : Monoid.CoprodI.Word.Pair M i) (m : M j) :
                        j, m (Monoid.CoprodI.Word.rcons p).toList j, m p.tail.toList m 1 ∃ (h : i = j), m = hp.head
                        def Monoid.CoprodI.Word.consRecOn {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {motive : Monoid.CoprodI.Word MSort u_4} (w : Monoid.CoprodI.Word M) (h_empty : motive Monoid.CoprodI.Word.empty) (h_cons : (i : ι) → (m : M i) → (w : Monoid.CoprodI.Word M) → (h1 : w.fstIdx some i) → (h2 : m 1) → motive wmotive (Monoid.CoprodI.Word.cons m w h1 h2)) :
                        motive w

                        Induct on a word by adding letters one at a time without reduction, effectively inducting on the underlying List.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem Monoid.CoprodI.Word.consRecOn_empty {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {motive : Monoid.CoprodI.Word MSort u_4} (h_empty : motive Monoid.CoprodI.Word.empty) (h_cons : (i : ι) → (m : M i) → (w : Monoid.CoprodI.Word M) → (h1 : w.fstIdx some i) → (h2 : m 1) → motive wmotive (Monoid.CoprodI.Word.cons m w h1 h2)) :
                          Monoid.CoprodI.Word.consRecOn Monoid.CoprodI.Word.empty h_empty h_cons = h_empty
                          @[simp]
                          theorem Monoid.CoprodI.Word.consRecOn_cons {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {motive : Monoid.CoprodI.Word MSort u_4} (i : ι) (m : M i) (w : Monoid.CoprodI.Word M) (h1 : w.fstIdx some i) (h2 : m 1) (h_empty : motive Monoid.CoprodI.Word.empty) (h_cons : (i : ι) → (m : M i) → (w : Monoid.CoprodI.Word M) → (h1 : w.fstIdx some i) → (h2 : m 1) → motive wmotive (Monoid.CoprodI.Word.cons m w h1 h2)) :
                          Monoid.CoprodI.Word.consRecOn (Monoid.CoprodI.Word.cons m w h1 h2) h_empty h_cons = h_cons i m w h1 h2 (Monoid.CoprodI.Word.consRecOn w h_empty h_cons)
                          def Monoid.CoprodI.Word.equivPair {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] (i : ι) :

                          The equivalence between words and pairs. Given a word, it decomposes it as a pair by removing the first letter if it comes from M i. Given a pair, it prepends the head to the tail.

                          Equations
                          Instances For
                            theorem Monoid.CoprodI.Word.equivPair_symm {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] (i : ι) (p : Monoid.CoprodI.Word.Pair M i) :
                            theorem Monoid.CoprodI.Word.equivPair_eq_of_fstIdx_ne {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} {w : Monoid.CoprodI.Word M} (h : w.fstIdx some i) :
                            (Monoid.CoprodI.Word.equivPair i) w = { head := 1, tail := w, fstIdx_ne := h }
                            theorem Monoid.CoprodI.Word.mem_equivPair_tail_iff {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} {j : ι} {w : Monoid.CoprodI.Word M} (m : M i) :
                            i, m ((Monoid.CoprodI.Word.equivPair j) w).tail.toList i, m w.toList.tail i j ∃ (h : w.toList []), w.toList.head h = i, m
                            theorem Monoid.CoprodI.Word.mem_of_mem_equivPair_tail {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} {j : ι} {w : Monoid.CoprodI.Word M} (m : M i) :
                            i, m ((Monoid.CoprodI.Word.equivPair j) w).tail.toListi, m w.toList
                            theorem Monoid.CoprodI.Word.equivPair_head {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} {w : Monoid.CoprodI.Word M} :
                            ((Monoid.CoprodI.Word.equivPair i) w).head = if h : ∃ (h : w.toList []), (w.toList.head h).fst = i then (w.toList.head ).snd else 1
                            instance Monoid.CoprodI.Word.summandAction {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] (i : ι) :
                            Equations
                            instance Monoid.CoprodI.Word.instMulAction {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] :
                            Equations
                            • Monoid.CoprodI.Word.instMulAction = MulAction.ofEndHom (Monoid.CoprodI.lift fun (x : ι) => MulAction.toEndHom)
                            theorem Monoid.CoprodI.Word.smul_def {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M) :
                            m w = Monoid.CoprodI.Word.rcons (let __src := (Monoid.CoprodI.Word.equivPair i) w; { head := m * ((Monoid.CoprodI.Word.equivPair i) w).head, tail := __src.tail, fstIdx_ne := })
                            theorem Monoid.CoprodI.Word.of_smul_def {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] (i : ι) (w : Monoid.CoprodI.Word M) (m : M i) :
                            Monoid.CoprodI.of m w = Monoid.CoprodI.Word.rcons (let __src := (Monoid.CoprodI.Word.equivPair i) w; { head := m * ((Monoid.CoprodI.Word.equivPair i) w).head, tail := __src.tail, fstIdx_ne := })
                            theorem Monoid.CoprodI.Word.equivPair_smul_same {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M) :
                            (Monoid.CoprodI.Word.equivPair i) (Monoid.CoprodI.of m w) = { head := m * ((Monoid.CoprodI.Word.equivPair i) w).head, tail := ((Monoid.CoprodI.Word.equivPair i) w).tail, fstIdx_ne := }
                            @[simp]
                            theorem Monoid.CoprodI.Word.equivPair_tail {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} (p : Monoid.CoprodI.Word.Pair M i) :
                            (Monoid.CoprodI.Word.equivPair i) p.tail = { head := 1, tail := p.tail, fstIdx_ne := }
                            theorem Monoid.CoprodI.Word.smul_eq_of_smul {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M) :
                            m w = Monoid.CoprodI.of m w
                            theorem Monoid.CoprodI.Word.mem_smul_iff {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} {j : ι} {m₁ : M i} {m₂ : M j} {w : Monoid.CoprodI.Word M} :
                            i, m₁ (Monoid.CoprodI.of m₂ w).toList ¬i = j i, m₁ w.toList m₁ 1 ∃ (hij : i = j), i, m₁ w.toList.tail (∃ (m' : M j), j, m' w.toList.head? m₁ = (m₂ * m')) w.fstIdx some j m₁ = m₂
                            theorem Monoid.CoprodI.Word.mem_smul_iff_of_ne {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} {j : ι} (hij : i j) {m₁ : M i} {m₂ : M j} {w : Monoid.CoprodI.Word M} :
                            i, m₁ (Monoid.CoprodI.of m₂ w).toList i, m₁ w.toList
                            theorem Monoid.CoprodI.Word.cons_eq_smul {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} {m : M i} {ls : Monoid.CoprodI.Word M} {h1 : ls.fstIdx some i} {h2 : m 1} :
                            Monoid.CoprodI.Word.cons m ls h1 h2 = Monoid.CoprodI.of m ls
                            theorem Monoid.CoprodI.Word.rcons_eq_smul {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} (p : Monoid.CoprodI.Word.Pair M i) :
                            Monoid.CoprodI.Word.rcons p = Monoid.CoprodI.of p.head p.tail
                            @[simp]
                            theorem Monoid.CoprodI.Word.equivPair_head_smul_equivPair_tail {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i : ι} (w : Monoid.CoprodI.Word M) :
                            Monoid.CoprodI.of ((Monoid.CoprodI.Word.equivPair i) w).head ((Monoid.CoprodI.Word.equivPair i) w).tail = w
                            theorem Monoid.CoprodI.Word.equivPair_tail_eq_inv_smul {ι : Type u_1} [DecidableEq ι] {G : ιType u_4} [(i : ι) → Group (G i)] [(i : ι) → DecidableEq (G i)] {i : ι} (w : Monoid.CoprodI.Word G) :
                            ((Monoid.CoprodI.Word.equivPair i) w).tail = (Monoid.CoprodI.of ((Monoid.CoprodI.Word.equivPair i) w).head)⁻¹ w
                            theorem Monoid.CoprodI.Word.smul_induction {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {C : Monoid.CoprodI.Word MProp} (h_empty : C Monoid.CoprodI.Word.empty) (h_smul : ∀ (i : ι) (m : M i) (w : Monoid.CoprodI.Word M), C wC (Monoid.CoprodI.of m w)) (w : Monoid.CoprodI.Word M) :
                            C w
                            @[simp]
                            theorem Monoid.CoprodI.Word.prod_smul {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] (m : Monoid.CoprodI M) (w : Monoid.CoprodI.Word M) :
                            (m w).prod = m * w.prod
                            def Monoid.CoprodI.Word.equiv {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] :

                            Each element of the free product corresponds to a unique reduced word.

                            Equations
                            • Monoid.CoprodI.Word.equiv = { toFun := fun (m : Monoid.CoprodI M) => m Monoid.CoprodI.Word.empty, invFun := fun (w : Monoid.CoprodI.Word M) => w.prod, left_inv := , right_inv := }
                            Instances For
                              instance Monoid.CoprodI.Word.instDecidableEq {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] :
                              Equations
                              instance Monoid.CoprodI.Word.instDecidableEq_1 {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] :
                              Equations
                              • Monoid.CoprodI.Word.instDecidableEq_1 = Monoid.CoprodI.Word.equiv.decidableEq
                              inductive Monoid.CoprodI.NeWord {ι : Type u_1} (M : ιType u_2) [(i : ι) → Monoid (M i)] :
                              ιιType (max u_1 u_2)

                              A NeWord M i j is a representation of a non-empty reduced words where the first letter comes from M i and the last letter comes from M j. It can be constructed from singletons and via concatenation, and thus provides a useful induction principle.

                              Instances For
                                def Monoid.CoprodI.NeWord.toList {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (_w : Monoid.CoprodI.NeWord M i j) :
                                List ((i : ι) × M i)

                                The list represented by a given NeWord

                                Equations
                                Instances For
                                  theorem Monoid.CoprodI.NeWord.toList_ne_nil {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord M i j) :
                                  w.toList []
                                  def Monoid.CoprodI.NeWord.head {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (_w : Monoid.CoprodI.NeWord M i j) :
                                  M i

                                  The first letter of a NeWord

                                  Equations
                                  Instances For
                                    def Monoid.CoprodI.NeWord.last {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (_w : Monoid.CoprodI.NeWord M i j) :
                                    M j

                                    The last letter of a NeWord

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Monoid.CoprodI.NeWord.toList_head? {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord M i j) :
                                      w.toList.head? = some i, w.head
                                      @[simp]
                                      theorem Monoid.CoprodI.NeWord.toList_getLast? {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord M i j) :
                                      w.toList.getLast? = some j, w.last
                                      def Monoid.CoprodI.NeWord.toWord {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord M i j) :

                                      The Word M represented by a NeWord M i j

                                      Equations
                                      • w.toWord = { toList := w.toList, ne_one := , chain_ne := }
                                      Instances For
                                        theorem Monoid.CoprodI.NeWord.of_word {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] (w : Monoid.CoprodI.Word M) (h : w Monoid.CoprodI.Word.empty) :
                                        ∃ (i : ι) (j : ι) (w' : Monoid.CoprodI.NeWord M i j), w'.toWord = w

                                        Every nonempty Word M can be constructed as a NeWord M i j

                                        def Monoid.CoprodI.NeWord.prod {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord M i j) :

                                        A non-empty reduced word determines an element of the free product, given by multiplication.

                                        Equations
                                        • w.prod = w.toWord.prod
                                        Instances For
                                          @[simp]
                                          theorem Monoid.CoprodI.NeWord.singleton_head {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} (x : M i) (hne_one : x 1) :
                                          @[simp]
                                          theorem Monoid.CoprodI.NeWord.singleton_last {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} (x : M i) (hne_one : x 1) :
                                          @[simp]
                                          theorem Monoid.CoprodI.NeWord.prod_singleton {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} (x : M i) (hne_one : x 1) :
                                          (Monoid.CoprodI.NeWord.singleton x hne_one).prod = Monoid.CoprodI.of x
                                          @[simp]
                                          theorem Monoid.CoprodI.NeWord.append_head {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} {k : ι} {l : ι} {w₁ : Monoid.CoprodI.NeWord M i j} {hne : j k} {w₂ : Monoid.CoprodI.NeWord M k l} :
                                          (w₁.append hne w₂).head = w₁.head
                                          @[simp]
                                          theorem Monoid.CoprodI.NeWord.append_last {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} {k : ι} {l : ι} {w₁ : Monoid.CoprodI.NeWord M i j} {hne : j k} {w₂ : Monoid.CoprodI.NeWord M k l} :
                                          (w₁.append hne w₂).last = w₂.last
                                          @[simp]
                                          theorem Monoid.CoprodI.NeWord.append_prod {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} {k : ι} {l : ι} {w₁ : Monoid.CoprodI.NeWord M i j} {hne : j k} {w₂ : Monoid.CoprodI.NeWord M k l} :
                                          (w₁.append hne w₂).prod = w₁.prod * w₂.prod
                                          def Monoid.CoprodI.NeWord.replaceHead {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (x : M i) (_hnotone : x 1) (_w : Monoid.CoprodI.NeWord M i j) :

                                          One can replace the first letter in a non-empty reduced word by an element of the same group

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem Monoid.CoprodI.NeWord.replaceHead_head {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (x : M i) (hnotone : x 1) (w : Monoid.CoprodI.NeWord M i j) :
                                            def Monoid.CoprodI.NeWord.mulHead {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord M i j) (x : M i) (hnotone : x * w.head 1) :

                                            One can multiply an element from the left to a non-empty reduced word if it does not cancel with the first element in the word.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem Monoid.CoprodI.NeWord.mulHead_head {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord M i j) (x : M i) (hnotone : x * w.head 1) :
                                              (w.mulHead x hnotone).head = x * w.head
                                              @[simp]
                                              theorem Monoid.CoprodI.NeWord.mulHead_prod {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord M i j) (x : M i) (hnotone : x * w.head 1) :
                                              (w.mulHead x hnotone).prod = Monoid.CoprodI.of x * w.prod
                                              def Monoid.CoprodI.NeWord.inv {ι : Type u_1} {G : ιType u_4} [(i : ι) → Group (G i)] {i : ι} {j : ι} (_w : Monoid.CoprodI.NeWord G i j) :

                                              The inverse of a non-empty reduced word

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem Monoid.CoprodI.NeWord.inv_prod {ι : Type u_1} {G : ιType u_4} [(i : ι) → Group (G i)] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord G i j) :
                                                w.inv.prod = w.prod⁻¹
                                                @[simp]
                                                theorem Monoid.CoprodI.NeWord.inv_head {ι : Type u_1} {G : ιType u_4} [(i : ι) → Group (G i)] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord G i j) :
                                                w.inv.head = w.last⁻¹
                                                @[simp]
                                                theorem Monoid.CoprodI.NeWord.inv_last {ι : Type u_1} {G : ιType u_4} [(i : ι) → Group (G i)] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord G i j) :
                                                w.inv.last = w.head⁻¹
                                                theorem Monoid.CoprodI.lift_word_ping_pong {ι : Type u_1} {G : Type u_4} [Group G] {H : ιType u_5} [(i : ι) → Group (H i)] (f : (i : ι) → H i →* G) {α : Type u_6} [MulAction G α] (X : ιSet α) (hpp : Pairwise fun (i j : ι) => ∀ (h : H i), h 1(f i) h X j X i) {i : ι} {j : ι} {k : ι} (w : Monoid.CoprodI.NeWord H i j) (hk : j k) :
                                                (Monoid.CoprodI.lift f) w.prod X k X i
                                                theorem Monoid.CoprodI.lift_word_prod_nontrivial_of_other_i {ι : Type u_1} {G : Type u_4} [Group G] {H : ιType u_5} [(i : ι) → Group (H i)] (f : (i : ι) → H i →* G) {α : Type u_6} [MulAction G α] (X : ιSet α) (hXnonempty : ∀ (i : ι), (X i).Nonempty) (hXdisj : Pairwise fun (i j : ι) => Disjoint (X i) (X j)) (hpp : Pairwise fun (i j : ι) => ∀ (h : H i), h 1(f i) h X j X i) {i : ι} {j : ι} {k : ι} (w : Monoid.CoprodI.NeWord H i j) (hhead : k i) (hlast : k j) :
                                                (Monoid.CoprodI.lift f) w.prod 1
                                                theorem Monoid.CoprodI.lift_word_prod_nontrivial_of_head_eq_last {ι : Type u_1} {G : Type u_4} [Group G] {H : ιType u_5} [(i : ι) → Group (H i)] (f : (i : ι) → H i →* G) {α : Type u_6} [MulAction G α] (X : ιSet α) (hXnonempty : ∀ (i : ι), (X i).Nonempty) (hXdisj : Pairwise fun (i j : ι) => Disjoint (X i) (X j)) (hpp : Pairwise fun (i j : ι) => ∀ (h : H i), h 1(f i) h X j X i) [Nontrivial ι] {i : ι} (w : Monoid.CoprodI.NeWord H i i) :
                                                (Monoid.CoprodI.lift f) w.prod 1
                                                theorem Monoid.CoprodI.lift_word_prod_nontrivial_of_head_card {ι : Type u_1} {G : Type u_4} [Group G] {H : ιType u_5} [(i : ι) → Group (H i)] (f : (i : ι) → H i →* G) {α : Type u_6} [MulAction G α] (X : ιSet α) (hXnonempty : ∀ (i : ι), (X i).Nonempty) (hXdisj : Pairwise fun (i j : ι) => Disjoint (X i) (X j)) (hpp : Pairwise fun (i j : ι) => ∀ (h : H i), h 1(f i) h X j X i) [Nontrivial ι] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord H i j) (hcard : 3 Cardinal.mk (H i)) (hheadtail : i j) :
                                                (Monoid.CoprodI.lift f) w.prod 1
                                                theorem Monoid.CoprodI.lift_word_prod_nontrivial_of_not_empty {ι : Type u_1} {G : Type u_4} [Group G] {H : ιType u_5} [(i : ι) → Group (H i)] (f : (i : ι) → H i →* G) (hcard : 3 Cardinal.mk ι ∃ (i : ι), 3 Cardinal.mk (H i)) {α : Type u_6} [MulAction G α] (X : ιSet α) (hXnonempty : ∀ (i : ι), (X i).Nonempty) (hXdisj : Pairwise fun (i j : ι) => Disjoint (X i) (X j)) (hpp : Pairwise fun (i j : ι) => ∀ (h : H i), h 1(f i) h X j X i) [Nontrivial ι] {i : ι} {j : ι} (w : Monoid.CoprodI.NeWord H i j) :
                                                (Monoid.CoprodI.lift f) w.prod 1
                                                theorem Monoid.CoprodI.empty_of_word_prod_eq_one {ι : Type u_1} {G : Type u_4} [Group G] {H : ιType u_5} [(i : ι) → Group (H i)] (f : (i : ι) → H i →* G) (hcard : 3 Cardinal.mk ι ∃ (i : ι), 3 Cardinal.mk (H i)) {α : Type u_6} [MulAction G α] (X : ιSet α) (hXnonempty : ∀ (i : ι), (X i).Nonempty) (hXdisj : Pairwise fun (i j : ι) => Disjoint (X i) (X j)) (hpp : Pairwise fun (i j : ι) => ∀ (h : H i), h 1(f i) h X j X i) [Nontrivial ι] {w : Monoid.CoprodI.Word H} (h : (Monoid.CoprodI.lift f) w.prod = 1) :
                                                w = Monoid.CoprodI.Word.empty
                                                theorem Monoid.CoprodI.lift_injective_of_ping_pong {ι : Type u_1} {G : Type u_4} [Group G] {H : ιType u_5} [(i : ι) → Group (H i)] (f : (i : ι) → H i →* G) (hcard : 3 Cardinal.mk ι ∃ (i : ι), 3 Cardinal.mk (H i)) {α : Type u_6} [MulAction G α] (X : ιSet α) (hXnonempty : ∀ (i : ι), (X i).Nonempty) (hXdisj : Pairwise fun (i j : ι) => Disjoint (X i) (X j)) (hpp : Pairwise fun (i j : ι) => ∀ (h : H i), h 1(f i) h X j X i) [Nontrivial ι] :
                                                Function.Injective (Monoid.CoprodI.lift f)

                                                The Ping-Pong-Lemma.

                                                Given a group action of G on X so that the H i acts in a specific way on disjoint subsets X i we can prove that lift f is injective, and thus the image of lift f is isomorphic to the free product of the H i.

                                                Often the Ping-Pong-Lemma is stated with regard to subgroups H i that generate the whole group; we generalize to arbitrary group homomorphisms f i : H i →* G and do not require the group to be generated by the images.

                                                Usually the Ping-Pong-Lemma requires that one group H i has at least three elements. This condition is only needed if # ι = 2, and we accept 3 ≤ # ι as an alternative.

                                                def Monoid.CoprodI.FreeGroupBasis.coprodI {ι : Type u_4} {X : ιType u_5} {G : ιType u_6} [(i : ι) → Group (G i)] (B : (i : ι) → FreeGroupBasis (X i) (G i)) :
                                                FreeGroupBasis ((i : ι) × X i) (Monoid.CoprodI G)

                                                Given a family of free groups with distinguished bases, then their free product is free, with a basis given by the union of the bases of the components.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  instance Monoid.CoprodI.instIsFreeGroup {ι : Type u_4} (G : ιType u_5) [(i : ι) → Group (G i)] [∀ (i : ι), IsFreeGroup (G i)] :

                                                  The free product of free groups is itself a free group.

                                                  Equations
                                                  • =

                                                  A free group is a free product of copies of the free_group over one generator.

                                                  Equations
                                                  • freeGroupEquivCoprodI = (FreeGroup.lift fun (i : ι) => Monoid.CoprodI.of (FreeGroup.of ())).toMulEquiv (Monoid.CoprodI.lift fun (i : ι) => FreeGroup.lift fun (x : Unit) => FreeGroup.of i)
                                                  Instances For
                                                    @[simp]
                                                    theorem freeGroupEquivCoprodI_symm_apply {ι : Type u_1} (a : Monoid.CoprodI fun (x : ι) => FreeGroup Unit) :
                                                    freeGroupEquivCoprodI.symm a = (Monoid.CoprodI.lift fun (i : ι) => FreeGroup.lift fun (x : Unit) => FreeGroup.of i) a
                                                    @[simp]
                                                    theorem freeGroupEquivCoprodI_apply {ι : Type u_1} (a : FreeGroup ι) :
                                                    freeGroupEquivCoprodI a = (FreeGroup.lift fun (i : ι) => Monoid.CoprodI.of (FreeGroup.of ())) a
                                                    theorem FreeGroup.injective_lift_of_ping_pong {ι : Type u_1} [Nontrivial ι] {G : Type u_1} [Group G] (a : ιG) {α : Type u_4} [MulAction G α] (X : ιSet α) (Y : ιSet α) (hXnonempty : ∀ (i : ι), (X i).Nonempty) (hXdisj : Pairwise fun (i j : ι) => Disjoint (X i) (X j)) (hYdisj : Pairwise fun (i j : ι) => Disjoint (Y i) (Y j)) (hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)) (hX : ∀ (i : ι), a i (Y i) X i) (hY : ∀ (i : ι), a⁻¹ i (X i) Y i) :
                                                    Function.Injective (FreeGroup.lift a)

                                                    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.