Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
chore(*): add mathlib4 synchronization comments (#19220)
Browse files Browse the repository at this point in the history
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`
  • Loading branch information
leanprover-community-bot committed Jun 30, 2023
1 parent 48fb5b5 commit d0b1936
Show file tree
Hide file tree
Showing 15 changed files with 45 additions and 0 deletions.
3 changes: 3 additions & 0 deletions src/algebra/category/fgModule/limits.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions src/algebra/homology/differential_object.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
3 changes: 3 additions & 0 deletions src/algebraic_geometry/AffineScheme.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
3 changes: 3 additions & 0 deletions src/algebraic_geometry/gluing.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions src/algebraic_geometry/limits.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down
3 changes: 3 additions & 0 deletions src/algebraic_geometry/properties.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions src/algebraic_geometry/pullbacks.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
3 changes: 3 additions & 0 deletions src/linear_algebra/clifford_algebra/even.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down
3 changes: 3 additions & 0 deletions src/number_theory/legendre_symbol/norm_num.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
3 changes: 3 additions & 0 deletions src/number_theory/zeta_function.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 `ζ : ℂ → ℂ`.
Expand Down
3 changes: 3 additions & 0 deletions src/order/category/omega_complete_partial_order.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down
3 changes: 3 additions & 0 deletions src/ring_theory/witt_vector/frobenius_fraction_field.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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`,
Expand Down
3 changes: 3 additions & 0 deletions src/set_theory/game/nim.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions src/set_theory/surreal/dyadic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
3 changes: 3 additions & 0 deletions src/topology/sheaves/skyscraper.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit d0b1936

Please sign in to comment.