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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Group.injective` * `algebra.category.Ring.basic` * `algebra.homology.augment` * `analysis.convex.contractible` * `analysis.convex.gauge` * `category_theory.abelian.homology` * `category_theory.subterminal` * `model_theory.bundled` * `model_theory.elementary_maps` * `model_theory.finitely_generated` * `model_theory.skolem` * `topology.category.Top.limits.cofiltered` * `topology.category.Top.limits.konig` * `topology.homotopy.contractible` * `topology.homotopy.path` * `topology.sheaves.abelian`
leanprover-community · May 15, 2023 · dbdf71c · dbdf71c
1 parent e9f2a83
commit dbdf71c
Show file tree

Hide file tree

Showing 16 changed files with 48 additions and 0 deletions.
diff --git a/src/algebra/category/Group/injective.lean b/src/algebra/category/Group/injective.lean
@@ -13,6 +13,9 @@ import ring_theory.principal_ideal_domain
 /-!
 # Injective objects in the category of abelian groups
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that divisible groups are injective object in category of (additive) abelian
 groups.
 

diff --git a/src/algebra/category/Ring/basic.lean b/src/algebra/category/Ring/basic.lean
@@ -11,6 +11,9 @@ import algebra.ring.equiv
 /-!
 # Category instances for semiring, ring, comm_semiring, and comm_ring.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce the bundled categories:
 * `SemiRing`
 * `Ring`

diff --git a/src/algebra/homology/augment.lean b/src/algebra/homology/augment.lean
@@ -7,6 +7,9 @@ import algebra.homology.single
 
 /-!
 # Augmentation and truncation of `ℕ`-indexed (co)chain complexes.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 noncomputable theory

diff --git a/src/analysis/convex/contractible.lean b/src/analysis/convex/contractible.lean
@@ -9,6 +9,9 @@ import topology.homotopy.contractible
 /-!
 # A convex set is contractible
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that a (star) convex set in a real topological vector space is a contractible
 topological space.
 -/

diff --git a/src/analysis/convex/gauge.lean b/src/analysis/convex/gauge.lean
@@ -12,6 +12,9 @@ import tactic.congrm
 /-!
 # The Minkowksi functional
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the Minkowski functional, aka gauge.
 
 The Minkowski functional of a set `s` is the function which associates each point to how much you

diff --git a/src/category_theory/abelian/homology.lean b/src/category_theory/abelian/homology.lean
@@ -9,6 +9,9 @@ import category_theory.limits.preserves.shapes.kernels
 import category_theory.limits.preserves.shapes.images
 
 /-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 
 The object `homology f g w`, where `w : f ≫ g = 0`, can be identified with either a
 cokernel or a kernel. The isomorphism with a cokernel is `homology_iso_cokernel_lift`, which

diff --git a/src/category_theory/subterminal.lean b/src/category_theory/subterminal.lean
@@ -10,6 +10,9 @@ import category_theory.subobject.mono_over
 /-!
 # Subterminal objects
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Subterminal objects are the objects which can be thought of as subobjects of the terminal object.
 In fact, the definition can be constructed to not require a terminal object, by defining `A` to be
 subterminal iff for any `Z`, there is at most one morphism `Z ⟶ A`.

diff --git a/src/model_theory/bundled.lean b/src/model_theory/bundled.lean
@@ -7,6 +7,9 @@ import model_theory.elementary_maps
 import category_theory.concrete_category.bundled
 /-!
 # Bundled First-Order Structures
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 This file bundles types together with their first-order structure.
 
 ## Main Definitions

diff --git a/src/model_theory/elementary_maps.lean b/src/model_theory/elementary_maps.lean
@@ -9,6 +9,9 @@ import model_theory.substructures
 /-!
 # Elementary Maps Between First-Order Structures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main Definitions
 * A `first_order.language.elementary_embedding` is an embedding that commutes with the
   realizations of formulas.

diff --git a/src/model_theory/finitely_generated.lean b/src/model_theory/finitely_generated.lean
@@ -7,6 +7,9 @@ import model_theory.substructures
 
 /-!
 # Finitely Generated First-Order Structures
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 This file defines what it means for a first-order (sub)structure to be finitely or countably
 generated, similarly to other finitely-generated objects in the algebra library.
 

diff --git a/src/model_theory/skolem.lean b/src/model_theory/skolem.lean
@@ -8,6 +8,9 @@ import model_theory.elementary_maps
 /-!
 # Skolem Functions and Downward Löwenheim–Skolem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main Definitions
 * `first_order.language.skolem₁` is a language consisting of Skolem functions for another language.
 

diff --git a/src/topology/category/Top/limits/cofiltered.lean b/src/topology/category/Top/limits/cofiltered.lean
@@ -8,6 +8,9 @@ import topology.category.Top.limits.basic
 /-!
 # Cofiltered limits in Top.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a *compatible* collection of topological bases for the factors in a cofiltered limit
 which contain `set.univ` and are closed under intersections, the induced *naive* collection
 of sets in the limit is, in fact, a topological basis.

diff --git a/src/topology/category/Top/limits/konig.lean b/src/topology/category/Top/limits/konig.lean
@@ -8,6 +8,9 @@ import topology.category.Top.limits.basic
 /-!
 # Topological Kőnig's lemma
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A topological version of Kőnig's lemma is that the inverse limit of nonempty compact Hausdorff
 spaces is nonempty.  (Note: this can be generalized further to inverse limits of nonempty compact
 T0 spaces, where all the maps are closed maps; see [Stone1979] --- however there is an erratum

diff --git a/src/topology/homotopy/contractible.lean b/src/topology/homotopy/contractible.lean
@@ -10,6 +10,9 @@ import topology.homotopy.equiv
 /-!
 # Contractible spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we define `contractible_space`, a space that is homotopy equivalent to `unit`.
 -/
 

diff --git a/src/topology/homotopy/path.lean b/src/topology/homotopy/path.lean
@@ -11,6 +11,9 @@ import analysis.convex.basic
 /-!
 # Homotopy between paths
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we define a `homotopy` between two `path`s. In addition, we define a relation
 `homotopic` on `path`s, and prove that it is an equivalence relation.
 

diff --git a/src/topology/sheaves/abelian.lean b/src/topology/sheaves/abelian.lean
@@ -11,6 +11,9 @@ import category_theory.sites.left_exact
 
 /-!
 # Category of sheaves is abelian
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Let `C, D` be categories and `J` be a grothendieck topology on `C`, when `D` is abelian and
 sheafification is possible in `C`, `Sheaf J D` is abelian as well (`Sheaf_is_abelian`).