additive_inverse_of_FullyFaithful

English

An equivalence of categories induces an additive structure on the inverse functor: the inverse functor is additive if F is fully faithful and the source category is equipped with the induced preadditive structure.

Русский

Эквивалентность категорий порождает аддитивность у обратного функторa, если исходная роль функторa F полностью точна и источник имеет индуцированную предаддитивную структуру.

LaTeX

$$$e^{-1}.Additive$$$

Lean4

/-- The preadditive structure on `C` induced by an equivalence `e : C ≌ D` makes `e.inverse` an
additive functor. -/
theorem additive_inverse_of_FullyFaithful (e : C ≌ D) :
    letI : Preadditive C := ofFullyFaithful e.fullyFaithfulFunctor
    e.inverse.Additive :=
  letI : Preadditive C := ofFullyFaithful e.fullyFaithfulFunctor
  letI : e.functor.Additive := e.fullyFaithfulFunctor.additive_ofFullyFaithful
  e.inverse_additive

Похожие утверждения