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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Mon.adjunctions` * `algebra.category.Semigroup.basic` * `algebraic_geometry.function_field` * `algebraic_geometry.morphisms.basic` * `algebraic_geometry.morphisms.open_immersion` * `algebraic_geometry.morphisms.universally_closed` * `analysis.complex.upper_half_plane.manifold` * `analysis.convex.cone.proper` * `category_theory.limits.constructions.over.basic` * `geometry.manifold.algebra.smooth_functions` * `geometry.manifold.derivation_bundle` * `number_theory.modular_forms.jacobi_theta.manifold` * `representation_theory.fdRep` * `representation_theory.invariants` * `ring_theory.witt_vector.isocrystal` * `set_theory.game.domineering` * `set_theory.game.short` * `set_theory.game.state` * `topology.homotopy.product`
leanprover-community · Jul 3, 2023 · 728ef9d · 728ef9d
1 parent e473c31
commit 728ef9d
Show file tree

Hide file tree

Showing 19 changed files with 57 additions and 0 deletions.
diff --git a/src/algebra/category/Mon/adjunctions.lean b/src/algebra/category/Mon/adjunctions.lean
@@ -11,6 +11,9 @@ import algebra.free_monoid.basic
 /-!
 # Adjunctions regarding the category of monoids
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the adjunction between adjoining a unit to a semigroup and the forgetful functor
 from monoids to semigroups.
 

diff --git a/src/algebra/category/Semigroup/basic.lean b/src/algebra/category/Semigroup/basic.lean
@@ -12,6 +12,9 @@ import category_theory.elementwise
 /-!
 # Category instances for has_mul, has_add, semigroup and add_semigroup
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce the bundled categories:
 * `Magma`
 * `AddMagma`

diff --git a/src/algebraic_geometry/function_field.lean b/src/algebraic_geometry/function_field.lean
@@ -8,6 +8,9 @@ import algebraic_geometry.properties
 /-!
 # Function field of integral schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the function field of an irreducible scheme as the stalk of the generic point.
 This is a field when the scheme is integral.
 

diff --git a/src/algebraic_geometry/morphisms/basic.lean b/src/algebraic_geometry/morphisms/basic.lean
@@ -10,6 +10,9 @@ import category_theory.morphism_property
 /-!
 # Properties of morphisms between Schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We provide the basic framework for talking about properties of morphisms between Schemes.
 
 A `morphism_property Scheme` is a predicate on morphisms between schemes, and an

diff --git a/src/algebraic_geometry/morphisms/open_immersion.lean b/src/algebraic_geometry/morphisms/open_immersion.lean
@@ -10,6 +10,9 @@ import algebraic_geometry.morphisms.basic
 
 # Open immersions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A morphism is an open immersions if the underlying map of spaces is an open embedding
 `f : X ⟶ U ⊆ Y`, and the sheaf map `Y(V) ⟶ f _* X(V)` is an iso for each `V ⊆ U`.
 

diff --git a/src/algebraic_geometry/morphisms/universally_closed.lean b/src/algebraic_geometry/morphisms/universally_closed.lean
@@ -9,6 +9,9 @@ import topology.local_at_target
 /-!
 # Universally closed morphism
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A morphism of schemes `f : X ⟶ Y` is universally closed if `X ×[Y] Y' ⟶ Y'` is a closed map
 for all base change `Y' ⟶ Y`.
 

diff --git a/src/analysis/complex/upper_half_plane/manifold.lean b/src/analysis/complex/upper_half_plane/manifold.lean
@@ -8,6 +8,9 @@ import geometry.manifold.cont_mdiff_mfderiv
 /-!
 # Manifold structure on the upper half plane.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define the complex manifold structure on the upper half-plane.
 -/
 

diff --git a/src/analysis/convex/cone/proper.lean b/src/analysis/convex/cone/proper.lean
@@ -9,6 +9,9 @@ import analysis.inner_product_space.adjoint
 /-!
 # Proper cones
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define a proper cone as a nonempty, closed, convex cone. Proper cones are used in defining conic
 programs which generalize linear programs. A linear program is a conic program for the positive
 cone. We then prove Farkas' lemma for conic programs following the proof in the reference below.

diff --git a/src/category_theory/limits/constructions/over/basic.lean b/src/category_theory/limits/constructions/over/basic.lean
@@ -12,6 +12,9 @@ import category_theory.limits.constructions.equalizers
 /-!
 # Limits in the over category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Declare instances for limits in the over category: If `C` has finite wide pullbacks, `over B` has
 finite limits, and if `C` has arbitrary wide pullbacks then `over B` has limits.
 -/

diff --git a/src/geometry/manifold/algebra/smooth_functions.lean b/src/geometry/manifold/algebra/smooth_functions.lean
@@ -9,6 +9,9 @@ import geometry.manifold.algebra.structures
 /-!
 # Algebraic structures over smooth functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we define instances of algebraic structures over smooth functions.
 -/
 

diff --git a/src/geometry/manifold/derivation_bundle.lean b/src/geometry/manifold/derivation_bundle.lean
@@ -11,6 +11,9 @@ import ring_theory.derivation.basic
 
 # Derivation bundle
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define the derivations at a point of a manifold on the algebra of smooth fuctions.
 Moreover, we define the differential of a function in terms of derivations.
 

diff --git a/src/number_theory/modular_forms/jacobi_theta/manifold.lean b/src/number_theory/modular_forms/jacobi_theta/manifold.lean
@@ -9,6 +9,9 @@ import analysis.complex.upper_half_plane.manifold
 /-!
 # Manifold differentiability of the Jacobi's theta function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we reformulate differentiability of the Jacobi's theta function in terms of manifold
 differentiability.
 

diff --git a/src/representation_theory/fdRep.lean b/src/representation_theory/fdRep.lean
@@ -11,6 +11,9 @@ import representation_theory.basic
 /-!
 # `fdRep k G` is the category of finite dimensional `k`-linear representations of `G`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `V : fdRep k G`, there is a coercion that allows you to treat `V` as a type,
 and this type comes equipped with `module k V` and `finite_dimensional k V` instances.
 Also `V.ρ` gives the homomorphism `G →* (V →ₗ[k] V)`.

diff --git a/src/representation_theory/invariants.lean b/src/representation_theory/invariants.lean
@@ -9,6 +9,9 @@ import representation_theory.fdRep
 /-!
 # Subspace of invariants a group representation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file introduces the subspace of invariants of a group representation
 and proves basic results about it.
 The main tool used is the average of all elements of the group, seen as an element of

diff --git a/src/ring_theory/witt_vector/isocrystal.lean b/src/ring_theory/witt_vector/isocrystal.lean
@@ -10,6 +10,9 @@ import ring_theory.witt_vector.frobenius_fraction_field
 
 ## F-isocrystals over a perfect field
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 When `k` is an integral domain, so is `𝕎 k`, and we can consider its field of fractions `K(p, k)`.
 The endomorphism `witt_vector.frobenius` lifts to `φ : K(p, k) → K(p, k)`; if `k` is perfect, `φ` is
 an automorphism.

diff --git a/src/set_theory/game/domineering.lean b/src/set_theory/game/domineering.lean
@@ -8,6 +8,9 @@ import set_theory.game.state
 /-!
 # Domineering as a combinatorial game.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the game of Domineering, played on a chessboard of arbitrary shape
 (possibly even disconnected).
 Left moves by placing a domino vertically, while Right moves by placing a domino horizontally.

diff --git a/src/set_theory/game/short.lean b/src/set_theory/game/short.lean
@@ -10,6 +10,9 @@ import set_theory.game.birthday
 /-!
 # Short games
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A combinatorial game is `short` [Conway, ch.9][conway2001] if it has only finitely many positions.
 In particular, this means there is a finite set of moves at every point.
 

diff --git a/src/set_theory/game/state.lean b/src/set_theory/game/state.lean
@@ -8,6 +8,9 @@ import set_theory.game.short
 /-!
 # Games described via "the state of the board".
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We provide a simple mechanism for constructing combinatorial (pre-)games, by describing
 "the state of the board", and providing an upper bound on the number of turns remaining.
 

diff --git a/src/topology/homotopy/product.lean b/src/topology/homotopy/product.lean
@@ -9,6 +9,9 @@ import topology.homotopy.path
 /-!
 # Product of homotopies
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we introduce definitions for the product of
 homotopies. We show that the products of relative homotopies
 are still relative homotopies. Finally, we specialize to the case