From 949d67ea28c2937f7fe449a310c6ac153efd027a Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Tue, 31 Oct 2023 00:19:28 +0000 Subject: [PATCH] chore(*): add mathlib4 synchronization comments --- src/algebraic_topology/dold_kan/equivalence.lean | 3 +++ src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean | 3 +++ src/combinatorics/quiver/covering.lean | 3 +++ src/linear_algebra/quadratic_form/dual.lean | 3 +++ 4 files changed, 12 insertions(+) diff --git a/src/algebraic_topology/dold_kan/equivalence.lean b/src/algebraic_topology/dold_kan/equivalence.lean index dc025a7938b2b..960d5589d5a72 100644 --- a/src/algebraic_topology/dold_kan/equivalence.lean +++ b/src/algebraic_topology/dold_kan/equivalence.lean @@ -11,6 +11,9 @@ import algebraic_topology.dold_kan.normalized # The Dold-Kan correspondence +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + The Dold-Kan correspondence states that for any abelian category `A`, there is an equivalence between the category of simplicial objects in `A` and the category of chain complexes in `A` (with degrees indexed by `ℕ` and the diff --git a/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean b/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean index 4d6fff16434a8..5514db73f68eb 100644 --- a/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean +++ b/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean @@ -12,6 +12,9 @@ import category_theory.idempotents.simplicial_object # The Dold-Kan correspondence for pseudoabelian categories +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + In this file, for any idempotent complete additive category `C`, the Dold-Kan equivalence `idempotents.dold_kan.equivalence C : simplicial_object C ≌ chain_complex C ℕ` diff --git a/src/combinatorics/quiver/covering.lean b/src/combinatorics/quiver/covering.lean index 18c98970d2cfd..4430c0d1b7e84 100644 --- a/src/combinatorics/quiver/covering.lean +++ b/src/combinatorics/quiver/covering.lean @@ -11,6 +11,9 @@ import logic.equiv.basic /-! # Covering +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + This file defines coverings of quivers as prefunctors that are bijective on the so-called stars and costars at each vertex of the domain. diff --git a/src/linear_algebra/quadratic_form/dual.lean b/src/linear_algebra/quadratic_form/dual.lean index 68ed89fab74cb..7edf39f9f5a0e 100644 --- a/src/linear_algebra/quadratic_form/dual.lean +++ b/src/linear_algebra/quadratic_form/dual.lean @@ -9,6 +9,9 @@ import linear_algebra.quadratic_form.prod /-! # Quadratic form structures related to `module.dual` +> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. +> Any changes to this file require a corresponding PR to mathlib4. + ## Main definitions * `bilin_form.dual_prod R M`, the bilinear form on `(f, x) : module.dual R M × M` defined as