By default, the push command does not push local tags onto the remote repository automatically. We need to specifically tell it to push them. To do so, we run
git push origin tag_name
where tag_name is the name we have our tag when creating it. If you pushed it by accident and need to delete it from the remote repository, you need to run
git push origin --delete tag_name
