Theorems · Definition · group theory
Monoid.CoprodI.lift
{ι : Type u_1} →
{M : ι → Type u_2} →
[inst : (i : ι) → Monoid (M i)] →
{N : Type u_3} → [inst_1 : 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.
- Defined in
- Mathlib.GroupTheory.CoprodI
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 49 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Equivstatement · cited by 8,337
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement and proof · cited by 3,629
- MonoidHom.compproof · cited by 469
- Monoid.CoprodIstatement and proof · cited by 52
- Monoid.CoprodI.ofproof · cited by 45
- conGenproof · cited by 23
- FreeMonoid.liftproof · cited by 20
- Con.liftproof · cited by 12
- Monoid.CoprodI.Relproof · cited by 3
Cited by25
Results whose statement or proof uses this declaration.
- Monoid.CoprodI.lift_ofstatement · cited by 8
- Monoid.PushoutI.ofCoprodIproof · cited by 8
- Monoid.PushoutI.liftproof · cited by 4
- freeGroupEquivCoprodIproof · cited by 3
- Monoid.CoprodI.lift_word_prod_nontrivial_of_head_eq_laststatement · cited by 2
- Monoid.CoprodI.lift_word_prod_nontrivial_of_other_istatement and proof · cited by 2
- Monoid.CoprodI.of_leftInversestatement · cited by 1
- Monoid.CoprodI.empty_of_word_prod_eq_onestatement and proof · cited by 1
- Monoid.CoprodI.iSup_mrange_ofproof · cited by 1
- Monoid.CoprodI.lift_comp_ofstatement and proof · cited by 1
- Monoid.CoprodI.lift_comp_of'statement and proof · cited by 1
- Monoid.CoprodI.lift_injective_of_ping_pongstatement and proof · cited by 1