Theorems · Theorem · category theory

CategoryTheory.Functor.ext

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h_obj : ∀ (X : C), F.obj X = G.obj X),
  autoParam
      (∀ (X Y : C) (f : X ⟶ Y),
        F.map f =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom ⋯)))
      CategoryTheory.Functor.ext._auto_1 →
    F = G

Proving equality between functors. This isn't an extensionality lemma, because usually you don't really want to do this.

Defined in

Mathlib.CategoryTheory.EqToHom

Cited by

31 results in Mathlib

Foundations

Depth 13 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category