English
Auxiliary definitions to support the construction of a linear structure on morphisms in Quotient r, including additive structure and additive functor actions.
Русский
Дополнительные определения для поддержки построения линейной структуры на морфизмах Quotient r, включая аддитивную структуру и действия функторов.
LaTeX
$$$\\text{module'}(hr)\\; = \\; \\text{Quotient}.module( r, hr)$$$
Lean4
/-- The addition on the morphisms in the category `Quotient r` when `r` is compatible
with the addition. -/
def add (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 g : X ⟶ Y) : X ⟶ Y :=
Quot.liftOn₂ f g (fun a b => Quot.mk _ (a + b))
(fun f g₁ g₂ h₁₂ => by
simp only [compClosure_iff_self] at h₁₂
erw [functor_map_eq_iff]
exact hr _ _ _ _ (Congruence.equivalence.refl f) h₁₂)
(fun f₁ f₂ g h₁₂ => by
simp only [compClosure_iff_self] at h₁₂
erw [functor_map_eq_iff]
exact hr _ _ _ _ h₁₂ (Congruence.equivalence.refl g))
