Theorems · Theorem · category theory

CategoryTheory.Limits.Sigma.hom_ext

∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] {X : C} (g₁ g₂ : ∐ f ⟶ X),
  (∀ (b : β),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) g₁ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) g₂) →
    g₁ = g₂

Without this lemma, limit.hom_ext would be applied, but the goal would involve terms in Discrete β rather than β itself.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Products

Cited by

31 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasCoproduct