English
There is an instance giving a linear functor structure on the functor Quotient.functor r, compatible with the linear structure on Quotient r.
Русский
Существует инстанс, задающий линейную структуру функтору Quotient.functor r, совместимую с линейной структурой Quotient r.
LaTeX
$$$\\text{linear_functor}(hr)$$$
Lean4
/-- The preadditive structure on the category `Quotient r` when `r` is compatible
with the addition. -/
def preadditive (hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y) (_ : r f₁ f₂) (_ : r g₁ g₂), r (f₁ + g₁) (f₂ + g₂)) :
Preadditive (Quotient r)
where
homGroup P
Q :=
let iZ : Zero (P ⟶ Q) := { zero := Quot.mk _ 0 }
let iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
let iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
{ add_assoc := by rintro ⟨_⟩ ⟨_⟩ ⟨_⟩; exact congr_arg (functor r).map (add_assoc _ _ _)
zero_add := by rintro ⟨_⟩; exact congr_arg (functor r).map (zero_add _)
add_zero := by rintro ⟨_⟩; exact congr_arg (functor r).map (add_zero _)
add_comm := by rintro ⟨_⟩ ⟨_⟩; exact congr_arg (functor r).map (add_comm _ _)
neg_add_cancel := by rintro ⟨_⟩;
exact
congr_arg (functor r).map
(neg_add_cancel _)
-- todo: use a better defeq
nsmul := nsmulRec
zsmul := zsmulRec }
add_comp := by
rintro _ _ _ ⟨_⟩ ⟨_⟩ ⟨_⟩
exact congr_arg (functor r).map (by apply Preadditive.add_comp)
comp_add := by
rintro _ _ _ ⟨_⟩ ⟨_⟩ ⟨_⟩
exact congr_arg (functor r).map (by apply Preadditive.comp_add)
