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

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.epi_mono` * `algebraic_topology.split_simplicial_object` * `analysis.asymptotics.specific_asymptotics` * `analysis.asymptotics.superpolynomial_decay` * `analysis.asymptotics.theta` * `analysis.box_integral.box.basic` * `analysis.locally_convex.balanced_core_hull` * `analysis.normed_space.extr` * `category_theory.limits.over` * `category_theory.sites.sheafification` * `linear_algebra.free_module.rank` * `order.filter.zero_and_bounded_at_filter` * `topology.category.Top.epi_mono`
leanprover-community · Apr 15, 2023 · 4f4a1c8 · 4f4a1c8
1 parent e95e4f9
commit 4f4a1c8
Show file tree

Hide file tree

Showing 13 changed files with 39 additions and 0 deletions.
diff --git a/src/algebra/category/Module/epi_mono.lean b/src/algebra/category/Module/epi_mono.lean
@@ -9,6 +9,9 @@ import algebra.category.Module.basic
 /-!
 # Monomorphisms in `Module R`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file shows that an `R`-linear map is a monomorphism in the category of `R`-modules
 if and only if it is injective, and similarly an epimorphism if and only if it is surjective.
 -/

diff --git a/src/algebraic_topology/split_simplicial_object.lean b/src/algebraic_topology/split_simplicial_object.lean
@@ -11,6 +11,9 @@ import category_theory.limits.shapes.finite_products
 
 # Split simplicial objects
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we introduce the notion of split simplicial object.
 If `C` is a category that has finite coproducts, a splitting
 `s : splitting X` of a simplical object `X` in `C` consists

diff --git a/src/analysis/asymptotics/specific_asymptotics.lean b/src/analysis/asymptotics/specific_asymptotics.lean
@@ -9,6 +9,9 @@ import analysis.asymptotics.asymptotics
 /-!
 # A collection of specific asymptotic results
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains specific lemmas about asymptotics which don't have their place in the general
 theory developped in `analysis.asymptotics.asymptotics`.
 -/

diff --git a/src/analysis/asymptotics/superpolynomial_decay.lean b/src/analysis/asymptotics/superpolynomial_decay.lean
@@ -11,6 +11,9 @@ import topology.algebra.order.liminf_limsup
 /-!
 # Super-Polynomial Function Decay
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines a predicate `asymptotics.superpolynomial_decay f` for a function satisfying
   one of following equivalent definitions (The definition is in terms of the first condition):
 

diff --git a/src/analysis/asymptotics/theta.lean b/src/analysis/asymptotics/theta.lean
@@ -8,6 +8,9 @@ import analysis.asymptotics.asymptotics
 /-!
 # Asymptotic equivalence up to a constant
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `asymptotics.is_Theta l f g` (notation: `f =Θ[l] g`) as
 `f =O[l] g ∧ g =O[l] f`, then prove basic properties of this equivalence relation.
 -/

diff --git a/src/analysis/box_integral/box/basic.lean b/src/analysis/box_integral/box/basic.lean
@@ -10,6 +10,9 @@ import topology.metric_space.basic
 /-!
 # Rectangular boxes in `ℝⁿ`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define rectangular boxes in `ℝⁿ`. As usual, we represent `ℝⁿ` as the type of
 functions `ι → ℝ` (usually `ι = fin n` for some `n`). When we need to interpret a box `[l, u]` as a
 set, we use the product `{x | ∀ i, l i < x i ∧ x i ≤ u i}` of half-open intervals `(l i, u i]`. We

diff --git a/src/analysis/locally_convex/balanced_core_hull.lean b/src/analysis/locally_convex/balanced_core_hull.lean
@@ -8,6 +8,9 @@ import analysis.locally_convex.basic
 /-!
 # Balanced Core and Balanced Hull
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 * `balanced_core`: The largest balanced subset of a set `s`.

diff --git a/src/analysis/normed_space/extr.lean b/src/analysis/normed_space/extr.lean
@@ -9,6 +9,9 @@ import topology.local_extr
 /-!
 # (Local) maximums in a normed space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove the following lemma, see `is_max_filter.norm_add_same_ray`. If `f : α → E` is
 a function such that `norm ∘ f` has a maximum along a filter `l` at a point `c` and `y` is a vector
 on the same ray as `f c`, then the function `λ x, ‖f x + y‖` has a maximul along `l` at `c`.

diff --git a/src/category_theory/limits/over.lean b/src/category_theory/limits/over.lean
@@ -13,6 +13,9 @@ import category_theory.limits.comma
 /-!
 # Limits and colimits in the over and under categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Show that the forgetful functor `forget X : over X ⥤ C` creates colimits, and hence `over X` has
 any colimits that `C` has (as well as the dual that `forget X : under X ⟶ C` creates limits).
 

diff --git a/src/category_theory/sites/sheafification.lean b/src/category_theory/sites/sheafification.lean
@@ -12,6 +12,9 @@ import category_theory.concrete_category.elementwise
 
 # Sheafification
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct the sheafification of a presheaf over a site `C` with values in `D` whenever
 `D` is a concrete category for which the forgetful functor preserves the appropriate (co)limits
 and reflects isomorphisms.

diff --git a/src/linear_algebra/free_module/rank.lean b/src/linear_algebra/free_module/rank.lean
@@ -10,6 +10,9 @@ import linear_algebra.dimension
 
 # Extra results about `module.rank`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains some extra results not in `linear_algebra.dimension`.
 
 -/

diff --git a/src/order/filter/zero_and_bounded_at_filter.lean b/src/order/filter/zero_and_bounded_at_filter.lean
@@ -10,6 +10,9 @@ import analysis.asymptotics.asymptotics
 /-!
 # Zero and Bounded at filter
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a filter `l` we define the notion of a function being `zero_at_filter` as well as being
 `bounded_at_filter`. Alongside this we construct the `submodule`, `add_submonoid` of functions
 that are `zero_at_filter`. Similarly, we construct the `submodule` and `subalgebra` of functions

diff --git a/src/topology/category/Top/epi_mono.lean b/src/topology/category/Top/epi_mono.lean
@@ -8,6 +8,9 @@ import topology.category.Top.adjunctions
 /-!
 # Epi- and monomorphisms in `Top`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file shows that a continuous function is an epimorphism in the category of topological spaces
 if and only if it is surjective, and that a continuous function is a monomorphism in the category of
 topological spaces if and only if it is injective.