feat(AlgebraicTopology): homology of contractible spaces

[erdOne]

---

[github-actions]

PR summary 5289bf289a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat	1717	1720	+3 (+0.17%)

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat	3

---

Declarations diff

+ instance (X : TopCat.{w}) [ContractibleSpace X] (R : C) (n : ℕ) :
+ instance : Unique (⊤_ TopCat.{u})
+ isZero_singularHomologyFunctor_of_contractibleSpace
+ singularHomologyFunctorHomotopyEquiv
+ singularHomologyFunctorZeroOfContractibleSpace
+ singularHomologyFunctor_obj_map_eq

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[dagurtomas]

The docstring of HomotopyEquiv.toFun/invFun says explicitly DO NOT USE, use coercion instead. However, there appears to be no coercion from X ≃ₕ Y to C(X, Y), only to plain functions. Could you add that?

[erdOne]

Do you mean using toContinuousMap via ContinuousMapClass or just tag toFun with @[coe]?

[erdOne]

invFun should definitely be switched to symm.toFun though so I did that for now.

But for toFun perhaps we should just rename toFun to toContinuousMap and remove the DO NOT USE.

[dagurtomas]

But for toFun perhaps we should just rename toFun to toContinuousMap and remove the DO NOT USE.

I think this is reasonable

[erdOne]

I'll open a PR to do that soon-ish.

[joelriou]

All the declarations use some TopCat as an input:

Suggested change

	namespace AlgebraicTopology
	namespace TopCat

I believe we should remove the namespace AlgebraicTopology globally (while keeping the folder Mathlib/AlgebraicTopology/), and move the declarations to CategoryTheory.SimplicialObject, SSet, TopCat.

[erdOne]

singularHomologyFunctor is in AlgebraicTopology and these declarations are mainly about singularHomologyFunctor so I believe the current namespace is the more sensible one.

In general I would tend to argue the opposite, that we should use theory names as top level namespaces more (e.g. Topology or AlgebraicGeometry or CategoryTheory).

[dagurtomas]

Probably, singularHomologyFunctor should be in the TopCat namespace. I disagree about using theory names more as top level namespaces. It will just make dot notation harder to use when mixing different theories.

[erdOne]

I am failing to see how using theory namespaces as top level namespaces cause issues with dot notation. E.g. is the CategoryTheory namespace causing any trouble?

[joelriou]

I would say the point is not very much about root namespaces. TopCat happens to be a root namespace. If it were CategoryTheory.TopCat or Topology.TopCat, I would still argue that singularHomologyFunctor should be *.TopCat.singularHomologyFunctor, because singular homology is a homology theory for topological spaces.

[vlad902]

Suggested change

	asIso (((singularHomologyFunctor C 0).obj R).map (terminal.from X)) ≪≫
	asIso (((singularHomologyFunctor C 0).obj R).map (terminal.from X)) ≪≫

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.