Theorems · Definition · group theory

AddMonoid.Coprod.clift

{M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_5} →
      [inst : AddZeroClass M] →
        [inst_1 : AddZeroClass N] →
          [inst_2 : AddZeroClass P] →
            (f : FreeAddMonoid (M ⊕ N) →+ P) →
              f (FreeAddMonoid.of (Sum.inl 0)) = 0 →
                f (FreeAddMonoid.of (Sum.inr 0)) = 0 →
                  (∀ (x y : M),
                      f (FreeAddMonoid.of (Sum.inl (x + y))) =
                        f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y))) →
                    (∀ (x y : N),
                        f (FreeAddMonoid.of (Sum.inr (x + y))) =
                          f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))) →
                      AddMonoid.Coprod M N →+ P

Lift an additive monoid homomorphism FreeAddMonoid (M ⊕ N) →+ P satisfying additional properties to AddMonoid.Coprod M N →+ P. Compared to AddMonoid.Coprod.lift, this definition allows a user to provide a custom computational behavior. Also, it only needs AddZeroClass assumptions while AddMonoid.Coprod.lift needs an AddMonoid structure.

Defined in

Mathlib.GroupTheory.Coprod.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddZeroClassAddZeroClassAddZeroClass