Theorems · Definition · category theory

CategoryTheory.InducedCategory.endEquiv

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      {F : D → C} → {X : CategoryTheory.InducedCategory C F} → CategoryTheory.End X ≃* CategoryTheory.End (F X)

The multiplicative bijection End X ≃* End (F X) when X : InducedCategory C F.

Defined in

Mathlib.CategoryTheory.Endomorphism

Cited by

5 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

CategoryTheory.Category