feat(Topology/Algebra/Group/Matrix): refactor; continuity of maps on GL(n) and SL(n)

[loefflerd]

Show that the maps Rˣ → Sˣ, SL n R → SL n S, and GL n R → GL n S induced by a ring/monoid morphism f : R → S are continuous / inducing / embedding / closed-embedding if f is.

Also add Real analogues of some existing Complex lemmas about the intCast map, e.g. Real.closedEmbedding_intCast, and refactor and clean up Topology/Algebra/Group/Matrix.lean.

---

[github-actions]

PR summary 1ba90ab6bb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Topology.IsClosedEmbedding.prodMap
+ _root_.Continuous.generalLinearGroup_map
+ _root_.Continuous.specialLinearGroup_map
+ _root_.Topology.IsClosedEmbedding.generalLinearGroup_map
+ _root_.Topology.IsClosedEmbedding.specialLinearGroup_map
+ _root_.Topology.IsClosedEmbedding.units_map
+ _root_.Topology.IsEmbedding.generalLinearGroup_map
+ _root_.Topology.IsEmbedding.specialLinearGroup_map
+ _root_.Topology.IsEmbedding.units_map
+ _root_.Topology.IsInducing.generalLinearGroup_map
+ _root_.Topology.IsInducing.specialLinearGroup_map
+ _root_.Topology.IsInducing.units_map
+ closedEmbedding_intCast
+ continuous_mapGL
+ instT1Space
+ isClosedEmbedding_mapGL
+ isClosed_range_intCast
+ isOpen_compl_range_intCast
+ isometry_intCast

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.

---

Decrease in tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type
6869	-2	backward.isDefEq.respectTransparency

Current commit bb444b6098
Reference commit 1ba90ab6bb

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

[mathlib-merge-conflicts]

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

[j-loreaux]

Suggested change

	theorem closedEmbedding_intCast : IsClosedEmbedding ((↑) : ℤ → ℝ) :=
	theorem isClosedEmbedding_intCast : IsClosedEmbedding ((↑) : ℤ → ℝ) :=

[j-loreaux]

Continuous (algebraMap R S) (with the pre-existing hypotheses) is equivalent to ContinuousSMul R S (see continuous_algebraMap_iff_smul). I suggest assuming ContinuousSMul R S instead so that the user does not need to supply this hypothesis.

[j-loreaux]

🤔 are we sure about this? This creates a bridge between layers in the fun_prop hierarchy. That is, IsEmbedding → IsInducing → Continuous already existed, but now you're adding a direct line. The net effect, because fun_prop by default only tries depth-1 transitions. So, by adding this, you're making it try certain things that would previously have been depth-2. I suspect that's not what we want.