refactor(Topology): redefine Topology.IsQuotientMap with Topology.IsCoinducing

[chrisflav]

Currently, varying formulations for f : X -> Y is coinducing are used: Examples are an equality of TopologicalSpace.coinduced or an explicit characterization of open sets.
We add a predicate Topology.IsCoinducing and redefine Topology.IsQuotientMap in terms of it.

---

[github-actions]

PR summary f2fa93365e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsCoinducing
+ Topology.IsCoinducing.image_connectedComponent
+ Topology.IsCoinducing.preimage_connectedComponent
+ Topology.IsCoinducing.restrictPreimage_of_isOpen
+ comp
+ continuous
+ id
+ isCoinducing_iff
+ isCoinducing_iff_isClosed
+ of_comp
+ of_comp_of_continuous
+ of_comp_of_isCoinducing
+ of_isClosed_preimage_iff_isClosed
+ of_isOpen_preimage_iff_isOpen
++- isClosed_preimage
++- isOpen_preimage
- isQuotientMap_iff

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

[plp127]

It seems to me that these being deprecated is the cause of a lot of changing h.isOpen_preimage to h.isCoinducing.isOpen_preimage, where if these didn't exist instead then h.isOpen_preimage would just work. In this case might we consider not deprecating instead, since it would only break explicit references to IsQuotientMap.isOpen_preimage, which should be rarer since it is usually used with the dot notation?

[chrisflav]

I had considered this, but eventually decided against it. Not deprecating brings only little benefit. The changes are all straightforward and while h.isCoinducing.isOpen_preimage is slightly worse, it is not bad either.