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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.algebra.subalgebra.basic`
* `algebra.algebra.subalgebra.tower`
* `algebra.free_non_unital_non_assoc_algebra`
* `algebra.monoid_algebra.basic`
* `algebra.monoid_algebra.support`
* `algebra.polynomial.big_operators`
* `algebra.star.subalgebra`
* `analysis.normed.group.ball_sphere`
* `analysis.normed.group.basic`
* `analysis.normed.group.completion`
* `analysis.normed.group.hom`
* `analysis.normed.group.hom_completion`
* `analysis.normed.group.infinite_sum`
* `analysis.normed.group.seminorm`
* `analysis.normed_space.indicator_function`
* `analysis.subadditive`
* `category_theory.abelian.images`
* `category_theory.abelian.non_preadditive`
* `category_theory.adjunction.comma`
* `category_theory.concrete_category.reflects_isomorphisms`
* `category_theory.is_connected`
* `category_theory.limits.bicones`
* `category_theory.limits.comma`
* `category_theory.limits.cone_category`
* `category_theory.limits.constructions.equalizers`
* `category_theory.limits.constructions.finite_products_of_binary_products`
* `category_theory.limits.constructions.limits_of_products_and_equalizers`
* `category_theory.limits.essentially_small`
* `category_theory.limits.kan_extension`
* `category_theory.limits.lattice`
* `category_theory.limits.mono_coprod`
* `category_theory.limits.opposites`
* `category_theory.limits.preserves.filtered`
* `category_theory.limits.preserves.shapes.biproducts`
* `category_theory.limits.preserves.shapes.zero`
* `category_theory.limits.shapes.biproducts`
* `category_theory.limits.shapes.finite_products`
* `category_theory.limits.shapes.functor_category`
* `category_theory.limits.shapes.kernels`
* `category_theory.limits.shapes.normal_mono.basic`
* `category_theory.limits.shapes.normal_mono.equalizers`
* `category_theory.limits.shapes.zero_morphisms`
* `category_theory.limits.small_complete`
* `category_theory.limits.types`
* `category_theory.linear.basic`
* `category_theory.linear.functor_category`
* `category_theory.monoidal.End`
* `category_theory.preadditive.additive_functor`
* `category_theory.preadditive.basic`
* `category_theory.preadditive.biproducts`
* `category_theory.preadditive.functor_category`
* `combinatorics.hindman`
* `control.bifunctor`
* `control.bitraversable.basic`
* `data.complex.basic`
* `data.nat.choose.cast`
* `data.nat.choose.vandermonde`
* `data.nat.factorial.cast`
* `data.polynomial.basic`
* `data.polynomial.cardinal`
* `data.polynomial.coeff`
* `data.polynomial.degree.definitions`
* `data.polynomial.degree.lemmas`
* `data.polynomial.degree.trailing_degree`
* `data.polynomial.derivative`
* `data.polynomial.erase_lead`
* `data.polynomial.eval`
* `data.polynomial.induction`
* `data.polynomial.inductions`
* `data.polynomial.monic`
* `data.polynomial.monomial`
* `data.polynomial.reverse`
* `data.real.sqrt`
* `data.tree`
* `linear_algebra.affine_space.slope`
* `logic.equiv.functor`
* `number_theory.basic`
* `order.jordan_holder`
* `ring_theory.adjoin.basic`
* `ring_theory.ideal.operations`
* `ring_theory.ideal.quotient`
* `ring_theory.localization.basic`
* `ring_theory.nilpotent`
* `ring_theory.polynomial.pochhammer`
* `topology.algebra.affine`
* `topology.algebra.localization`
* `topology.algebra.ring.ideal`
* `topology.fiber_bundle.trivialization`
* `topology.instances.ennreal`
* `topology.metric_space.completion`
* `topology.metric_space.gluing`
* `topology.metric_space.isometric_smul`
* `topology.metric_space.isometry`
* `topology.uniform_space.compare_reals`
* `topology.unit_interval`

src/algebra/algebra/subalgebra/basic.lean

@@ -11,6 +11,9 @@ import ring_theory.ideal.operations
 /-!
 # Subalgebras over Commutative Semiring
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `subalgebra`s and the usual operations on them (`map`, `comap`).
 
 More lemmas about `adjoin` can be found in `ring_theory.adjoin`.

src/algebra/algebra/subalgebra/tower.lean

@@ -10,6 +10,9 @@ import algebra.algebra.tower
 /-!
 # Subalgebras in towers of algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove facts about subalgebras in towers of algebra.
 
 An algebra tower A/S/R is expressed by having instances of `algebra A S`,

src/algebra/free_non_unital_non_assoc_algebra.lean

@@ -9,6 +9,9 @@ import algebra.monoid_algebra.basic
 /-!
 # Free algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a semiring `R` and a type `X`, we construct the free non-unital, non-associative algebra on
 `X` with coefficients in `R`, together with its universal property. The construction is valuable
 because it can be used to build free algebras with more structure, e.g., free Lie algebras.

src/algebra/monoid_algebra/basic.lean

@@ -12,6 +12,9 @@ import linear_algebra.finsupp
 /-!
 # Monoid algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 When the domain of a `finsupp` has a multiplicative or additive structure, we can define
 a convolution product. To mathematicians this structure is known as the "monoid algebra",
 i.e. the finite formal linear combinations over a given semiring of elements of the monoid.

src/algebra/monoid_algebra/support.lean

@@ -7,6 +7,9 @@ import algebra.monoid_algebra.basic
 
 /-!
 #  Lemmas about the support of a finitely supported function
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 universes u₁ u₂ u₃

src/algebra/polynomial/big_operators.lean

@@ -8,6 +8,9 @@ import data.polynomial.monic
 /-!
 # Lemmas for the interaction between polynomials and `∑` and `∏`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Recall that `∑` and `∏` are notation for `finset.sum` and `finset.prod` respectively.
 
 ## Main results

src/algebra/star/subalgebra.lean

@@ -12,6 +12,9 @@ import ring_theory.adjoin.basic
 /-!
 # Star subalgebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A *-subalgebra is a subalgebra of a *-algebra which is closed under *.
 
 The centralizer of a *-closed set is a *-subalgebra.

src/analysis/normed/group/ball_sphere.lean

@@ -8,6 +8,9 @@ import analysis.normed.group.basic
 /-!
 # Negation on spheres and balls
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `has_involutive_neg` instances for spheres, open balls, and closed balls in a
 semi normed group.
 -/

src/analysis/normed/group/basic.lean

@@ -14,6 +14,9 @@ import topology.sequences
 /-!
 # Normed (semi)groups
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define 10 classes:
 
 * `has_norm`, `has_nnnorm`: auxiliary classes endowing a type `α` with a function `norm : α → ℝ`

src/analysis/normed/group/completion.lean

@@ -10,6 +10,9 @@ import topology.metric_space.completion
 /-!
 # Completion of a normed group
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that the completion of a (semi)normed group is a normed group.
 
 ## Tags

src/analysis/normed/group/hom.lean

@@ -8,6 +8,9 @@ import analysis.normed.group.basic
 /-!
 # Normed groups homomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file gathers definitions and elementary constructions about bounded group homomorphisms
 between normed (abelian) groups (abbreviated to "normed group homs").
 

src/analysis/normed/group/hom_completion.lean

@@ -9,6 +9,9 @@ import analysis.normed.group.completion
 /-!
 # Completion of normed group homs
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given two (semi) normed groups `G` and `H` and a normed group hom `f : normed_add_group_hom G H`,
 we build and study a normed group hom
 `f.completion  : normed_add_group_hom (completion G) (completion H)` such that the diagram

src/analysis/normed/group/infinite_sum.lean

@@ -10,6 +10,9 @@ import topology.instances.nnreal
 /-!
 # Infinite sums in (semi)normed groups
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In a complete (semi)normed group,
 
 - `summable_iff_vanishing_norm`: a series `∑' i, f i` is summable if and only if for any `ε > 0`,

src/analysis/normed/group/seminorm.lean

@@ -9,6 +9,9 @@ import data.real.nnreal
 /-!
 # Group seminorms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines norms and seminorms in a group. A group seminorm is a function to the reals which
 is positive-semidefinite and subadditive. A norm further only maps zero to zero.
 

src/analysis/normed_space/indicator_function.lean

@@ -9,6 +9,9 @@ import algebra.indicator_function
 /-!
 # Indicator function and norm
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains a few simple lemmas about `set.indicator` and `norm`.
 
 ## Tags

src/analysis/subadditive.lean

@@ -9,6 +9,9 @@ import order.filter.archimedean
 /-!
 # Convergence of subadditive sequences
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A subadditive sequence `u : ℕ → ℝ` is a sequence satisfying `u (m + n) ≤ u m + u n` for all `m, n`.
 We define this notion as `subadditive u`, and prove in `subadditive.tendsto_lim` that, if `u n / n`
 is bounded below, then it converges to a limit (that we denote by `subadditive.lim` for

src/category_theory/abelian/images.lean

@@ -8,6 +8,9 @@ import category_theory.limits.shapes.kernels
 /-!
 # The abelian image and coimage.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In an abelian category we usually want the image of a morphism `f` to be defined as
 `kernel (cokernel.π f)`, and the coimage to be defined as `cokernel (kernel.ι f)`.
 

src/category_theory/abelian/non_preadditive.lean

@@ -12,6 +12,9 @@ import category_theory.preadditive.basic
 /-!
 # Every non_preadditive_abelian category is preadditive
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In mathlib, we define an abelian category as a preadditive category with a zero object,
 kernels and cokernels, products and coproducts and in which every monomorphism and epimorphis is
 normal.

src/category_theory/adjunction/comma.lean

@@ -10,6 +10,9 @@ import category_theory.structured_arrow
 /-!
 # Properties of comma categories relating to adjunctions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file shows that for a functor `G : D ⥤ C` the data of an initial object in each
 `structured_arrow` category on `G` is equivalent to a left adjoint to `G`, as well as the dual.
 

src/category_theory/concrete_category/reflects_isomorphisms.lean

@@ -7,6 +7,9 @@ import category_theory.concrete_category.basic
 import category_theory.functor.reflects_isomorphisms
 
 /-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A `forget₂ C D` forgetful functor between concrete categories `C` and `D`
 whose forgetful functors both reflect isomorphisms, itself reflects isomorphisms.
 -/

src/category_theory/is_connected.lean

@@ -11,6 +11,9 @@ import category_theory.category.ulift
 /-!
 # Connected category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Define a connected category as a _nonempty_ category for which every functor
 to a discrete category is isomorphic to the constant functor.
 

src/category_theory/limits/bicones.lean

@@ -9,6 +9,9 @@ import category_theory.fin_category
 /-!
 # Bicones
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a category `J`, a walking `bicone J` is a category whose objects are the objects of `J` and
 two extra vertices `bicone.left` and `bicone.right`. The morphisms are the morphisms of `J` and
 `left ⟶ j`, `right ⟶ j` for each `j : J` such that `⬝ ⟶ j` and `⬝ ⟶ k` commutes with each

src/category_theory/limits/comma.lean

@@ -12,6 +12,9 @@ import category_theory.structured_arrow
 /-!
 # Limits and colimits in comma categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We build limits in the comma category `comma L R` provided that the two source categories have
 limits and `R` preserves them.
 This is used to construct limits in the arrow category, structured arrow category and under

src/category_theory/limits/cone_category.lean

@@ -11,6 +11,9 @@ import category_theory.limits.shapes.equivalence
 /-!
 # Limits and the category of (co)cones
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This files contains results that stem from the limit API. For the definition and the category
 instance of `cone`, please refer to `category_theory/limits/cones.lean`.
 

src/category_theory/limits/constructions/equalizers.lean

@@ -12,6 +12,9 @@ import category_theory.limits.preserves.shapes.binary_products
 /-!
 # Constructing equalizers from pullbacks and binary products.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If a category has pullbacks and binary products, then it has equalizers.
 
 TODO: generalize universe

src/category_theory/limits/constructions/finite_products_of_binary_products.lean

@@ -12,6 +12,9 @@ import logic.equiv.fin
 /-!
 # Constructing finite products from binary products and terminal.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If a category has binary products and a terminal object then it has finite products.
 If a functor preserves binary products and the terminal object then it preserves finite products.
 

src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean

@@ -17,6 +17,9 @@ import category_theory.limits.constructions.binary_products
 /-!
 # Constructing limits from products and equalizers.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If a category has all products, and all equalizers, then it has all limits.
 Similarly, if it has all finite products, and all equalizers, then it has all finite limits.
 

src/category_theory/limits/essentially_small.lean

@@ -9,6 +9,9 @@ import category_theory.essentially_small
 /-!
 # Limits over essentially small indexing categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `C` has limits of size `w` and `J` is `w`-essentially small, then `C` has limits of shape `J`.
 
 -/

src/category_theory/limits/kan_extension.lean

@@ -11,6 +11,9 @@ import category_theory.structured_arrow
 
 # Kan extensions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the right and left Kan extensions of a functor.
 They exist under the assumption that the target category has enough limits
 resp. colimits.

src/category_theory/limits/lattice.lean

@@ -12,6 +12,9 @@ import category_theory.limits.shapes.finite_limits
 
 /-!
 # Limits in lattice categories are given by infimums and supremums.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 universes w u

src/category_theory/limits/mono_coprod.lean

@@ -11,6 +11,9 @@ import category_theory.limits.shapes.zero_morphisms
 
 # Categories where inclusions into coproducts are monomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `C` is a category, the class `mono_coprod C` expresses that left
 inclusions `A ⟶ A ⨿ B` are monomorphisms when `has_coproduct A B`
 is satisfied. If it is so, it is shown that right inclusions are

src/category_theory/limits/opposites.lean

@@ -11,6 +11,9 @@ import tactic.equiv_rw
 /-!
 # Limits in `C` give colimits in `Cᵒᵖ`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We also give special cases for (co)products,
 (co)equalizers, and pullbacks / pushouts.
 

src/category_theory/limits/preserves/filtered.lean

@@ -8,6 +8,9 @@ import category_theory.filtered
 
 /-!
 # Preservation of filtered colimits and cofiltered limits.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Typically forgetful functors from algebraic categories preserve filtered colimits
 (although not general colimits). See e.g. `algebra/category/Mon/filtered_colimits`.
 

src/category_theory/limits/preserves/shapes/biproducts.lean

@@ -9,6 +9,9 @@ import category_theory.limits.preserves.shapes.zero
 /-!
 # Preservation of biproducts
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the image of a (binary) bicone under a functor that preserves zero morphisms and define
 classes `preserves_biproduct` and `preserves_binary_biproduct`. We then
 

src/category_theory/limits/preserves/shapes/zero.lean

@@ -9,6 +9,9 @@ import category_theory.limits.shapes.zero_morphisms
 /-!
 # Preservation of zero objects and zero morphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the class `preserves_zero_morphisms` and show basic properties.
 
 ## Main results

src/category_theory/limits/shapes/biproducts.lean

@@ -10,6 +10,9 @@ import category_theory.limits.shapes.kernels
 /-!
 # Biproducts and binary biproducts
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce the notion of (finite) biproducts and binary biproducts.
 
 These are slightly unusual relative to the other shapes in the library,

src/category_theory/limits/shapes/finite_products.lean

@@ -9,6 +9,9 @@ import category_theory.limits.shapes.products
 /-!
 # Categories with finite (co)products
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Typeclasses representing categories with (co)products over finite indexing types.
 -/
 

src/category_theory/limits/shapes/functor_category.lean

@@ -9,6 +9,9 @@ import category_theory.limits.functor_category
 /-!
 # If `D` has finite (co)limits, so do the functor categories `C ⥤ D`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 These are boiler-plate instances, in their own file as neither import otherwise needs the other.
 -/
 

src/category_theory/limits/shapes/kernels.lean

@@ -8,6 +8,9 @@ import category_theory.limits.preserves.shapes.zero
 /-!
 # Kernels and cokernels
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In a category with zero morphisms, the kernel of a morphism `f : X ⟶ Y` is
 the equalizer of `f` and `0 : X ⟶ Y`. (Similarly the cokernel is the coequalizer.)
 

src/category_theory/limits/shapes/normal_mono/basic.lean

@@ -10,6 +10,9 @@ import category_theory.limits.preserves.basic
 /-!
 # Definitions and basic properties of normal monomorphisms and epimorphisms.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A normal monomorphism is a morphism that is the kernel of some other morphism.
 
 We give the construction `normal_mono → regular_mono` (`category_theory.normal_mono.regular_mono`)