From d0b1936853671209a866fa35b9e54949c81116e2 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Fri, 30 Jun 2023 15:09:19 +0000 Subject: [PATCH] chore(*): add mathlib4 synchronization comments (#19220) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.fgModule.limits` * `algebra.homology.differential_object` * `algebraic_geometry.AffineScheme` * `algebraic_geometry.gluing` * `algebraic_geometry.limits` * `algebraic_geometry.properties` * `algebraic_geometry.pullbacks` * `linear_algebra.clifford_algebra.even` * `number_theory.legendre_symbol.norm_num` * `number_theory.zeta_function` * `order.category.omega_complete_partial_order` * `ring_theory.witt_vector.frobenius_fraction_field` * `set_theory.game.nim` * `set_theory.surreal.dyadic` * `topology.sheaves.skyscraper` --- src/algebra/category/fgModule/limits.lean | 3 +++ src/algebra/homology/differential_object.lean | 3 +++ src/algebraic_geometry/AffineScheme.lean | 3 +++ src/algebraic_geometry/gluing.lean | 3 +++ src/algebraic_geometry/limits.lean | 3 +++ src/algebraic_geometry/properties.lean | 3 +++ src/algebraic_geometry/pullbacks.lean | 3 +++ src/linear_algebra/clifford_algebra/even.lean | 3 +++ src/number_theory/legendre_symbol/norm_num.lean | 3 +++ src/number_theory/zeta_function.lean | 3 +++ src/order/category/omega_complete_partial_order.lean | 3 +++ src/ring_theory/witt_vector/frobenius_fraction_field.lean | 3 +++ src/set_theory/game/nim.lean | 3 +++ src/set_theory/surreal/dyadic.lean | 3 +++ src/topology/sheaves/skyscraper.lean | 3 +++ 15 files changed, 45 insertions(+) diff --git a/src/algebra/category/fgModule/limits.lean b/src/algebra/category/fgModule/limits.lean index f4c114b7dccdb..6c02caa86c100 100644 --- a/src/algebra/category/fgModule/limits.lean +++ b/src/algebra/category/fgModule/limits.lean @@ -14,6 +14,9 @@ import category_theory.limits.constructions.limits_of_products_and_equalizers /-! # `forget₂ (fgModule K) (Module K)` creates all finite limits. +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + And hence `fgModule K` has all finite limits. ## Future work diff --git a/src/algebra/homology/differential_object.lean b/src/algebra/homology/differential_object.lean index 12a6920cb0ba9..03f8f3839d349 100644 --- a/src/algebra/homology/differential_object.lean +++ b/src/algebra/homology/differential_object.lean @@ -9,6 +9,9 @@ import category_theory.differential_object /-! # Homological complexes are differential graded objects. +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We verify that a `homological_complex` indexed by an `add_comm_group` is essentially the same thing as a differential graded object. diff --git a/src/algebraic_geometry/AffineScheme.lean b/src/algebraic_geometry/AffineScheme.lean index 4def63a940a0a..827f2d0f8852b 100644 --- a/src/algebraic_geometry/AffineScheme.lean +++ b/src/algebraic_geometry/AffineScheme.lean @@ -11,6 +11,9 @@ import ring_theory.localization.inv_submonoid /-! # Affine schemes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We define the category of `AffineScheme`s as the essential image of `Spec`. We also define predicates about affine schemes and affine open sets. diff --git a/src/algebraic_geometry/gluing.lean b/src/algebraic_geometry/gluing.lean index 2a5345bbf6a65..15c3b25257934 100644 --- a/src/algebraic_geometry/gluing.lean +++ b/src/algebraic_geometry/gluing.lean @@ -9,6 +9,9 @@ import algebraic_geometry.open_immersion.Scheme /-! # Gluing Schemes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + Given a family of gluing data of schemes, we may glue them together. ## Main definitions diff --git a/src/algebraic_geometry/limits.lean b/src/algebraic_geometry/limits.lean index 6268fba92246e..22c9fbc92cf7f 100644 --- a/src/algebraic_geometry/limits.lean +++ b/src/algebraic_geometry/limits.lean @@ -9,6 +9,9 @@ import algebraic_geometry.AffineScheme /-! # (Co)Limits of Schemes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We construct various limits and colimits in the category of schemes. * The existence of fibred products was shown in `algebraic_geometry/pullbacks.lean`. diff --git a/src/algebraic_geometry/properties.lean b/src/algebraic_geometry/properties.lean index 62429e066242e..7dbae1c65bc70 100644 --- a/src/algebraic_geometry/properties.lean +++ b/src/algebraic_geometry/properties.lean @@ -12,6 +12,9 @@ import ring_theory.local_properties /-! # Basic properties of schemes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We provide some basic properties of schemes ## Main definition diff --git a/src/algebraic_geometry/pullbacks.lean b/src/algebraic_geometry/pullbacks.lean index 726ffd94eed13..5173a80bbca4d 100644 --- a/src/algebraic_geometry/pullbacks.lean +++ b/src/algebraic_geometry/pullbacks.lean @@ -11,6 +11,9 @@ import category_theory.limits.shapes.diagonal /-! # Fibred products of schemes +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file we construct the fibred product of schemes via gluing. We roughly follow [har77] Theorem 3.3. diff --git a/src/linear_algebra/clifford_algebra/even.lean b/src/linear_algebra/clifford_algebra/even.lean index e977571460879..a374a0ead8693 100644 --- a/src/linear_algebra/clifford_algebra/even.lean +++ b/src/linear_algebra/clifford_algebra/even.lean @@ -9,6 +9,9 @@ import linear_algebra.clifford_algebra.grading /-! # The universal property of the even subalgebra +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## Main definitions * `clifford_algebra.even Q`: The even subalgebra of `clifford_algebra Q`. diff --git a/src/number_theory/legendre_symbol/norm_num.lean b/src/number_theory/legendre_symbol/norm_num.lean index 00cfe5eb881ff..a47ded8453ec7 100644 --- a/src/number_theory/legendre_symbol/norm_num.lean +++ b/src/number_theory/legendre_symbol/norm_num.lean @@ -8,6 +8,9 @@ import number_theory.legendre_symbol.jacobi_symbol /-! # A `norm_num` extension for Jacobi and Legendre symbols +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + We extend the `tactic.interactive.norm_num` tactic so that it can be used to provably compute the value of the Jacobi symbol `J(a | b)` or the Legendre symbol `legendre_sym p a` when the arguments are numerals. diff --git a/src/number_theory/zeta_function.lean b/src/number_theory/zeta_function.lean index b3dc94155d253..cda925a279f9f 100644 --- a/src/number_theory/zeta_function.lean +++ b/src/number_theory/zeta_function.lean @@ -10,6 +10,9 @@ import number_theory.zeta_values /-! # Definition of the Riemann zeta function +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## Main definitions: * `riemann_zeta`: the Riemann zeta function `ζ : ℂ → ℂ`. diff --git a/src/order/category/omega_complete_partial_order.lean b/src/order/category/omega_complete_partial_order.lean index 65d74186c9172..15b627c09c367 100644 --- a/src/order/category/omega_complete_partial_order.lean +++ b/src/order/category/omega_complete_partial_order.lean @@ -13,6 +13,9 @@ import category_theory.concrete_category.bundled_hom /-! # Category of types with a omega complete partial order +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file, we bundle the class `omega_complete_partial_order` into a concrete category and prove that continuous functions also form a `omega_complete_partial_order`. diff --git a/src/ring_theory/witt_vector/frobenius_fraction_field.lean b/src/ring_theory/witt_vector/frobenius_fraction_field.lean index d251d81d5ad0b..e9cd65c73af4f 100644 --- a/src/ring_theory/witt_vector/frobenius_fraction_field.lean +++ b/src/ring_theory/witt_vector/frobenius_fraction_field.lean @@ -10,6 +10,9 @@ import ring_theory.witt_vector.discrete_valuation_ring /-! # Solving equations about the Frobenius map on the field of fractions of `𝕎 k` +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + The goal of this file is to prove `witt_vector.exists_frobenius_solution_fraction_ring`, which says that for an algebraically closed field `k` of characteristic `p` and `a, b` in the field of fractions of Witt vectors over `k`, diff --git a/src/set_theory/game/nim.lean b/src/set_theory/game/nim.lean index fbbbb91d3abbd..93d6b3f894ccd 100644 --- a/src/set_theory/game/nim.lean +++ b/src/set_theory/game/nim.lean @@ -10,6 +10,9 @@ import set_theory.game.impartial /-! # Nim and the Sprague-Grundy theorem +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file contains the definition for nim for any ordinal `o`. In the game of `nim o₁` both players may move to `nim o₂` for any `o₂ < o₁`. We also define a Grundy value for an impartial game `G` and prove the Sprague-Grundy theorem, that diff --git a/src/set_theory/surreal/dyadic.lean b/src/set_theory/surreal/dyadic.lean index e663ebaecd75e..0f666a31e2705 100644 --- a/src/set_theory/surreal/dyadic.lean +++ b/src/set_theory/surreal/dyadic.lean @@ -10,6 +10,9 @@ import ring_theory.localization.basic /-! # Dyadic numbers + +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. Dyadic numbers are obtained by localizing ℤ away from 2. They are the initial object in the category of rings with no 2-torsion. diff --git a/src/topology/sheaves/skyscraper.lean b/src/topology/sheaves/skyscraper.lean index c02f854b23030..08b19fe467af6 100644 --- a/src/topology/sheaves/skyscraper.lean +++ b/src/topology/sheaves/skyscraper.lean @@ -10,6 +10,9 @@ import topology.sheaves.functors /-! # Skyscraper (pre)sheaves +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + A skyscraper (pre)sheaf `𝓕 : (pre)sheaf C X` is the (pre)sheaf with value `A` at point `p₀` that is supported only at open sets contain `p₀`, i.e. `𝓕(U) = A` if `p₀ ∈ U` and `𝓕(U) = *` if `p₀ ∉ U` where `*` is a terminal object of `C`. In terms of stalks, `𝓕` is supported at all specializations