inverse_additive — Mathlib

English

Let e: C ≌ D be an equivalence with e.functor additive. Then the inverse functor e.inverse is additive.

Русский

Пусть e: C ≌ D — эквивалентность, у которой функтор является аддитивным. Тогда обратный функтор e.inverse аддитивен.

LaTeX

$$$e^{-1}.Additive$ при условии $e.\text{functor.Additive}$$$

Lean4

instance inverse_additive (e : C ≌ D) [e.functor.Additive] : e.inverse.Additive where
  map_add {f g} := e.functor.map_injective (by simp)

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