Theorems · Theorem · category theory

CategoryTheory.Functor.linear_comp_iff_of_full_of_essSurj

∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Linear R F] {E : Type u_4}
  [inst_8 : CategoryTheory.Category.{v_3, u_4} E] [inst_9 : CategoryTheory.Preadditive E]
  [inst_10 : CategoryTheory.Linear R E] (G : CategoryTheory.Functor D E) [F.Full] [F.EssSurj],
  CategoryTheory.Functor.Linear R (F.comp G) ↔ CategoryTheory.Functor.Linear R G

Defined in

Mathlib.CategoryTheory.Linear.LinearFunctor

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.PreadditiveCategoryTheory.LinearCategoryTheory.LinearCategoryTheory.Functor.LinearCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.LinearCategoryTheory.Functor.FullCategoryTheory.Functor.EssSurj