feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and `mk`

[yoh-tanimoto]

Define the mk and lifts of normed spaces and normed groups by the inseparable setoid as NormedAddGroupHom, CLM, etc.

Motivation: In the GNS representation, operators in the original C^*-algebra are represented as bounded linear operators.

This PR splits from #16707.

[github-actions[bot]]

messageFile.md

[YaelDillies]

The import increases look quite bad. Do you think you can do something about them?

[yoh-tanimoto]

I'm not sure, as for Mathlib.Topology.Algebra.SeparationQuotient.Basic, I added Mathlib.Topology.Algebra.ContinuousMonoidHom which is necessary because I define liftContinuousMonoidHom. I don't understand Mathlib.Analysis.Normed.Group.Hom, I don't add any import?

[github-actions[bot]]

messageFile.md

[YaelDillies]

Can you merge master to fix the bot?

[github-actions[bot]]

PR summary 2ae70a42c6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Algebra.SeparationQuotient.Hom (new file)	1121
Mathlib.Analysis.Normed.Group.SeparationQuotient (new file)	1268

---

Declarations diff

+ apply_eq_apply_of_inseparable + instance : ContinuousMapClass (NormedAddGroupHom V₁ V₂) V₁ V₂ + liftCLM + liftCLM_mk + liftContinuousCommMonoidHom_mk + liftContinuousMonoidHom + liftNormedAddGroupHom + liftNormedAddGroupHomEquiv + liftNormedAddGroupHom_normNoninc + liftNormedAddGroupHom_norm_le + nhds_mk + norm_liftNormedAddGroupHom_apply_le + norm_liftNormedAddGroupHom_le + norm_normedMk_eq_one + norm_normedMk_le + normedMk + normedMk_eq_zero_iff + ofClass

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.

---

No changes to technical debt.

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

[YaelDillies]

for Mathlib.Topology.Algebra.SeparationQuotient.Basic, I added Mathlib.Topology.Algebra.ContinuousMonoidHom which is necessary because I define liftContinuousMonoidHom

Can you maybe move liftContinuousMonoidHom to a new file Mathlib.Topology.Algebra.SeparationQuotient.Hom? The import increases are currently unacceptably large

[yoh-tanimoto]

Thanks, I splitted the file and now it seems ok?

[j-loreaux]

LGTM too, thanks!

bors d+

[mathlib-bors[bot]]

:v: yoh-tanimoto can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[yoh-tanimoto]

thanks for your reviews!

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build