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

Commit 0b7c740

Browse files
author
github-actions[bot]
committed
chore(*): add mathlib4 synchronization comments (#19099)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Group.abelian` * `algebra.category.Group.colimits` * `algebra.category.Group.images` * `algebra.category.Module.abelian` * `algebra.category.Module.biproducts` * `algebra.category.Module.images` * `algebra.category.Ring.constructions` * `algebra.category.Ring.filtered_colimits` * `algebra.category.Ring.limits` * `algebra.module.graded_module` * `algebra.module.torsion` * `algebraic_geometry.presheafed_space.has_colimits` * `algebraic_geometry.prime_spectrum.maximal` * `algebraic_geometry.prime_spectrum.noetherian` * `algebraic_geometry.sheafed_space` * `analysis.box_integral.partition.filter` * `analysis.calculus.conformal.inner_product` * `analysis.calculus.conformal.normed_space` * `analysis.calculus.fderiv.bilinear` * `analysis.calculus.fderiv.mul` * `analysis.complex.arg` * `analysis.complex.conformal` * `analysis.complex.unit_disc.basic` * `analysis.convex.krein_milman` * `analysis.convex.specific_functions.basic` * `analysis.inner_product_space.basic` * `analysis.inner_product_space.conformal_linear_map` * `analysis.inner_product_space.dual` * `analysis.inner_product_space.orthogonal` * `analysis.inner_product_space.projection` * `analysis.inner_product_space.symmetric` * `analysis.locally_convex.abs_convex` * `analysis.locally_convex.weak_dual` * `analysis.mean_inequalities` * `analysis.mean_inequalities_pow` * `analysis.normed_space.dual` * `analysis.normed_space.hahn_banach.separation` * `analysis.normed_space.pi_Lp` * `analysis.normed_space.star.multiplier` * `analysis.normed_space.weak_dual` * `analysis.p_series` * `analysis.special_functions.pow.asymptotics` * `analysis.special_functions.pow.continuity` * `category_theory.abelian.injective` * `category_theory.abelian.injective_resolution` * `category_theory.abelian.projective` * `category_theory.abelian.right_derived` * `category_theory.preadditive.yoneda.limits` * `data.nat.squarefree` * `data.zmod.quotient` * `field_theory.ratfunc` * `geometry.euclidean.angle.unoriented.affine` * `geometry.euclidean.angle.unoriented.basic` * `geometry.euclidean.angle.unoriented.conformal` * `geometry.euclidean.basic` * `geometry.euclidean.inversion` * `geometry.manifold.conformal_groupoid` * `group_theory.exponent` * `group_theory.p_group` * `group_theory.specific_groups.cyclic` * `group_theory.specific_groups.dihedral` * `group_theory.torsion` * `linear_algebra.free_module.ideal_quotient` * `linear_algebra.matrix.bilinear_form` * `linear_algebra.matrix.sesquilinear_form` * `measure_theory.function.egorov` * `measure_theory.function.special_functions.inner` * `measure_theory.function.strongly_measurable.inner` * `measure_theory.integral.mean_inequalities` * `model_theory.graph` * `model_theory.satisfiability` * `model_theory.types` * `model_theory.ultraproducts` * `number_theory.bernoulli` * `number_theory.padics.hensel` * `number_theory.padics.padic_integers` * `order.category.FinPartOrd` * `probability.probability_mass_function.constructions` * `ring_theory.adjoin.field` * `ring_theory.algebraic_independent` * `ring_theory.integral_domain` * `ring_theory.is_tensor_product` * `ring_theory.polynomial.dickson` * `topology.continuous_function.compact` * `topology.instances.complex` * `topology.metric_space.holder` * `topology.sheaves.functors` * `topology.sheaves.sheaf_condition.equalizer_products` * `topology.sheaves.sheaf_condition.pairwise_intersections`
1 parent c4015ac commit 0b7c740

89 files changed

Lines changed: 267 additions & 0 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎src/algebra/category/Group/abelian.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,9 @@ import category_theory.abelian.basic
1111

1212
/-!
1313
# The category of abelian groups is abelian
14+
15+
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
16+
> Any changes to this file require a corresponding PR to mathlib4.
1417
-/
1518

1619
open category_theory

‎src/algebra/category/Group/colimits.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,9 @@ import category_theory.concrete_category.elementwise
1111
/-!
1212
# The category of additive commutative groups has all colimits.
1313
14+
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
15+
> Any changes to this file require a corresponding PR to mathlib4.
16+
1417
This file uses a "pre-automated" approach, just as for `Mon/colimits.lean`.
1518
It is a very uniform approach, that conceivably could be synthesised directly
1619
by a tactic that analyses the shape of `add_comm_group` and `monoid_hom`.

‎src/algebra/category/Group/images.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,9 @@ import category_theory.limits.shapes.images
99
/-!
1010
# The category of commutative additive groups has images.
1111
12+
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
13+
> Any changes to this file require a corresponding PR to mathlib4.
14+
1215
Note that we don't need to register any of the constructions here as instances, because we get them
1316
from the fact that `AddCommGroup` is an abelian category.
1417
-/

‎src/algebra/category/Module/abelian.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,9 @@ import category_theory.abelian.exact
1111
/-!
1212
# The category of left R-modules is abelian.
1313
14+
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
15+
> Any changes to this file require a corresponding PR to mathlib4.
16+
1417
Additionally, two linear maps are exact in the categorical sense iff `range f = ker g`.
1518
-/
1619

‎src/algebra/category/Module/biproducts.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,9 @@ import algebra.homology.short_exact.abelian
1010

1111
/-!
1212
# The category of `R`-modules has finite biproducts
13+
14+
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
15+
> Any changes to this file require a corresponding PR to mathlib4.
1316
-/
1417

1518
open category_theory

‎src/algebra/category/Module/images.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,9 @@ import category_theory.limits.shapes.images
99
/-!
1010
# The category of R-modules has images.
1111
12+
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
13+
> Any changes to this file require a corresponding PR to mathlib4.
14+
1215
Note that we don't need to register any of the constructions here as instances, because we get them
1316
from the fact that `Module R` is an abelian category.
1417
-/

‎src/algebra/category/Ring/constructions.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,9 @@ import ring_theory.subring.basic
1313
/-!
1414
# Constructions of (co)limits in CommRing
1515
16+
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
17+
> Any changes to this file require a corresponding PR to mathlib4.
18+
1619
In this file we provide the explicit (co)cones for various (co)limits in `CommRing`, including
1720
* tensor product is the pushout
1821
* `Z` is the initial object

‎src/algebra/category/Ring/filtered_colimits.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,9 @@ import algebra.category.Group.filtered_colimits
99
/-!
1010
# The forgetful functor from (commutative) (semi-) rings preserves filtered colimits.
1111
12+
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
13+
> Any changes to this file require a corresponding PR to mathlib4.
14+
1215
Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend
1316
to preserve _filtered_ colimits.
1417

‎src/algebra/category/Ring/limits.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,9 @@ import ring_theory.subring.basic
1111
/-!
1212
# The category of (commutative) rings has all limits
1313
14+
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
15+
> Any changes to this file require a corresponding PR to mathlib4.
16+
1417
Further, these limits are preserved by the forgetful functor --- that is,
1518
the underlying types are just the limits in the category of types.
1619
-/

‎src/algebra/module/graded_module.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,9 @@ import algebra.module.big_operators
1212
/-!
1313
# Graded Module
1414
15+
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
16+
> Any changes to this file require a corresponding PR to mathlib4.
17+
1518
Given an `R`-algebra `A` graded by `𝓐`, a graded `A`-module `M` is expressed as
1619
`direct_sum.decomposition 𝓜` and `set_like.has_graded_smul 𝓐 𝓜`.
1720
Then `⨁ i, 𝓜 i` is an `A`-module and is isomorphic to `M`.

0 commit comments

Comments
 (0)