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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.algebra.operations`
* `algebra.algebra.restrict_scalars`
* `algebra.lie.non_unital_non_assoc_algebra`
* `algebra.order.algebra`
* `algebra.star.module`
* `algebra.star.star_alg_hom`
* `category_theory.adjunction.evaluation`
* `category_theory.adjunction.limits`
* `category_theory.category.pairwise`
* `category_theory.concrete_category.basic`
* `category_theory.limits.constructions.binary_products`
* `category_theory.limits.constructions.epi_mono`
* `category_theory.limits.constructions.pullbacks`
* `category_theory.limits.creates`
* `category_theory.limits.exact_functor`
* `category_theory.limits.full_subcategory`
* `category_theory.limits.functor_category`
* `category_theory.limits.preserves.finite`
* `category_theory.limits.preserves.shapes.binary_products`
* `category_theory.limits.preserves.shapes.equalizers`
* `category_theory.limits.preserves.shapes.products`
* `category_theory.limits.preserves.shapes.pullbacks`
* `category_theory.limits.preserves.shapes.terminal`
* `category_theory.limits.shapes.binary_products`
* `category_theory.limits.shapes.disjoint_coproduct`
* `category_theory.limits.shapes.equalizers`
* `category_theory.limits.shapes.equivalence`
* `category_theory.limits.shapes.finite_limits`
* `category_theory.limits.shapes.images`
* `category_theory.limits.shapes.products`
* `category_theory.limits.shapes.pullbacks`
* `category_theory.limits.shapes.regular_mono`
* `category_theory.limits.shapes.split_coequalizer`
* `category_theory.limits.shapes.strict_initial`
* `category_theory.limits.shapes.terminal`
* `category_theory.limits.shapes.zero_objects`
* `category_theory.limits.unit`
* `category_theory.limits.yoneda`
* `category_theory.over`
* `category_theory.path_category`
* `category_theory.quotient`
* `category_theory.sites.sieves`
* `category_theory.structured_arrow`
* `combinatorics.simple_graph.hasse`
* `combinatorics.simple_graph.metric`
* `combinatorics.simple_graph.prod`
* `combinatorics.simple_graph.regularity.energy`
* `combinatorics.simple_graph.trails`
* `control.lawful_fix`
* `group_theory.solvable`
* `linear_algebra.affine_space.affine_map`
* `linear_algebra.dfinsupp`
* `topology.algebra.field`
* `topology.algebra.group_completion`
* `topology.algebra.infinite_sum.basic`
* `topology.algebra.infinite_sum.order`
* `topology.algebra.infinite_sum.real`
* `topology.algebra.infinite_sum.ring`
* `topology.algebra.order.field`
* `topology.algebra.order.upper_lower`
* `topology.algebra.ring.basic`
* `topology.algebra.uniform_mul_action`
* `topology.instances.int`
* `topology.instances.nat`
* `topology.instances.nnreal`
* `topology.instances.rat`
* `topology.instances.real`
* `topology.locally_constant.algebra`
* `topology.metric_space.algebra`
* `topology.metric_space.antilipschitz`
* `topology.metric_space.basic`
* `topology.metric_space.emetric_paracompact`
* `topology.metric_space.emetric_space`
* `topology.metric_space.equicontinuity`
* `topology.metric_space.infsep`
* `topology.metric_space.lipschitz`
* `topology.metric_space.metric_separated`
* `topology.metric_space.shrinking_lemma`
* `topology.sequences`

src/algebra/algebra/operations.lean

@@ -17,6 +17,9 @@ import group_theory.group_action.sub_mul_action.pointwise
 /-!
 # Multiplication and division of submodules of an algebra.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 An interface for multiplication and division of sub-R-modules of an R-algebra A is developed.
 
 ## Main definitions

src/algebra/algebra/restrict_scalars.lean

@@ -9,6 +9,9 @@ import algebra.algebra.tower
 
 # The `restrict_scalars` type alias
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 See the documentation attached to the `restrict_scalars` definition for advice on how and when to
 use this type alias. As described there, it is often a better choice to use the `is_scalar_tower`
 typeclass instead.

src/algebra/lie/non_unital_non_assoc_algebra.lean

@@ -9,6 +9,9 @@ import algebra.lie.basic
 /-!
 # Lie algebras as non-unital, non-associative algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The definition of Lie algebras uses the `has_bracket` typeclass for multiplication whereas we have a
 separate `has_mul` typeclass used for general algebras.
 

src/algebra/order/algebra.lean

@@ -10,6 +10,9 @@ import algebra.order.smul
 /-!
 # Ordered algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 An ordered algebra is an ordered semiring, which is an algebra over an ordered commutative semiring,
 for which scalar multiplication is "compatible" with the two orders.
 

src/algebra/star/module.lean

@@ -10,6 +10,9 @@ import linear_algebra.prod
 /-!
 # The star operation, bundled as a star-linear equiv
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define `star_linear_equiv`, which is the star operation bundled as a star-linear map.
 It is defined on a star algebra `A` over the base ring `R`.
 

src/algebra/star/star_alg_hom.lean

@@ -11,6 +11,9 @@ import algebra.algebra.prod
 /-!
 # Morphisms of star algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines morphisms between `R`-algebras (unital or non-unital) `A` and `B` where both
 `A` and `B` are equipped with a `star` operation. These morphisms, namely `star_alg_hom` and
 `non_unital_star_alg_hom` are direct extensions of their non-`star`red counterparts with a field

src/category_theory/adjunction/evaluation.lean

@@ -11,6 +11,9 @@ import category_theory.functor.epi_mono
 
 # Adjunctions involving evaluation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We show that evaluation of functors have adjoints, given the existence of (co)products.
 
 -/

src/category_theory/adjunction/limits.lean

@@ -9,6 +9,9 @@ import category_theory.limits.creates
 /-!
 # Adjunctions and limits
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A left adjoint preserves colimits (`category_theory.adjunction.left_adjoint_preserves_colimits`),
 and a right adjoint preserves limits (`category_theory.adjunction.right_adjoint_preserves_limits`).
 

src/category_theory/category/pairwise.lean

@@ -10,6 +10,9 @@ import category_theory.limits.is_limit
 /-!
 # The category of "pairwise intersections".
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given `ι : Type v`, we build the diagram category `pairwise ι`
 with objects `single i` and `pair i j`, for `i j : ι`,
 whose only non-identity morphisms are

src/category_theory/concrete_category/basic.lean

@@ -10,6 +10,9 @@ import category_theory.limits.constructions.epi_mono
 /-!
 # Concrete categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A concrete category is a category `C` with a fixed faithful functor
 `forget : C ⥤ Type*`.  We define concrete categories using `class
 concrete_category`.  In particular, we impose no restrictions on the

src/category_theory/limits/constructions/binary_products.lean

@@ -12,6 +12,9 @@ import category_theory.limits.preserves.shapes.terminal
 /-!
 # Constructing binary product from pullbacks and terminal object.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The product is the pullback over the terminal objects. In particular, if a category
 has pullbacks and a terminal object, then it has binary products.
 

src/category_theory/limits/constructions/epi_mono.lean

@@ -10,6 +10,9 @@ import category_theory.limits.preserves.shapes.pullbacks
 /-!
 # Relating monomorphisms and epimorphisms to limits and colimits
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `F` preserves (resp. reflects) pullbacks, then it preserves (resp. reflects) monomorphisms.
 
 We also provide the dual version for epimorphisms.

src/category_theory/limits/constructions/pullbacks.lean

@@ -10,6 +10,9 @@ import category_theory.limits.shapes.pullbacks
 /-!
 # Constructing pullbacks from binary products and equalizers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If a category as binary products and equalizers, then it has pullbacks.
 Also, if a category has binary coproducts and coequalizers, then it has pushouts
 -/

src/category_theory/limits/creates.lean

@@ -8,6 +8,9 @@ import category_theory.limits.preserves.basic
 /-!
 # Creating (co)limits
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We say that `F` creates limits of `K` if, given any limit cone `c` for `K ⋙ F`
 (i.e. below) we can lift it to a cone "above", and further that `F` reflects
 limits for `K`.

src/category_theory/limits/exact_functor.lean

@@ -8,6 +8,9 @@ import category_theory.limits.preserves.finite
 /-!
 # Bundled exact functors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We say that a functor `F` is left exact if it preserves finite limits, it is right exact if it
 preserves finite colimits, and it is exact if it is both left exact and right exact.
 

src/category_theory/limits/full_subcategory.lean

@@ -8,6 +8,9 @@ import category_theory.limits.creates
 /-!
 # Limits in full subcategories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce the notion of a property closed under taking limits and show that if `P` is closed
 under taking limits, then limits in `full_subcategory P` can be constructed from limits in `C`.
 More precisely, the inclusion creates such limits.

src/category_theory/limits/functor_category.lean

@@ -8,6 +8,9 @@ import category_theory.limits.preserves.limits
 /-!
 # (Co)limits in functor categories.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We show that if `D` has limits, then the functor category `C ⥤ D` also has limits
 (`category_theory.limits.functor_category_has_limits`),
 and the evaluation functors preserve limits

src/category_theory/limits/preserves/finite.lean

@@ -9,6 +9,9 @@ import category_theory.fin_category
 /-!
 # Preservation of finite (co)limits.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 These functors are also known as left exact (flat) or right exact functors when the categories
 involved are abelian, or more generally, finitely (co)complete.
 

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

@@ -9,6 +9,9 @@ import category_theory.limits.preserves.basic
 /-!
 # Preserving binary products
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Constructions to relate the notions of preserving binary products and reflecting binary products
 to concrete binary fans.
 

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

@@ -9,6 +9,9 @@ import category_theory.limits.preserves.basic
 /-!
 # Preserving (co)equalizers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Constructions to relate the notions of preserving (co)equalizers and reflecting (co)equalizers
 to concrete (co)forks.
 

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

@@ -9,6 +9,9 @@ import category_theory.limits.preserves.basic
 /-!
 # Preserving products
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Constructions to relate the notions of preserving products and reflecting products
 to concrete fans.
 

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

@@ -9,6 +9,9 @@ import category_theory.limits.preserves.basic
 /-!
 # Preserving pullbacks
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Constructions to relate the notions of preserving pullbacks and reflecting pullbacks to concrete
 pullback cones.
 

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

@@ -9,6 +9,9 @@ import category_theory.limits.preserves.basic
 /-!
 # Preserving terminal object
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Constructions to relate the notions of preserving terminal objects and reflecting terminal objects
 to concrete objects.
 

src/category_theory/limits/shapes/binary_products.lean

@@ -11,6 +11,9 @@ import category_theory.over
 /-!
 # Binary (co)products
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define a category `walking_pair`, which is the index category
 for a binary (co)product diagram. A convenience method `pair X Y`
 constructs the functor from the walking pair, hitting the given objects.

src/category_theory/limits/shapes/disjoint_coproduct.lean

@@ -9,6 +9,9 @@ import category_theory.limits.shapes.pullbacks
 /-!
 # Disjoint coproducts
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Defines disjoint coproducts: coproducts where the intersection is initial and the coprojections
 are monic.
 Shows that a category with disjoint coproducts is `initial_mono_class`.

src/category_theory/limits/shapes/equalizers.lean

@@ -9,6 +9,9 @@ import category_theory.limits.has_limits
 /-!
 # Equalizers and coequalizers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines (co)equalizers as special cases of (co)limits.
 
 An equalizer is the categorical generalization of the subobject {a ∈ A | f(a) = g(a)} known

src/category_theory/limits/shapes/equivalence.lean

@@ -9,6 +9,9 @@ import category_theory.limits.shapes.terminal
 /-!
 # Transporting existence of specific limits across equivalences
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 For now, we only treat the case of initial and terminal objects, but other special shapes can be
 added in the future.
 -/

src/category_theory/limits/shapes/finite_limits.lean

@@ -13,6 +13,9 @@ import data.fintype.option
 /-!
 # Categories with finite limits.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A typeclass for categories with all finite (co)limits.
 -/
 

src/category_theory/limits/shapes/images.lean

@@ -10,6 +10,9 @@ import category_theory.limits.shapes.strong_epi
 /-!
 # Categorical images
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the categorical image of `f` as a factorisation `f = e ≫ m` through a monomorphism `m`,
 so that `m` factors through the `m'` in any other such factorisation.
 

src/category_theory/limits/shapes/products.lean

@@ -9,6 +9,9 @@ import category_theory.discrete_category
 /-!
 # Categorical (co)products
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines (co)products as special cases of (co)limits.
 
 A product is the categorical generalization of the object `Π i, f i` where `f : ι → C`. It is a

src/category_theory/limits/shapes/pullbacks.lean

@@ -9,6 +9,9 @@ import category_theory.limits.shapes.binary_products
 /-!
 # Pullbacks
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define a category `walking_cospan` (resp. `walking_span`), which is the index category
 for the given data for a pullback (resp. pushout) diagram. Convenience methods `cospan f g`
 and `span f g` construct functors from the walking (co)span, hitting the given morphisms.

src/category_theory/limits/shapes/regular_mono.lean

@@ -10,6 +10,9 @@ import category_theory.limits.shapes.equalizers
 /-!
 # Definitions and basic properties of regular monomorphisms and epimorphisms.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A regular monomorphism is a morphism that is the equalizer of some parallel pair.
 
 We give the constructions

src/category_theory/limits/shapes/split_coequalizer.lean

@@ -8,6 +8,9 @@ import category_theory.limits.shapes.equalizers
 /-!
 # Split coequalizers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define what it means for a triple of morphisms `f g : X ⟶ Y`, `π : Y ⟶ Z` to be a split
 coequalizer: there is a section `s` of `π` and a section `t` of `g`, which additionally satisfy
 `t ≫ f = π ≫ s`.

src/category_theory/limits/shapes/strict_initial.lean

@@ -10,6 +10,9 @@ import category_theory.limits.shapes.binary_products
 /-!
 # Strict initial objects
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file sets up the basic theory of strict initial objects: initial objects where every morphism
 to it is an isomorphism. This generalises a property of the empty set in the category of sets:
 namely that the only function to the empty set is from itself.

src/category_theory/limits/shapes/terminal.lean

@@ -11,6 +11,9 @@ import category_theory.category.preorder
 /-!
 # Initial and terminal objects in a category.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## References
 * [Stacks: Initial and final objects](https://stacks.math.columbia.edu/tag/002B)
 -/

src/category_theory/limits/shapes/zero_objects.lean

@@ -8,6 +8,9 @@ import category_theory.limits.shapes.terminal
 /-!
 # Zero objects
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A category "has a zero object" if it has an object which is both initial and terminal. Having a
 zero object provides zero morphisms, as the unique morphisms factoring through the zero object;
 see `category_theory.limits.shapes.zero_morphisms`.

src/category_theory/limits/unit.lean

@@ -10,6 +10,9 @@ import category_theory.limits.has_limits
 /-!
 # `discrete punit` has limits and colimits
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Mostly for the sake of constructing trivial examples, we show all (co)cones into `discrete punit`
 are (co)limit (co)cones. We also show that such (co)cones exist, and that `discrete punit` has all
 (co)limits.

src/category_theory/limits/yoneda.lean

@@ -9,6 +9,9 @@ import tactic.assert_exists
 /-!
 # Limit properties relating to the (co)yoneda embedding.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We calculate the colimit of `Y ↦ (X ⟶ Y)`, which is just `punit`.
 (This is used in characterising cofinal functors.)
 

src/category_theory/over.lean

@@ -11,6 +11,9 @@ import category_theory.functor.epi_mono
 /-!
 # Over and under categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Over (and under) categories are special cases of comma categories.
 * If `L` is the identity functor and `R` is a constant functor, then `comma L R` is the "slice" or
   "over" category over the object `R` maps to.

src/category_theory/path_category.lean

@@ -9,6 +9,9 @@ import combinatorics.quiver.path
 
 /-!
 # The category paths on a quiver.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 When `C` is a quiver, `paths C` is the category of paths.
 
 ## When the quiver is itself a category