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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following PRs: * `algebra.order.sub.canonical`: leanprover-community/mathlib4#814 * `category_theory.category.Rel`: leanprover-community/mathlib4#822 * `category_theory.category.basic`: leanprover-community/mathlib4#749 * `category_theory.functor.basic`: leanprover-community/mathlib4#749 * `category_theory.functor.category`: leanprover-community/mathlib4#749 * `category_theory.functor.functorial`: leanprover-community/mathlib4#822 * `category_theory.isomorphism`: leanprover-community/mathlib4#749 * `category_theory.natural_transformation`: leanprover-community/mathlib4#749 * `category_theory.thin`: leanprover-community/mathlib4#822 * `combinatorics.quiver.basic`: leanprover-community/mathlib4#749 * `combinatorics.quiver.path`: leanprover-community/mathlib4#811 * `data.psigma.order`: leanprover-community/mathlib4#815 * `data.stream.defs`: leanprover-community/mathlib4#665 * `order.boolean_algebra`: leanprover-community/mathlib4#794 * `order.heyting.basic`: leanprover-community/mathlib4#793 * `order.rel_iso.group`: leanprover-community/mathlib4#813
leanprover-community · Dec 3, 2022 · 308f6d0 · 308f6d0
1 parent e469260
commit 308f6d0
Show file tree

Hide file tree

Showing 16 changed files with 64 additions and 0 deletions.
diff --git a/src/algebra/order/sub/canonical.lean b/src/algebra/order/sub/canonical.lean
@@ -8,6 +8,10 @@ import algebra.order.sub.defs
 
 /-!
 # Lemmas about subtraction in canonically ordered monoids
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/814
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 variables {α : Type*}

diff --git a/src/category_theory/category/Rel.lean b/src/category_theory/category/Rel.lean
@@ -6,6 +6,10 @@ Authors: Scott Morrison
 import category_theory.category.basic
 
 /-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/822
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The category of types with binary relations as morphisms.
 -/
 

diff --git a/src/category_theory/category/basic.lean b/src/category_theory/category/basic.lean
@@ -8,6 +8,10 @@ import combinatorics.quiver.basic
 /-!
 # Categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/749
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Defines a category, as a type class parametrised by the type of objects.
 
 ## Notations

diff --git a/src/category_theory/functor/basic.lean b/src/category_theory/functor/basic.lean
@@ -9,6 +9,10 @@ import category_theory.category.basic
 /-!
 # Functors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/749
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Defines a functor between categories, extending a `prefunctor` between quivers.
 
 Introduces notation `C ⥤ D` for the type of all functors from `C` to `D`.

diff --git a/src/category_theory/functor/category.lean b/src/category_theory/functor/category.lean
@@ -9,6 +9,10 @@ import category_theory.isomorphism
 /-!
 # The category of functors and natural transformations between two fixed categories.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/749
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We provide the category instance on `C ⥤ D`, with morphisms the natural transformations.
 
 ## Universes

diff --git a/src/category_theory/functor/functorial.lean b/src/category_theory/functor/functorial.lean
@@ -7,6 +7,10 @@ import category_theory.functor.basic
 
 /-!
 # Unbundled functors, as a typeclass decorating the object-level function.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/822
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 namespace category_theory

diff --git a/src/category_theory/isomorphism.lean b/src/category_theory/isomorphism.lean
@@ -8,6 +8,10 @@ import category_theory.functor.basic
 /-!
 # Isomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/749
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines isomorphisms between objects of a category.
 
 ## Main definitions

diff --git a/src/category_theory/natural_transformation.lean b/src/category_theory/natural_transformation.lean
@@ -8,6 +8,10 @@ import category_theory.functor.basic
 /-!
 # Natural transformations
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/749
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Defines natural transformations between functors.
 
 A natural transformation `α : nat_trans F G` consists of morphisms `α.app X : F.obj X ⟶ G.obj X`,

diff --git a/src/category_theory/thin.lean b/src/category_theory/thin.lean
@@ -9,6 +9,10 @@ import category_theory.isomorphism
 /-!
 # Thin categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/822
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A thin category (also known as a sparse category) is a category with at most one morphism between
 each pair of objects.
 

diff --git a/src/combinatorics/quiver/basic.lean b/src/combinatorics/quiver/basic.lean
@@ -8,6 +8,10 @@ import data.opposite
 /-!
 # Quivers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/749
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This module defines quivers. A quiver on a type `V` of vertices assigns to every
 pair `a b : V` of vertices a type `a ⟶ b` of arrows from `a` to `b`. This
 is a very permissive notion of directed graph.

diff --git a/src/combinatorics/quiver/path.lean b/src/combinatorics/quiver/path.lean
@@ -9,6 +9,10 @@ import logic.lemmas
 /-!
 # Paths in quivers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/811
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a quiver `V`, we define the type of paths from `a : V` to `b : V` as an inductive
 family. We define composition of paths and the action of prefunctors on paths.
 -/

diff --git a/src/data/psigma/order.lean b/src/data/psigma/order.lean
@@ -9,6 +9,10 @@ import order.bounded_order
 /-!
 # Lexicographic order on a sigma type
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/815
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the lexicographic order on `Σₗ' i, α i`. `a` is less than `b` if its summand is
 strictly less than the summand of `b` or they are in the same summand and `a` is less than `b`
 there.

diff --git a/src/data/stream/defs.lean b/src/data/stream/defs.lean
@@ -7,6 +7,10 @@ Authors: Leonardo de Moura
 /-!
 # Definition of `stream` and functions on streams
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/665
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A stream `stream α` is an infinite sequence of elements of `α`. One can also think about it as an
 infinite list. In this file we define `stream` and some functions that take and/or return streams.
 -/

diff --git a/src/order/boolean_algebra.lean b/src/order/boolean_algebra.lean
@@ -8,6 +8,10 @@ import order.heyting.basic
 /-!
 # (Generalized) Boolean algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/794
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A Boolean algebra is a bounded distributive lattice with a complement operator. Boolean algebras
 generalize the (classical) logic of propositions and the lattice of subsets of a set.
 

diff --git a/src/order/heyting/basic.lean b/src/order/heyting/basic.lean
@@ -8,6 +8,10 @@ import order.prop_instances
 /-!
 # Heyting algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/793
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines Heyting, co-Heyting and bi-Heyting algebras.
 
 An Heyting algebra is a bounded distributive lattice with an implication operation `⇨` such that

diff --git a/src/order/rel_iso/group.lean b/src/order/rel_iso/group.lean
@@ -8,6 +8,10 @@ import order.rel_iso.basic
 
 /-!
 # Relation isomorphisms form a group
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/813
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 variables {α: Type*}