PR summary f8f8363b30

Import changes exceeding 2%

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

./scripts/technical-debt-metrics.sh pr_summary

Overall this looks very good and a lot of proofs got cleaner! Did you run your magic erw -> rw tool? I could imagine there is some potential.

I hope you don't mind that I pushed some small changes to get rid of some more erws.

I tried to add a test file similar to the one for AlgebraCat, but I am running into this:

import Mathlib
open CategoryTheory ModuleCat
variable (R : Type u) [CommRing R]

/-
ambiguous, possible interpretations 
  ↟f : of R X ⟶ of R Y
  
  ↾⇑f : X ⟶ Y
-/
example {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] (f : X →ₗ[R] Y)
    (x : X) : (asHom f) x = f x := by simp

Do you understand this?

I think the testcase fails because there is also the definition CategoryTheory.asHom which is ModuleCat.asHom but for the category of types. So we either apply ModuleCat.asHom and then coerce back to a function, or we coerce f to a function, apply CategoryTheory.asHom to make it a morphism, and then coerce it back to a plain function. And since both of the end results have the same types and applicability, Lean can't choose and throws an error.

I think the testcase fails because there is also the definition CategoryTheory.asHom which is ModuleCat.asHom but for the category of types. So we either apply ModuleCat.asHom and then coerce back to a function, or we coerce f to a function, apply CategoryTheory.asHom to make it a morphism, and then coerce it back to a plain function. And since both of the end results have the same types and applicability, Lean can't choose and throws an error.

Ah, silly me, I didn't think of CategoryTheory.asHom and was not aware of the notation. Replacing the asHom with ModuleCat.asHom makes everything work.

I put the tests in 554ba63, if you like them feel free to cherry-pick (or tell me to push it here).

Thank you! Feel free to push your commit directly to this branch. :)

Overall this looks very good and a lot of proofs got cleaner! Did you run your magic erw -> rw tool? I could imagine there is some potential.

I hope you don't mind that I pushed some small changes to get rid of some more erws.

I did run it on an earlier version of the branch, let me see if anything got cleared up in the meantime.

(It should be as easy as merging the try_this-erw branch into the current branch, and then cherry-picking any of the warnings it produces.)

No free erw eliminations found on this branch, but I did find a few in other bits of Mathlib so time to make a little PR for that :D

This PR/issue depends on:

• [Merged by Bors] - chore(Algebra/Category/ModuleCat): rename ModuleCat.asHom to ModuleCat.ofHom #19705
  By Dependent Issues (🤖). Happy coding!

!bench

Here are the benchmark results for commit f8f8363.
There were significant changes against commit a38db99:

  Benchmark                                                    Metric         Change
  ==================================================================================
- ~Mathlib.Algebra.Category.ModuleCat.Algebra                  instructions   227.1%
- ~Mathlib.Algebra.Category.ModuleCat.Basic                    instructions    46.7%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings            instructions   -30.3%
- ~Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf   instructions    15.2%
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf                 instructions   -16.9%
- ~Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings   instructions    28.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal        instructions   -16.7%
- ~Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward     instructions    19.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify        instructions   -13.4%
- ~Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits           instructions    61.8%
- ~Mathlib.Algebra.Homology.ShortComplex.ModuleCat             instructions    71.3%
- ~Mathlib.AlgebraicGeometry.Modules.Tilde                     instructions    24.1%
- ~Mathlib.CategoryTheory.Linear.Yoneda                        instructions    19.8%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.Module             instructions    -9.2%
- ~Mathlib.RepresentationTheory.Rep                            instructions    12.1%

Hmmm, we still don't get the helpful report... Don't know why not 😢

bors d+

✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

I checked again and am happy with the PR, so let's get this merged!

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style