[Merged by Bors] - refactor(Algebra/Category/ModuleCat): make ModuleCat.Hom a structure

[Vierkantor]

This PR follows the approach of #19065 to solve painful definitional equalities problems by forbidding the identification of A ⟶ B and A →ₗ[R] B. These are not equal reducibly, so tactics get confused if one is replaced by the other.

There seem to be a few regressions caused by defeq abuse that we were able to get away with previously, but some subtle elaboration differences made it evident. Otherwise the cost is inserting many .homs and asHoms.

A few steps that might clean up the diff, but would be too much work to incorporate in this PR:

• Make the ext tactic pick up TensorProduct.ext again.
• Replace the defeq abuse between (restrictScalars f).obj M and M with explicit maps going back and forth.

Overall quite a few proofs could be cleaned up at the cost of more bookkeeping.

---

• depends on: [Merged by Bors] - chore(Algebra/Category/ModuleCat): rename ModuleCat.asHom to ModuleCat.ofHom #19705

[github-actions]

PR summary f8f8363b30

Import changes exceeding 2%

%	File
+18.89%	Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures	614	730	+116 (+18.89%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures	116

---

Declarations diff

+ FGModuleCatEvaluation_apply'
+ Hom
+ Hom.hom₂
+ Hom.hom₂_ofHom₂
+ Hom.instModule
+ HomEquiv.fromRestriction_hom_apply_apply
+ HomEquiv.toRestriction_hom_apply
+ Iso.conj_hom_eq_conj
+ asHom
+ comp_apply
+ endMulEquiv
+ endMulEquiv_comp_ρ
+ endMulEquiv_symm_comp_ρ
+ forget_obj
+ homAddEquiv
+ homEquiv
+ homLinearEquiv
+ hom_action_ρ
+ hom_add
+ hom_bijective
+ hom_comp
+ hom_id
+ hom_injective
+ hom_inv_apply
+ hom_neg
+ hom_nsmul
+ hom_ofHom
+ hom_smul
+ hom_sub
+ hom_sum
+ hom_surjective
+ hom_zero
+ hom_zsmul
+ instance : Add (M ⟶ N)
+ instance : AddCommGroup (M ⟶ N)
+ instance : CoeFun (obj' f M) fun _ => S → M
+ instance : Inhabited (ModuleCat R)
+ instance : Neg (M ⟶ N)
+ instance : SMul S (M ⟶ N)
+ instance : SMul ℕ (M ⟶ N)
+ instance : SMul ℤ (M ⟶ N)
+ instance : Sub (M ⟶ N)
+ instance : Zero (M ⟶ N)
+ instance {M N : ModuleCat.{v} R} : CoeFun (M ⟶ N) (fun _ ↦ M → N)
+ inv_hom_apply
+ ofHom_apply
+ ofHom_comp
+ ofHom_hom
+ ofHom_id
+ ofHom_ρ
+ ofHom₂
+ ofHom₂_compr₂
+ ofHom₂_hom₂
+ pushforward_map_app_apply'
+ pushforward_obj_map_apply'
+ toSheafify_app_apply'
+ ρ_hom
++ hom_ext
++ ofHom
++-- of
- ModuleCat.asHom
- ModuleCat.ofHom
- ModuleCat.ofHom_apply
- coe_comp
- comp_def
- ext
- instance : CoeFun (obj' f M) fun _ => S → M where coe g := g.toFun
- instance {M N : FGModuleCat R} : FunLike (M ⟶ N) M N
- instance {M N : FGModuleCat R} : LinearMapClass (M ⟶ N) R M N
- instance {M N : ModuleCat.{v} R} : AddCommGroup (M ⟶ N) := LinearMap.addCommGroup
- instance {M N : ModuleCat.{v} R} : FunLike (M ⟶ N) M N
- instance {M N : ModuleCat.{v} R} : LinearMapClass (M ⟶ N) R M N
- instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f : R →+* S}
- ofUnique

You can run this locally as follows

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (5.49, 0.03)

Current number	Change	Type
4981	-30	porting notes
202	-2	disabled simpNF lints
1498	-24	erw

Current commit f8f8363b30
Reference commit a38db992d0

You can run this locally as

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

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Vierkantor]

Having to type-ascribe asHom suggests there is some defeq abuse going on.

[Vierkantor]

This proof got uglier, not sure what the concrete cause is.

[Vierkantor]

I tried a few things and it seems there was already a lot of defeq abuse that got exposed now.

[Vierkantor]

This proof got a lot uglier, not sure what the concrete cause is.

[chrisflav]

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.

[chrisflav]

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?

[Vierkantor]

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.

[chrisflav]

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.

[chrisflav]

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

[Vierkantor]

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

[Vierkantor]

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.)

[Vierkantor]

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

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

[jcommelin]

!bench

[leanprover-bot]

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%

[jcommelin]

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

[kim-em]

bors d+

[mathlib-bors]

✌️ 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.

[Vierkantor]

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

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style