Lean4
/-- The category of algebras over an additive endofunctor on a preadditive category is preadditive.
-/
@[simps]
instance algebraPreadditive : Preadditive (Endofunctor.Algebra F)
where
homGroup A₁
A₂ :=
{ add := fun α β =>
{ f := α.f + β.f
h := by simp only [Functor.map_add, add_comp, Endofunctor.Algebra.Hom.h, comp_add] }
zero :=
{ f := 0
h := by simp only [Functor.map_zero, zero_comp, comp_zero] }
nsmul := fun n α =>
{ f := n • α.f
h := by rw [comp_nsmul, Functor.map_nsmul, nsmul_comp, Endofunctor.Algebra.Hom.h] }
neg := fun α =>
{ f := -α.f
h := by simp only [Functor.map_neg, neg_comp, Endofunctor.Algebra.Hom.h, comp_neg] }
sub := fun α β =>
{ f := α.f - β.f
h := by simp only [Functor.map_sub, sub_comp, Endofunctor.Algebra.Hom.h, comp_sub] }
zsmul := fun r α =>
{ f := r • α.f
h := by rw [comp_zsmul, Functor.map_zsmul, zsmul_comp, Endofunctor.Algebra.Hom.h] }
add_assoc := by
intros
apply Algebra.Hom.ext
apply add_assoc
zero_add := by
intros
apply Algebra.Hom.ext
apply zero_add
add_zero := by
intros
apply Algebra.Hom.ext
apply add_zero
nsmul_zero := by
intros
apply Algebra.Hom.ext
apply zero_smul
nsmul_succ := by
intros
apply Algebra.Hom.ext
apply succ_nsmul
sub_eq_add_neg := by
intros
apply Algebra.Hom.ext
apply sub_eq_add_neg
zsmul_zero' := by
intros
apply Algebra.Hom.ext
apply zero_smul
zsmul_succ' := by
intros
apply Algebra.Hom.ext
simp only [natCast_zsmul, succ_nsmul]
rfl
zsmul_neg' := by
intros
apply Algebra.Hom.ext
simp only [negSucc_zsmul, ← Nat.cast_smul_eq_nsmul ℤ]
neg_add_cancel := by
intros
apply Algebra.Hom.ext
apply neg_add_cancel
add_comm := by
intros
apply Algebra.Hom.ext
apply add_comm }
add_comp := by
intros
apply Algebra.Hom.ext
apply add_comp
comp_add := by
intros
apply Algebra.Hom.ext
apply comp_add
