Theorems · Definition · group theory

Monoid.PushoutI.homEquiv

{ι : 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} → (Monoid.PushoutI φ →* K) ≃ { f // ∀ (i : ι), (f.1 i).comp (φ 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 satisfies a commutativity condition.

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

2 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidMonoidMonoid