…cal complexes (#11713)

We construct an isomorphism `mapBifunctor K₂ K₁ F.flip c ≅ mapBifunctor K₁ K₂ F c` when `F` is a bifunctor, and `K₁` and `K₂` are two homological complexes. This is under the assumption of a certain instance of `TotalComplexShapeSymmetry` which provides compatible signs for this isomorphism.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…cal complexes (#11713)

We construct an isomorphism `mapBifunctor K₂ K₁ F.flip c ≅ mapBifunctor K₁ K₂ F c` when `F` is a bifunctor, and `K₁` and `K₂` are two homological complexes. This is under the assumption of a certain instance of `TotalComplexShapeSymmetry` which provides compatible signs for this isomorphism.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

commit 9ef973d
Merge: 0bf4baf c3a48ab
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 20:41:16 2024 +0200

    Merge remote-tracking branch 'origin/master' into test/merge_assert_up

commit c3a48ab
Author: Jakob von Raumer <jakob@von-raumer.de>
Date:   Mon Aug 12 17:47:56 2024 +0000

    feat(CategoryTheory): Composing `Comma.map` with `Comma.fst` and `Comma.snd` (#15730)

commit 795a856
Author: Kim Morrison <kim@tqft.net>
Date:   Mon Aug 12 16:50:11 2024 +0000

    chore: uncomment some now viable assert_not_exists (#15715)

    Per [zulip](https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/.60assert_not_exists.60.20at.20top.20or.20bottom.20of.20file.3F/near/459960523) discussion.

    Co-authored-by: adomani <adomani@gmail.com>
    Co-authored-by: Johan Commelin <johan@commelin.net>

commit 0bf4baf
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 18:36:54 2024 +0200

    reorders

commit f2cd6ef
Author: Etienne <etienne.marion@ens-lyon.fr>
Date:   Mon Aug 12 16:36:26 2024 +0000

    doc: Add a note on how to use `CompactlyGeneratedSpace` (#15132)

    Following this discussion : https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Compactly.20generated.20spaces/near/453958229.
    Indicate that `CompactlyGeneratedSpace` should be used with an explicit universe parameter.

commit 09c4c46
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 18:33:33 2024 +0200

    dedups

commit d75c706
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 17:46:41 2024 +0200

    small fixes

commit d6d9c22
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Mon Aug 12 15:39:15 2024 +0000

    chore: remove unnecessary _root_ qualifications (#15704)

commit 821f584
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 17:31:21 2024 +0200

    fix one

commit 75da87b
Author: grunweg <rothgami@math.hu-berlin.de>
Date:   Mon Aug 12 15:28:15 2024 +0000

    perf(Geometry/Manifold/Instances/Sphere): speed up (#15488)

    Speed up the file by 9% by doing the following
    - squeeze simps where the full form is short and this is a clear win
    - "squeeze" three really slow field_simp calls: replace them by the equivalent simp invocation and squeeze that
    - avoid one slow `convert`
    - squeeze two really slow nlinarith calls (they're still slow, but much better)
    - replace one congr! by congr

    This is a reduced version of #13456, which is hopefully less controversial.

commit eb19004
Author: grunweg <rothgami@math.hu-berlin.de>
Date:   Mon Aug 12 15:28:14 2024 +0000

    perf(Geometry/Euclidean): squeeze slow field_simp calls (#13497)

    Replace them by the equivalent `simp` call and squeeze that. We leave `field_simp` calls slower than roughly 150ms in place. A few calls cannot easily be replaced; we leave these alone as well.

    Speeds up all affected files, including `Euclidean/Circumcenter` by 4%, `Inversion/Basic` by 27% and `Triangle` by 52%.

commit 2215b9e
Author: Ralf Stephan <ralf@ark.in-berlin.de>
Date:   Mon Aug 12 15:04:35 2024 +0000

    doc(Tactics): fix typo (#15739)

    Fix minor typo in `compute_degree` docstring.

commit f57201f
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date:   Mon Aug 12 15:04:34 2024 +0000

    chore: deduplicate `inv_mul_cancel`/`mul_inv_cancel`, etc. (#15717)

    * `mul_left_inv`, `inv_mul_self` → `inv_mul_cancel` (for `Group`)
    * `mul_right_inv`, `mul_inv_self` → `mul_inv_cancel`
    * `add_left_neg`, `neg_add_self` → `neg_add_cancel` (for `AddGroup`)
    * `add_right_neg`, `add_neg_self` → `add_neg_cancel`
    * `inv_mul_cancel` → `inv_mul_cancel₀` (for `GroupWithZero`)
    * `mul_inv_cancel` → `mul_inv_cancel₀`

commit 9bb9d9e
Author: Tomáš Skřivan <skrivantomas@seznam.cz>
Date:   Mon Aug 12 15:04:33 2024 +0000

    fix(fun_prop):  few bug fixes for fun_prop (#11092)

    Bug fixes
    1. Fix infinite loop triggered by `(by fun_prop : ?m)`
    2. Support for multiple lambda theorems. For example `ContinuousOn` has multiple versions of composition theorem.
    3. Support for special constant lambda theorem. For example `IsLinearMap R fun _ => 0` should be registered as constant lambda theorem
    4. Improved error messages when trying `fun_prop` on non-fun_prop goal
    5. Improved error messages when missing lambda theorems

commit e04c5f0
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date:   Mon Aug 12 14:21:50 2024 +0000

    feat(Algebra/Homology): signs for the associativity compatibility of the total complex (#15719)

    This PR introduces a typeclass `ComplexShape.Associative` which takes as inputs six complex shapes `c₁`, `c₂`, `c₃`, `c₁₂`, `c₂₃` and `c`, and asserts compatibilities of signs for the associativity of the total complex of a triple complex. It shall also be used in the construction of the associator isomorphism for the tensor product of homological complexes.

    Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

commit 43258d6
Merge: e636099 0de4943
Author: adomani <adomani@gmail.com>
Date:   Mon Aug 12 15:56:11 2024 +0200

    Merge remote-tracking branch 'origin/uncomment_assert_not_exists' into test/merge_assert_up

commit 639e997
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date:   Mon Aug 12 13:31:36 2024 +0000

    feat(CategoryTheory/Sites): gluing of sections for Mayer-Vietoris squares (#14957)

    Co-authored-by: Markus Himmel <markus@lean-fro.org>

    Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

commit 46a72de
Author: Yury G. Kudryashov <urkud@urkud.name>
Date:   Mon Aug 12 13:31:34 2024 +0000

    feat(Ergodic): the left action of a group on itself is ergodic (#14596)

commit f9b79d6
Author: Violeta Hernández <vi.hdz.p@gmail.com>
Date:   Mon Aug 12 13:06:56 2024 +0000

    chore(SetTheory/Game/PGame): Add note on `NatCast` (#15713)

    I explain that this is not in fact the usual definition for natural numbers as games (a fact that just cost me a few hours of dev time...)

commit 40b6b14
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date:   Mon Aug 12 13:06:54 2024 +0000

    feat(Algebra/Homology): develop the API for the action of bifunctors on homological complexes (#15712)

commit a83f96c
Author: grhkm21 <grhkm21@gmail.com>
Date:   Mon Aug 12 13:06:52 2024 +0000

    chore: Fix enccard typo in Cardinal file (#15709)

    Fix typo in theorem name

    Moves:
    - Function.Embedding.enccard_le -> Function.Embedding.encard_le

commit 58d29b1
Author: Pim Otte <otte.pim@gmail.com>
Date:   Mon Aug 12 13:06:50 2024 +0000

    feat(Combinatorics/SimpleGraph/Matching): Add matching free graphs (#15357)

    Add supporting lemmas for graphs free of matchings in preperation for Tuttes theorem

commit ac8cc94
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date:   Mon Aug 12 13:06:49 2024 +0000

    feat(Algebra/Homology): action of the flip of a bifunctor on homological complexes (#11713)

    We construct an isomorphism `mapBifunctor K₂ K₁ F.flip c ≅ mapBifunctor K₁ K₂ F c` when `F` is a bifunctor, and `K₁` and `K₂` are two homological complexes. This is under the assumption of a certain instance of `TotalComplexShapeSymmetry` which provides compatible signs for this isomorphism.

    Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

commit b1f62bd
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Mon Aug 12 12:57:15 2024 +0000

    chore: remove unused argument from Behrend.map_injOn (#15735)

commit a9c4c79
Author: Kim Morrison <kim@tqft.net>
Date:   Mon Aug 12 11:58:20 2024 +0000

    chore: update Mathlib dependencies 2024-08-12 (#15728)

    Co-authored-by: mathlib-bors <150093616+mathlib-bors@users.noreply.github.com>

commit 81b928c
Author: Jakob von Raumer <jakob@von-raumer.de>
Date:   Mon Aug 12 10:18:59 2024 +0000

    feat(CategoryTheory): Equivalence between certain comma categories and products (#15648)

commit 815eabc
Author: Jakob von Raumer <jakob@von-raumer.de>
Date:   Mon Aug 12 10:09:28 2024 +0000

    feat(CategoryTheory): Finality of functors from filtered categories into PUnit (#15641)

commit 0de4943
Author: Kim Morrison <kim@tqft.net>
Date:   Mon Aug 12 16:52:22 2024 +1000

    move

commit 07189b5
Author: Kim Morrison <kim@tqft.net>
Date:   Mon Aug 12 16:40:40 2024 +1000

    chore: uncomment some now viable assert_not_exists

…cal complexes (#11713)

We construct an isomorphism `mapBifunctor K₂ K₁ F.flip c ≅ mapBifunctor K₁ K₂ F c` when `F` is a bifunctor, and `K₁` and `K₂` are two homological complexes. This is under the assumption of a certain instance of `TotalComplexShapeSymmetry` which provides compatible signs for this isomorphism.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…cal complexes (#11713)

We construct an isomorphism `mapBifunctor K₂ K₁ F.flip c ≅ mapBifunctor K₁ K₂ F c` when `F` is a bifunctor, and `K₁` and `K₂` are two homological complexes. This is under the assumption of a certain instance of `TotalComplexShapeSymmetry` which provides compatible signs for this isomorphism.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…cal complexes (#11713)

We construct an isomorphism `mapBifunctor K₂ K₁ F.flip c ≅ mapBifunctor K₁ K₂ F c` when `F` is a bifunctor, and `K₁` and `K₂` are two homological complexes. This is under the assumption of a certain instance of `TotalComplexShapeSymmetry` which provides compatible signs for this isomorphism.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>