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