Theorems · Definition · group theory

Monoid.PushoutI.lift

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

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

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

4 results in Mathlib

Foundations

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

Assumes

MonoidMonoidMonoid