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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.category.Mon.limits`
* `algebra.char_p.local_ring`
* `algebra.direct_sum.decomposition`
* `algebra.direct_sum.internal`
* `algebra.module.bimodule`
* `algebraic_topology.fundamental_groupoid.fundamental_group`
* `algebraic_topology.fundamental_groupoid.punit`
* `analysis.complex.operator_norm`
* `analysis.normed_space.affine_isometry`
* `analysis.normed_space.banach_steinhaus`
* `analysis.normed_space.completion`
* `analysis.normed_space.extend`
* `analysis.normed_space.multilinear`
* `analysis.special_functions.complex.arg`
* `analysis.special_functions.complex.log`
* `analysis.special_functions.pow.complex`
* `category_theory.bicategory.free`
* `category_theory.groupoid.free_groupoid`
* `category_theory.monoidal.free.coherence`
* `category_theory.monoidal.of_chosen_finite_products.basic`
* `category_theory.monoidal.types.basic`
* `data.matrix.kronecker`
* `data.nat.factorial.double_factorial`
* `data.polynomial.expand`
* `linear_algebra.matrix.is_diag`
* `linear_algebra.tensor_product.matrix`
* `linear_algebra.unitary_group`
* `number_theory.legendre_symbol.mul_character`
* `number_theory.multiplicity`
* `ring_theory.finite_presentation`
* `ring_theory.ideal.local_ring`
* `ring_theory.jacobson_ideal`
* `ring_theory.localization.at_prime`
* `ring_theory.matrix_algebra`
* `ring_theory.nakayama`
* `set_theory.game.pgame`
* `topology.category.TopCommRing`
* `topology.fiber_bundle.constructions`
* `topology.sheaves.limits`
* `topology.sheaves.presheaf`
* `topology.sheaves.presheaf_of_functions`
* `topology.sheaves.sheaf`

src/algebra/category/Mon/limits.lean

@@ -12,6 +12,9 @@ import group_theory.submonoid.operations
 /-!
 # The category of (commutative) (additive) monoids has all limits
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Further, these limits are preserved by the forgetful functor --- that is,
 the underlying types are just the limits in the category of types.
 

src/algebra/char_p/local_ring.lean

@@ -11,6 +11,9 @@ import data.nat.factorization.basic
 /-!
 # Characteristics of local rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main result
 
 - `char_p_zero_or_prime_power`: In a commutative local ring the characteristics is either

src/algebra/direct_sum/decomposition.lean

@@ -9,6 +9,9 @@ import algebra.module.submodule.basic
 /-!
 # Decompositions of additive monoids, groups, and modules into direct sums
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 * `direct_sum.decomposition ℳ`: A typeclass to provide a constructive decomposition from

src/algebra/direct_sum/internal.lean

@@ -11,6 +11,9 @@ import algebra.direct_sum.algebra
 /-!
 # Internally graded rings and algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This module provides `gsemiring` and `gcomm_semiring` instances for a collection of subobjects `A`
 when a `set_like.graded_monoid` instance is available:
 

src/algebra/module/bimodule.lean

@@ -8,6 +8,9 @@ import ring_theory.tensor_product
 /-!
 # Bimodules
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 One frequently encounters situations in which several sets of scalars act on a single space, subject
 to compatibility condition(s). A distinguished instance of this is the theory of bimodules: one has
 two rings `R`, `S` acting on an additive group `M`, with `R` acting covariantly ("on the left")

src/algebraic_topology/fundamental_groupoid/fundamental_group.lean

@@ -12,6 +12,9 @@ import algebraic_topology.fundamental_groupoid.basic
 /-!
 # Fundamental group of a space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a topological space `X` and a basepoint `x`, the fundamental group is the automorphism group
 of `x` i.e. the group with elements being loops based at `x` (quotiented by homotopy equivalence).
 -/

src/algebraic_topology/fundamental_groupoid/punit.lean

@@ -9,6 +9,9 @@ import algebraic_topology.fundamental_groupoid.basic
 /-!
 # Fundamental groupoid of punit
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The fundamental groupoid of punit is naturally isomorphic to `category_theory.discrete punit`
 -/
 

src/analysis/complex/operator_norm.lean

@@ -9,6 +9,9 @@ import data.complex.determinant
 
 /-! # The basic continuous linear maps associated to `ℂ`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The continuous linear maps `complex.re_clm` (real part), `complex.im_clm` (imaginary part),
 `complex.conj_cle` (conjugation), and `complex.of_real_clm` (inclusion of `ℝ`) were introduced in
 `analysis.complex.operator_norm`.  This file contains a few calculations requiring more imports:

src/analysis/normed_space/affine_isometry.lean

@@ -12,6 +12,9 @@ import algebra.char_p.invertible
 /-!
 # Affine isometries
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `affine_isometry 𝕜 P P₂` to be an affine isometric embedding of normed
 add-torsors `P` into `P₂` over normed `𝕜`-spaces and `affine_isometry_equiv` to be an affine
 isometric equivalence between `P` and `P₂`.

src/analysis/normed_space/banach_steinhaus.lean

@@ -9,6 +9,9 @@ import topology.algebra.module.basic
 /-!
 # The Banach-Steinhaus theorem: Uniform Boundedness Principle
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Herein we prove the Banach-Steinhaus theorem: any collection of bounded linear maps
 from a Banach space into a normed space which is pointwise bounded is uniformly bounded.
 

src/analysis/normed_space/completion.lean

@@ -10,6 +10,9 @@ import topology.algebra.uniform_ring
 /-!
 # Normed space structure on the completion of a normed space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `E` is a normed space over `𝕜`, then so is `uniform_space.completion E`. In this file we provide
 necessary instances and define `uniform_space.completion.to_complₗᵢ` - coercion
 `E → uniform_space.completion E` as a bundled linear isometry.

src/analysis/normed_space/extend.lean

@@ -11,6 +11,9 @@ import data.is_R_or_C.basic
 /-!
 # Extending a continuous `ℝ`-linear map to a continuous `𝕜`-linear map
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we provide a way to extend a continuous `ℝ`-linear map to a continuous `𝕜`-linear map
 in a way that bounds the norm by the norm of the original map, when `𝕜` is either `ℝ` (the
 extension is trivial) or `ℂ`. We formulate the extension uniformly, by assuming `is_R_or_C 𝕜`.

src/analysis/normed_space/multilinear.lean

@@ -9,6 +9,9 @@ import topology.algebra.module.multilinear
 /-!
 # Operator norm on the space of continuous multilinear maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 When `f` is a continuous multilinear map in finitely many variables, we define its norm `‖f‖` as the
 smallest number such that `‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖` for all `m`.
 

src/analysis/special_functions/complex/arg.lean

@@ -9,6 +9,9 @@ import analysis.special_functions.trigonometric.inverse
 /-!
 # The argument of a complex number.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define `arg : ℂ → ℝ`, returing a real number in the range (-π, π],
 such that for `x ≠ 0`, `sin (arg x) = x.im / x.abs` and `cos (arg x) = x.re / x.abs`,
 while `arg 0` defaults to `0`

src/analysis/special_functions/complex/log.lean

@@ -9,6 +9,9 @@ import analysis.special_functions.log.basic
 /-!
 # The complex `log` function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Basic properties, relationship with `exp`.
 -/
 

src/analysis/special_functions/pow/complex.lean

@@ -8,6 +8,9 @@ import analysis.special_functions.complex.log
 
 /-! # Power function on `ℂ`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct the power functions `x ^ y`, where `x` and `y` are complex numbers.
 -/
 

src/category_theory/bicategory/free.lean

@@ -8,6 +8,9 @@ import category_theory.bicategory.functor
 /-!
 # Free bicategories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the free bicategory over a quiver. In this bicategory, the 1-morphisms are freely
 generated by the arrows in the quiver, and the 2-morphisms are freely generated by the formal
 identities, the formal unitors, and the formal associators modulo the relation derived from the

src/category_theory/groupoid/free_groupoid.lean

@@ -14,6 +14,9 @@ import combinatorics.quiver.symmetric
 /-!
 # Free groupoid on a quiver
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the free groupoid on a quiver, the lifting of a prefunctor to its unique
 extension as a functor from the free groupoid, and proves uniqueness of this extension.
 

src/category_theory/monoidal/free/coherence.lean

@@ -10,6 +10,9 @@ import category_theory.discrete_category
 /-!
 # The monoidal coherence theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we prove the monoidal coherence theorem, stated in the following form: the free
 monoidal category over any type `C` is thin.
 

src/category_theory/monoidal/of_chosen_finite_products/basic.lean

@@ -10,6 +10,9 @@ import category_theory.pempty
 /-!
 # The monoidal structure on a category with chosen finite products.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This is a variant of the development in `category_theory.monoidal.of_has_finite_products`,
 which uses specified choices of the terminal object and binary product,
 enabling the construction of a cartesian category with specific definitions of the tensor unit

src/category_theory/monoidal/types/basic.lean

@@ -10,6 +10,9 @@ import logic.equiv.fin
 
 /-!
 # The category of types is a monoidal category
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open category_theory

src/data/matrix/kronecker.lean

@@ -14,6 +14,9 @@ import ring_theory.tensor_product
 /-!
 # Kronecker product of matrices
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This defines the [Kronecker product](https://en.wikipedia.org/wiki/Kronecker_product).
 
 ## Main definitions

src/data/nat/factorial/double_factorial.lean

@@ -9,6 +9,9 @@ import tactic.ring
 /-!
 # Double factorials
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the double factorial,
   `n‼ := n * (n - 2) * (n - 4) * ...`.
 

src/data/polynomial/expand.lean

@@ -10,6 +10,9 @@ import tactic.ring_exp
 /-!
 # Expand a polynomial by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 * `polynomial.expand R p f`: expand the polynomial `f` with coefficients in a

src/linear_algebra/matrix/is_diag.lean

@@ -10,6 +10,9 @@ import data.matrix.kronecker
 /-!
 # Diagonal matrices
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains the definition and basic results about diagonal matrices.
 
 ## Main results

src/linear_algebra/tensor_product/matrix.lean

@@ -11,6 +11,9 @@ import linear_algebra.tensor_product_basis
 /-!
 # Connections between `tensor_product` and `matrix`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains results about the matrices corresponding to maps between tensor product types,
 where the correspondance is induced by `basis.tensor_product`
 

src/linear_algebra/unitary_group.lean

@@ -11,6 +11,9 @@ import algebra.star.unitary
 /-!
 # The Unitary Group
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines elements of the unitary group `unitary_group n α`, where `α` is a `star_ring`.
 This consists of all `n` by `n` matrices with entries in `α` such that the star-transpose is its
 inverse. In addition, we define the group structure on `unitary_group n α`, and the embedding into

src/number_theory/legendre_symbol/mul_character.lean

@@ -10,6 +10,9 @@ import data.fintype.units
 /-!
 # Multiplicative characters of finite rings and fields
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `R` and `R'` be a commutative rings.
 A *multiplicative character* of `R` with values in `R'` is a morphism of
 monoids from the multiplicative monoid of `R` into that of `R'`

src/number_theory/multiplicity.lean

@@ -12,6 +12,9 @@ import ring_theory.ideal.quotient_operations
 /-!
 # Multiplicity in Number Theory
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains results in number theory relating to multiplicity.
 
 ## Main statements

src/ring_theory/finite_presentation.lean

@@ -11,6 +11,9 @@ import ring_theory.ideal.quotient_operations
 /-!
 # Finiteness conditions in commutative algebra
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define several notions of finiteness that are common in commutative algebra.
 
 ## Main declarations

src/ring_theory/ideal/local_ring.lean

@@ -13,6 +13,9 @@ import logic.equiv.transfer_instance
 
 # Local rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Define local rings as commutative rings having a unique maximal ideal.
 
 ## Main definitions

src/ring_theory/jacobson_ideal.lean

@@ -9,6 +9,9 @@ import ring_theory.polynomial.quotient
 /-!
 # Jacobson radical
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The Jacobson radical of a ring `R` is defined to be the intersection of all maximal ideals of `R`.
 This is similar to how the nilradical is equal to the intersection of all prime ideals of `R`.
 

src/ring_theory/localization/at_prime.lean

@@ -9,6 +9,9 @@ import ring_theory.localization.ideal
 /-!
 # Localizations of commutative rings at the complement of a prime ideal
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
  * `is_localization.at_prime (I : ideal R) [is_prime I] (S : Type*)` expresses that `S` is a

src/ring_theory/matrix_algebra.lean

@@ -7,6 +7,9 @@ import data.matrix.basis
 import ring_theory.tensor_product
 
 /-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We show `matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R)`.
 -/
 

src/ring_theory/nakayama.lean

@@ -8,6 +8,9 @@ import ring_theory.jacobson_ideal
 /-!
 # Nakayama's lemma
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains some alternative statements of Nakayama's Lemma as found in
 [Stacks: Nakayama's Lemma](https://stacks.math.columbia.edu/tag/00DV).
 

src/set_theory/game/pgame.lean

@@ -11,6 +11,9 @@ import order.game_add
 /-!
 # Combinatorial (pre-)games.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The basic theory of combinatorial games, following Conway's book `On Numbers and Games`. We
 construct "pregames", define an ordering and arithmetic operations on them, then show that the
 operations descend to "games", defined via the equivalence relation `p ≈ q ↔ p ≤ q ∧ q ≤ p`.

src/topology/category/TopCommRing.lean

@@ -10,6 +10,9 @@ import topology.algebra.ring.basic
 /-!
 # Category of topological commutative rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce the category `TopCommRing` of topological commutative rings together with the relevant
 forgetful functors to topological spaces and commutative rings.
 -/

src/topology/fiber_bundle/constructions.lean

@@ -8,6 +8,9 @@ import topology.fiber_bundle.basic
 /-!
 # Standard constructions on fiber bundles
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains several standard constructions on fiber bundles:
 
 * `bundle.trivial.fiber_bundle 𝕜 B F`: the trivial fiber bundle with model fiber `F` over the base

src/topology/sheaves/limits.lean

@@ -9,6 +9,9 @@ import category_theory.limits.functor_category
 
 /-!
 # Presheaves in `C` have limits and colimits when `C` does.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 noncomputable theory

src/topology/sheaves/presheaf.lean

@@ -10,6 +10,9 @@ import category_theory.adjunction.opposites
 /-!
 # Presheaves on a topological space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define `presheaf C X` simply as `(opens X)ᵒᵖ ⥤ C`,
 and inherit the category structure with natural transformations as morphisms.