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

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.tannaka` * `algebra.homology.homotopy_category` * `algebra.homology.short_exact.preadditive` * `algebraic_topology.dold_kan.equivalence_additive` * `algebraic_topology.dold_kan.functor_gamma` * `algebraic_topology.dold_kan.gamma_comp_n` * `algebraic_topology.dold_kan.homotopy_equivalence` * `algebraic_topology.dold_kan.n_comp_gamma` * `algebraic_topology.dold_kan.normalized` * `analysis.box_integral.partition.basic` * `analysis.box_integral.partition.split` * `analysis.convex.caratheodory` * `analysis.convex.combination` * `analysis.convex.independent` * `analysis.convex.jensen` * `analysis.convex.join` * `analysis.convex.normed` * `analysis.convex.simplicial_complex.basic` * `analysis.convex.topology` * `analysis.locally_convex.bounded` * `analysis.normed_space.conformal_linear_map` * `analysis.normed_space.linear_isometry` * `analysis.normed_space.star.basic` * `analysis.seminorm` * `category_theory.abelian.opposite` * `category_theory.abelian.subobject` * `category_theory.adjunction.adjoint_functor_theorems` * `category_theory.concrete_category.unbundled_hom` * `category_theory.generator` * `category_theory.limits.constructions.weakly_initial` * `category_theory.limits.preserves.functor_category` * `category_theory.limits.presheaf` * `category_theory.limits.shapes.wide_equalizers` * `category_theory.linear.yoneda` * `category_theory.preadditive.generator` * `category_theory.preadditive.yoneda.basic` * `category_theory.subobject.comma` * `data.real.hyperreal` * `data.string.defs` * `linear_algebra.affine_space.basis` * `linear_algebra.finite_dimensional` * `linear_algebra.matrix.absolute_value` * `linear_algebra.matrix.circulant` * `linear_algebra.matrix.nonsingular_inverse` * `linear_algebra.vandermonde` * `topology.extremally_disconnected` * `topology.instances.matrix`
leanprover-community · Apr 27, 2023 · 9d2f074 · 9d2f074
1 parent 57911c5
commit 9d2f074
Show file tree

Hide file tree

Showing 47 changed files with 144 additions and 3 deletions.
diff --git a/src/algebra/category/Module/tannaka.lean b/src/algebra/category/Module/tannaka.lean
@@ -9,6 +9,9 @@ import linear_algebra.span
 /-!
 # Tannaka duality for rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A ring `R` is equivalent to
 the endomorphisms of the additive forgetful functor `Module R ⥤ AddCommGroup`.
 

diff --git a/src/algebra/homology/homotopy_category.lean b/src/algebra/homology/homotopy_category.lean
@@ -9,6 +9,9 @@ import category_theory.quotient
 /-!
 # The homotopy category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 `homotopy_category V c` gives the category of chain complexes of shape `c` in `V`,
 with chain maps identified when they are homotopic.
 -/

diff --git a/src/algebra/homology/short_exact/preadditive.lean b/src/algebra/homology/short_exact/preadditive.lean
@@ -9,6 +9,9 @@ import category_theory.preadditive.additive_functor
 /-!
 # Short exact sequences, and splittings.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 `short_exact f g` is the proposition that `0 ⟶ A -f⟶ B -g⟶ C ⟶ 0` is an exact sequence.
 
 We define when a short exact sequence is left-split, right-split, and split.

diff --git a/src/algebraic_topology/dold_kan/equivalence_additive.lean b/src/algebraic_topology/dold_kan/equivalence_additive.lean
@@ -6,7 +6,10 @@ Authors: Joël Riou
 
 import algebraic_topology.dold_kan.n_comp_gamma
 
-/-! The Dold-Kan equivalence for additive categories.
+/-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+ The Dold-Kan equivalence for additive categories.
 
 This file defines `preadditive.dold_kan.equivalence` which is the equivalence
 of categories `karoubi (simplicial_object C) ≌ karoubi (chain_complex C ℕ)`.

diff --git a/src/algebraic_topology/dold_kan/functor_gamma.lean b/src/algebraic_topology/dold_kan/functor_gamma.lean
@@ -10,6 +10,9 @@ import algebraic_topology.dold_kan.split_simplicial_object
 
 # Construction of the inverse functor of the Dold-Kan equivalence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 
 In this file, we construct the functor `Γ₀ : chain_complex C ℕ ⥤ simplicial_object C`
 which shall be the inverse functor of the Dold-Kan equivalence in the case of abelian categories,

diff --git a/src/algebraic_topology/dold_kan/gamma_comp_n.lean b/src/algebraic_topology/dold_kan/gamma_comp_n.lean
@@ -7,7 +7,10 @@ Authors: Joël Riou
 import algebraic_topology.dold_kan.functor_gamma
 import category_theory.idempotents.homological_complex
 
-/-! The counit isomorphism of the Dold-Kan equivalence
+/-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+ The counit isomorphism of the Dold-Kan equivalence
 
 The purpose of this file is to construct natural isomorphisms
 `N₁Γ₀ : Γ₀ ⋙ N₁ ≅ to_karoubi (chain_complex C ℕ)`

diff --git a/src/algebraic_topology/dold_kan/homotopy_equivalence.lean b/src/algebraic_topology/dold_kan/homotopy_equivalence.lean
@@ -10,6 +10,9 @@ import algebraic_topology.dold_kan.normalized
 
 # The normalized Moore complex and the alternating face map complex are homotopy equivalent
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, when the category `A` is abelian, we obtain the homotopy equivalence
 `homotopy_equiv_normalized_Moore_complex_alternating_face_map_complex` between the
 normalized Moore complex and the alternating face map complex of a simplicial object in `A`.

diff --git a/src/algebraic_topology/dold_kan/n_comp_gamma.lean b/src/algebraic_topology/dold_kan/n_comp_gamma.lean
@@ -7,7 +7,10 @@ Authors: Joël Riou
 import algebraic_topology.dold_kan.gamma_comp_n
 import algebraic_topology.dold_kan.n_reflects_iso
 
-/-! The unit isomorphism of the Dold-Kan equivalence
+/-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+ The unit isomorphism of the Dold-Kan equivalence
 
 In order to construct the unit isomorphism of the Dold-Kan equivalence,
 we first construct natural transformations

diff --git a/src/algebraic_topology/dold_kan/normalized.lean b/src/algebraic_topology/dold_kan/normalized.lean
@@ -10,6 +10,9 @@ import algebraic_topology.dold_kan.functor_n
 
 # Comparison with the normalized Moore complex functor
 
+> 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 show that when the category `A` is abelian,

diff --git a/src/analysis/box_integral/partition/basic.lean b/src/analysis/box_integral/partition/basic.lean
@@ -9,6 +9,9 @@ import analysis.box_integral.box.basic
 /-!
 # Partitions of 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 (pre)partitions of rectangular boxes in `ℝⁿ`.  A partition of a box `I` in
 `ℝⁿ` (see `box_integral.prepartition` and `box_integral.prepartition.is_partition`) is a finite set
 of pairwise disjoint boxes such that their union is exactly `I`. We use `boxes : finset (box ι)` to

diff --git a/src/analysis/box_integral/partition/split.lean b/src/analysis/box_integral/partition/split.lean
@@ -8,6 +8,9 @@ import analysis.box_integral.partition.basic
 /-!
 # Split a box along one or more hyperplanes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 A hyperplane `{x : ι → ℝ | x i = a}` splits a rectangular box `I : box_integral.box ι` into two

diff --git a/src/analysis/convex/caratheodory.lean b/src/analysis/convex/caratheodory.lean
@@ -10,6 +10,9 @@ import tactic.field_simp
 /-!
 # Carathéodory's convexity theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Convex hull can be regarded as a refinement of affine span. Both are closure operators but whereas
 convex hull takes values in the lattice of convex subsets, affine span takes values in the much
 coarser sublattice of affine subspaces.

diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean
@@ -10,6 +10,9 @@ import linear_algebra.affine_space.basis
 /-!
 # Convex combinations
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines convex combinations of points in a vector space.
 
 ## Main declarations

diff --git a/src/analysis/convex/independent.lean b/src/analysis/convex/independent.lean
@@ -9,6 +9,9 @@ import analysis.convex.extreme
 /-!
 # Convex independence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines convex independent families of points.
 
 Convex independence is closely related to affine independence. In both cases, no point can be

diff --git a/src/analysis/convex/jensen.lean b/src/analysis/convex/jensen.lean
@@ -9,6 +9,9 @@ import analysis.convex.function
 /-!
 # Jensen's inequality and maximum principle for convex functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we prove the finite Jensen inequality and the finite maximum principle for convex
 functions. The integral versions are to be found in `analysis.convex.integral`.
 

diff --git a/src/analysis/convex/join.lean b/src/analysis/convex/join.lean
@@ -8,6 +8,9 @@ import analysis.convex.combination
 /-!
 # Convex join
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the convex join of two sets. The convex join of `s` and `t` is the union of the
 segments with one end in `s` and the other in `t`. This is notably a useful gadget to deal with
 convex hulls of finite sets.

diff --git a/src/analysis/convex/normed.lean b/src/analysis/convex/normed.lean
@@ -11,6 +11,9 @@ import analysis.normed_space.ray
 /-!
 # Topological and metric properties of convex sets in normed spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove the following facts:
 
 * `convex_on_norm`, `convex_on_dist` : norm and distance to a fixed point is convex on any convex

diff --git a/src/analysis/convex/simplicial_complex/basic.lean b/src/analysis/convex/simplicial_complex/basic.lean
@@ -9,6 +9,9 @@ import linear_algebra.affine_space.independent
 /-!
 # Simplicial complexes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we define simplicial complexes in `𝕜`-modules. A simplicial complex is a collection
 of simplices closed by inclusion (of vertices) and intersection (of underlying sets).
 

diff --git a/src/analysis/convex/topology.lean b/src/analysis/convex/topology.lean
@@ -12,6 +12,9 @@ import topology.algebra.module.basic
 /-!
 # Topological properties of convex sets
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove the following facts:
 
 * `convex.interior` : interior of a convex set is convex;

diff --git a/src/analysis/locally_convex/bounded.lean b/src/analysis/locally_convex/bounded.lean
@@ -13,6 +13,9 @@ import topology.uniform_space.cauchy
 /-!
 # Von Neumann Boundedness
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines natural or von Neumann bounded sets and proves elementary properties.
 
 ## Main declarations

diff --git a/src/analysis/normed_space/conformal_linear_map.lean b/src/analysis/normed_space/conformal_linear_map.lean
@@ -9,6 +9,9 @@ import analysis.normed_space.linear_isometry
 /-!
 # Conformal Linear Maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A continuous linear map between `R`-normed spaces `X` and `Y` `is_conformal_map` if it is
 a nonzero multiple of a linear isometry.
 

diff --git a/src/analysis/normed_space/linear_isometry.lean b/src/analysis/normed_space/linear_isometry.lean
@@ -10,6 +10,9 @@ import linear_algebra.basis
 /-!
 # (Semi-)linear isometries
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `linear_isometry σ₁₂ E E₂` (notation: `E →ₛₗᵢ[σ₁₂] E₂`) to be a semilinear
 isometric embedding of `E` into `E₂` and `linear_isometry_equiv` (notation: `E ≃ₛₗᵢ[σ₁₂] E₂`) to be
 a semilinear isometric equivalence between `E` and `E₂`.  The notation for the associated purely

diff --git a/src/analysis/normed_space/star/basic.lean b/src/analysis/normed_space/star/basic.lean
@@ -14,6 +14,9 @@ import topology.algebra.star_subalgebra
 /-!
 # Normed star rings and algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A normed star group is a normed group with a compatible `star` which is isometric.
 
 A C⋆-ring is a normed star group that is also a ring and that verifies the stronger

diff --git a/src/analysis/seminorm.lean b/src/analysis/seminorm.lean
@@ -11,6 +11,9 @@ import analysis.normed.group.add_torsor
 /-!
 # Seminorms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines seminorms.
 
 A seminorm is a function to the reals which is positive-semidefinite, absolutely homogeneous, and

diff --git a/src/category_theory/abelian/opposite.lean b/src/category_theory/abelian/opposite.lean
@@ -9,6 +9,9 @@ import category_theory.limits.opposites
 
 /-!
 # The opposite of an abelian category is abelian.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 noncomputable theory

diff --git a/src/category_theory/abelian/subobject.lean b/src/category_theory/abelian/subobject.lean
@@ -9,6 +9,9 @@ import category_theory.abelian.basic
 /-!
 # Equivalence between subobjects and quotients in an abelian category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 open category_theory category_theory.limits opposite

diff --git a/src/category_theory/adjunction/adjoint_functor_theorems.lean b/src/category_theory/adjunction/adjoint_functor_theorems.lean
@@ -12,6 +12,9 @@ import category_theory.subobject.comma
 /-!
 # Adjoint functor theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the (general) adjoint functor theorem, in the form:
 * If `G : D ⥤ C` preserves limits and `D` has limits, and satisfies the solution set condition,
   then it has a left adjoint: `is_right_adjoint_of_preserves_limits_of_solution_set_condition`.

diff --git a/src/category_theory/concrete_category/unbundled_hom.lean b/src/category_theory/concrete_category/unbundled_hom.lean
@@ -8,6 +8,9 @@ import category_theory.concrete_category.bundled_hom
 /-!
 # Category instances for structures that use unbundled homs
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides basic infrastructure to define concrete
 categories using unbundled homs (see `class unbundled_hom`), and
 define forgetful functors between them (see

diff --git a/src/category_theory/generator.lean b/src/category_theory/generator.lean
@@ -14,6 +14,9 @@ import data.set.opposite
 /-!
 # Separating and detecting sets
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 There are several non-equivalent notions of a generator of a category. Here, we consider two of
 them:
 

diff --git a/src/category_theory/limits/constructions/weakly_initial.lean b/src/category_theory/limits/constructions/weakly_initial.lean
@@ -10,6 +10,9 @@ import category_theory.limits.shapes.terminal
 /-!
 # Constructions related to weakly initial objects
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file gives constructions related to weakly initial objects, namely:
 * If a category has small products and a small weakly initial set of objects, then it has a weakly
   initial object.

diff --git a/src/category_theory/limits/preserves/functor_category.lean b/src/category_theory/limits/preserves/functor_category.lean
@@ -11,6 +11,9 @@ import category_theory.limits.presheaf
 /-!
 # Preservation of (co)limits in the functor category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 * Show that if `X ⨯ -` preserves colimits in `D` for any `X : D`, then the product functor `F ⨯ -`
 for `F : C ⥤ D` preserves colimits.
 

diff --git a/src/category_theory/limits/presheaf.lean b/src/category_theory/limits/presheaf.lean
@@ -14,6 +14,9 @@ import category_theory.limits.types
 /-!
 # Colimit of representables
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file constructs an adjunction `yoneda_adjunction` between `(Cᵒᵖ ⥤ Type u)` and `ℰ` given a
 functor `A : C ⥤ ℰ`, where the right adjoint sends `(E : ℰ)` to `c ↦ (A.obj c ⟶ E)` (provided `ℰ`
 has colimits).

diff --git a/src/category_theory/limits/shapes/wide_equalizers.lean b/src/category_theory/limits/shapes/wide_equalizers.lean
@@ -9,6 +9,9 @@ import category_theory.limits.shapes.equalizers
 /-!
 # Wide equalizers and wide coequalizers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines wide (co)equalizers as special cases of (co)limits.
 
 A wide equalizer for the family of morphisms `X ⟶ Y` indexed by `J` is the categorical

diff --git a/src/category_theory/linear/yoneda.lean b/src/category_theory/linear/yoneda.lean
@@ -10,6 +10,9 @@ import category_theory.preadditive.yoneda.basic
 /-!
 # The Yoneda embedding for `R`-linear categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The Yoneda embedding for `R`-linear categories `C`,
 sends an object `X : C` to the `Module R`-valued presheaf on `C`,
 with value on `Y : Cᵒᵖ` given by `Module.of R (unop Y ⟶ X)`.

diff --git a/src/category_theory/preadditive/generator.lean b/src/category_theory/preadditive/generator.lean
@@ -9,6 +9,9 @@ import category_theory.preadditive.yoneda.basic
 /-!
 # Separators in preadditive categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains characterizations of separating sets and objects that are valid in all
 preadditive categories.
 

diff --git a/src/category_theory/preadditive/yoneda/basic.lean b/src/category_theory/preadditive/yoneda/basic.lean
@@ -11,6 +11,9 @@ import algebra.category.Group.preadditive
 /-!
 # The Yoneda embedding for preadditive categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The Yoneda embedding for preadditive categories sends an object `Y` to the presheaf sending an
 object `X` to the group of morphisms `X ⟶ Y`. At each point, we get an additional `End Y`-module
 structure.

diff --git a/src/category_theory/subobject/comma.lean b/src/category_theory/subobject/comma.lean
@@ -10,6 +10,9 @@ import category_theory.limits.shapes.finite_limits
 /-!
 # Subobjects in the category of structured arrows
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We compute the subobjects of an object `A` in the category `structured_arrow S T` for `T : C ⥤ D`
 and `S : D` as a subtype of the subobjects of `A.right`. We deduce that `structured_arrow S T` is
 well-powered if `C` is.

diff --git a/src/data/real/hyperreal.lean b/src/data/real/hyperreal.lean
@@ -8,6 +8,9 @@ import analysis.specific_limits.basic
 
 /-!
 # Construction of the hyperreal numbers as an ultraproduct of real sequences.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open filter filter.germ

diff --git a/src/data/string/defs.lean b/src/data/string/defs.lean
@@ -8,6 +8,9 @@ import data.list.defs
 /-!
 # Definitions for `string`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines a bunch of functions for the `string` datatype.
 -/