Theorems · Definition · category theory

CategoryTheory.InducedCategory.homLinearEquiv

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {R : Type w} →
        [inst_2 : Semiring R] →
          [inst_3 : CategoryTheory.Linear R C] →
            {D : Type u'} → {F : D → C} → {X Y : CategoryTheory.InducedCategory C F} → (X ⟶ Y) ≃ₗ[R] F X ⟶ F Y

The linear equivalence (X ⟶ Y) ≃+ (F X ⟶ F Y) when F : D → C and C is a R-linear category.

Defined in

Mathlib.CategoryTheory.Linear.Basic

Cited by

2 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveSemiringCategoryTheory.Linear