chore(*): add mathlib4 synchronization comments (#18851)

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.monoid_algebra.ideal`
* `algebra.ring_quot`
* `algebraic_topology.dold_kan.decomposition`
* `algebraic_topology.dold_kan.degeneracies`
* `algebraic_topology.dold_kan.n_reflects_iso`
* `algebraic_topology.dold_kan.split_simplicial_object`
* `category_theory.adjunction.over`
* `data.polynomial.module`
* `linear_algebra.affine_space.independent`
* `linear_algebra.matrix.adjugate`
* `linear_algebra.matrix.nondegenerate`
* `ring_theory.mv_polynomial.ideal`

src/algebra/monoid_algebra/ideal.lean

@@ -9,6 +9,9 @@ import ring_theory.ideal.basic
 
 /-!
 # Lemmas about ideals of `monoid_algebra` and `add_monoid_algebra`
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 variables {k A G : Type*}

src/algebra/ring_quot.lean

@@ -9,6 +9,9 @@ import ring_theory.ideal.quotient
 /-!
 # Quotients of non-commutative rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Unfortunately, ideals have only been developed in the commutative case as `ideal`,
 and it's not immediately clear how one should formalise ideals in the non-commutative case.
 

src/algebraic_topology/dold_kan/decomposition.lean

@@ -10,6 +10,9 @@ import algebraic_topology.dold_kan.p_infty
 
 # Decomposition of the Q endomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we obtain a lemma `decomposition_Q` which expresses
 explicitly the projection `(Q q).f (n+1) : X _[n+1] ⟶ X _[n+1]`
 (`X : simplicial_object C` with `C` a preadditive category) as

src/algebraic_topology/dold_kan/degeneracies.lean

@@ -11,6 +11,9 @@ import tactic.fin_cases
 
 # Behaviour of P_infty with respect to degeneracies
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 For any `X : simplicial_object C` where `C` is an abelian category,
 the projector `P_infty : K[X] ⟶ K[X]` is supposed to be the projection
 on the normalized subcomplex, parallel to the degenerate subcomplex, i.e.

src/algebraic_topology/dold_kan/n_reflects_iso.lean

@@ -13,6 +13,9 @@ import category_theory.idempotents.karoubi_karoubi
 
 # N₁ and N₂ reflects isomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, it is shown that the functors
 `N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)` and
 `N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ))`

src/algebraic_topology/dold_kan/split_simplicial_object.lean

@@ -12,6 +12,9 @@ import algebraic_topology.dold_kan.functor_n
 
 # Split simplicial objects in preadditive categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define a functor `nondeg_complex : simplicial_object.split C ⥤ chain_complex C ℕ`
 when `C` is a preadditive category with finite coproducts, and get an isomorphism
 `to_karoubi_nondeg_complex_iso_N₁ : nondeg_complex ⋙ to_karoubi _ ≅ forget C ⋙ dold_kan.N₁`.

src/category_theory/adjunction/over.lean

@@ -10,6 +10,9 @@ import category_theory.over
 /-!
 # Adjunctions related to the over category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Construct the left adjoint `star X` to `over.forget X : over X ⥤ C`.
 
 ## TODO

src/data/polynomial/module.lean

@@ -9,6 +9,9 @@ import ring_theory.finite_type
 /-!
 # Polynomial module
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we define the polynomial module for an `R`-module `M`, i.e. the `R[X]`-module `M[X]`.
 
 This is defined as an type alias `polynomial_module R M := ℕ →₀ M`, since there might be different

src/linear_algebra/affine_space/independent.lean

@@ -13,6 +13,9 @@ import linear_algebra.basis
 /-!
 # Affine independence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines affinely independent families of points.
 
 ## Main definitions

src/linear_algebra/matrix/adjugate.lean

@@ -11,6 +11,9 @@ import ring_theory.polynomial.basic
 /-!
 # Cramer's rule and adjugate matrices
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The adjugate matrix is the transpose of the cofactor matrix.
 It is calculated with Cramer's rule, which we introduce first.
 The vectors returned by Cramer's rule are given by the linear map `cramer`,

src/linear_algebra/matrix/nondegenerate.lean

@@ -10,6 +10,9 @@ import linear_algebra.matrix.adjugate
 /-!
 # Matrices associated with non-degenerate bilinear forms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 * `matrix.nondegenerate A`: the proposition that when interpreted as a bilinear form, the matrix `A`

src/ring_theory/mv_polynomial/ideal.lean

@@ -9,6 +9,9 @@ import data.mv_polynomial.division
 /-!
 # Lemmas about ideals of `mv_polynomial`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Notably this contains results about monomial ideals.
 
 ## Main results