chore(*): add mathlib4 synchronization comments (#18578)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.char_p.basic`
* `algebra.char_p.invertible`
* `algebra.char_p.pi`
* `algebra.char_p.subring`
* `algebra.char_p.two`
* `algebra.polynomial.group_ring_action`
* `analysis.normed.field.basic`
* `analysis.normed.field.infinite_sum`
* `analysis.normed.field.unit_ball`
* `analysis.normed.order.lattice`
* `analysis.normed_space.int`
* `category_theory.bicategory.locally_discrete`
* `category_theory.category.Cat.limit`
* `category_theory.category.Pointed`
* `category_theory.category.Quiv`
* `category_theory.connected_components`
* `category_theory.limits.colimit_limit`
* `category_theory.limits.connected`
* `category_theory.limits.constructions.filtered`
* `category_theory.limits.constructions.over.connected`
* `category_theory.limits.constructions.zero_objects`
* `category_theory.limits.final`
* `category_theory.limits.pi`
* `category_theory.limits.preserves.opposites`
* `category_theory.limits.preserves.shapes.images`
* `category_theory.limits.preserves.shapes.kernels`
* `category_theory.limits.shapes.comm_sq`
* `category_theory.linear.linear_functor`
* `category_theory.preadditive.left_exact`
* `combinatorics.catalan`
* `data.polynomial.algebra_map`
* `data.polynomial.hasse_deriv`
* `data.polynomial.integral_normalization`
* `data.polynomial.lifts`
* `data.polynomial.taylor`
* `group_theory.free_abelian_group`
* `linear_algebra.smodeq`
* `ring_theory.localization.integer`
* `ring_theory.polynomial.scale_roots`
* `ring_theory.polynomial.tower`
* `topology.homotopy.basic`
* `topology.instances.ereal`
* `topology.metric_space.cau_seq_filter`
* `topology.semicontinuous`
