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]

messageFile.md

[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]

messageFile.md

[YaelDillies]

Can you merge master to fix the bot?

[github-actions]

PR summary f55a802e8a

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)	1195
Mathlib.Analysis.Normed.Group.SeparationQuotient (new file)	1313

---

Declarations diff

+ apply_eq_apply_of_inseparable
+ instance : ContinuousMapClass (NormedAddGroupHom V₁ V₂) V₁ V₂
+ liftCLM
+ liftCLM_mk
+ liftContinuousCommMonoidHom_mk
+ liftContinuousMonoidHom
+ liftNormedAddGroupHom
+ liftNormedAddGroupHom_equiv
+ 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
+ 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?

[YaelDillies]

Maybe use the notation?

Suggested change

	nhds (mk x) = Filter.map mk (nhds x) :=
	𝒩 (mk x) = .map mk (𝒩 x) :=

[yoh-tanimoto]

This fails, does it mean that I should import something?

[YaelDillies]

We're trying to get rid of those coercions, see #21031. Can you replace this by a function ContinuousMonoidHom.ofClass if you really need it? More likely, you don't actually need it and can write something.toContinuousMonoidHom instead

[yoh-tanimoto]

I think I added this because it was asked here #18178 (comment)

What should I do? I added a def for the moment

[YaelDillies]

Can you use where here?

[yoh-tanimoto]

done