Theorems · Definition · group theory

Monoid.Coprod.clift

{M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_5} →
      [inst : MulOneClass M] →
        [inst_1 : MulOneClass N] →
          [inst_2 : MulOneClass P] →
            (f : FreeMonoid (M ⊕ N) →* P) →
              f (FreeMonoid.of (Sum.inl 1)) = 1 →
                f (FreeMonoid.of (Sum.inr 1)) = 1 →
                  (∀ (x y : M),
                      f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))) →
                    (∀ (x y : N),
                        f (FreeMonoid.of (Sum.inr (x * y))) =
                          f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))) →
                      Monoid.Coprod M N →* P

Lift a monoid homomorphism FreeMonoid (M ⊕ N) →* P satisfying additional properties to M ∗ N →* P. In many cases, Coprod.lift is more convenient. Compared to Coprod.lift, this definition allows a user to provide a custom computational behavior. Also, it only needs MulOneClass assumptions while Coprod.lift needs a Monoid structure.

Defined in

Mathlib.GroupTheory.Coprod.Basic

Cited by

5 results in Mathlib

Foundations

Depth 44 from the axioms · uses propext, Quot.sound

Assumes

MulOneClassMulOneClassMulOneClass