chore(*): add mathlib4 synchronization comments (#18845)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.category.Module.products`
* `algebra.homology.additive`
* `algebra.homology.homotopy`
* `algebraic_topology.alternating_face_map_complex`
* `algebraic_topology.cech_nerve`
* `algebraic_topology.dold_kan.faces`
* `algebraic_topology.dold_kan.functor_n`
* `algebraic_topology.dold_kan.homotopies`
* `algebraic_topology.dold_kan.notations`
* `algebraic_topology.dold_kan.p_infty`
* `algebraic_topology.dold_kan.projections`
* `analysis.normed_space.ball_action`
* `category_theory.idempotents.homological_complex`
* `category_theory.monad.adjunction`
* `category_theory.monad.algebra`
* `category_theory.monad.limits`
* `category_theory.monad.products`
* `category_theory.preadditive.eilenberg_moore`
* `category_theory.preadditive.opposite`
* `category_theory.sites.limits`
* `data.complex.cardinality`
* `data.matrix.notation`
* `data.matrix.reflection`
* `data.mv_polynomial.funext`
* `linear_algebra.free_module.pid`
* `linear_algebra.matrix.determinant`
* `linear_algebra.matrix.mv_polynomial`
* `linear_algebra.matrix.polynomial`
* `linear_algebra.matrix.reindex`
* `logic.equiv.transfer_instance`
* `ring_theory.chain_of_divisors`
* `ring_theory.localization.submodule`
* `topology.metric_space.polish`
