Theorems · Theorem · category theory

CategoryTheory.Limits.Pi.hom_ext

∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ᶜ f),
  (∀ (b : β),
      CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Pi.π f b) =
        CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Pi.π f b)) →
    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

28 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasProduct