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

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.products` * `algebra.homology.additive` * `algebra.homology.homotopy` * `algebraic_topology.alternating_face_map_complex` * `algebraic_topology.cech_nerve` * `algebraic_topology.dold_kan.faces` * `algebraic_topology.dold_kan.functor_n` * `algebraic_topology.dold_kan.homotopies` * `algebraic_topology.dold_kan.notations` * `algebraic_topology.dold_kan.p_infty` * `algebraic_topology.dold_kan.projections` * `analysis.normed_space.ball_action` * `category_theory.idempotents.homological_complex` * `category_theory.monad.adjunction` * `category_theory.monad.algebra` * `category_theory.monad.limits` * `category_theory.monad.products` * `category_theory.preadditive.eilenberg_moore` * `category_theory.preadditive.opposite` * `category_theory.sites.limits` * `data.complex.cardinality` * `data.matrix.notation` * `data.matrix.reflection` * `data.mv_polynomial.funext` * `linear_algebra.free_module.pid` * `linear_algebra.matrix.determinant` * `linear_algebra.matrix.mv_polynomial` * `linear_algebra.matrix.polynomial` * `linear_algebra.matrix.reindex` * `logic.equiv.transfer_instance` * `ring_theory.chain_of_divisors` * `ring_theory.localization.submodule` * `topology.metric_space.polish`
leanprover-community · Apr 21, 2023 · 86d1873 · 86d1873
1 parent e49764d
commit 86d1873
Show file tree

Hide file tree

Showing 33 changed files with 99 additions and 0 deletions.
diff --git a/src/algebra/category/Module/products.lean b/src/algebra/category/Module/products.lean
@@ -8,6 +8,9 @@ import algebra.category.Module.basic
 
 /-!
 # The concrete products in the category of modules are products in the categorical sense.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open category_theory

diff --git a/src/algebra/homology/additive.lean b/src/algebra/homology/additive.lean
@@ -10,6 +10,9 @@ import category_theory.preadditive.additive_functor
 /-!
 # Homology is an additive functor
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 When `V` is preadditive, `homological_complex V c` is also preadditive,
 and `homology_functor` is additive.
 

diff --git a/src/algebra/homology/homotopy.lean b/src/algebra/homology/homotopy.lean
@@ -9,6 +9,9 @@ import tactic.abel
 /-!
 # Chain homotopies
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define chain homotopies, and prove that homotopic chain maps induce the same map on homology.
 -/
 

diff --git a/src/algebraic_topology/alternating_face_map_complex.lean b/src/algebraic_topology/alternating_face_map_complex.lean
@@ -15,6 +15,9 @@ import tactic.equiv_rw
 
 # The alternating face map complex of a simplicial object in a preadditive category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct the alternating face map complex, as a
 functor `alternating_face_map_complex : simplicial_object C ⥤ chain_complex C ℕ`
 for any preadditive category `C`. For any simplicial object `X` in `C`,

diff --git a/src/algebraic_topology/cech_nerve.lean b/src/algebraic_topology/cech_nerve.lean
@@ -13,6 +13,9 @@ import category_theory.arrow
 
 # The Čech Nerve
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides a definition of the Čech nerve associated to an arrow, provided
 the base category has the correct wide pullbacks.
 

diff --git a/src/algebraic_topology/dold_kan/faces.lean b/src/algebraic_topology/dold_kan/faces.lean
@@ -11,6 +11,9 @@ import tactic.ring_exp
 
 # Study of face maps for the Dold-Kan correspondence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 TODO (@joelriou) continue adding the various files referenced below
 
 In this file, we obtain the technical lemmas that are used in the file

diff --git a/src/algebraic_topology/dold_kan/functor_n.lean b/src/algebraic_topology/dold_kan/functor_n.lean
@@ -10,6 +10,9 @@ import algebraic_topology.dold_kan.p_infty
 
 # Construction of functors N for the Dold-Kan correspondence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 TODO (@joelriou) continue adding the various files referenced below
 
 In this file, we construct functors `N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)`

diff --git a/src/algebraic_topology/dold_kan/homotopies.lean b/src/algebraic_topology/dold_kan/homotopies.lean
@@ -11,6 +11,9 @@ import algebraic_topology.dold_kan.notations
 
 # Construction of homotopies for the Dold-Kan correspondence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 TODO (@joelriou) continue adding the various files referenced below
 
 (The general strategy of proof of the Dold-Kan correspondence is explained

diff --git a/src/algebraic_topology/dold_kan/notations.lean b/src/algebraic_topology/dold_kan/notations.lean
@@ -10,6 +10,9 @@ import algebraic_topology.alternating_face_map_complex
 
 # Notations for the Dold-Kan equivalence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the notation `K[X] : chain_complex C ℕ` for the alternating face
 map complex of `(X : simplicial_object C)` where `C` is a preadditive category, as well
 as `N[X]` for the normalized subcomplex in the case `C` is an abelian category.

diff --git a/src/algebraic_topology/dold_kan/p_infty.lean b/src/algebraic_topology/dold_kan/p_infty.lean
@@ -12,6 +12,9 @@ import category_theory.idempotents.functor_extension
 
 # Construction of the projection `P_infty` for the Dold-Kan correspondence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 TODO (@joelriou) continue adding the various files referenced below
 
 In this file, we construct the projection `P_infty : K[X] ⟶ K[X]` by passing

diff --git a/src/algebraic_topology/dold_kan/projections.lean b/src/algebraic_topology/dold_kan/projections.lean
@@ -11,6 +11,9 @@ import category_theory.idempotents.basic
 
 # Construction of projections for the Dold-Kan correspondence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 TODO (@joelriou) continue adding the various files referenced below
 
 In this file, we construct endomorphisms `P q : K[X] ⟶ K[X]` for all

diff --git a/src/analysis/normed_space/ball_action.lean b/src/analysis/normed_space/ball_action.lean
@@ -9,6 +9,9 @@ import analysis.normed_space.basic
 /-!
 # Multiplicative actions of/on balls and spheres
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `E` be a normed vector space over a normed field `𝕜`. In this file we define the following
 multiplicative actions.
 

diff --git a/src/category_theory/idempotents/homological_complex.lean b/src/category_theory/idempotents/homological_complex.lean
@@ -10,6 +10,9 @@ import category_theory.idempotents.karoubi
 /-!
 # Idempotent completeness and homological complexes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains simplifications lemmas for categories
 `karoubi (homological_complex C c)` and the construction of an equivalence
 of categories `karoubi (homological_complex C c) ≌ homological_complex (karoubi C) c`.

diff --git a/src/category_theory/monad/adjunction.lean b/src/category_theory/monad/adjunction.lean
@@ -9,6 +9,9 @@ import category_theory.monad.algebra
 /-!
 # Adjunctions and monads
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We develop the basic relationship between adjunctions and monads.
 
 Given an adjunction `h : L ⊣ R`, we have `h.to_monad : monad C` and `h.to_comonad : comonad D`.

diff --git a/src/category_theory/monad/algebra.lean b/src/category_theory/monad/algebra.lean
@@ -10,6 +10,9 @@ import category_theory.functor.epi_mono
 /-!
 # Eilenberg-Moore (co)algebras for a (co)monad
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines Eilenberg-Moore (co)algebras for a (co)monad,
 and provides the category instance for them.
 

diff --git a/src/category_theory/monad/limits.lean b/src/category_theory/monad/limits.lean
@@ -10,6 +10,9 @@ import category_theory.limits.shapes.terminal
 /-!
 # Limits and colimits in the category of algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file shows that the forgetful functor `forget T : algebra T ⥤ C` for a monad `T : C ⥤ C`
 creates limits and creates any colimits which `T` preserves.
 This is used to show that `algebra T` has any limits which `C` has, and any colimits which `C` has

diff --git a/src/category_theory/monad/products.lean b/src/category_theory/monad/products.lean
@@ -10,6 +10,9 @@ import category_theory.limits.shapes.binary_products
 /-!
 # Algebras for the coproduct monad
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The functor `Y ↦ X ⨿ Y` forms a monad, whose category of monads is equivalent to the under category
 of `X`. Similarly, `Y ↦ X ⨯ Y` forms a comonad, whose category of comonads is equivalent to the
 over category of `X`.

diff --git a/src/category_theory/preadditive/eilenberg_moore.lean b/src/category_theory/preadditive/eilenberg_moore.lean
@@ -11,6 +11,9 @@ import category_theory.preadditive.additive_functor
 /-!
 # Preadditive structure on algebras over a monad
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `C` is a preadditive categories and `T` is an additive monad on `C` then `algebra T` is also
 preadditive. Dually, if `U` is an additive comonad on `C` then `coalgebra U` is preadditive as well.
 

diff --git a/src/category_theory/preadditive/opposite.lean b/src/category_theory/preadditive/opposite.lean
@@ -9,6 +9,9 @@ import logic.equiv.transfer_instance
 /-!
 # If `C` is preadditive, `Cᵒᵖ` has a natural preadditive structure.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 open opposite

diff --git a/src/category_theory/sites/limits.lean b/src/category_theory/sites/limits.lean
@@ -10,6 +10,9 @@ import category_theory.sites.sheafification
 
 # Limits and colimits of sheaves
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Limits
 
 We prove that the forgetful functor from `Sheaf J D` to presheaves creates limits.

diff --git a/src/data/complex/cardinality.lean b/src/data/complex/cardinality.lean
@@ -10,6 +10,9 @@ import data.real.cardinality
 /-!
 # The cardinality of the complex numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file shows that the complex numbers have cardinality continuum, i.e. `#ℂ = 𝔠`.
 -/
 

diff --git a/src/data/matrix/notation.lean b/src/data/matrix/notation.lean
@@ -11,6 +11,9 @@ import algebra.big_operators.fin
 /-!
 # Matrix and vector notation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file includes `simp` lemmas for applying operations in `data.matrix.basic` to values built out
 of the matrix notation `![a, b] = vec_cons a (vec_cons b vec_empty)` defined in
 `data.fin.vec_notation`.

diff --git a/src/data/matrix/reflection.lean b/src/data/matrix/reflection.lean
@@ -10,6 +10,9 @@ import data.fin.tuple.reflection
 /-!
 # Lemmas for concrete matrices `matrix (fin m) (fin n) α`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains alternative definitions of common operators on matrices that expand
 definitionally to the expected expression when evaluated on `!![]` notation.
 

diff --git a/src/data/mv_polynomial/funext.lean b/src/data/mv_polynomial/funext.lean
@@ -10,6 +10,9 @@ import ring_theory.polynomial.basic
 /-!
 ## Function extensionality for multivariate polynomials
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we show that two multivariate polynomials over an infinite integral domain are equal
 if they are equal upon evaluating them on an arbitrary assignment of the variables.
 

diff --git a/src/linear_algebra/free_module/pid.lean b/src/linear_algebra/free_module/pid.lean
@@ -11,6 +11,9 @@ import ring_theory.finiteness
 
 /-! # Free modules over PID
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A free `R`-module `M` is a module with a basis over `R`,
 equivalently it is an `R`-module linearly equivalent to `ι →₀ R` for some `ι`.
 

diff --git a/src/linear_algebra/matrix/determinant.lean b/src/linear_algebra/matrix/determinant.lean
@@ -17,6 +17,9 @@ import linear_algebra.pi
 /-!
 # Determinant of a matrix
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the determinant of a matrix, `matrix.det`, and its essential properties.
 
 ## Main definitions

diff --git a/src/linear_algebra/matrix/mv_polynomial.lean b/src/linear_algebra/matrix/mv_polynomial.lean
@@ -10,6 +10,9 @@ import data.mv_polynomial.comm_ring
 /-!
 # Matrices of multivariate polynomials
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we prove results about matrices over an mv_polynomial ring.
 In particular, we provide `matrix.mv_polynomial_X` which associates every entry of a matrix with a
 unique variable.

diff --git a/src/linear_algebra/matrix/polynomial.lean b/src/linear_algebra/matrix/polynomial.lean
@@ -10,6 +10,9 @@ import linear_algebra.matrix.determinant
 /-!
 # Matrices of polynomials and polynomials of matrices
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we prove results about matrices over a polynomial ring.
 In particular, we give results about the polynomial given by
 `det (t * I + A)`.

diff --git a/src/linear_algebra/matrix/reindex.lean b/src/linear_algebra/matrix/reindex.lean
@@ -9,6 +9,9 @@ import linear_algebra.matrix.determinant
 /-!
 # Changing the index type of a matrix
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file concerns the map `matrix.reindex`, mapping a `m` by `n` matrix
 to an `m'` by `n'` matrix, as long as `m ≃ m'` and `n ≃ n'`.
 

diff --git a/src/logic/equiv/transfer_instance.lean b/src/logic/equiv/transfer_instance.lean
@@ -10,6 +10,9 @@ import logic.equiv.defs
 /-!
 # Transfer algebraic structures across `equiv`s
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove theorems of the following form: if `β` has a
 group structure and `α ≃ β` then `α` has a group structure, and
 similarly for monoids, semigroups, rings, integral domains, fields and

diff --git a/src/ring_theory/chain_of_divisors.lean b/src/ring_theory/chain_of_divisors.lean
@@ -12,6 +12,9 @@ import algebra.gcd_monoid.basic
 
 # Chains of divisors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The results in this file show that in the monoid `associates M` of a `unique_factorization_monoid`
 `M`, an element `a` is an n-th prime power iff its set of divisors is a strictly increasing chain
 of length `n + 1`, meaning that we can find a strictly increasing bijection between `fin (n + 1)`

diff --git a/src/ring_theory/localization/submodule.lean b/src/ring_theory/localization/submodule.lean
@@ -10,6 +10,9 @@ import ring_theory.principal_ideal_domain
 /-!
 # Submodules in localizations of commutative rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Implementation notes
 
 See `src/ring_theory/localization/basic.lean` for a design overview.

diff --git a/src/topology/metric_space/polish.lean b/src/topology/metric_space/polish.lean
@@ -11,6 +11,9 @@ import analysis.normed.field.basic
 /-!
 # Polish spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A topological space is Polish if its topology is second-countable and there exists a compatible
 complete metric. This is the class of spaces that is well-behaved with respect to measure theory.
 In this file, we establish the basic properties of Polish spaces.