English
Provides the linear structure on Quotient r that makes the quotient functor additive and compatible with the linear structure of C.
Русский
Задаётся линейная структура на Quotient r, делающая квотиентный функтор аддитивным и совместимым с линейной структурой C.
LaTeX
$$$\\text{linear}:\\; \\text{Linear } R (\\mathrm{Quotient}(r))$$$
Lean4
/-- The negation on the morphisms in the category `Quotient r` when `r` is compatible
with the addition. -/
def neg (hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y) (_ : r f₁ f₂) (_ : r g₁ g₂), r (f₁ + g₁) (f₂ + g₂)) {X Y : Quotient r}
(f : X ⟶ Y) : X ⟶ Y :=
Quot.liftOn f (fun a => Quot.mk _ (-a))
(fun f g => by
intro hfg
simp only [compClosure_iff_self] at hfg
erw [functor_map_eq_iff]
apply Congruence.equivalence.symm
convert hr f g _ _ hfg (Congruence.equivalence.refl (-f - g)) using 1 <;> abel)
