instEpiNegHom

Mathlib.CategoryTheory.Preadditive.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Preadditive.instEpiNegHom

English

If f is epi, then its negation −f is also epi.

Русский

Если f — эпиморфизм, то и его отрицание −f тоже эпиморфизм.

LaTeX

$$$\operatorname{Epi}(f) \Rightarrow \operatorname{Epi}(-f)$$$

Lean4

instance {P Q : C} {f : P ⟶ Q} [Epi f] : Epi (-f) :=
  ⟨fun g g' H => by rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru